7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaDescription : Interface for the E Theorem Prover.
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaCopyright : (c) Eugen Kuksa University of Magdeburg 2017
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaLicense : GPLv2 or higher, see LICENSE.txt
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaMaintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de>
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaStability : provisional
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaPortability : non-portable (imports Logic)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksamodule TPTP.Prover.EProver (eprover) where
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport Interfaces.GenericATPState hiding (proverState)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport Logic.Prover hiding (proofLines)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaeprover :: Prover Sign Sentence Morphism Sublogic ProofTree
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaeprover = mkProver binary_name prover_name sublogics runTheProver
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksabinary_name :: String
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksabinary_name = "eprover"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaprover_name :: String
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaprover_name = "EProver"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksasublogics :: Sublogic
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksasublogics = FOF
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksarunTheProver :: ProverState
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa {- ^ logical part containing the input Sign and axioms and possibly
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa goals that have been proved earlier as additional axioms -}
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa -> GenericConfig ProofTree -- ^ configuration to use
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa -> Bool -- ^ True means save TPTP file
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa -> String -- ^ name of the theory in the DevGraph
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa -> Named Sentence -- ^ goal to prove
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa -> IO (ATPRetval, GenericConfig ProofTree)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa -- ^ (retval, configuration with proof status and complete output)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksarunTheProver proverState cfg saveTPTPFile theoryName namedGoal = do
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa let proverTimeLimitS = show $ getTimeLimit cfg
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa allOptions = [ "--tstp-format"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , "--proof-object"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , "--output-level=0"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , "--cpu-limit=" ++ proverTimeLimitS
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , "--memory-limit=4096"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa problemFileName <-
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa prepareProverInput proverState cfg saveTPTPFile theoryName namedGoal prover_name
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (_, out, wallTimeUsed) <-
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa executeTheProver binary_name (allOptions ++ [problemFileName])
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa let szsStatusLine = findSZS out
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa let reportedTimeUsed = parseTimeUsed out
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa let resultedTimeUsed =
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa if reportedTimeUsed == -1
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa then wallTimeUsed
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa else timeToTimeOfDay $ secondsToDiffTime $
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa toInteger reportedTimeUsed
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa let proofLines = filterProofLines out
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa axiomsUsed <- if szsProved szsStatusLine || szsDisproved szsStatusLine
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa then case axiomsFromProofObject proofLines of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (axiomNames, []) -> return axiomNames
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (_, errs) -> do
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa putStrLn $ unlines errs
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa return $ getAxioms proverState
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa else return $ getAxioms proverState
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa let (atpRetval, resultedProofStatus) =
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa atpRetValAndProofStatus cfg namedGoal resultedTimeUsed axiomsUsed
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa szsStatusLine prover_name
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa return (atpRetval, cfg { proofStatus = resultedProofStatus
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , resultOutput = out
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , timeUsed = resultedTimeUsed })