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 = depqbfPath "depqbf"
parseLiteral :: String -> (Int, Bool)
parseLiteral ('-':xs) = (read xs, False)
parseLiteral xs = (read xs, True)
depqbfPath :: MonadIO m => FilePath -> Solver QSAT m
depqbfPath path problem = liftIO $
withTempFiles ".cnf" "" $ \problemPath _ -> do
withFile problemPath WriteMode $ \fh ->
hPutBuilder fh (qdimacs problem)
(exit, out, _err) <-
readProcessWithExitCode path [problemPath, "--qdo"] []
let result = resultOf exit
return $ (,) result $
case result of
Satisfied ->
I.fromList $ map (parseLiteral . head . tail . words) $ tail $ lines out
_ ->
I.empty