--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
-- <http://lonsing.github.io/depqbf/ DepQBF> is a solver capable of
-- solving quantified boolean formulae ('QBF').
--------------------------------------------------------------------
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)

-- | This is a 'Solver' for 'QSAT' problems that runs the @depqbf@ solver using
-- the current @PATH@, it tries to run an executable named @depqbf@.
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)

-- Parse the QDIMACS output format, which is described in
-- http://www.qbflib.org/qdimacs.html#output
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

-- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable.
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