--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Ersatz.Solver.Z3
  ( z3
  , z3Path
  ) where

import Control.Monad.IO.Class
import Ersatz.Problem ( SAT, writeDimacs' )
import Ersatz.Solution
import Ersatz.Solver.Common
import System.Process (readProcessWithExitCode)

-- | 'Solver' for 'SAT' problems that tries to invoke the @z3@ executable from the @PATH@
z3 :: MonadIO m => Solver SAT m
z3 :: forall (m :: * -> *). MonadIO m => Solver SAT m
z3 = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
z3Path FilePath
"z3"

-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes @z3@ compatible arguments.
--
-- The 'FilePath' refers to the path to the executable.
z3Path :: MonadIO m => FilePath -> Solver SAT m
z3Path :: forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
z3Path FilePath
path SAT
problem = IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall a. IO a -> m a
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 -> SAT -> IO ()
forall (m :: * -> *) t.
(MonadIO m, DIMACS t) =>
FilePath -> t -> m ()
writeDimacs' FilePath
problemPath 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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
result, FilePath -> IntMap Bool
parseSolution5 FilePath
out)