module Satchmo.Solver.Minisat
( solve
, using
)
where
import Satchmo.Data
import qualified Satchmo.Solve
import Satchmo.Solver.Internal
import Satchmo.SAT
import qualified Data.ByteString.Char8 as S
import qualified Data.ByteString.Lazy.Char8 as BS
import Data.Monoid
import System.IO (stderr, hFlush, hClose, hPutStrLn, hGetContents
, hSetBuffering, BufferMode (..) )
import System.Process
import Control.Monad ( when )
import Control.Concurrent
import Control.Exception
import qualified Control.Exception as C
import qualified Data.Map as M
solve = using "/usr/bin/minisat2"
using fp = Satchmo.Solve.solve $ minisat fp
minisat :: FilePath -> Satchmo.Solve.Implementation
minisat fp cs Header{numVars=numVars, numClauses=numClauses} = do
let header = mkDimacsHeader numVars numClauses
cs' = BS.pack header `mappend` cs
let debug = False
if debug
then BS.hPut stderr cs'
else hPutStrLn stderr header >> hFlush stderr
( Just inh, Just outh, Just errh, pid ) <-
createProcess ( proc fp [ "/dev/stdin", "/dev/stdout" ] )
{ std_in = CreatePipe, std_out = CreatePipe, std_err = CreatePipe }
outMVar <- newEmptyMVar
out <- hGetContents outh
_ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()
err <- hGetContents errh
_ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()
do BS.hPut inh cs'; hFlush inh ; hClose inh
takeMVar outMVar `Control.Exception.catch` \ ( _ :: AsyncException ) -> do
terminateProcess pid
takeMVar outMVar `Control.Exception.catch` \ ( _ :: AsyncException ) -> do
terminateProcess pid
hClose outh ; hClose errh
ex <- waitForProcess pid
hPutStrLn stderr $ unwords [ "output", "length", show ( length out ) ]
case lines out of
"SAT" : xs : _ -> do
let dict = Just $ M.fromList $ do
l <- map read $ takeWhile ( /= "0" ) $ words xs
return ( variable l, positive l )
when debug $ print dict
return dict
_ -> return $ Nothing