Darwin.hs revision 7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7f
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncDescription : Interface for the E Theorem Prover.
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncCopyright : (c) Eugen Kuksa University of Magdeburg 2017
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncLicense : GPLv2 or higher, see LICENSE.txt
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncMaintainer : Eugen Kuksa <kuksa@iks.cs.ovgu.de>
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncStability : provisional
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncPortability : non-portable (imports Logic)
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncmodule TPTP.Prover.Darwin (darwin) where
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync-- The relevant output of Darwin is the same as the output of EProver.
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncimport TPTP.Prover.EProver.ProofParser (parseTimeUsed)
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncimport Interfaces.GenericATPState hiding (proverState)
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncimport Logic.Prover hiding (proofLines)
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncdarwin :: Prover Sign Sentence Morphism Sublogic ProofTree
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncdarwin = mkProver binary_name prover_name sublogics runTheProver
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncbinary_name :: String
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncbinary_name = "darwin"
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncprover_name :: String
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncprover_name = "Darwin"
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncsublogics :: Sublogic
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncsublogics = FOF
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncrunTheProver :: ProverState
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync {- ^ logical part containing the input Sign and axioms and possibly
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync goals that have been proved earlier as additional axioms -}
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync -> GenericConfig ProofTree -- ^ configuration to use
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync -> Bool -- ^ True means save TPTP file
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync -> String -- ^ name of the theory in the DevGraph
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync -> Named Sentence -- ^ goal to prove
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync -> IO (ATPRetval, GenericConfig ProofTree)
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync -- ^ (retval, configuration with proof status and complete output)
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsyncrunTheProver proverState cfg saveTPTPFile theoryName namedGoal = do
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync let proverTimeLimitS = show $ getTimeLimit cfg
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync allOptions = [ "--print-configuration", "false"
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync , "--print-statistics", "true"
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync , "--input-format", "tptp"
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync , "--timeout-cpu", proverTimeLimitS
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync , "--memory-limit", show (4096 :: Int)
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync problemFileName <-
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync prepareProverInput proverState cfg saveTPTPFile theoryName namedGoal prover_name
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync (_, out, wallTimeUsed) <-
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync executeTheProver binary_name (allOptions ++ [problemFileName])
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync let szsStatusLine = findSZS out
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync let reportedTimeUsed = parseTimeUsed out
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync let resultedTimeUsed =
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync if reportedTimeUsed == -1
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync then wallTimeUsed
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync else timeToTimeOfDay $ secondsToDiffTime $ toInteger reportedTimeUsed
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync let axiomsUsed = getAxioms proverState
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync let (atpRetval, resultedProofStatus) =
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync atpRetValAndProofStatus cfg namedGoal resultedTimeUsed axiomsUsed
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync szsStatusLine prover_name
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync return (atpRetval, cfg { proofStatus = resultedProofStatus
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync , resultOutput = out
74fe172698ba936102e120dae998c9ebd09cfbdfvboxsync , timeUsed = resultedTimeUsed })