module Satchmo.SAT.External
( SAT
, fresh
, emit
, solve
)
where
import Satchmo.Data
import Satchmo.Boolean hiding ( not )
import Satchmo.Code
import Control.Monad.Reader
import Control.Monad.State
import System.IO
import Control.Lens
import Control.Applicative
import Control.Concurrent
import Control.DeepSeq (rnf)
import Foreign.C
import System.Process
import Control.Exception
import GHC.IO.Exception ( IOErrorType(..), IOException(..) )
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.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
-> [String]
-> SAT (Dec a)
-> 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
output <- hGetContents sout
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
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