content: {- |
  Module      :  ./TPTP/Prover/Vampire.hs
  Description :  Interface for the Vampire theorem 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.Vampire (vampire) where
  
  import TPTP.Prover.Common
  import TPTP.Prover.Vampire.ProofParser
  import TPTP.Prover.ProofParser hiding (filterProofLines)
  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)
  
  vampire :: Prover Sign Sentence Morphism Sublogic ProofTree
  vampire = mkProver binary_name prover_name sublogics runTheProver
  
  binary_name :: String
  binary_name = "vampire"
  
  -- renamed so it does not clash with Vampire for SoftFOL
  prover_name :: String
  prover_name = "Vampire-TPTP"
  
  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
        allOptions = [ "--input_syntax", "tptp"
                     , "--proof", "tptp"
                     , "--output_axiom_names", "on"
                     , "--time_limit", proverTimeLimitS
                     , "--memory_limit", "4096"
                     , "--mode", "vampire"
                     ]
  
    problemFileName <-
      prepareProverInput proverState cfg saveTPTPFile theoryName namedGoal prover_name
  
    (_, out, _) <-
      executeTheProver binary_name (allOptions ++ [problemFileName])
    let szsStatusLine = parseStatus out
    let resultedTimeUsed = parseTimeUsed out
    let proofLines = filterProofLines out
    axiomsUsed <- if szsProved szsStatusLine || szsDisproved szsStatusLine
                  then case axiomsFromProofObject proofLines of
                         (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 })
  