--------------------------------------------------------------------
-- |
-- 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 :: Solver QSAT m
depqbf = FilePath -> Solver QSAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver QSAT m
depqbfPath FilePath
"depqbf"

parseLiteral :: String -> (Int, Bool)
parseLiteral :: FilePath -> (Int, Bool)
parseLiteral (Char
'-':FilePath
xs) = (FilePath -> Int
forall a. Read a => FilePath -> a
read FilePath
xs, Bool
False)
parseLiteral FilePath
xs = (FilePath -> Int
forall a. Read a => FilePath -> a
read FilePath
xs, Bool
True)

-- | 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 :: FilePath -> Solver QSAT m
depqbfPath FilePath
path QSAT
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 (QSAT -> Builder
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

    (Result, IntMap Bool) -> IO (Result, IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Result, IntMap Bool) -> IO (Result, IntMap Bool))
-> (Result, IntMap Bool) -> IO (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$ (,) Result
result (IntMap Bool -> (Result, IntMap Bool))
-> IntMap Bool -> (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$
      case Result
result of
        Result
Satisfied ->
          [(Int, Bool)] -> IntMap Bool
forall a. [(Int, a)] -> IntMap a
I.fromList ([(Int, Bool)] -> IntMap Bool) -> [(Int, Bool)] -> IntMap Bool
forall a b. (a -> b) -> a -> b
$ (FilePath -> (Int, Bool)) -> [FilePath] -> [(Int, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> (Int, Bool)
parseLiteral (FilePath -> (Int, Bool))
-> (FilePath -> FilePath) -> FilePath -> (Int, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> FilePath
forall a. [a] -> a
head ([FilePath] -> FilePath)
-> (FilePath -> [FilePath]) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> [FilePath]
forall a. [a] -> [a]
tail ([FilePath] -> [FilePath])
-> (FilePath -> [FilePath]) -> FilePath -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
words) ([FilePath] -> [(Int, Bool)]) -> [FilePath] -> [(Int, Bool)]
forall a b. (a -> b) -> a -> b
$ [FilePath] -> [FilePath]
forall a. [a] -> [a]
tail ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath]
lines FilePath
out
        Result
_ ->
          IntMap Bool
forall a. IntMap a
I.empty