module Satchmo.Solver.Minisat
( solve
, using
)
where
import Satchmo.Data
import qualified Satchmo.Solve
import Satchmo.Solver.Internal
import Satchmo.SAT.Seq
import qualified Data.ByteString.Char8 as BS
import Data.Monoid
import System.IO
import System.Process
import Control.Monad ( when )
import Control.Concurrent
import Control.Exception
import System.TimeIt
import Text.Printf
import qualified Data.Array as A
solve = using "minisat2"
using fp = Satchmo.Solve.solve $ minisat fp
minisat :: FilePath -> Satchmo.Solve.Implementation
minisat fp cs Header{numVars=numVars, numClauses=numClauses} = do
let header = BS.pack $ mkDimacsHeader numVars numClauses
let debug = False
when debug $ do
BS.hPutStrLn stderr header
BS.hPutStrLn stderr cs
( hin, hout, herr, proc ) <- runInteractiveCommand
( unwords [ fp, "/dev/stdin", "/dev/stdout" ] )
container <- newEmptyMVar
streamer <- forkIO $ do
BS.hPutStr hin ( mappend header cs )
ds <- hGetContents hout
hPutStrLn stderr $ unwords [ "output", "length", show (length ds) ]
hPutStrLn stderr $ take 80 ds
putMVar container ds
out <- takeMVar container `Control.Exception.catch` \ ( _ :: AsyncException ) -> do
killThread streamer
terminateProcess proc
return ""
case lines out of
"SAT" : xs : _ -> do
let dict = Just $ A.listArray (1,numVars) $ do
(v,l) <- zip [1..] $ map read $ takeWhile ( /= "0" ) $ words xs
return $ if variable l == v then positive l else error "huh"
seq (length out) $ return dict
_ -> return $ Nothing
timeItMsg msg action = do
(time, res) <- timeItT action
hPrintf stderr "CPU time: %6.2fs for %s\n" time msg
hFlush stderr
return res