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)
parseOutput :: String -> [(Int, Bool)]
parseOutput :: FilePath -> [(Int, Bool)]
parseOutput FilePath
out =
case FilePath -> [FilePath]
lines FilePath
out of
(FilePath
_preamble:[FilePath]
certLines) -> forall a b. (a -> b) -> [a] -> [b]
map FilePath -> (Int, Bool)
parseCertLine [FilePath]
certLines
[] -> forall a. HasCallStack => FilePath -> a
error FilePath
"QDIMACS output without preamble"
where
parseCertLine :: String -> (Int, Bool)
parseCertLine :: FilePath -> (Int, Bool)
parseCertLine FilePath
certLine =
case FilePath -> [FilePath]
words FilePath
certLine of
(FilePath
_v:FilePath
lit:[FilePath]
_) -> FilePath -> (Int, Bool)
parseLiteral FilePath
lit
[FilePath]
_ -> forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"Malformed QDIMACS certificate line: " forall a. [a] -> [a] -> [a]
++ FilePath
certLine
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
$ FilePath -> [(Int, Bool)]
parseOutput FilePath
out
Result
_ ->
forall a. IntMap a
I.empty