content: {- |
  Module      :  ./TPTP/Prover/Geo3.hs
  Description :  Interface for the Leo-III Prover.
  Copyright   :  (c) Eugen Kuksa University of Magdeburg 2017
  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.Geo3 (geo3) 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
  
  geo3 :: Prover Sign Sentence Morphism Sublogic ProofTree
  geo3 = mkProver binary_name prover_name sublogics runTheProver
  
  binary_name :: String
  binary_name = "geo3"
  
  prover_name :: String
  prover_name = "Geo-III"
  
  sublogics :: Sublogic
  sublogics = 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 proverState cfg saveTPTPFile theoryName namedGoal = do
    let proverTimeLimitS = show $ getTimeLimit cfg
    let allOptions = ["-tptp_input", "-tptp_output"]
  
    problemFileName <-
      prepareProverInput proverState cfg saveTPTPFile theoryName namedGoal prover_name
  
    -- Geo-III does not support timeouts, so we need to quit it by force:
    timeoutBin <- gnuTimeout
    (exitCode, out, wallTimeUsed) <-
      executeTheProver timeoutBin (proverTimeLimitS
                                   : binary_name
                                   : allOptions
                                   ++ ["-inputfile", problemFileName ])
  
    let timedOut = exitCode == ExitFailure 124
    let szsStatusLine = if timedOut then "Timeout" else findSZS out
    let resultedTimeUsed = wallTimeUsed
    let proofLines = filterProofLines out
    axiomsUsed <- if szsProved szsStatusLine || szsDisproved szsStatusLine
                  then case axiomsFromProofObject proofLines of
                         -- TODO: As long as geo3 does not support tptp output,
                         -- the parsed list of used axioms is always empty. Return
                         -- all axioms in this case.
                         ([], []) -> return $ getAxioms proverState
                         (axiomNames, []) -> return axiomNames
                         (_, errs) -> do
                           putStrLn $ unlines errs
                           return $ getAxioms proverState
                  else return $ getAxioms proverState
    let (atpRetval, resultedProofStatus) =
          atpRetValAndProofStatus cfg namedGoal resultedTimeUsed axiomsUsed
            szsStatusLine prover_name
    return (atpRetval, cfg { proofStatus = resultedProofStatus
                           , resultOutput = out
                           , timeUsed = resultedTimeUsed })
  