{- |

Module : ./THF/SZSProver.hs

Description : General Interface to a prover using SZS status messages

Copyright : (c) Jonathan von Schroeder, DFKI Bremen 2012

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>

Stability : provisional

Portability : non-portable (imports Prover)

Isabelle theorem prover for THF

-}

module THF.SZSProver

( createSZSProver

, ProverType

, ProverFuncs (..)

) where

import Logic.Prover

import THF.As (THFFormula)

import THF.Sign

import THF.ProverState

import THF.Sublogic

import Common.AS_Annotation as AS_Anno

import Common.Result

import Common.ProofTree

import Common.Utils (basename, timeoutCommand)

import Common.SZSOntology

import GUI.GenericATP

import Interfaces.GenericATPState

import Control.Monad (unless)

import qualified Control.Concurrent as Concurrent

import Proofs.BatchProcessing

import System.Directory

import Data.List

import Data.Maybe

import Data.Time (timeToTimeOfDay)

import Data.Time.Clock (secondsToDiffTime)

data ProverFuncs = ProverFuncs {

cfgTimeout :: GenericConfig ProofTree -> Int, -- in seconds

proverCommand :: Int -> String -> GenericConfig ProofTree ->

IO (String, [String]),

-- timeout -> problem file

getMessage :: String -> String -> String -> String,

-- result -> std out -> std err

getTimeUsed :: String -> Maybe Int -- in seconds

}

type ProverType = Prover SignTHF THFFormula MorphismTHF THFSl ProofTree

createSZSProver :: String -> String -> String -> ProverFuncs ->

ProverType

createSZSProver bin name hlp d = mkAutomaticProver bin name tHF0

(proverGUI hlp name d)

(proverCMDLautomaticBatch hlp name d)

atpFun :: ProverFuncs

-> String -- name

-> String -- ^ theory name

-> String -- help text

-> ATPFunctions SignTHF THFFormula MorphismTHF ProofTree ProverStateTHF

atpFun d name _ hlp = ATPFunctions

{ initialProverState = initialProverStateTHF

, atpTransSenName = id

, atpInsertSentence = insertSentenceTHF

, goalOutput = showProblemTHF

, proverHelpText = hlp

, batchTimeEnv = "HETS_TPTP_BATCH_TIME_LIMIT"

, fileExtensions = FileExtensions {

problemOutput = ".p"

, proverOutput = ""

, theoryConfiguration = "" }

, runProver = runProverT d name

, createProverOptions = extraOpts }

proverGUI :: String -- help text

-> String -- name

-> ProverFuncs

-> String -- ^ theory name

-> Theory SignTHF THFFormula ProofTree

-> [FreeDefMorphism THFFormula MorphismTHF] -- ^ freeness constraints

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

proverGUI hlp name d thName th freedefs =

genericATPgui (atpFun d name thName hlp) True name thName th

freedefs emptyProofTree

proverCMDLautomaticBatch

:: String -- help

-> String -- name

-> ProverFuncs

-> Bool -- ^ True means include proved theorems

-> Bool -- ^ True means save problem file

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

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

-> String -- ^ theory name

-> TacticScript -- ^ default tactic script

-> Theory SignTHF THFFormula ProofTree

-- ^ theory consisting of a signature and sentences

-> [FreeDefMorphism THFFormula MorphismTHF] -- ^ 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 -}

proverCMDLautomaticBatch hlp name d inclProvedThs saveProblem_batch resultMVar

thName defTS th freedefs =

genericCMDLautomaticBatch (atpFun d name thName hlp) inclProvedThs

saveProblem_batch

resultMVar name thName

(parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

runProverT :: ProverFuncs

-> String -- name

-> ProverStateTHF

-> GenericConfig ProofTree -- ^ configuration to use

-> Bool -- ^ True means save THF file

-> String -- ^ name of the theory in the DevGraph

-> Named THFFormula -- ^ goal to prove

-> IO (ATPRetval, GenericConfig ProofTree)

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

runProverT d name pst cfg saveTHF thName nGoal = do

let tout = cfgTimeout d cfg

tmpFileName = thName ++ '_' : AS_Anno.senAttr nGoal

prob <- showProblemTHF pst nGoal []

runRes <- runProverProcess d cfg tout saveTHF tmpFileName prob

case runRes of

Nothing -> return (ATPTLimitExceeded, cfg

{ proofStatus =

(openProofStatus (AS_Anno.senAttr nGoal)

name emptyProofTree)

{ usedTime =

timeToTimeOfDay $ secondsToDiffTime $

toInteger tout

, tacticScript = TacticScript

$ show ATPTacticScript

{ tsTimeLimit = configTimeLimit cfg,

tsExtraOpts = [] } }

, timeUsed =

timeToTimeOfDay $ secondsToDiffTime $

toInteger tout })

Just (exitCode, out, tUsed) ->

let (err, retval) = case () of

_ | szsProved exitCode -> (ATPSuccess, provedStatus)

_ | szsDisproved exitCode -> (ATPSuccess, disProvedStatus)

_ | szsTimeout exitCode ->

(ATPTLimitExceeded, defaultProofStatus)

_ | szsStopped exitCode ->

(ATPBatchStopped, defaultProofStatus)

_ ->

(ATPError exitCode, defaultProofStatus)

defaultProofStatus =

(openProofStatus (AS_Anno.senAttr nGoal) name emptyProofTree)

{ usedTime =

timeToTimeOfDay $ secondsToDiffTime $

toInteger tUsed

, tacticScript = TacticScript $ show ATPTacticScript

{ tsTimeLimit = configTimeLimit cfg,

tsExtraOpts = [] } }

disProvedStatus = defaultProofStatus {goalStatus = Disproved}

provedStatus = defaultProofStatus { goalStatus = Proved True

, usedAxioms = getAxioms pst }

in return (err, cfg { proofStatus = retval

, resultOutput = out

, timeUsed =

timeToTimeOfDay $ secondsToDiffTime $

toInteger tUsed })

runProverProcess

:: ProverFuncs

-> GenericConfig ProofTree -- config

-> Int -- ^ timeout time in seconds

-> Bool -- ^ save problem

-> String -- ^ filename without extension

-> String -- ^ problem

-> IO (Maybe (String, [String], Int))

runProverProcess d cfg tout saveTHF tmpFileName prob = do

let tmpFile = basename tmpFileName ++ ".p"

writeFile tmpFile prob

(cmd, args) <- proverCommand d tout tmpFile cfg

mres <- timeoutCommand tout cmd args

maybe (return Nothing) (\ (_, pout, perr) -> do

let l = lines pout

(res', _, tUsed) = parseOutput d l

res = getMessage d res' pout perr

unless saveTHF $ removeFile tmpFile

return $ Just (res, l, tUsed)) mres

-- parse the output and return the szsStatus and the used time.

parseOutput :: ProverFuncs -> [String] -> (String, Bool, Int)

-- ^ (exit code, status found, used time ins ms)

parseOutput d = foldl checkLine ("", False, -1) where

checkLine (exCode, stateFound, to) line = case getSZSStatusWord line of

Just szsState | not stateFound -> (szsState, True, to)

_ -> case getTimeUsed d line of

Just secs -> (exCode, stateFound, secs)

Nothing -> (exCode, stateFound, to)

-- try to read the szs status from a given String

getSZSStatusWord :: String -> Maybe String

getSZSStatusWord line =

case words (fromMaybe "" $ stripPrefix "% SZS status" line) of

[] -> Nothing

w : _ -> Just w