module Satchmo.Solver.Clasp
( 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 "clasp"
using fp = Satchmo.Solve.solve $ clasp fp
clasp :: FilePath -> Satchmo.Solve.Implementation
clasp fp cs Header{numVars=numVars, numClauses=numClauses} = do
let header = mkDimacsHeader numVars numClauses
cs' = BS.pack ( header ++ "\n" ) `mappend` cs
let debug = False
if debug
then BS.hPut stderr cs'
else hPutStrLn stderr header
( hin, hout, herr, proc ) <-
System.Process.runInteractiveCommand
$ unwords [ fp, "--dimacs", "--number=1", "--sat-p=20,25,150"
, "--hParam=0,512" ]
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
assign = M.fromList $ do
'v' : xs <- lines out
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
return $ Just assign
_ -> do
return $ Nothing