{-# language OverloadedStrings #-}
module Ersatz.Solver.Minisat
( minisat
, cryptominisat
, minisatPath
, cryptominisat5
, cryptominisat5Path
) 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
cryptominisat5 :: MonadIO m => Solver SAT m
cryptominisat5 = cryptominisat5Path "cryptominisat5"
cryptominisat5Path :: MonadIO m => FilePath -> Solver SAT m
cryptominisat5Path path problem = liftIO $
withTempFiles ".cnf" "" $ \problemPath _ -> do
withFile problemPath WriteMode $ \fh ->
hPutBuilder fh (dimacs problem)
(exit, out, _err) <-
readProcessWithExitCode path [problemPath] []
let sol = parseSolution5 out
return (resultOf exit, sol)
parseSolution5 :: String -> IntMap Bool
parseSolution5 txt = IntMap.fromList [(abs v, v > 0) | v <- vars, v /= 0]
where
vlines = [l | ('v':l) <- lines txt]
vars = map read (foldMap words vlines)