{- |
Module      :  ./Propositional/Prove.hs
Description :  Provers for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

This is the connection of the SAT-Solver minisat to Hets
-}

module Propositional.Prove
    ( zchaffProver                   -- the zChaff II Prover
    , propConsChecker
    ) where

import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
import qualified Propositional.Conversions as Cons
import qualified Propositional.Conversions as PC
import qualified Propositional.Morphism as PMorphism
import qualified Propositional.ProverState as PState
import qualified Propositional.Sign as Sig
import Propositional.Sublogic (PropSL, top)

import Proofs.BatchProcessing

import qualified Logic.Prover as LP

import Interfaces.GenericATPState
import GUI.GenericATP

import Common.IO
import Common.ProofTree
import Common.Utils
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.OrderedMap as OMap
import qualified Common.Result as Result

import Control.Monad (when)
import qualified Control.Concurrent as Concurrent

import Data.List
import Data.Maybe
import Data.Time (TimeOfDay, timeToTimeOfDay, midnight)

import System.Directory
import System.Exit

-- * Prover implementation

zchaffHelpText :: String
zchaffHelpText :: String
zchaffHelpText = "Zchaff is a very fast SAT-Solver \n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                 "No additional Options are available" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                 "for it!"

-- | the name of the prover
zchaffS :: String
zchaffS :: String
zchaffS = "zchaff"

{- |
  The Prover implementation.

  Implemented are: a prover GUI, and both commandline prover interfaces.
-}
zchaffProver
  :: LP.Prover Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism PropSL ProofTree
zchaffProver :: Prover Sign FORMULA Morphism PropSL ProofTree
zchaffProver = String
-> String
-> PropSL
-> (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 PropSL 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
LP.mkAutomaticProver String
zchaffS String
zchaffS PropSL
top String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO [ProofStatus ProofTree]
zchaffProveGUI
  Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (ThreadId, MVar ())
zchaffProveCMDLautomaticBatch

{- |
   The Consistency Cheker.
-}
propConsChecker :: LP.ConsChecker Sig.Sign AS_BASIC.FORMULA PropSL
                                  PMorphism.Morphism ProofTree
propConsChecker :: ConsChecker Sign FORMULA PropSL Morphism ProofTree
propConsChecker = String
-> String
-> PropSL
-> (String
    -> TacticScript
    -> TheoryMorphism Sign FORMULA Morphism ProofTree
    -> [FreeDefMorphism FORMULA Morphism]
    -> IO (CCStatus ProofTree))
-> ConsChecker Sign FORMULA PropSL Morphism ProofTree
forall sublogics sign sentence morphism proof_tree.
String
-> String
-> sublogics
-> (String
    -> TacticScript
    -> TheoryMorphism sign sentence morphism proof_tree
    -> [FreeDefMorphism sentence morphism]
    -> IO (CCStatus proof_tree))
-> ConsChecker sign sentence sublogics morphism proof_tree
LP.mkUsableConsChecker String
zchaffS String
zchaffS PropSL
top String
-> TacticScript
-> TheoryMorphism Sign FORMULA Morphism ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (CCStatus ProofTree)
consCheck

consCheck :: String -> LP.TacticScript
   -> LP.TheoryMorphism Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism ProofTree
   -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]
    -- ^ free definitions
   -> IO (LP.CCStatus ProofTree)
consCheck :: String
-> TacticScript
-> TheoryMorphism Sign FORMULA Morphism ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (CCStatus ProofTree)
consCheck thName :: String
thName _ tm :: TheoryMorphism Sign FORMULA Morphism ProofTree
tm _ =
    case TheoryMorphism Sign FORMULA Morphism ProofTree
-> Theory Sign FORMULA ProofTree
forall sign sen mor proof_tree.
TheoryMorphism sign sen mor proof_tree
-> Theory sign sen proof_tree
LP.tTarget TheoryMorphism Sign FORMULA Morphism ProofTree
tm of
      LP.Theory sig :: Sign
sig nSens :: ThSens FORMULA (ProofStatus ProofTree)
nSens -> do
            let axioms :: [Named FORMULA]
axioms = [SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA]
getAxioms ([SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA])
-> [SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA]
forall a b. (a -> b) -> a -> b
$ ([String], [SenStatus FORMULA (ProofStatus ProofTree)])
-> [SenStatus FORMULA (ProofStatus ProofTree)]
forall a b. (a, b) -> b
snd (([String], [SenStatus FORMULA (ProofStatus ProofTree)])
 -> [SenStatus FORMULA (ProofStatus ProofTree)])
-> ([String], [SenStatus FORMULA (ProofStatus ProofTree)])
-> [SenStatus FORMULA (ProofStatus ProofTree)]
forall a b. (a -> b) -> a -> b
$ [(String, SenStatus FORMULA (ProofStatus ProofTree))]
-> ([String], [SenStatus FORMULA (ProofStatus ProofTree)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(String, SenStatus FORMULA (ProofStatus ProofTree))]
 -> ([String], [SenStatus FORMULA (ProofStatus ProofTree)]))
-> [(String, SenStatus FORMULA (ProofStatus ProofTree))]
-> ([String], [SenStatus FORMULA (ProofStatus ProofTree)])
forall a b. (a -> b) -> a -> b
$ ThSens FORMULA (ProofStatus ProofTree)
-> [(String, SenStatus FORMULA (ProofStatus ProofTree))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens FORMULA (ProofStatus ProofTree)
nSens
                thName_clean :: String
thName_clean = String -> String
basename String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_cc.zchaff.dimacs"
            String
dimacsOutput <- String
-> Sign -> [Named FORMULA] -> Maybe (Named FORMULA) -> IO String
PC.showDIMACSProblem (String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_cc")
                             Sign
sig [Named FORMULA]
axioms Maybe (Named FORMULA)
forall a. Maybe a
Nothing
            String
tmpFile <- String -> String -> IO String
getTempFile String
dimacsOutput String
thName_clean
            (exitCode :: ExitCode
exitCode, resultHf :: String
resultHf, err :: String
err) <-
              String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
zchaffS [String
tmpFile] ""
            CCStatus ProofTree -> IO (CCStatus ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (CCStatus ProofTree -> IO (CCStatus ProofTree))
-> CCStatus ProofTree -> IO (CCStatus ProofTree)
forall a b. (a -> b) -> a -> b
$ if ExitCode
exitCode ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
/= ExitCode
ExitSuccess then ProofTree -> TimeOfDay -> Maybe Bool -> CCStatus ProofTree
forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
LP.CCStatus
                   (String -> ProofTree
ProofTree (String -> ProofTree) -> String -> ProofTree
forall a b. (a -> b) -> a -> b
$ (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
err then "" else String
err String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")
                                  String -> String -> String
forall a. [a] -> [a] -> [a]
++ "error by call zchaff " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
thName)
                   TimeOfDay
midnight Maybe Bool
forall a. Maybe a
Nothing
               else ProofTree -> TimeOfDay -> Maybe Bool -> CCStatus ProofTree
forall proof_tree.
proof_tree -> TimeOfDay -> Maybe Bool -> CCStatus proof_tree
LP.CCStatus (String -> ProofTree
ProofTree String
resultHf) TimeOfDay
midnight
                       (Maybe Bool -> CCStatus ProofTree)
-> Maybe Bool -> CCStatus ProofTree
forall a b. (a -> b) -> a -> b
$ String -> Maybe Bool
searchResult String
resultHf
    where
        getAxioms :: [LP.SenStatus AS_BASIC.FORMULA (LP.ProofStatus ProofTree)]
                  -> [AS_Anno.Named AS_BASIC.FORMULA]
        getAxioms :: [SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA]
getAxioms f :: [SenStatus FORMULA (ProofStatus ProofTree)]
f = (SenStatus FORMULA (ProofStatus ProofTree) -> Named FORMULA)
-> [SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (String -> FORMULA -> Named FORMULA
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed "consistency" (FORMULA -> Named FORMULA)
-> (SenStatus FORMULA (ProofStatus ProofTree) -> FORMULA)
-> SenStatus FORMULA (ProofStatus ProofTree)
-> Named FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenStatus FORMULA (ProofStatus ProofTree) -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence)
          ([SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA])
-> [SenStatus FORMULA (ProofStatus ProofTree)] -> [Named FORMULA]
forall a b. (a -> b) -> a -> b
$ (SenStatus FORMULA (ProofStatus ProofTree) -> Bool)
-> [SenStatus FORMULA (ProofStatus ProofTree)]
-> [SenStatus FORMULA (ProofStatus ProofTree)]
forall a. (a -> Bool) -> [a] -> [a]
filter SenStatus FORMULA (ProofStatus ProofTree) -> Bool
forall s a. SenAttr s a -> Bool
AS_Anno.isAxiom [SenStatus FORMULA (ProofStatus ProofTree)]
f
        searchResult :: String -> Maybe Bool
        searchResult :: String -> Maybe Bool
searchResult hf :: String
hf = let ls :: [String]
ls = String -> [String]
lines String
hf in
          if (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf String
reUNSAT) [String]
ls then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False else
          if (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf String
reSAT) [String]
ls then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
          else Maybe Bool
forall a. Maybe a
Nothing

-- ** GUI

{- |
  Invokes the generic prover GUI.
-}
zchaffProveGUI :: String -- ^ theory name
          -> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree
          -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]
          -- ^ free definitions
          -> IO [LP.ProofStatus ProofTree] -- ^ proof status for each goal
zchaffProveGUI :: String
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO [ProofStatus ProofTree]
zchaffProveGUI thName :: String
thName th :: Theory Sign FORMULA ProofTree
th freedefs :: [FreeDefMorphism FORMULA Morphism]
freedefs =
    ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
-> 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 PropProverState
atpFun String
thName) Bool
True (Prover Sign FORMULA Morphism PropSL ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
LP.proverName Prover Sign FORMULA Morphism PropSL ProofTree
zchaffProver) String
thName Theory Sign FORMULA ProofTree
th
                  [FreeDefMorphism FORMULA Morphism]
freedefs ProofTree
emptyProofTree
{- |
  Parses a given default tactic script into a
  'Interfaces.GenericATPState.ATPTacticScript' if possible.
-}
parseZchaffTacticScript :: LP.TacticScript -> ATPTacticScript
parseZchaffTacticScript :: TacticScript -> ATPTacticScript
parseZchaffTacticScript = Int -> [String] -> TacticScript -> ATPTacticScript
parseTacticScript Int
batchTimeLimit []

-- ** command line function

{- |
  Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
  automatic command line interface to the zchaff prover.
  zchaff specific functions are omitted by data type ATPFunctions.
-}
zchaffProveCMDLautomaticBatch ::
           Bool -- ^ True means include proved theorems
        -> Bool -- ^ True means save problem file
        -> Concurrent.MVar (Result.Result [LP.ProofStatus ProofTree])
           -- ^ used to store the result of the batch run
        -> String -- ^ theory name
        -> LP.TacticScript -- ^ default tactic script
        -> LP.Theory Sig.Sign AS_BASIC.FORMULA ProofTree
        -- ^ theory consisting of a signature and a list of Named sentences
        -> [LP.FreeDefMorphism AS_BASIC.FORMULA PMorphism.Morphism]
        -- ^ free definitions
        -> IO (Concurrent.ThreadId, Concurrent.MVar ())
           {- ^ fst: identifier of the batch thread for killing it
           snd: MVar to wait for the end of the thread -}
zchaffProveCMDLautomaticBatch :: Bool
-> Bool
-> MVar (Result [ProofStatus ProofTree])
-> String
-> TacticScript
-> Theory Sign FORMULA ProofTree
-> [FreeDefMorphism FORMULA Morphism]
-> IO (ThreadId, MVar ())
zchaffProveCMDLautomaticBatch 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 PropProverState
-> 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 PropProverState
atpFun String
thName) Bool
inclProvedThs Bool
saveProblem_batch
        MVar (Result [ProofStatus ProofTree])
resultMVar (Prover Sign FORMULA Morphism PropSL ProofTree -> String
forall theory sentence morphism sublogics proof_tree.
ProverTemplate theory sentence morphism sublogics proof_tree
-> String
LP.proverName Prover Sign FORMULA Morphism PropSL ProofTree
zchaffProver) String
thName
        (TacticScript -> ATPTacticScript
parseZchaffTacticScript TacticScript
defTS) Theory Sign FORMULA ProofTree
th [FreeDefMorphism FORMULA Morphism]
freedefs ProofTree
emptyProofTree

{- |
  Record for prover specific functions. This is used by both GUI and command
  line interface.
-}
atpFun :: String            -- Theory name
  -> ATPFunctions Sig.Sign AS_BASIC.FORMULA PMorphism.Morphism ProofTree
     PState.PropProverState
atpFun :: String
-> ATPFunctions Sign FORMULA Morphism ProofTree PropProverState
atpFun thName :: String
thName = ATPFunctions :: forall sign sentence morphism proof_tree pst.
InitialProverState sign sentence morphism pst
-> (String -> String)
-> (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 PropProverState
initialProverState = InitialProverState Sign FORMULA Morphism PropProverState
PState.propProverState
                , goalOutput :: PropProverState -> Named FORMULA -> [String] -> IO String
goalOutput = String -> PropProverState -> Named FORMULA -> [String] -> IO String
Cons.goalDIMACSProblem String
thName
                , atpTransSenName :: String -> String
atpTransSenName = String -> String
PState.transSenName
                , atpInsertSentence :: PropProverState -> Named FORMULA -> PropProverState
atpInsertSentence = PropProverState -> Named FORMULA -> PropProverState
PState.insertSentence
                , proverHelpText :: String
proverHelpText = String
zchaffHelpText
                , runProver :: RunProver FORMULA ProofTree PropProverState
runProver = RunProver FORMULA ProofTree PropProverState
runZchaff
                , batchTimeEnv :: String
batchTimeEnv = "HETS_ZCHAFF_BATCH_TIME_LIMIT"
                , fileExtensions :: FileExtensions
fileExtensions = FileExtensions :: String -> String -> String -> FileExtensions
FileExtensions
                    { problemOutput :: String
problemOutput = ".dimacs"
                    , proverOutput :: String
proverOutput = ".zchaff"
                    , theoryConfiguration :: String
theoryConfiguration = ".czchaff"}
                , createProverOptions :: GenericConfig ProofTree -> [String]
createProverOptions = GenericConfig ProofTree -> [String]
createZchaffOptions }

{- |
  Runs zchaff. zchaff is assumed to reside in PATH.
-}

runZchaff :: PState.PropProverState
           {- 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 DIMACS file
           -> String
           -- Name of the theory
           -> AS_Anno.Named AS_BASIC.FORMULA
           -- Goal to prove
           -> IO (ATPRetval
                 , GenericConfig ProofTree
                 )
           -- (retval, configuration with proof status and complete output)
runZchaff :: RunProver FORMULA ProofTree PropProverState
runZchaff pState :: PropProverState
pState cfg :: GenericConfig ProofTree
cfg saveDIMACS :: Bool
saveDIMACS thName :: String
thName nGoal :: Named FORMULA
nGoal = do
      String
prob <- String -> PropProverState -> Named FORMULA -> [String] -> IO String
Cons.goalDIMACSProblem String
thName PropProverState
pState Named FORMULA
nGoal []
      let thName_clean :: String
thName_clean =
              String -> String
basename String
thName String -> String -> String
forall a. [a] -> [a] -> [a]
++ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".dimacs"
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveDIMACS (String -> String -> IO ()
writeFile String
thName_clean String
prob)
      String
zFileName <- String -> String -> IO String
getTempFile String
prob String
thName_clean
      (_, zchaffOut :: String
zchaffOut, _) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
zchaffS
        (String
zFileName String -> [String] -> [String]
forall a. a -> [a] -> [a]
: GenericConfig ProofTree -> [String]
createZchaffOptions GenericConfig ProofTree
cfg) ""
      (res :: Either ATPRetval GoalStatus
res, usedAxs :: [String]
usedAxs, tUsed :: TimeOfDay
tUsed) <- String
-> PropProverState
-> IO (Either ATPRetval GoalStatus, [String], TimeOfDay)
analyzeZchaff String
zchaffOut PropProverState
pState
      let defaultProofStatus :: ProofStatus ProofTree
defaultProofStatus =
                      (String -> String -> ProofTree -> ProofStatus ProofTree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
LP.openProofStatus (Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal) String
zchaffS
                                        ProofTree
emptyProofTree)
                      {tacticScript :: TacticScript
LP.tacticScript = String -> TacticScript
LP.TacticScript (String -> TacticScript) -> String -> TacticScript
forall a b. (a -> b) -> a -> b
$ ATPTacticScript -> String
forall a. Show a => a -> String
show
                            ATPTacticScript :: Int -> [String] -> ATPTacticScript
ATPTacticScript
                             { tsTimeLimit :: Int
tsTimeLimit = GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg
                             , tsExtraOpts :: [String]
tsExtraOpts = []} }
          (err :: ATPRetval
err, retval :: ProofStatus ProofTree
retval) = case Either ATPRetval GoalStatus
res of
                      Right p :: GoalStatus
p -> (ATPRetval
ATPSuccess,
                        ProofStatus ProofTree
defaultProofStatus
                                {goalStatus :: GoalStatus
LP.goalStatus = GoalStatus
p
                                , usedAxioms :: [String]
LP.usedAxioms = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter
                                    (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
nGoal) [String]
usedAxs
                                , proofTree :: ProofTree
LP.proofTree = String -> ProofTree
ProofTree String
zchaffOut })
                      Left a :: ATPRetval
a -> (ATPRetval
a, ProofStatus ProofTree
defaultProofStatus)
      () -> IO () -> IO ()
forall a. a -> IO a -> IO a
catchIOException () (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
removeFile String
zFileName
      (ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
err, GenericConfig ProofTree
cfg
              { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree
retval
              , resultOutput :: [String]
resultOutput = [String
zchaffOut]
              , timeUsed :: TimeOfDay
timeUsed = TimeOfDay
tUsed })

-- | analysis of output
analyzeZchaff :: String -> PState.PropProverState
  -> IO (Either ATPRetval LP.GoalStatus, [String], TimeOfDay)
analyzeZchaff :: String
-> PropProverState
-> IO (Either ATPRetval GoalStatus, [String], TimeOfDay)
analyzeZchaff str' :: String
str' pState :: PropProverState
pState =
    let unsat :: Bool
unsat = String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf String
reUNSAT String
str'
        sat :: Bool
sat = String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf String
reSAT String
str'
        timeLine :: String
timeLine = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "0" (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix String
reTIME String
str'
        timeout :: Bool
timeout = String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf String
reEndto String
str' Bool -> Bool -> Bool
|| String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf String
reEndmo String
str'
        time :: TimeOfDay
time = String -> TimeOfDay
calculateTime String
timeLine
        usedAx :: [String]
usedAx = (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 ([Named FORMULA] -> [String]) -> [Named FORMULA] -> [String]
forall a b. (a -> b) -> a -> b
$ PropProverState -> [Named FORMULA]
PState.initialAxioms PropProverState
pState
    in (Either ATPRetval GoalStatus, [String], TimeOfDay)
-> IO (Either ATPRetval GoalStatus, [String], TimeOfDay)
forall (m :: * -> *) a. Monad m => a -> m a
return (case () of
         _ | Bool
timeout -> ATPRetval -> Either ATPRetval GoalStatus
forall a b. a -> Either a b
Left ATPRetval
ATPTLimitExceeded
         _ | Bool
sat Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
unsat -> GoalStatus -> Either ATPRetval GoalStatus
forall a b. b -> Either a b
Right GoalStatus
LP.Disproved
         _ | Bool -> Bool
not Bool
sat Bool -> Bool -> Bool
&& Bool
unsat -> GoalStatus -> Either ATPRetval GoalStatus
forall a b. b -> Either a b
Right (GoalStatus -> Either ATPRetval GoalStatus)
-> GoalStatus -> Either ATPRetval GoalStatus
forall a b. (a -> b) -> a -> b
$ Bool -> GoalStatus
LP.Proved Bool
True
         _ -> ATPRetval -> Either ATPRetval GoalStatus
forall a b. a -> Either a b
Left (ATPRetval -> Either ATPRetval GoalStatus)
-> ATPRetval -> Either ATPRetval GoalStatus
forall a b. (a -> b) -> a -> b
$ String -> ATPRetval
ATPError "Internal error.", [String]
usedAx, TimeOfDay
time)

-- | Calculated the time need for the proof in seconds
calculateTime :: String -> TimeOfDay
calculateTime :: String -> TimeOfDay
calculateTime timeLine :: String
timeLine =
    DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Double -> DiffTime
forall a b. (Real a, Fractional b) => a -> b
realToFrac (Double -> Maybe Double -> Double
forall a. a -> Maybe a -> a
fromMaybe
         (String -> Double
forall a. HasCallStack => String -> a
error (String -> Double) -> String -> Double
forall a b. (a -> b) -> a -> b
$ "calculateTime " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
timeLine) (Maybe Double -> Double) -> Maybe Double -> Double
forall a b. (a -> b) -> a -> b
$ String -> Maybe Double
forall a. Read a => String -> Maybe a
readMaybe String
timeLine
             :: Double)

reUNSAT :: String
reUNSAT :: String
reUNSAT = "RESULT:\tUNSAT"
reSAT :: String
reSAT :: String
reSAT = "RESULT:\tSAT"
reTIME :: String
reTIME :: String
reTIME = "Total Run Time"

reEndto :: String
reEndto :: String
reEndto = "TIME OUT"
reEndmo :: String
reEndmo :: String
reEndmo = "MEM OUT"

{- |
  Creates a list of all options the zChaff prover runs with.
  Only Option is the timelimit
-}
createZchaffOptions :: GenericConfig ProofTree -> [String]
createZchaffOptions :: GenericConfig ProofTree -> [String]
createZchaffOptions cfg :: GenericConfig ProofTree
cfg =
    [Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> Int
forall proof_tree. GenericConfig proof_tree -> Int
configTimeLimit GenericConfig ProofTree
cfg]