module Satchmo.Solver.Pcosat
( solve
, using
)
where
import Satchmo.Data
import Satchmo.SAT
import qualified Satchmo.Solve
import Satchmo.Solver.Internal
import Data.Monoid
import System.Process
import System.Exit
import System.IO
import Control.Monad ( when )
import Control.Concurrent
import Control.Exception
import qualified Data.ByteString.Char8 as S
import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Data.Map as M
solve = using "precosat"
using fp = Satchmo.Solve.solve $ pcosat fp
debug :: Bool
debug = False
pcosat :: FilePath -> Satchmo.Solve.Implementation
pcosat fp cs Header{numVars=numVars, numClauses=numClauses} = do
let header = mkDimacsHeader numVars numClauses
cs' = BS.pack ( header ++ "\n" ) `mappend` cs
if debug
then BS.hPut stderr cs'
else hPutStrLn stderr header
( hin, hout, herr, proc ) <-
System.Process.runInteractiveCommand
$ unwords [ fp ]
container <- newEmptyMVar
forkIO $ do
BS.hPut hin cs'
ds <- hGetContents hout
hPutStrLn stderr $ unwords [ "output", "length", show ( length ds ) ]
putMVar container ds
out <- takeMVar container
`Control.Exception.catch` \ ( _ :: AsyncException ) -> do
terminateProcess proc
return ""
when debug $ hPutStrLn stdout out
let core = filter ( \ cs -> take 1 cs /= "c" ) $ lines out
assign = M.fromList $ do
'v' : xs <- core
l <- map read $ takeWhile ( /= "0" ) $ words xs
return ( variable l, positive l )
status = filter ( \ cs -> take 1 cs == "s" ) $ lines out
case status of
"s SATISFIABLE" : post -> do
when debug $ hPutStrLn stderr $ show assign
return $ Just assign
_ -> do
return $ Nothing