module Ersatz.Solver.DepQBF
( depqbf
, depqbfPath
) where
import Data.ByteString.Builder
import Control.Monad.IO.Class
import Ersatz.Problem
import Ersatz.Solution
import Ersatz.Solver.Common
import qualified Data.IntMap as I
import System.IO
import System.Process (readProcessWithExitCode)
depqbf :: MonadIO m => Solver QSAT m
depqbf :: forall (m :: * -> *). MonadIO m => Solver QSAT m
depqbf = forall (m :: * -> *). MonadIO m => FilePath -> Solver QSAT m
depqbfPath FilePath
"depqbf"
parseLiteral :: String -> (Int, Bool)
parseLiteral :: FilePath -> (Int, Bool)
parseLiteral (Char
'-':FilePath
xs) = (forall a. Read a => FilePath -> a
read FilePath
xs, Bool
False)
parseLiteral FilePath
xs = (forall a. Read a => FilePath -> a
read FilePath
xs, Bool
True)
depqbfPath :: MonadIO m => FilePath -> Solver QSAT m
depqbfPath :: forall (m :: * -> *). MonadIO m => FilePath -> Solver QSAT m
depqbfPath FilePath
path QSAT
problem = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
MonadIO m =>
FilePath -> FilePath -> (FilePath -> FilePath -> IO a) -> m a
withTempFiles FilePath
".cnf" FilePath
"" forall a b. (a -> b) -> a -> b
$ \FilePath
problemPath FilePath
_ -> do
forall r. FilePath -> IOMode -> (Handle -> IO r) -> IO r
withFile FilePath
problemPath IOMode
WriteMode forall a b. (a -> b) -> a -> b
$ \Handle
fh ->
Handle -> Builder -> IO ()
hPutBuilder Handle
fh (forall t. QDIMACS t => t -> Builder
qdimacs QSAT
problem)
(ExitCode
exit, FilePath
out, FilePath
_err) <-
FilePath
-> [FilePath] -> FilePath -> IO (ExitCode, FilePath, FilePath)
readProcessWithExitCode FilePath
path [FilePath
problemPath, FilePath
"--qdo"] []
let result :: Result
result = ExitCode -> Result
resultOf ExitCode
exit
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (,) Result
result forall a b. (a -> b) -> a -> b
$
case Result
result of
Result
Satisfied ->
forall a. [(Int, a)] -> IntMap a
I.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> (Int, Bool)
parseLiteral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
tail forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
words) forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
tail forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath]
lines FilePath
out
Result
_ ->
forall a. IntMap a
I.empty