{-# 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 = [Solver SAT IO] -> Solver SAT IO
forall s. [Solver s IO] -> Solver s IO
trySolvers [Solver SAT IO
forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat5, Solver SAT IO
forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat, Solver SAT IO
forall (m :: * -> *). MonadIO m => Solver SAT m
minisat]
minisat :: MonadIO m => Solver SAT m
minisat :: Solver SAT m
minisat = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
minisatPath FilePath
"minisat"
cryptominisat :: MonadIO m => Solver SAT m
cryptominisat :: Solver SAT m
cryptominisat = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
minisatPath FilePath
"cryptominisat"
minisatPath :: MonadIO m => FilePath -> Solver SAT m
minisatPath :: FilePath -> Solver SAT m
minisatPath 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
solutionPath -> 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
problemPath, FilePath
solutionPath] []
IntMap Bool
sol <- FilePath -> IO (IntMap Bool)
parseSolutionFile FilePath
solutionPath
(Result, IntMap Bool) -> IO (Result, IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode -> Result
resultOf ExitCode
exit, IntMap Bool
sol)
parseSolutionFile :: FilePath -> IO (IntMap Bool)
parseSolutionFile :: FilePath -> IO (IntMap Bool)
parseSolutionFile FilePath
path = (IOException -> IO (IntMap Bool))
-> IO (IntMap Bool) -> IO (IntMap Bool)
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle IOException -> IO (IntMap Bool)
handler (ByteString -> IntMap Bool
parseSolution (ByteString -> IntMap Bool) -> IO ByteString -> IO (IntMap Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO ByteString
B.readFile FilePath
path)
where
handler :: IOException -> IO (IntMap Bool)
handler :: IOException -> IO (IntMap Bool)
handler IOException
_ = IntMap Bool -> IO (IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap Bool
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 ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
"SAT" ->
(IntMap Bool -> ByteString -> IntMap Bool)
-> IntMap Bool -> [ByteString] -> IntMap Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ( \ IntMap Bool
m ByteString
y -> let Just (Int
v,ByteString
_) = ByteString -> Maybe (Int, ByteString)
B.readInt ByteString
y
in if Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
v then IntMap Bool
m else Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Int -> Int
forall a. Num a => a -> a
abs Int
v) (Int
vInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
0) IntMap Bool
m
) IntMap Bool
forall a. IntMap a
IntMap.empty [ByteString]
ys
[ByteString]
_ -> IntMap Bool
forall a. IntMap a
IntMap.empty
cryptominisat5 :: MonadIO m => Solver SAT m
cryptominisat5 :: Solver SAT m
cryptominisat5 = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
cryptominisat5Path FilePath
"cryptominisat5"
cryptominisat5Path :: MonadIO m => FilePath -> Solver SAT m
cryptominisat5Path :: FilePath -> Solver SAT m
cryptominisat5Path 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
problemPath] []
let sol :: IntMap Bool
sol = FilePath -> IntMap Bool
parseSolution5 FilePath
out
(Result, IntMap Bool) -> IO (Result, IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode -> Result
resultOf ExitCode
exit, IntMap Bool
sol)
parseSolution5 :: String -> IntMap Bool
parseSolution5 :: FilePath -> IntMap Bool
parseSolution5 FilePath
txt = [(Int, Bool)] -> IntMap Bool
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int -> Int
forall a. Num a => a -> a
abs Int
v, Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) | Int
v <- [Int]
vars, Int
v Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0]
where
vlines :: [FilePath]
vlines = [FilePath
l | (Char
'v':FilePath
l) <- FilePath -> [FilePath]
lines FilePath
txt]
vars :: [Int]
vars = (FilePath -> Int) -> [FilePath] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Int
forall a. Read a => FilePath -> a
read ((FilePath -> [FilePath]) -> [FilePath] -> [FilePath]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap FilePath -> [FilePath]
words [FilePath]
vlines)