{- |

Module : ./SoftFOL/ProveMetis.hs

Copyright : (c) Christian Maeder, DFKI GmbH 2010

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : non-portable (ATP GUI)

call metis prover

-}

module SoftFOL.ProveMetis

( metisProver

, metisProveCMDLautomaticBatch

) where

import Common.AS_Annotation as AS_Anno

import Common.ProofTree

import Common.Timing

import Common.Utils

import Common.SZSOntology

import qualified Common.Result as Result

import qualified Control.Concurrent as Concurrent

import Control.Monad

import Data.List

import Data.Maybe

import GUI.GenericATP

import Interfaces.GenericATPState

import Logic.Prover

import Proofs.BatchProcessing

import SoftFOL.ProverState

import SoftFOL.Sign

import SoftFOL.Translate

import System.Directory

import System.Exit

-- | The Prover implementation.

metisProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree

metisProver = mkAutomaticProver "metis" "metis" () metisGUI

metisProveCMDLautomaticBatch

{- |

Record for prover specific functions. This is used by both GUI and command

line interface.

-}

atpFun :: String -- ^ theory name

-> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState

atpFun thName = ATPFunctions

{ initialProverState = spassProverState

, atpTransSenName = transSenName

, atpInsertSentence = insertSentenceGen

, goalOutput = showTPTPProblem thName

, proverHelpText = ""

, batchTimeEnv = ""

, fileExtensions = FileExtensions

{ problemOutput = ".tptp"

, proverOutput = ".spass"

, theoryConfiguration = "" }

, runProver = runMetis

, createProverOptions = extraOpts }

{- |

Invokes the generic prover GUI.

-}

metisGUI :: String -- ^ theory name

-> Theory Sign Sentence ProofTree

{- ^ theory consisting of a SoftFOL.Sign.Sign

and a list of Named SoftFOL.Sign.Sentence -}

-> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints

-> IO [ProofStatus ProofTree] -- ^ proof status for each goal

metisGUI thName th freedefs =

genericATPgui (atpFun thName) True (proverName metisProver) thName th

freedefs emptyProofTree

-- ** command line function

{- |

Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an

automatic command line interface to the Metis prover.

-}

metisProveCMDLautomaticBatch ::

Bool -- ^ True means include proved theorems

-> Bool -- ^ True means save problem file

-> Concurrent.MVar (Result.Result [ProofStatus ProofTree])

-- ^ used to store the result of the batch run

-> String -- ^ theory name

-> TacticScript -- ^ default tactic script

-> Theory Sign Sentence ProofTree {- ^ theory consisting of a

'SoftFOL.Sign.Sign' and a list of Named 'SoftFOL.Sign.Sentence' -}

-> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints

-> IO (Concurrent.ThreadId, Concurrent.MVar ())

{- ^ fst: identifier of the batch thread for killing it

snd: MVar to wait for the end of the thread -}

metisProveCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar

thName defTS th freedefs =

genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch

resultMVar (proverName metisProver) thName

(parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

runMetis :: SoftFOLProverState

{- ^ 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

-> AS_Anno.Named SPTerm -- ^ goal to prove

-> IO (ATPRetval, GenericConfig ProofTree)

-- ^ (retval, configuration with proof status and complete output)

runMetis sps cfg saveTPTP thName nGoal = do

let saveFile = basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".tptp"

prob <- showTPTPProblem thName sps nGoal []

when saveTPTP (writeFile saveFile prob)

timeTmpFile <- getTempFile prob saveFile

start <- getHetsTime

-- try timeout using perl

(ex, out, err) <- executeProcess "perl"

["-e", "alarm shift @ARGV; exec @ARGV"

, show (configTimeLimit cfg), "metis", timeTmpFile] ""

finish <- getHetsTime

let executetime = diffHetsTime finish start

newCfg = cfg

{ timeUsed = executetime

, proofStatus = (proofStatus cfg) {usedTime = executetime}}

finCfg = newCfg { resultOutput = lines $ out ++ err }

removeFile timeTmpFile

return $ case ex of

ExitSuccess ->

( ATPSuccess

, finCfg

{ proofStatus = (proofStatus finCfg)

{ usedAxioms = getAxioms sps

, goalStatus = getGoalStatus out }})

ExitFailure e -> if e == 14 then

( ATPTLimitExceeded

, newCfg

{ timeLimitExceeded = True

, resultOutput = ["TimeOut"] })

else (ATPError err, finCfg)

-- | mapping from SZS Status to Goalstatus

getGoalStatus :: String -> GoalStatus

getGoalStatus l = let ll = lines l in

case mapMaybe (stripPrefix "SZS status") ll of

[] -> Open (Reason ll)

z@(s : _) -> case words s of

w : _

| szsProved w -> Proved True

| szsDisproved w -> Disproved

_ -> Open (Reason z)