--------------------------------------------------------------------
-- |
-- 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
  , depqbfPathArgs
  ) where

import Control.Monad.IO.Class
import Data.Version (Version, makeVersion, parseVersion)
import Ersatz.Problem ( QSAT, writeQdimacs' )
import Ersatz.Solution
import Ersatz.Solver.Common
import qualified Data.IntMap as I
import System.Exit (ExitCode(..))
import System.Process (readProcessWithExitCode)
import qualified Text.ParserCombinators.ReadP as P

-- | 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 = 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)

-- 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 -> Bool) -> [FilePath] -> [FilePath]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Bool
comment) ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath]
lines FilePath
out of
    (FilePath
_preamble:[FilePath]
certLines) -> (FilePath -> (Int, Bool)) -> [FilePath] -> [(Int, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> (Int, Bool)
parseCertLine [FilePath]
certLines
    [] -> FilePath -> [(Int, Bool)]
forall a. HasCallStack => FilePath -> a
error FilePath
"QDIMACS output without preamble"
  where
    comment :: FilePath -> Bool
comment [] = Bool
True
    comment (Char
'c' : FilePath
_) = Bool
True
    comment FilePath
_ = Bool
False

    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]
_ -> FilePath -> (Int, Bool)
forall a. HasCallStack => FilePath -> a
error (FilePath -> (Int, Bool)) -> FilePath -> (Int, Bool)
forall a b. (a -> b) -> a -> b
$ FilePath
"Malformed QDIMACS certificate line: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
certLine

-- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable.
-- This passes different arguments to @depqbf@ depending on its version:
--
-- * If using version 6.03 or later, this passes @[\"--qdo\", \"--no-dynamic-nenofex\"]@.
--
-- * Otherwise, this passes @[\"--qdo\"]@.
depqbfPath :: MonadIO m => FilePath -> Solver QSAT m
depqbfPath :: forall (m :: * -> *). MonadIO m => FilePath -> Solver QSAT m
depqbfPath FilePath
path QSAT
problem = do
  Version
ver <- IO Version -> m Version
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Version -> m Version) -> IO Version -> m Version
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Version
depqbfVersion FilePath
path
  let args :: [FilePath]
args | Version
ver Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
>= [Int] -> Version
makeVersion [Int
6,Int
03]
           = [ FilePath
"--qdo", FilePath
"--no-dynamic-nenofex" ]
           | Bool
otherwise
           = [ FilePath
"--qdo" ]
  FilePath -> [FilePath] -> Solver QSAT m
forall (m :: * -> *).
MonadIO m =>
FilePath -> [FilePath] -> Solver QSAT m
depqbfPathArgs FilePath
path [FilePath]
args QSAT
problem

-- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable
-- as well as a list of command line arguments. They will appear after the problem file name.
depqbfPathArgs :: MonadIO m => FilePath -> [String] -> Solver QSAT m
depqbfPathArgs :: forall (m :: * -> *).
MonadIO m =>
FilePath -> [FilePath] -> Solver QSAT m
depqbfPathArgs FilePath
path [FilePath]
args QSAT
problem = IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall a. IO a -> m a
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 -> QSAT -> IO ()
forall (m :: * -> *) t.
(MonadIO m, QDIMACS t) =>
FilePath -> t -> m ()
writeQdimacs' FilePath
problemPath QSAT
problem

    (ExitCode
exit, FilePath
out, FilePath
_err) <-
      FilePath
-> [FilePath] -> FilePath -> IO (ExitCode, FilePath, FilePath)
readProcessWithExitCode FilePath
path (FilePath
problemPath FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
args) []

    let result :: Result
result = ExitCode -> Result
resultOf ExitCode
exit

    (Result, IntMap Bool) -> IO (Result, IntMap Bool)
forall a. a -> IO a
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)]
parseOutput FilePath
out
        Result
_ ->
          IntMap Bool
forall a. IntMap a
I.empty

-- | Query @depqbf@'s 'Version' by invoking @depqbf --version@ and parsing the
-- output. This assumes that the output can be parsed as a valid 'Version' and
-- that @depqbf@ versions increase in a way that is compatible with the
-- 'Ord Version' instance (see 'depqbfPath', which compares 'Version's using
-- ('>=')).
depqbfVersion :: FilePath -> IO Version
depqbfVersion :: FilePath -> IO Version
depqbfVersion FilePath
path = do
  (ExitCode
exit, FilePath
out, FilePath
err) <-
    FilePath
-> [FilePath] -> FilePath -> IO (ExitCode, FilePath, FilePath)
readProcessWithExitCode FilePath
path [FilePath
"--version"] []

  let parseError :: FilePath -> m a
parseError FilePath
reason =
        FilePath -> m a
forall a. FilePath -> m a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> m a) -> FilePath -> m a
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines
          [ FilePath
"Could not query depqbf version (" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
reason FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
")"
          , FilePath
"Standard output:"
          , FilePath
out
          , FilePath
""
          , FilePath
"Standard error:"
          , FilePath
err
          ]

  case ExitCode
exit of
    ExitCode
ExitSuccess -> do
      -- Should be something like "DepQBF 6.03"
      FilePath
verStrLine <-
        case FilePath -> [FilePath]
lines FilePath
err of
          FilePath
line:[FilePath]
_ -> FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FilePath
line
          [] -> FilePath -> IO FilePath
forall {m :: * -> *} {a}. MonadFail m => FilePath -> m a
parseError FilePath
"no lines of standard error"
      -- Should be something like "6.03"
      FilePath
verStr <-
        case FilePath -> [FilePath]
words FilePath
verStrLine of
          FilePath
_depQBF:FilePath
ver:[FilePath]
_ -> FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FilePath
ver
          [FilePath]
_ -> FilePath -> IO FilePath
forall {m :: * -> *} {a}. MonadFail m => FilePath -> m a
parseError (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"unexpected version number " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
verStrLine
      -- Convert the string to a full Version
      case ReadP Version -> FilePath -> Either FilePath Version
forall a. ReadP a -> FilePath -> Either FilePath a
readEitherP ReadP Version
parseVersion FilePath
verStr of
        Left FilePath
reason -> FilePath -> IO Version
forall {m :: * -> *} {a}. MonadFail m => FilePath -> m a
parseError FilePath
reason
        Right Version
v -> Version -> IO Version
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Version
v
    ExitFailure Int
i ->
      FilePath -> IO Version
forall {m :: * -> *} {a}. MonadFail m => FilePath -> m a
parseError (FilePath -> IO Version) -> FilePath -> IO Version
forall a b. (a -> b) -> a -> b
$ FilePath
"exit code " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
")"

-- | Like @readEither@ from "Text.Read", but accepting an arbitrary 'P.ReadP'
-- argument instead of requiring a 'Read' constraint.
readEitherP :: P.ReadP a -> String -> Either String a
readEitherP :: forall a. ReadP a -> FilePath -> Either FilePath a
readEitherP ReadP a
rp FilePath
s =
  case [ a
x | (a
x,FilePath
"") <- ReadP a -> ReadS a
forall a. ReadP a -> ReadS a
P.readP_to_S ReadP a
read' FilePath
s ] of
    [a
x] -> a -> Either FilePath a
forall a b. b -> Either a b
Right a
x
    []  -> FilePath -> Either FilePath a
forall a b. a -> Either a b
Left FilePath
"no parse"
    [a]
_   -> FilePath -> Either FilePath a
forall a b. a -> Either a b
Left FilePath
"ambiguous parse"
 where
  read' :: ReadP a
read' = do
    a
x <- ReadP a
rp
    ReadP ()
P.skipSpaces
    a -> ReadP a
forall a. a -> ReadP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x