{- |
Module      :  ./QBF/ProveDepQBF.hs
Description :  Interface to the theorem prover e-krhyper in CASC-mode.
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  provisional
Portability :  needs POSIX

see <http://fmv.jku.at/depqbf/ for more information
on the depqbf prover and <http://www.qbflib.org/qdimacs.html>
and <http://www.qbflib.org/Draft/qDimacs.ps.gz>
for more information on the qdimacs input format

-}

module QBF.ProveDepQBF (depQBFProver)
    where

import Logic.Prover

import Common.ProofTree
import qualified Common.Result as Result
import Common.AS_Annotation as AS_Anno
import Common.Timing
import Common.Utils

import Propositional.Sign
import QBF.ProverState
import qualified QBF.AS_BASIC_QBF as AS
import QBF.Morphism
import QBF.Sublogic (QBFSL, top)

import GUI.GenericATP
import Proofs.BatchProcessing
import Interfaces.GenericATPState

import System.Directory

import Control.Monad (when)
import qualified Control.Concurrent as Concurrent
import System.Exit (ExitCode (..))

import Data.List

import Data.Time.LocalTime (TimeOfDay)

-- Prover

depqbfS :: String
depqbfS :: String
depqbfS = "depqbf"

-- | The Prover implementation.
depQBFProver :: Prover Sign AS.FORMULA Morphism QBFSL ProofTree
depQBFProver :: Prover Sign FORMULA Morphism QBFSL ProofTree
depQBFProver =
  String
-> String
-> QBFSL
-> (String
    -> Theory Sign FORMULA ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO [ProofStatus ProofTree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus ProofTree])
    -> String
    -> TacticScript
    -> Theory Sign FORMULA ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO (ThreadId, MVar ()))
-> Prover Sign FORMULA Morphism QBFSL ProofTree
forall sublogics theory sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO [ProofStatus proof_tree])
-> (Bool
    -> Bool
    -> MVar (Result [ProofStatus proof_tree])
    -> String
    -> TacticScript
    -> theory
    -> [FreeDefMorphism sentence morphism]
    -> IO (ThreadId, MVar ()))
-> ProverTemplate theory sentence morphism sublogics proof_tree
mkAutomaticProver String
depqbfS String
depqbfS QBFSL
top String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO [ProofStatus ProofTree]
depQBFGUI Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (ThreadId, MVar ())
depQBFCMDLautomaticBatch

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: String -- ^ theory name
  -> ATPFunctions Sign AS.FORMULA Morphism ProofTree QBFProverState
atpFun :: String
-> ATPFunctions Sign FORMULA Morphism ProofTree QBFProverState
atpFun thName :: String
thName = ATPFunctions :: forall sign sentence morphism proof_tree pst.
InitialProverState sign sentence morphism pst
-> TransSenName
-> (pst -> Named sentence -> pst)
-> (pst -> Named sentence -> [String] -> IO String)
-> String
-> String
-> FileExtensions
-> RunProver sentence proof_tree pst
-> (GenericConfig proof_tree -> [String])
-> ATPFunctions sign sentence morphism proof_tree pst
ATPFunctions
  { initialProverState :: InitialProverState Sign FORMULA Morphism QBFProverState
initialProverState = InitialProverState Sign FORMULA Morphism QBFProverState
qbfProverState
  , atpTransSenName :: TransSenName
atpTransSenName = TransSenName
transSenName
  , atpInsertSentence :: QBFProverState -> Named FORMULA -> QBFProverState
atpInsertSentence = QBFProverState -> Named FORMULA -> QBFProverState
insertSentence
  , goalOutput :: QBFProverState -> Named FORMULA -> [String] -> IO String
goalOutput = String -> QBFProverState -> Named FORMULA -> [String] -> IO String
showQDIMACSProblem String
thName
  , proverHelpText :: String
proverHelpText = "for more information visit " String -> TransSenName
forall a. [a] -> [a] -> [a]
++
                     "http://fmv.jku.at/depqbf/"
  , batchTimeEnv :: String
batchTimeEnv = ""
  , fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions
      { problemOutput :: String
problemOutput = ".qdimacs"
      , proverOutput :: String
proverOutput = ""        -- prover doesn't output any files
      , theoryConfiguration :: String
theoryConfiguration = "" -- prover doesn't use any configuration files
      }
  , runProver :: RunProver FORMULA ProofTree QBFProverState
runProver = RunProver FORMULA ProofTree QBFProverState
runDepQBF
  , createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts }

{- |
  Invokes the generic prover GUI.
-}
depQBFGUI :: String -- ^ theory name
           -> Theory Sign AS.FORMULA ProofTree
           -> [FreeDefMorphism AS.FORMULA Morphism] -- ^ freeness constraints
           -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
depQBFGUI :: String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO [ProofStatus ProofTree]
depQBFGUI thName :: String
thName th :: Theory Sign FORMULA ProofTree
th freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs =
    ATPFunctions Sign FORMULA Morphism ProofTree QBFProverState
-> Bool
-> String
-> String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> ProofTree
-> IO [ProofStatus ProofTree]
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> String
-> String
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO [ProofStatus proof_tree]
genericATPgui (String
-> ATPFunctions Sign FORMULA Morphism ProofTree QBFProverState
atpFun String
thName) Bool
True (Prover Sign FORMULA Morphism QBFSL ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign FORMULA Morphism QBFSL ProofTree
depQBFProver) String
thName Theory Sign FORMULA ProofTree
th
                  [FreeDefMorphism FORMULA Morphism]
freedefs ProofTree
emptyProofTree

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the prover.
-}
depQBFCMDLautomaticBatch ::
           Bool -- ^ True means include proved theorems
        -> Bool -- ^ True means save problem file
        -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])
           -- ^ used to store the result of the batch run
        -> String -- ^ theory name
        -> TacticScript -- ^ default tactic script
        -> Theory Sign AS.FORMULA ProofTree
        -> [FreeDefMorphism AS.FORMULA Morphism] -- ^ freeness constraints
        -> IO (Concurrent.ThreadId, Concurrent.MVar ())
           {- ^ fst: identifier of the batch thread for killing it
           snd: MVar to wait for the end of the thread -}
depQBFCMDLautomaticBatch :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (ThreadId, MVar ())
depQBFCMDLautomaticBatch inclProvedThs :: Bool
inclProvedThs saveProblem_batch :: Bool
saveProblem_batch resultMVar :: MVar (Result [ProofStatus ProofTree])
resultMVar
                        thName :: String
thName defTS :: TacticScript
defTS th :: Theory Sign FORMULA ProofTree
th freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs =
    ATPFunctions Sign FORMULA Morphism ProofTree QBFProverState
-> Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> String
-> ATPTacticScript
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> ProofTree
-> IO (ThreadId, MVar ())
forall sentence proof_tree sign mor pst.
(Show sentence, Ord proof_tree, Ord sentence) =>
ATPFunctions sign sentence mor proof_tree pst
-> Bool
-> Bool
-> MVar (Result [ProofStatus proof_tree])
-> String
-> String
-> ATPTacticScript
-> Theory sign sentence proof_tree
-> [FreeDefMorphism sentence mor]
-> proof_tree
-> IO (ThreadId, MVar ())
genericCMDLautomaticBatch (String
-> ATPFunctions Sign FORMULA Morphism ProofTree QBFProverState
atpFun String
thName) Bool
inclProvedThs Bool
saveProblem_batch
        MVar (Result [ProofStatus ProofTree])
resultMVar (Prover Sign FORMULA Morphism QBFSL ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign FORMULA Morphism QBFSL ProofTree
depQBFProver) String
thName
        (Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit [] TacticScript
defTS) Theory Sign FORMULA ProofTree
th [FreeDefMorphism FORMULA Morphism]
freedefs ProofTree
emptyProofTree

runDepQBF :: QBFProverState
           {- ^ logical part containing the input Sign and axioms and possibly
           goals that have been proved earlier as additional axioms -}
           -> GenericConfig ProofTree -- ^ configuration to use
           -> Bool -- ^ True means save QDIMACS file
           -> String -- ^ name of the theory in the DevGraph
           -> AS_Anno.Named AS.FORMULA -- ^ goal to prove
           -> IO (ATPRetval, GenericConfig ProofTree)
           -- ^ (retval, configuration with proof status and complete output)
runDepQBF :: RunProver FORMULA ProofTree QBFProverState
runDepQBF ps :: QBFProverState
ps cfg :: GenericConfig ProofTree
cfg saveQDIMACS :: Bool
saveQDIMACS thName :: String
thName nGoal :: Named FORMULA
nGoal = do
    let saveFile :: String
saveFile = TransSenName
basename String
thName String -> TransSenName
forall a. [a] -> [a] -> [a]
++ '_' Char -> TransSenName
forall a. a -> [a] -> [a]
: Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal String -> TransSenName
forall a. [a] -> [a] -> [a]
++ ".qdimacs"
        tl :: Int
tl = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg
    String
prob <- String -> QBFProverState -> Named FORMULA -> [String] -> IO String
showQDIMACSProblem String
thName QBFProverState
ps Named FORMULA
nGoal []
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveQDIMACS (String -> String -> IO ()
writeFile String
saveFile String
prob)
    String
stpTmpFile <- String -> String -> IO String
getTempFile String
prob String
saveFile
    HetsTime
t_start <- IO HetsTime
getHetsTime
    (exitCode :: ExitCode
exitCode, stdoutC :: String
stdoutC, stderrC :: String
stderrC) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
depqbfS
        (Int -> String
forall a. Show a => a -> String
show Int
tl String -> [String] -> [String]
forall a. a -> [a] -> [a]
: GenericConfig ProofTree -> [String]
forall proof_tree. GenericConfig proof_tree -> [String]
extraOpts GenericConfig ProofTree
cfg [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
stpTmpFile]) ""
    HetsTime
t_end <- IO HetsTime
getHetsTime
    String -> IO ()
removeFile String
stpTmpFile
    let t_u :: TimeOfDay
t_u = HetsTime -> HetsTime -> TimeOfDay
diffHetsTime HetsTime
t_end HetsTime
t_start
        exitCode' :: Int
exitCode' = case ExitCode
exitCode of
                      ExitSuccess -> 0
                      ExitFailure i :: Int
i -> Int
i
    (pStat :: ATPRetval
pStat, ret :: ProofStatus ProofTree
ret) <- QBFProverState
-> GenericConfig ProofTree
-> String
-> String
-> Int
-> Named FORMULA
-> TimeOfDay
-> Int
-> IO (ATPRetval, ProofStatus ProofTree)
examineProof QBFProverState
ps GenericConfig ProofTree
cfg String
stdoutC String
stderrC Int
exitCode' Named FORMULA
nGoal TimeOfDay
t_u Int
tl
    (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
pStat, GenericConfig ProofTree
cfg
            { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree
ret
            , resultOutput :: [String]
resultOutput = String -> [String]
lines (String
stdoutC String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
stderrC)
            , timeUsed :: TimeOfDay
timeUsed = ProofStatus ProofTree -> TimeOfDay
forall proof_tree. ProofStatus proof_tree -> TimeOfDay
usedTime ProofStatus ProofTree
ret })

-- | examine Prover output
examineProof :: QBFProverState
             -> GenericConfig ProofTree
             -> String
             -> String
             -> Int
             -> AS_Anno.Named AS.FORMULA
             -> TimeOfDay
             -> Int
             -> IO (ATPRetval, ProofStatus ProofTree)
examineProof :: QBFProverState
-> GenericConfig ProofTree
-> String
-> String
-> Int
-> Named FORMULA
-> TimeOfDay
-> Int
-> IO (ATPRetval, ProofStatus ProofTree)
examineProof ps :: QBFProverState
ps _ stdoutC :: String
stdoutC _ exitCode :: Int
exitCode nGoal :: Named FORMULA
nGoal tUsed :: TimeOfDay
tUsed _ =
    let
        defaultStatus :: ProofStatus ProofTree
defaultStatus = (String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus
          (Named FORMULA -> String
forall s a. SenAttr s a -> a
senAttr Named FORMULA
nGoal)
          (Prover Sign FORMULA Morphism QBFSL ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
proverName Prover Sign FORMULA Morphism QBFSL ProofTree
depQBFProver)
          (ProofTree
emptyProofTree)) { usedTime :: TimeOfDay
usedTime = TimeOfDay
tUsed }
        getAxioms :: [String]
getAxioms = (Named FORMULA -> String) -> [Named FORMULA] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr (QBFProverState -> [Named FORMULA]
initialAxioms QBFProverState
ps)
    in case Int -> String -> DepQBFResult
getDepQBFResult Int
exitCode String
stdoutC of
               DepQBFProved -> (ATPRetval, ProofStatus ProofTree)
-> IO (ATPRetval, ProofStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
ATPSuccess, ProofStatus ProofTree
defaultStatus
                                  {
                                    goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True
                                  , usedAxioms :: [String]
usedAxioms = [String]
getAxioms
                                  })
               DepQBFTimeout -> (ATPRetval, ProofStatus ProofTree)
-> IO (ATPRetval, ProofStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
ATPTLimitExceeded, ProofStatus ProofTree
defaultStatus)
               DepQBFDisproved -> (ATPRetval, ProofStatus ProofTree)
-> IO (ATPRetval, ProofStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
ATPSuccess, ProofStatus ProofTree
defaultStatus
                                     {
                                       goalStatus :: GoalStatus
goalStatus = GoalStatus
Disproved
                                     , usedAxioms :: [String]
usedAxioms = [String]
getAxioms
                                     })
               DepQBFError s :: String
s -> (ATPRetval, ProofStatus ProofTree)
-> IO (ATPRetval, ProofStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> ATPRetval
ATPError ("Internal Errorr."
                                           String -> TransSenName
forall a. [a] -> [a] -> [a]
++ "\nMessage:\n\n" String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
s)
                                , ProofStatus ProofTree
defaultStatus)

data DepQBFResult = DepQBFProved | DepQBFDisproved
                  | DepQBFTimeout | DepQBFError String

getDepQBFResult :: Int -> String -> DepQBFResult
getDepQBFResult :: Int -> String -> DepQBFResult
getDepQBFResult exitCode :: Int
exitCode out :: String
out = case Int
exitCode of
                                 10 -> if "SAT" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
out
                                       then DepQBFResult
DepQBFProved
                                       else String -> DepQBFResult
DepQBFError
                                         "Unexpected behaviour of prover!"
                                 20 -> if "UNSAT" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
out
                                       then DepQBFResult
DepQBFDisproved
                                       else String -> DepQBFResult
DepQBFError
                                         "Unexpected behaviour of prover!"
                                 _ -> if "SIGALRM" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` String
out
                                      then DepQBFResult
DepQBFTimeout
                                      else String -> DepQBFResult
DepQBFError
                                        ("Uknown error: " String -> TransSenName
forall a. [a] -> [a] -> [a]
++ String
out)