diff --git a/Satchmo/Boolean/Data.hs b/Satchmo/Boolean/Data.hs --- a/Satchmo/Boolean/Data.hs +++ b/Satchmo/Boolean/Data.hs @@ -2,6 +2,8 @@ {-# language TypeSynonymInstances #-} {-# language FlexibleInstances #-} {-# language NoMonomorphismRestriction #-} +{-# language TemplateHaskell #-} +{-# language DeriveGeneric #-} module Satchmo.Boolean.Data @@ -24,17 +26,23 @@ import Satchmo.Data import Satchmo.MonadSAT - - +import Data.Function.Memoize import Data.Array import Data.Maybe ( fromJust ) import Data.List ( partition ) import Control.Monad.Reader -data Boolean = Boolean { encode :: Literal } +import GHC.Generics (Generic) +import Data.Hashable + +data Boolean = Boolean { encode :: ! Literal } | Constant { value :: ! Bool } + deriving (Eq, Ord, Show, Generic) +instance Hashable Boolean + +$(deriveMemoizable ''Boolean) {- diff --git a/Satchmo/Data.hs b/Satchmo/Data.hs --- a/Satchmo/Data.hs +++ b/Satchmo/Data.hs @@ -4,6 +4,8 @@ {-# language TypeFamilies #-} {-# language GeneralizedNewtypeDeriving #-} +{-# language TemplateHaskell #-} +{-# language DeriveGeneric #-} module Satchmo.Data @@ -23,7 +25,11 @@ import qualified Data.Foldable as F import Data.Monoid import Data.List ( nub ) +import Data.Function.Memoize +import GHC.Generics (Generic) +import Data.Hashable + -- * variables and literals type Variable = Int @@ -32,7 +38,11 @@ Literal { variable :: ! Variable , positive :: ! Bool } - deriving ( Eq, Ord ) + deriving ( Eq, Ord, Generic ) + +instance Hashable Literal + +$(deriveMemoizable ''Literal) instance Show Literal where show l = ( if positive l then "" else "-" ) diff --git a/Satchmo/MonadSAT.hs b/Satchmo/MonadSAT.hs --- a/Satchmo/MonadSAT.hs +++ b/Satchmo/MonadSAT.hs @@ -31,7 +31,8 @@ type Weight = Int -class (MonadFix m, Applicative m, Monad m) => MonadSAT m where +class ( -- MonadFix m, + Applicative m, Monad m) => MonadSAT m where fresh, fresh_forall :: m Literal emit :: Clause -> m () @@ -53,8 +54,6 @@ } deriving Show -{- - -- ------------------------------------------------------- -- MonadSAT liftings for standard monad transformers -- ------------------------------------------------------- @@ -63,54 +62,62 @@ fresh = lift fresh fresh_forall = lift fresh_forall emit = lift . emit - emitW = (lift.) . emitW + -- emitW = (lift.) . emitW + note = lift . note instance (Monad m, MonadSAT m) => MonadSAT (ReaderT r m) where fresh = lift fresh fresh_forall = lift fresh_forall emit = lift . emit - emitW = (lift.) . emitW + -- emitW = (lift.) . emitW + note = lift . note instance (Monad m, MonadSAT m) => MonadSAT (Lazy.StateT s m) where fresh = lift fresh fresh_forall = lift fresh_forall emit = lift . emit - emitW = (lift.) . emitW + -- emitW = (lift.) . emitW + note = lift . note instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.RWST r w s m) where fresh = lift fresh fresh_forall = lift fresh_forall emit = lift . emit - emitW = (lift.) . emitW + -- emitW = (lift.) . emitW + note = lift . note instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.WriterT w m) where fresh = lift fresh fresh_forall = lift fresh_forall emit = lift . emit - emitW = (lift.) . emitW + -- emitW = (lift.) . emitW + note = lift . note instance (Monad m, MonadSAT m) => MonadSAT (Strict.StateT s m) where fresh = lift fresh fresh_forall = lift fresh_forall emit = lift . emit - emitW = (lift.) . emitW + -- emitW = (lift.) . emitW + note = lift . note instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.RWST r w s m) where fresh = lift fresh fresh_forall = lift fresh_forall emit = lift . emit - emitW = (lift.) . emitW + -- emitW = (lift.) . emitW + note = lift . note instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.WriterT w m) where fresh = lift fresh fresh_forall = lift fresh_forall emit = lift . emit - emitW = (lift.) . emitW + -- emitW = (lift.) . emitW + note = lift . note instance (Monad m, MonadSAT m) => MonadSAT (ContT s m) where fresh = lift fresh fresh_forall = lift fresh_forall emit = lift . emit - emitW = (lift.) . emitW + -- emitW = (lift.) . emitW + note = lift . note --} diff --git a/Satchmo/SAT/External.hs b/Satchmo/SAT/External.hs new file mode 100644 --- /dev/null +++ b/Satchmo/SAT/External.hs @@ -0,0 +1,179 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE DoAndIfThenElse #-} +{-# LANGUAGE PatternSignatures #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# language TemplateHaskell #-} + +-- | call an external solver as separate process, +-- communicate via pipes. + +module Satchmo.SAT.External + +( SAT +, fresh +, emit +, solve +-- , solve_with_timeout +) + +where + +import Satchmo.Data +import Satchmo.Boolean hiding ( not ) +import Satchmo.Code +-- import Satchmo.MonadSAT + +import Control.Monad.Reader +import Control.Monad.State +-- import Control.Monad.IO.Class +import System.IO +import Control.Lens +import Control.Applicative + +import Control.Concurrent +import Control.DeepSeq (rnf) + +import Foreign.C +-- import System.Exit (ExitCode(..)) +import System.Process +-- import System.IO.Error +-- import System.Posix.Types +import Control.Exception +import GHC.IO.Exception ( IOErrorType(..), IOException(..) ) +-- import System.Posix.Signals + +import qualified Control.Exception as C +import qualified Data.ByteString.Char8 as BS +import qualified Data.Map.Strict as M +import Data.List (isPrefixOf) + +tracing = False +report s = when tracing $ hPutStrLn stderr s + +data S = S + { _next_variable :: ! Int + , _solver_input :: ! Handle + } + +$(makeLenses ''S) + +newtype SAT a = SAT (StateT S IO a) + deriving (Functor, Applicative, Monad, MonadIO) + +type Assignment = M.Map Int Bool + +newtype Dec a = Dec (Reader Assignment a) + deriving (Functor, Applicative, Monad) + +instance MonadSAT SAT where + fresh = SAT $ do + n <- use next_variable + next_variable .= succ n + return $ literal True $ fromEnum n + emit cl = SAT $ do + h <- use solver_input + let s = BS.pack $ show cl + -- liftIO $ BS.putStrLn s + liftIO $ BS.hPutStrLn h s + + note msg = SAT $ liftIO $ hPutStrLn stderr msg + + type Decoder SAT = Dec + +instance Decode Dec Boolean Bool where + decode b = case b of + Constant c -> return c + Boolean l -> do + v <- dv $ variable l + return $ if positive l then v else not v + +dv v = Dec $ do + assignment <- ask + return $ case M.lookup v assignment of + Just v -> v + Nothing -> error $ unwords [ "unassigned", "variable", show v ] + + +solve :: String -- ^ command, e.g., glucose + -> [String] -- ^ options, e.g., -model + -> SAT (Dec a) -- ^ action that builds the formula and returns the decoder + -> IO (Maybe a) +solve command opts (SAT action) = bracket + ( do + report "Satchmo.SAT.External: creating process" + createProcess $ (proc command opts) + { std_in = CreatePipe + , std_out = CreatePipe + , create_group = True + } ) + ( \ (Just sin, Just sout, _, ph) -> do + report "Satchmo.SAT.External: bracket closing" + interruptProcessGroupOf ph + ) + $ \ (Just sin, Just sout, _, ph) -> do + + dec <- newEmptyMVar + + -- fork off a thread to start consuming the output + output <- hGetContents sout -- lazy IO + withForkWait (C.evaluate $ rnf output) $ \ waitOut -> + ignoreSigPipe $ do + report $ "S.S.External: waiter forked" + + let s0 = S { _next_variable=1, _solver_input=sin} + report $ "S.S.External: writing output" + Dec decoder <- evalStateT action s0 + putMVar dec decoder + hClose sin + + waitOut + hClose sout + report $ "S.S.External: waiter done" + + report "Satchmo.SAT.External: start waiting" + waitForProcess ph + decoder <- takeMVar dec + report "Satchmo.SAT.External: waiting done" + + let vlines = do + line <- lines output + guard $ isPrefixOf "v" line + return line + report $ show vlines + let vs = do + line <- vlines + w <- tail $ words line + return (read w :: Int) + return $ do + guard $ not $ null vlines + let m = M.fromList $ do + v <- vs ; guard $ v /= 0 ; return (abs v, v>0) + return $ runReader decoder m + +-- * code from System.Process +-- http://hackage.haskell.org/package/process-1.2.3.0/docs/src/System-Process.html#readProcess +-- but they are not exporting withForkWait, so I have to copy it + +-- | Fork a thread while doing something else, but kill it if there's an +-- exception. +-- +-- This is important in the cases above because we want to kill the thread +-- that is holding the Handle lock, because when we clean up the process we +-- try to close that handle, which could otherwise deadlock. +-- +withForkWait :: IO () -> (IO () -> IO a) -> IO a +withForkWait async body = do + waitVar <- newEmptyMVar :: IO (MVar (Either SomeException ())) + mask $ \restore -> do + tid <- forkIO $ try (restore async) >>= putMVar waitVar + let wait = takeMVar waitVar >>= either throwIO return + restore (body wait) `C.onException` killThread tid + +ignoreSigPipe :: IO () -> IO () +ignoreSigPipe = C.handle $ \e -> case e of + IOError { ioe_type = ResourceVanished + , ioe_errno = Just ioe } + | Errno ioe == ePIPE -> return () + _ -> throwIO e diff --git a/Satchmo/SAT/Mini.hs b/Satchmo/SAT/Mini.hs --- a/Satchmo/SAT/Mini.hs +++ b/Satchmo/SAT/Mini.hs @@ -29,6 +29,7 @@ import Control.Exception import Control.Monad ( when ) import Control.Monad.Fix +import Control.Monad.IO.Class import Control.Applicative import System.IO @@ -47,6 +48,10 @@ return x = SAT $ \ s -> return x SAT m >>= f = SAT $ \ s -> do x <- m s ; let { SAT n = f x } ; n s + +-- | need this for hashtables +instance MonadIO SAT where + liftIO comp = SAT $ \ s -> comp instance Applicative SAT where pure = return diff --git a/satchmo.cabal b/satchmo.cabal --- a/satchmo.cabal +++ b/satchmo.cabal @@ -1,5 +1,5 @@ Name: satchmo -Version: 2.9.7.3 +Version: 2.9.9 License: GPL License-file: gpl-2.0.txt @@ -21,8 +21,8 @@ Library ghc-options: -funbox-strict-fields Build-depends: mtl, process, containers, base == 4.*, - -- lens, - array, bytestring, directory, minisat >= 0.1, async + array, bytestring, directory, minisat >= 0.1, async, + memoize, hashable, transformers, lens, deepseq Exposed-modules: Satchmo.Data -- Satchmo.Data.Default @@ -56,6 +56,7 @@ Satchmo.SAT Satchmo.SAT.Tmpfile Satchmo.SAT.Mini + Satchmo.SAT.External -- Satchmo.SAT.CNF -- Satchmo.SAT.BS -- Satchmo.SAT.Seq