{-# language OverloadedStrings #-}
module Ersatz.Solver.Minisat
( minisat
, cryptominisat
, minisatPath
) where
import Data.ByteString.Builder
import Control.Exception (IOException, handle)
import Control.Monad.IO.Class
import Data.IntMap (IntMap)
import Ersatz.Problem
import Ersatz.Solution
import Ersatz.Solver.Common
import qualified Data.IntMap.Strict as IntMap
import System.IO
import System.Process (readProcessWithExitCode)
import qualified Data.ByteString.Char8 as B
import Data.List ( foldl' )
minisat :: MonadIO m => Solver SAT m
minisat = minisatPath "minisat"
cryptominisat :: MonadIO m => Solver SAT m
cryptominisat = minisatPath "cryptominisat"
minisatPath :: MonadIO m => FilePath -> Solver SAT m
minisatPath path problem = liftIO $
withTempFiles ".cnf" "" $ \problemPath solutionPath -> do
withFile problemPath WriteMode $ \fh ->
hPutBuilder fh (dimacs problem)
(exit, _out, _err) <-
readProcessWithExitCode path [problemPath, solutionPath] []
sol <- parseSolutionFile solutionPath
return (resultOf exit, sol)
parseSolutionFile :: FilePath -> IO (IntMap Bool)
parseSolutionFile path = handle handler (parseSolution <$> B.readFile path)
where
handler :: IOException -> IO (IntMap Bool)
handler _ = return IntMap.empty
parseSolution :: B.ByteString -> IntMap Bool
parseSolution s =
case B.words s of
x : ys | x == "SAT" ->
foldl' ( \ m y -> let Just (v,_) = B.readInt y
in if 0 == v then m else IntMap.insert (abs v) (v>0) m
) IntMap.empty ys
_ -> IntMap.empty