{- |
Module      :  ./TPTP/Prover/EProver.hs
Description :  Interface for the E Theorem Prover.
Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017, Tom Kranz 2021-2022
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Eugen Kuksa <kuksa@iks.cs.ovgu.de>
Stability   :  provisional
Portability :  non-portable (imports Logic)
-}

module TPTP.Prover.EProver (eprover) where

import TPTP.Prover.Common
import TPTP.Prover.EProver.ProofParser
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 Data.Time.LocalTime
import Data.Time.Clock

eprover :: Prover Sign Sentence Morphism Sublogic ProofTree
eprover :: Prover Sign Sentence Morphism Sublogic ProofTree
eprover = 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 = "eprover"

prover_name :: String
prover_name :: String
prover_name = "EProver"

sublogics :: Sublogic
sublogics :: Sublogic
sublogics = Sublogic
FOF

runTheProver :: ProverState
                {- ^ 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 TPTP file
             -> String -- ^ name of the theory in the DevGraph
             -> Named Sentence -- ^ goal to prove
             -> IO (ATPRetval, GenericConfig ProofTree)
                -- ^ (retval, configuration with proof status and complete output)
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
      allOptions :: [String]
allOptions = [ "--tstp-format"
                   , "--proof-object"
                   , "--output-level=0"
                   , "--auto"
                   , "--cpu-limit=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
proverTimeLimitS
                   , "--memory-limit=4096"
                   ]

  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

  (_, out :: [String]
out, wallTimeUsed :: TimeOfDay
wallTimeUsed) <-
    String -> [String] -> IO (ExitCode, [String], TimeOfDay)
executeTheProver String
binary_name ([String]
allOptions [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
problemFileName])

  let szsStatusLine :: String
szsStatusLine = [String] -> String
findSZS [String]
out
  let reportedTimeUsed :: Int
reportedTimeUsed = [String] -> Int
parseTimeUsed [String]
out
  let resultedTimeUsed :: TimeOfDay
resultedTimeUsed =
        if Int
reportedTimeUsed Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== -1
        then TimeOfDay
wallTimeUsed
        else DiffTime -> TimeOfDay
timeToTimeOfDay (DiffTime -> TimeOfDay) -> DiffTime -> TimeOfDay
forall a b. (a -> b) -> a -> b
$ Integer -> DiffTime
secondsToDiffTime (Integer -> DiffTime) -> Integer -> DiffTime
forall a b. (a -> b) -> a -> b
$
               Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
reportedTimeUsed
  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 proofGraph :: ProofTree
proofGraph = if String -> Bool
szsProved String
szsStatusLine Bool -> Bool -> Bool
|| String -> Bool
szsDisproved String
szsStatusLine
                then [String] -> ProofTree
graphFromProofObject [String]
proofLines
                else ProofStatus ProofTree -> ProofTree
forall proof_tree. ProofStatus proof_tree -> proof_tree
proofTree (GenericConfig ProofTree -> ProofStatus ProofTree
forall proof_tree.
GenericConfig proof_tree -> ProofStatus proof_tree
proofStatus GenericConfig ProofTree
cfg)
  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 { proofTree :: ProofTree
proofTree = ProofTree
proofGraph }
                         , resultOutput :: [String]
resultOutput = [String]
out
                         , timeUsed :: TimeOfDay
timeUsed = TimeOfDay
resultedTimeUsed })