{- |
Module      :  ./TPTP/Prover/SPASS.hs
Description :  Interface for the SPASS 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.SPASS (spass) where

import TPTP.Prover.Common
import TPTP.Prover.SPASS.ProofParser
import TPTP.Prover.ProverState
import TPTP.Morphism
import TPTP.Sign
import TPTP.Sublogic

import Common.AS_Annotation
import Common.ProofTree
import Interfaces.GenericATPState hiding (proverState)
import Logic.Prover hiding (proofLines)

import Data.List
import Data.Graph.Inductive.Graph (mkGraph)

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

prover_name :: String
prover_name :: String
prover_name = "SPASS"

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 = [ "-TPTP"
                   , "-DocProof"
                   , "-TimeLimit=" String -> String -> String
forall a. [a] -> [a] -> [a]
++ 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

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

  let (mResult :: Maybe String
mResult, axiomsUsed :: [String]
axiomsUsed, outputExists :: Bool
outputExists, resultedTimeUsed :: TimeOfDay
resultedTimeUsed, _, clNodes :: [(Int, ProofGraphNode)]
clNodes, clEdges :: [(Int, Int, Int)]
clEdges) =
        Named Sentence
-> [String]
-> (Maybe String, [String], Bool, TimeOfDay, Bool,
    [(Int, ProofGraphNode)], [(Int, Int, Int)])
parseOutput Named Sentence
namedGoal [String]
out
  let (defaultProofStatus :: ProofStatus ProofTree
defaultProofStatus, provedStatus :: ProofStatus ProofTree
provedStatus, disprovedStatus :: ProofStatus ProofTree
disprovedStatus) =
        GenericConfig ProofTree
-> Named Sentence
-> TimeOfDay
-> [String]
-> String
-> (ProofStatus ProofTree, ProofStatus ProofTree,
    ProofStatus ProofTree)
proofStatuses GenericConfig ProofTree
cfg Named Sentence
namedGoal TimeOfDay
resultedTimeUsed [String]
axiomsUsed String
prover_name
  let (atpRetval :: ATPRetval
atpRetval, resultedProofStatus :: ProofStatus ProofTree
resultedProofStatus) = case Maybe String
mResult of
        Nothing -> (String -> ATPRetval
ATPError (String -> ATPRetval) -> String -> ATPRetval
forall a b. (a -> b) -> a -> b
$ Bool -> String
errorMessage Bool
outputExists, ProofStatus ProofTree
defaultProofStatus)
        Just result :: String
result
          | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Proof found." String
result ->
             (ATPRetval
ATPSuccess, ProofStatus ProofTree
provedStatus { proofTree :: ProofTree
proofTree = Gr ProofGraphNode Int -> ProofTree
ProofGraph (Gr ProofGraphNode Int -> ProofTree)
-> Gr ProofGraphNode Int -> ProofTree
forall a b. (a -> b) -> a -> b
$ [(Int, ProofGraphNode)]
-> [(Int, Int, Int)] -> Gr ProofGraphNode Int
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [(Int, ProofGraphNode)]
clNodes [(Int, Int, Int)]
clEdges })
          | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Completion found." String
result -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
disprovedStatus)
          | String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf "Ran out of time." String
result ->
              (ATPRetval
ATPTLimitExceeded, ProofStatus ProofTree
defaultProofStatus)
        _ -> (ATPRetval
ATPSuccess, ProofStatus ProofTree
defaultProofStatus)
  (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 })
  where
    errorMessage :: Bool -> String
    errorMessage :: Bool -> String
errorMessage outputExists :: Bool
outputExists =
      "No " String -> String -> String
forall a. [a] -> [a] -> [a]
++
        (if Bool
outputExists then "result" else "output") String -> String -> String
forall a. [a] -> [a] -> [a]
++
        " of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
prover_name String -> String -> String
forall a. [a] -> [a] -> [a]
++ " found."