module TPTP.Prover.Leo2 (leo2) where
import TPTP.Prover.Common
import TPTP.Prover.ProofParser
import TPTP.Prover.ProverState
import TPTP.Morphism
import TPTP.Sign
import TPTP.Sublogic
import Common.AS_Annotation
import Common.ProofTree
import Common.SZSOntology
import Interfaces.GenericATPState hiding (proverState)
import Logic.Prover hiding (proofLines)
import System.Exit
leo2 :: Prover Sign Sentence Morphism Sublogic ProofTree
leo2 :: Prover Sign Sentence Morphism Sublogic ProofTree
leo2 = String
-> String
-> Sublogic
-> RunTheProverType
-> Prover Sign Sentence Morphism Sublogic ProofTree
mkProver String
binary_name String
prover_name Sublogic
sublogics RunTheProverType
runTheProver
binary_name :: String
binary_name :: String
binary_name = "leo"
prover_name :: String
prover_name :: String
prover_name = "Leo-II"
sublogics :: Sublogic
sublogics :: Sublogic
sublogics = Sublogic
THF
runTheProver :: ProverState
-> GenericConfig ProofTree
-> Bool
-> String
-> Named Sentence
-> IO (ATPRetval, GenericConfig ProofTree)
runTheProver :: RunTheProverType
runTheProver proverState :: ProverState
proverState cfg :: GenericConfig ProofTree
cfg saveTPTPFile :: Bool
saveTPTPFile theoryName :: String
theoryName namedGoal :: Named Sentence
namedGoal = do
let proverTimeLimitS :: String
proverTimeLimitS = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> Int
getTimeLimit GenericConfig ProofTree
cfg
hardTimeLimitS :: String
hardTimeLimitS = Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ GenericConfig ProofTree -> Int
hardTimeLimit GenericConfig ProofTree
cfg
allOptions :: [String]
allOptions = [ "--proofoutput", "3"
, "--timeout", String
proverTimeLimitS
]
String
problemFileName <-
ProverState
-> GenericConfig ProofTree
-> Bool
-> String
-> Named Sentence
-> String
-> IO String
prepareProverInput ProverState
proverState GenericConfig ProofTree
cfg Bool
saveTPTPFile String
theoryName Named Sentence
namedGoal String
prover_name
String
timeoutBin <- IO String
gnuTimeout
(exitCode :: ExitCode
exitCode, out :: [String]
out, wallTimeUsed :: TimeOfDay
wallTimeUsed) <-
String -> [String] -> IO (ExitCode, [String], TimeOfDay)
executeTheProver String
timeoutBin (String
hardTimeLimitS String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
binary_name String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
[String]
allOptions [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
problemFileName])
let timedOut :: Bool
timedOut = ExitCode
exitCode ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> ExitCode
ExitFailure 124
let szsStatusLine :: String
szsStatusLine = if Bool
timedOut then "Timeout" else [String] -> String
findSZS [String]
out
let resultedTimeUsed :: TimeOfDay
resultedTimeUsed = TimeOfDay
wallTimeUsed
let proofLines :: [String]
proofLines = [String] -> [String]
filterProofLines [String]
out
[String]
axiomsUsed <- if String -> Bool
szsProved String
szsStatusLine Bool -> Bool -> Bool
|| String -> Bool
szsDisproved String
szsStatusLine
then case [String] -> ([String], [String])
axiomsFromProofObject [String]
proofLines of
(axiomNames :: [String]
axiomNames, []) -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return [String]
axiomNames
(_, errs :: [String]
errs) -> do
String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
errs
[String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ ProverState -> [String]
getAxioms ProverState
proverState
else [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ ProverState -> [String]
getAxioms ProverState
proverState
let (atpRetval :: ATPRetval
atpRetval, resultedProofStatus :: ProofStatus ProofTree
resultedProofStatus) =
GenericConfig ProofTree
-> Named Sentence
-> TimeOfDay
-> [String]
-> String
-> String
-> (ATPRetval, ProofStatus ProofTree)
atpRetValAndProofStatus GenericConfig ProofTree
cfg Named Sentence
namedGoal TimeOfDay
resultedTimeUsed [String]
axiomsUsed
String
szsStatusLine String
prover_name
(ATPRetval, GenericConfig ProofTree)
-> IO (ATPRetval, GenericConfig ProofTree)
forall (m :: * -> *) a. Monad m => a -> m a
return (ATPRetval
atpRetval, GenericConfig ProofTree
cfg { proofStatus :: ProofStatus ProofTree
proofStatus = ProofStatus ProofTree
resultedProofStatus
, resultOutput :: [String]
resultOutput = [String]
out
, timeUsed :: TimeOfDay
timeUsed = TimeOfDay
resultedTimeUsed })