{-# language OverloadedStrings #-}
module Ersatz.Solver.Minisat
( minisat
, cryptominisat
, minisatPath
, cryptominisat5
, cryptominisat5Path
, anyminisat
) 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' )
anyminisat :: Solver SAT IO
anyminisat :: Solver SAT IO
anyminisat = forall s. [Solver s IO] -> Solver s IO
trySolvers [forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat5, forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat, forall (m :: * -> *). MonadIO m => Solver SAT m
minisat]
minisat :: MonadIO m => Solver SAT m
minisat :: forall (m :: * -> *). MonadIO m => Solver SAT m
minisat = forall (m :: * -> *). MonadIO m => [Char] -> Solver SAT m
minisatPath [Char]
"minisat"
cryptominisat :: MonadIO m => Solver SAT m
cryptominisat :: forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat = forall (m :: * -> *). MonadIO m => [Char] -> Solver SAT m
minisatPath [Char]
"cryptominisat"
minisatPath :: MonadIO m => FilePath -> Solver SAT m
minisatPath :: forall (m :: * -> *). MonadIO m => [Char] -> Solver SAT m
minisatPath [Char]
path SAT
problem = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
MonadIO m =>
[Char] -> [Char] -> ([Char] -> [Char] -> IO a) -> m a
withTempFiles [Char]
".cnf" [Char]
"" forall a b. (a -> b) -> a -> b
$ \[Char]
problemPath [Char]
solutionPath -> do
forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
withFile [Char]
problemPath IOMode
WriteMode forall a b. (a -> b) -> a -> b
$ \Handle
fh ->
Handle -> Builder -> IO ()
hPutBuilder Handle
fh (forall t. DIMACS t => t -> Builder
dimacs SAT
problem)
(ExitCode
exit, [Char]
_out, [Char]
_err) <-
[Char] -> [[Char]] -> [Char] -> IO (ExitCode, [Char], [Char])
readProcessWithExitCode [Char]
path [[Char]
problemPath, [Char]
solutionPath] []
IntMap Bool
sol <- [Char] -> IO (IntMap Bool)
parseSolutionFile [Char]
solutionPath
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode -> Result
resultOf ExitCode
exit, IntMap Bool
sol)
parseSolutionFile :: FilePath -> IO (IntMap Bool)
parseSolutionFile :: [Char] -> IO (IntMap Bool)
parseSolutionFile [Char]
path = forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle IOException -> IO (IntMap Bool)
handler (ByteString -> IntMap Bool
parseSolution forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO ByteString
B.readFile [Char]
path)
where
handler :: IOException -> IO (IntMap Bool)
handler :: IOException -> IO (IntMap Bool)
handler IOException
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. IntMap a
IntMap.empty
parseSolution :: B.ByteString -> IntMap Bool
parseSolution :: ByteString -> IntMap Bool
parseSolution ByteString
s =
case ByteString -> [ByteString]
B.words ByteString
s of
ByteString
x : [ByteString]
ys | ByteString
x forall a. Eq a => a -> a -> Bool
== ByteString
"SAT" ->
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ( \ IntMap Bool
m ByteString
y -> case ByteString -> Maybe (Int, ByteString)
B.readInt ByteString
y of
Just (Int
v,ByteString
_) -> if Int
0 forall a. Eq a => a -> a -> Bool
== Int
v then IntMap Bool
m else forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (forall a. Num a => a -> a
abs Int
v) (Int
vforall a. Ord a => a -> a -> Bool
>Int
0) IntMap Bool
m
Maybe (Int, ByteString)
Nothing -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"parseSolution: Expected an Int, received " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ByteString
y
) forall a. IntMap a
IntMap.empty [ByteString]
ys
[ByteString]
_ -> forall a. IntMap a
IntMap.empty
cryptominisat5 :: MonadIO m => Solver SAT m
cryptominisat5 :: forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat5 = forall (m :: * -> *). MonadIO m => [Char] -> Solver SAT m
cryptominisat5Path [Char]
"cryptominisat5"
cryptominisat5Path :: MonadIO m => FilePath -> Solver SAT m
cryptominisat5Path :: forall (m :: * -> *). MonadIO m => [Char] -> Solver SAT m
cryptominisat5Path [Char]
path SAT
problem = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
MonadIO m =>
[Char] -> [Char] -> ([Char] -> [Char] -> IO a) -> m a
withTempFiles [Char]
".cnf" [Char]
"" forall a b. (a -> b) -> a -> b
$ \[Char]
problemPath [Char]
_ -> do
forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
withFile [Char]
problemPath IOMode
WriteMode forall a b. (a -> b) -> a -> b
$ \Handle
fh ->
Handle -> Builder -> IO ()
hPutBuilder Handle
fh (forall t. DIMACS t => t -> Builder
dimacs SAT
problem)
(ExitCode
exit, [Char]
out, [Char]
_err) <-
[Char] -> [[Char]] -> [Char] -> IO (ExitCode, [Char], [Char])
readProcessWithExitCode [Char]
path [[Char]
problemPath] []
let sol :: IntMap Bool
sol = [Char] -> IntMap Bool
parseSolution5 [Char]
out
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode -> Result
resultOf ExitCode
exit, IntMap Bool
sol)