module Ersatz.Solver.Z3
( z3
, z3Path
) where
import Data.ByteString.Builder
import Control.Monad.IO.Class
import Ersatz.Problem
import Ersatz.Solution
import Ersatz.Solver.Common
import System.IO
import System.Process (readProcessWithExitCode)
z3 :: MonadIO m => Solver SAT m
z3 :: Solver SAT m
z3 = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
z3Path FilePath
"z3"
z3Path :: MonadIO m => FilePath -> Solver SAT m
z3Path :: FilePath -> Solver SAT m
z3Path FilePath
path SAT
problem = IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Result, IntMap Bool) -> m (Result, IntMap Bool))
-> IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$
FilePath
-> FilePath
-> (FilePath -> FilePath -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall (m :: * -> *) a.
MonadIO m =>
FilePath -> FilePath -> (FilePath -> FilePath -> IO a) -> m a
withTempFiles FilePath
".cnf" FilePath
"" ((FilePath -> FilePath -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool))
-> (FilePath -> FilePath -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$ \FilePath
problemPath FilePath
_ -> do
FilePath -> IOMode -> (Handle -> IO ()) -> IO ()
forall r. FilePath -> IOMode -> (Handle -> IO r) -> IO r
withFile FilePath
problemPath IOMode
WriteMode ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
fh ->
Handle -> Builder -> IO ()
hPutBuilder Handle
fh (SAT -> Builder
forall t. DIMACS t => t -> Builder
dimacs SAT
problem)
(ExitCode
_exit, FilePath
out, FilePath
_err) <-
FilePath
-> [FilePath] -> FilePath -> IO (ExitCode, FilePath, FilePath)
readProcessWithExitCode FilePath
path [FilePath
"-dimacs", FilePath
problemPath] []
let result :: Result
result = case FilePath -> [FilePath]
lines FilePath
out of
FilePath
"s SATISFIABLE":[FilePath]
_ -> Result
Satisfied
FilePath
"s UNSATISFIABLE":[FilePath]
_ -> Result
Unsatisfied
[FilePath]
_ -> Result
Unsolved
(Result, IntMap Bool) -> IO (Result, IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
result, FilePath -> IntMap Bool
parseSolution5 FilePath
out)