-------------------------------------------------------------------- -- | -- Copyright : (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013 -- License : BSD3 -- Maintainer: Edward Kmett -- Stability : experimental -- Portability: non-portable -- -------------------------------------------------------------------- module Ersatz.Solver.Minisat ( minisat , cryptominisat , minisatPath ) where import Control.Applicative import Control.Exception (IOException, handle) import Control.Monad import Control.Monad.IO.Class import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap import Ersatz.Internal.Parser import Ersatz.Problem (qdimacs) import Ersatz.Solution import System.Exit (ExitCode(..)) import System.IO.Temp (withSystemTempDirectory) import System.Process (readProcessWithExitCode) minisat :: MonadIO m => Solver m minisat = minisatPath "minisat" cryptominisat :: MonadIO m => Solver m cryptominisat = minisatPath "cryptominisat" minisatPath :: MonadIO m => FilePath -> Solver m minisatPath path qbf = liftIO $ withSystemTempDirectory "ersatz" $ \dir -> do let problemPath = dir ++ "/problem.cnf" solutionPath = dir ++ "/solution" writeFile problemPath (qdimacs qbf) (exit, _out, _err) <- readProcessWithExitCode path [problemPath, solutionPath] [] sol <- parseSolutionFile solutionPath return (resultOf exit, sol) resultOf :: ExitCode -> Result resultOf (ExitFailure 10) = Satisfied resultOf (ExitFailure 20) = Unsatisfied resultOf _ = Unsolved parseSolutionFile :: FilePath -> IO (IntMap Bool) parseSolutionFile path = handle handler $ do parseSolution <$> readFile path where handler :: IOException -> IO (IntMap Bool) handler _ = return IntMap.empty parseSolution :: String -> (IntMap Bool) parseSolution input = case runParser solution input of (s:_) -> s _ -> IntMap.empty solution :: Parser Char (IntMap Bool) solution = do _ <- string "SAT\n" IntMap.fromList <$> values values :: Parser Char [(Int, Bool)] values = (value `sepBy` token ' ') <* string " 0" <* (() <$ token '\n' <|> eof) value :: Parser Char (Int, Bool) value = do i <- integer guard (i /= 0) return (toPair i) where toPair n | n >= 0 = ( n, True) | otherwise = (-n, False)