SZSProver.hs revision ad1df93673cf323534cdfe18981ad5daae4c90c0
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederModule : $Header$
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederDescription : General Interface to a prover using SZS status messages
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederCopyright : (c) Jonathan von Schroeder, DFKI Bremen 2012
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
ad1df93673cf323534cdfe18981ad5daae4c90c0Jonathan von SchroederMaintainer : Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederStability : provisional
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederPortability : non-portable (imports Prover)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederIsabelle theorem prover for THF
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder ( createSZSProver
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder , ProverFuncs (..)
8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroederimport THF.As (THFFormula)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederimport Common.AS_Annotation as AS_Anno
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederimport Common.Utils (basename, timeoutCommand)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederimport qualified Control.Concurrent as Concurrent
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederimport Data.Time (timeToTimeOfDay)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederimport Data.Time.Clock (secondsToDiffTime)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroederdata ProverFuncs = ProverFuncs {
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder cfgTimeout :: GenericConfig ProofTree -> Int, -- in seconds
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder proverCommand :: Int -> String -> GenericConfig ProofTree ->
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder IO (String, [String]),
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -- timeout -> problem file
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder getMessage :: String -> String -> String -> String,
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -- result -> std out -> std err
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder getTimeUsed :: String -> Maybe Int -- in seconds
8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroedertype ProverType = Prover SignTHF THFFormula MorphismTHF THFSl ProofTree
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroedercreateSZSProver :: String -> String -> ProverFuncs ->
55dfa79a16e5f0ddb60bceab3717c07e62e65846Jonathan von SchroedercreateSZSProver name hlp d = mkAutomaticProver name tHF0
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder (proverGUI hlp name d)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder (proverCMDLautomaticBatch hlp name d)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederatpFun :: ProverFuncs
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- name
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- ^ theory name
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- help text
8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder -> ATPFunctions SignTHF THFFormula MorphismTHF ProofTree ProverStateTHF
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederatpFun d name _ hlp = ATPFunctions
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder { initialProverState = initialProverStateTHF
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , atpTransSenName = id
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , atpInsertSentence = insertSentenceTHF
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , goalOutput = showProblemTHF
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , proverHelpText = hlp
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , batchTimeEnv = "HETS_TPTP_BATCH_TIME_LIMIT"
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder , fileExtensions = FileExtensions {
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder problemOutput = ".p"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , proverOutput = ""
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , theoryConfiguration = "" }
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , runProver = runProverT d name
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , createProverOptions = extraOpts }
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederproverGUI :: String -- help text
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- name
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- ^ theory name
8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder -> Theory SignTHF THFFormula ProofTree
8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder -> [FreeDefMorphism THFFormula MorphismTHF] -- ^ freeness constraints
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederproverGUI hlp name d thName th freedefs =
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder genericATPgui (atpFun d name thName hlp) True name thName th
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder freedefs emptyProofTree
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederproverCMDLautomaticBatch
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder :: String -- help
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- name
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> Bool -- ^ True means include proved theorems
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> Bool -- ^ True means save problem file
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> Concurrent.MVar (Result [ProofStatus ProofTree])
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -- ^ used to store the result of the batch run
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- ^ theory name
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> TacticScript -- ^ default tactic script
8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder -> Theory SignTHF THFFormula ProofTree
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -- ^ theory consisting of a signature and sentences
8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder -> [FreeDefMorphism THFFormula MorphismTHF] -- ^ freeness constraints
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> IO (Concurrent.ThreadId, Concurrent.MVar ())
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder {- ^ fst: identifier of the batch thread for killing it
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder snd: MVar to wait for the end of the thread -}
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederproverCMDLautomaticBatch hlp name d inclProvedThs saveProblem_batch resultMVar
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder thName defTS th freedefs =
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder genericCMDLautomaticBatch (atpFun d name thName hlp) inclProvedThs
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder saveProblem_batch
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder resultMVar name thName
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederrunProverT :: ProverFuncs
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- name
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> ProverStateTHF
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> GenericConfig ProofTree -- ^ configuration to use
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> Bool -- ^ True means save THF file
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- ^ name of the theory in the DevGraph
8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder -> Named THFFormula -- ^ goal to prove
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> IO (ATPRetval, GenericConfig ProofTree)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -- ^ (retval, configuration with proof status and complete output)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederrunProverT d name pst cfg saveTHF thName nGoal = do
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder let tout = cfgTimeout d cfg
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder tmpFileName = thName ++ '_' : AS_Anno.senAttr nGoal
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder prob <- showProblemTHF pst nGoal []
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder runRes <- runProverProcess d cfg tout saveTHF tmpFileName prob
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder Nothing -> return (ATPTLimitExceeded, cfg
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder { proofStatus =
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder (openProofStatus (AS_Anno.senAttr nGoal)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder name emptyProofTree)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder timeToTimeOfDay $ secondsToDiffTime $
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , tacticScript = TacticScript
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder $ show ATPTacticScript
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder { tsTimeLimit = configTimeLimit cfg,
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder tsExtraOpts = [] } }
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder timeToTimeOfDay $ secondsToDiffTime $
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder toInteger tout })
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder Just (exitCode, out, tUsed) ->
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder let (err, retval) = case () of
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder _ | szsProved exitCode -> (ATPSuccess, provedStatus)
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder _ | szsDisproved exitCode -> (ATPSuccess, disProvedStatus)
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder _ | szsTimeout exitCode ->
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder (ATPTLimitExceeded, defaultProofStatus)
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder _ | szsStopped exitCode ->
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder (ATPBatchStopped, defaultProofStatus)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder (ATPError exitCode, defaultProofStatus)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder defaultProofStatus =
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder (openProofStatus (AS_Anno.senAttr nGoal) name emptyProofTree)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder timeToTimeOfDay $ secondsToDiffTime $
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder toInteger tUsed
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , tacticScript = TacticScript $ show ATPTacticScript
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder { tsTimeLimit = configTimeLimit cfg,
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder tsExtraOpts = [] } }
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder disProvedStatus = defaultProofStatus {goalStatus = Disproved}
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder provedStatus = defaultProofStatus { goalStatus = Proved True
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , usedAxioms = getAxioms pst }
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder in return (err, cfg { proofStatus = retval
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder , resultOutput = out
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder timeToTimeOfDay $ secondsToDiffTime $
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder toInteger tUsed })
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederrunProverProcess
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> GenericConfig ProofTree -- config
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> Int -- ^ timeout time in seconds
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> Bool -- ^ save problem
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- ^ filename without extension
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> String -- ^ problem
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -> IO (Maybe (String, [String], Int))
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederrunProverProcess d cfg tout saveTHF tmpFileName prob = do
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder let tmpFile = basename tmpFileName ++ ".p"
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder writeFile tmpFile prob
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder (cmd, args) <- proverCommand d tout tmpFile cfg
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder mres <- timeoutCommand tout cmd args
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder maybe (return Nothing) (\ (_, pout, perr) -> do
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder let l = lines pout
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder (res', _, tUsed) = parseOutput d l
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder res = getMessage d res' pout perr
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder unless saveTHF $ removeFile tmpFile
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder return $ Just (res, l, tUsed)) mres
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder-- parse the output and return the szsStatus and the used time.
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederparseOutput :: ProverFuncs -> [String] -> (String, Bool, Int)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder -- ^ (exit code, status found, used time ins ms)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroederparseOutput d = foldl checkLine ("", False, -1) where
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder checkLine (exCode, stateFound, to) line = case getSZSStatusWord line of
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder Just szsState | not stateFound -> (szsState, True, to)
8f115733923ad2b5f4ce3bf7f4206007cea2070dChristian Maeder _ -> case getTimeUsed d line of
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder Just secs -> (exCode, stateFound, secs)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder Nothing -> (exCode, stateFound, to)
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder-- try to read the szs status from a given String
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroedergetSZSStatusWord :: String -> Maybe String
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von SchroedergetSZSStatusWord line =
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder case words (fromMaybe "" $ stripPrefix "% SZS status" line) of
f9096659967df62573bb5a5fd069c41bf5a0eca1Jonathan von Schroeder w : _ -> Just w