0N/A{- |

0N/AModule : $Header$

0N/ADescription : Interface to the theorem prover e-krhyper in CASC-mode.

0N/ACopyright : (c) Dominik Luecke, Uni Bremen 2010

0N/ALicense : GPLv2 or higher

157N/AMaintainer : luecke@informatik.uni-bremen.de

0N/AStability : provisional

0N/APortability : needs POSIX

0N/A

0N/ACheck out

0N/Afor details. For the ease of maintenance we are using e-krhyper in

157N/Aits CASC-mode, aka tptp-input. It works for single input files and

0N/Afof-style.

0N/A-}

0N/A

0N/Amodule SoftFOL.ProveHyperHyper (hyperProver, hyperConsChecker)

0N/A where

0N/A

0N/Aimport Logic.Prover

0N/A

0N/Aimport Common.ProofTree

0N/Aimport qualified Common.Result as Result

0N/Aimport Common.AS_Annotation as AS_Anno

0N/Aimport Common.SZSOntology

0N/Aimport Common.Timing

0N/A

0N/Aimport SoftFOL.Sign

0N/Aimport SoftFOL.Translate

0N/Aimport SoftFOL.ProverState

0N/A

0N/Aimport GUI.GenericATP

0N/Aimport Proofs.BatchProcessing

0N/Aimport Interfaces.GenericATPState

0N/A

0N/Aimport System.IO

0N/Aimport System.Process

0N/Aimport System.Directory

0N/A

0N/Aimport Control.Monad (when)

0N/Aimport qualified Control.Concurrent as Concurrent

0N/A

0N/Aimport Data.Char

0N/Aimport Data.List

0N/Aimport Data.Maybe

0N/A

0N/Aimport Data.Time.LocalTime (TimeOfDay, midnight)

0N/Aimport Data.Time.Clock (UTCTime(..), getCurrentTime)

0N/A

0N/A-- Prover

0N/A

0N/A{- | The Prover implementation. -}

0N/AhyperProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree

0N/AhyperProver = mkAutomaticProver "ekrhyper" () hyperGUI hyperCMDLautomaticBatch

0N/A

0N/A{- |

0N/A Record for prover specific functions. This is used by both GUI and command

0N/A line interface.

0N/A-}

0N/AatpFun :: String -- ^ theory name

-> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState

atpFun thName = ATPFunctions

{ initialProverState = spassProverState

, atpTransSenName = transSenName

, atpInsertSentence = insertSentenceGen

, goalOutput = showTPTPProblem thName

, proverHelpText = "for more information visit " ++

"http://www.uni-koblenz.de/~bpelzer/ekrhyper/"

, batchTimeEnv = "HETS_HYPER_BATCH_TIME_LIMIT"

, fileExtensions = FileExtensions

{ problemOutput = ".tptp"

, proverOutput = ".hyper"

, theoryConfiguration = ".hypcf" }

, runProver = runHyper

, createProverOptions = extraOpts }

{- |

Invokes the generic prover GUI.

-}

hyperGUI :: 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

hyperGUI thName th freedefs =

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

freedefs emptyProofTree

{- |

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

automatic command line interface to the prover.

-}

hyperCMDLautomaticBatch ::

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

hyperCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar

thName defTS th freedefs =

genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch

resultMVar (proverName hyperProver) thName

(parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

prelTxt :: String -> String

prelTxt t =

"% only print essential output\n" ++

"#(set_verbosity(1)).\n\n" ++

"% assume all input to be in tptp-syntax\n" ++

"#(set_parameter(input_type, 2)).\n\n" ++

"% To prevent blowing up my memory\n" ++

"#(set_memory_limit(500)).\n\n" ++

"% produce SZS results\n" ++

"#(set_flag(szs_output_flag, true)).\n\n" ++

"% do not use special evaluable symbols\n" ++

"#(clear_builtins).\n\n" ++

"% initial term weight bound, 3 recommended for TPTP-problems\n" ++

"#(set_parameter(max_weight_initial, 3)).\n\n" ++

"% Terminate if out of memory\n" ++

"#(set_parameter(limit_termination_method,0)).\n\n" ++

"% Terminate if out of time\n" ++

"#(set_parameter(timeout_termination_method,0)).\n\n" ++

"% Start timer\n" ++

"#(start_wallclock_timer("++ t ++".0)).\n"

uniteOptions :: [String] -> [String]

uniteOptions opts =

case opts of

[] -> []

a:[] -> a:[]

a:b:cs ->

if ("#(" `isPrefixOf` a && ")." `isSuffixOf` a)

then

a:(uniteOptions (b:cs))

else

(a ++ b):(uniteOptions cs)

runTxt :: String

runTxt =

"% start derivation with the input received so far\n" ++

"#(run).\n\n" ++

"% print normal E-KRHyper proof\n" ++

"%#(print_proof).\n\n" ++

"% print result and proof using SZS terminology;\n" ++

"% requires postprocessing with post_szs script for proper legibility\n" ++

"#(print_szs_proof).\n"

runHyper :: 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)

runHyper sps cfg saveTPTP thName nGoal =

let

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

tmpFile = (reverse $ fst $ span (/='/') $ reverse thName) ++

'_':AS_Anno.senAttr nGoal

prelFile = "prelude_" ++ (reverse $ fst $ span (/='/') $ reverse

thName)

++ '_':AS_Anno.senAttr nGoal

runFile = "run_" ++ (reverse $ fst $ span (/='/') $ reverse

thName)

++ '_':AS_Anno.senAttr nGoal

simpleOptions = uniteOptions $ extraOpts cfg

tl = configTimeLimit cfg

in

do

let chk = and $ map (\x ->

"#(" `isPrefixOf` x &&

")." `isSuffixOf` x

) simpleOptions

if chk

then

do

prob <- showTPTPProblem thName sps nGoal $ []

when saveTPTP

(writeFile (saveFile ++".tptp") prob)

t <- getCurrentTime

let stpTmpFile = "/tmp/" ++ tmpFile ++ (show $ utctDay t) ++

"-" ++ (show $ utctDayTime t) ++ ".tptp"

stpPrelFile = "/tmp/" ++ prelFile ++ (show $ utctDay t) ++

"-" ++ (show $ utctDayTime t) ++ ".tme"

stpRunFile = "/tmp/" ++ runFile ++ (show $ utctDay t) ++

"-" ++ (show $ utctDayTime t) ++ ".tme"

writeFile stpPrelFile $

((prelTxt $ show tl) ++ "\n" ++ unlines

simpleOptions)

writeFile stpRunFile $ runTxt

writeFile stpTmpFile $ prob

let command = "ekrh " ++ stpPrelFile ++ " " ++ stpTmpFile ++

" " ++ stpRunFile

t_start <- getHetsTime

(_, stdouth, stderrh, proch) <- runInteractiveCommand command

waitForProcess proch

t_end <- getHetsTime

removeFile stpPrelFile

removeFile stpRunFile

removeFile stpTmpFile

let t_u = diffHetsTime t_end t_start

stdoutC <- hGetContents stdouth

stderrC <- hGetContents stderrh

(pStat, ret) <- examineProof sps cfg stdoutC stderrC nGoal t_u tl

return (pStat, cfg

{

proofStatus = ret

, resultOutput = lines (stdoutC ++ stderrC)

, timeUsed = usedTime ret

})

else

do

let tScript opts = TacticScript $ show ATPTacticScript

{ tsTimeLimit = configTimeLimit cfg

, tsExtraOpts = opts }

return $

(ATPError "Syntax error in options"

, cfg

{proofStatus =

ProofStatus { goalName = senAttr nGoal

, goalStatus = openGoalStatus

, usedAxioms = []

, usedProver = proverName hyperProver

, proofTree = emptyProofTree

, usedTime = midnight

, tacticScript = tScript $

(filter

(\x -> "#" `isPrefixOf` x)$

lines $ (prelTxt $ show tl)

++ runTxt)}

, resultOutput = ["Parse Error"]

, timeUsed = midnight

})

{- | Mapping type from SZS to Hets -}

data HyperResult = HProved | HDisproved | HTimeout | HError | HMemout

getHyperResult :: [String] -> HyperResult

getHyperResult out = case map (takeWhile isAlpha . dropWhile isSpace)

$ mapMaybe (stripPrefix "% SZS status ") out of

[s] | szsProved s -> HProved

| szsDisproved s -> HDisproved

| szsTimeout s -> HTimeout

| szsMemoryOut s -> HMemout

_ -> HError

{- | examine SZS output -}

examineProof :: SoftFOLProverState

-> GenericConfig ProofTree

-> String

-> String

-> AS_Anno.Named SPTerm

-> TimeOfDay

-> Int

-> IO (ATPRetval, ProofStatus ProofTree)

examineProof sps cfg stdoutC stderrC nGoal tUsed tl =

let

tScript opts = TacticScript $ show ATPTacticScript

{ tsTimeLimit = configTimeLimit cfg

, tsExtraOpts = opts }

defaultStatus =

ProofStatus { goalName = senAttr nGoal

, goalStatus = openGoalStatus

, usedAxioms = []

, usedProver = proverName hyperProver

, proofTree = emptyProofTree

, usedTime = tUsed

, tacticScript = tScript $ (filter

(\x -> "#" `isPrefixOf` x) $

lines $ (prelTxt $ show tl) ++ runTxt)}

getAxioms =

let

fl = formulaLists $ initialLogicalPart sps

fs = concatMap formulae $ filter (\x ->

case originType x of

SPOriginAxioms -> True

_ -> False

) fl

in map AS_Anno.senAttr fs

in case getHyperResult $ lines stdoutC of

HProved -> return (ATPSuccess, defaultStatus

{

goalStatus = Proved True

, usedAxioms = getAxioms

, proofTree = ProofTree stdoutC

})

HTimeout -> return (ATPTLimitExceeded, defaultStatus)

HDisproved -> return (ATPSuccess, defaultStatus

{

goalStatus = Disproved

, usedAxioms = getAxioms

, proofTree = ProofTree stdoutC

})

HMemout -> return (ATPError ("Out of Memory."

++ "\nOutput was:\n\n" ++

stdoutC ++ stderrC)

, defaultStatus)

HError -> return (ATPError ("Internal Error in ekrhyper."

++ "\nOutput was:\n\n" ++

stdoutC ++ stderrC)

, defaultStatus)

-- Consistency Checker

hyperConsChecker :: ConsChecker Sign Sentence () SoftFOLMorphism ProofTree

hyperConsChecker = (mkConsChecker "ekrhyper" () consCheck)

{ ccNeedsTimer = False }

{- |

Runs the krhyper cons-chcker. The tactic script only contains a string for the

time limit.

-}

runTxtC :: String

runTxtC =

"% start derivation with the input received so far\n" ++

"#(run).\n\n" ++

"% print normal E-KRHyper proof\n" ++

"%#(print_proof).\n\n" ++

"% print result and proof using SZS terminology;\n" ++

"% requires postprocessing with post_szs script for proper legibility\n" ++

"%#(print_szs_proof).\n\n" ++

"% Show the model\n" ++

"#(print_model).\n"

consCheck :: String

-> TacticScript

-> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree

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

-> IO(CCStatus ProofTree)

consCheck thName (TacticScript tl) tm freedefs =

case tTarget tm of

Theory sig nSens ->

let

saveTPTP = False

proverStateI = spassProverState sig (toNamedList nSens) freedefs

problem = showTPTPProblemM thName proverStateI []

saveFile = reverse $ fst $ span (/= '/') $ reverse thName

tmpFile = (reverse $ fst $ span (/='/') $ reverse thName)

prelFile = "prelude_" ++ (reverse $ fst $ span (/='/') $ reverse

thName)

runFile = "run_" ++ (reverse $ fst $ span (/='/') $ reverse

thName)

in

do

prob <- problem

when saveTPTP

(writeFile (saveFile ++".tptp") prob)

t <- getCurrentTime

let stpTmpFile = "/tmp/" ++ tmpFile ++ (show $ utctDay t) ++

"-" ++ (show $ utctDayTime t) ++ ".tptp"

stpPrelFile = "/tmp/" ++ prelFile ++ (show $ utctDay t) ++

"-" ++ (show $ utctDayTime t) ++ ".tme"

stpRunFile = "/tmp/" ++ runFile ++ (show $ utctDay t) ++

"-" ++ (show $ utctDayTime t) ++ ".tme"

writeFile stpPrelFile $ prelTxt tl

writeFile stpRunFile $ runTxtC

writeFile stpTmpFile $ prob

let command = "ekrh " ++ stpPrelFile ++ " " ++ stpTmpFile ++

" " ++ stpRunFile

t_start <- getHetsTime

(_, stdouth, stderrh, proch) <- runInteractiveCommand command

waitForProcess proch

t_end <- getHetsTime

removeFile stpPrelFile

removeFile stpRunFile

removeFile stpTmpFile

stdoutC <- hGetContents stdouth

stderrC <- hGetContents stderrh

let t_u = diffHetsTime t_end t_start

outstate = CCStatus

{ ccResult = Nothing

, ccProofTree = ProofTree $ stdoutC ++ stderrC

, ccUsedTime = t_u }

case getHyperResult $ lines stdoutC of

HProved -> return outstate

{

ccResult = Just True

}

HDisproved -> return outstate

{

ccResult = Just False

}

_ -> return outstate