7c5b9e36788476b052a83f4c815f956a507139abDominik LueckeDescription : Interface to the theorem prover e-krhyper in CASC-mode.
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckeCopyright : (c) Dominik Luecke, Uni Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckeMaintainer : luecke@informatik.uni-bremen.de
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckeStability : provisional
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckePortability : needs POSIX
7c5b9e36788476b052a83f4c815f956a507139abDominik Lueckefor details. For the ease of maintenance we are using e-krhyper in
7c5b9e36788476b052a83f4c815f956a507139abDominik Lueckeits CASC-mode, aka tptp-input. It works for single input files and
7b336a27b56727a0f016ba99abe635a1f488ace9Christian Maedermodule SoftFOL.ProveHyperHyper (hyperS, hyperProver, hyperConsChecker)
7c5b9e36788476b052a83f4c815f956a507139abDominik Lueckeimport qualified Common.Result as Result
7c5b9e36788476b052a83f4c815f956a507139abDominik Lueckeimport qualified Control.Concurrent as Concurrent
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maederimport Data.Time.LocalTime (TimeOfDay, midnight)
7b336a27b56727a0f016ba99abe635a1f488ace9Christian MaederhyperS :: String
7b336a27b56727a0f016ba99abe635a1f488ace9Christian MaederhyperS = "ekrh"
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder-- | The Prover implementation.
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckehyperProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederhyperProver =
e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder mkAutomaticProver hyperS hyperS () hyperGUI hyperCMDLautomaticBatch
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke Record for prover specific functions. This is used by both GUI and command
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke line interface.
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckeatpFun :: String -- ^ theory name
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckeatpFun thName = ATPFunctions
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke { initialProverState = spassProverState
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , atpTransSenName = transSenName
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , atpInsertSentence = insertSentenceGen
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , goalOutput = showTPTPProblem thName
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , proverHelpText = "for more information visit " ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "http://www.uni-koblenz.de/~bpelzer/ekrhyper/"
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , batchTimeEnv = "HETS_HYPER_BATCH_TIME_LIMIT"
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , fileExtensions = FileExtensions
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke { problemOutput = ".tptp"
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , proverOutput = ".hyper"
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , theoryConfiguration = ".hypcf" }
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , runProver = runHyper
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke , createProverOptions = extraOpts }
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke Invokes the generic prover GUI.
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckehyperGUI :: String -- ^ theory name
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> Theory Sign Sentence ProofTree
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder {- ^ theory consisting of a SoftFOL.Sign.Sign
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder and a list of Named SoftFOL.Sign.Sentence -}
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckehyperGUI thName th freedefs =
7b336a27b56727a0f016ba99abe635a1f488ace9Christian Maeder genericATPgui (atpFun thName) True hyperS thName th
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke freedefs emptyProofTree
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke automatic command line interface to the prover.
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckehyperCMDLautomaticBatch ::
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke Bool -- ^ True means include proved theorems
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> Bool -- ^ True means save problem file
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> Concurrent.MVar (Result.Result [ProofStatus ProofTree])
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -- ^ used to store the result of the batch run
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> String -- ^ theory name
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> TacticScript -- ^ default tactic script
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder -> Theory Sign Sentence ProofTree {- ^ theory consisting of a
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder 'SoftFOL.Sign.Sign' and a list of Named 'SoftFOL.Sign.Sentence' -}
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder -> IO (Concurrent.ThreadId, Concurrent.MVar ())
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder {- ^ fst: identifier of the batch thread for killing it
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder snd: MVar to wait for the end of the thread -}
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckehyperCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke thName defTS th freedefs =
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
7b336a27b56727a0f016ba99abe635a1f488ace9Christian Maeder resultMVar hyperS thName
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik LueckeprelTxt :: String -> String
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% only print essential output\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "#(set_verbosity(1)).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% assume all input to be in tptp-syntax\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "#(set_parameter(input_type, 2)).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% To prevent blowing up my memory\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "#(set_memory_limit(500)).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% produce SZS results\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "#(set_flag(szs_output_flag, true)).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% do not use special evaluable symbols\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "#(clear_builtins).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% initial term weight bound, 3 recommended for TPTP-problems\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "#(set_parameter(max_weight_initial, 3)).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% Terminate if out of memory\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "#(set_parameter(limit_termination_method,0)).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% Terminate if out of time\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "#(set_parameter(timeout_termination_method,0)).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% Start timer\n" ++
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder "#(start_wallclock_timer(" ++ t ++ ".0)).\n"
3edfc414dcff69e925308383a21d5d6357c82f55Christian MaedercheckOption :: String -> Bool
3edfc414dcff69e925308383a21d5d6357c82f55Christian MaedercheckOption a = isPrefixOf "#(" a && isSuffixOf ")." a
f08abfeef7f30b42e2b2ca143653acc95449d494Dominik LueckeuniteOptions :: [String] -> [String]
f08abfeef7f30b42e2b2ca143653acc95449d494Dominik LueckeuniteOptions opts =
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder a : b : cs ->
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder if checkOption a
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder a : uniteOptions (b : cs)
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder (a ++ b) : uniteOptions cs
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckerunTxt :: String
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% start derivation with the input received so far\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "#(run).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% print normal E-KRHyper proof\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "%#(print_proof).\n\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% print result and proof using SZS terminology;\n" ++
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke "% requires postprocessing with post_szs script for proper legibility\n" ++
f08abfeef7f30b42e2b2ca143653acc95449d494Dominik Luecke "#(print_szs_proof).\n"
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckerunHyper :: SoftFOLProverState
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder {- ^ logical part containing the input Sign and axioms and possibly
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder goals that have been proved earlier as additional axioms -}
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> GenericConfig ProofTree -- ^ configuration to use
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> Bool -- ^ True means save TPTP file
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> String -- ^ name of the theory in the DevGraph
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> AS_Anno.Named SPTerm -- ^ goal to prove
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -> IO (ATPRetval, GenericConfig ProofTree)
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke -- ^ (retval, configuration with proof status and complete output)
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckerunHyper sps cfg saveTPTP thName nGoal =
7ac8badfe78c05f13bf9132aba697ff37e450431Christian Maeder saveFile = basename thName ++ '_' : AS_Anno.senAttr nGoal ++ ".tptp"
f08abfeef7f30b42e2b2ca143653acc95449d494Dominik Luecke simpleOptions = uniteOptions $ extraOpts cfg
7c5b9e36788476b052a83f4c815f956a507139abDominik Luecke tl = configTimeLimit cfg
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder tScript = TacticScript $ show ATPTacticScript
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder { tsTimeLimit = tl
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder , tsExtraOpts = filter (isPrefixOf "#")
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder $ lines $ prelTxt (show tl) ++ runTxt }
070dd5578b66422393405b2fc38b950987e59fd5Eugen Kuksa defProofStat = (openProofStatus
070dd5578b66422393405b2fc38b950987e59fd5Eugen Kuksa (senAttr nGoal)
070dd5578b66422393405b2fc38b950987e59fd5Eugen Kuksa emptyProofTree) { tacticScript = tScript }
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder if all checkOption simpleOptions
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder prob <- showTPTPProblem thName sps nGoal []
7ac8badfe78c05f13bf9132aba697ff37e450431Christian Maeder when saveTPTP (writeFile saveFile prob)
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder (stdoutC, stderrC, t_u) <- runHyperProcess prob saveFile (show tl)
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder ('\n' : unlines simpleOptions) runTxt
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder let (pStat, ret) = examineProof sps stdoutC stderrC
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder defProofStat { usedTime = t_u }
f08abfeef7f30b42e2b2ca143653acc95449d494Dominik Luecke return (pStat, cfg
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder { proofStatus = ret
f08abfeef7f30b42e2b2ca143653acc95449d494Dominik Luecke , resultOutput = lines (stdoutC ++ stderrC)
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder , timeUsed = usedTime ret })
f08abfeef7f30b42e2b2ca143653acc95449d494Dominik Luecke (ATPError "Syntax error in options"
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder { proofStatus = defProofStat
f08abfeef7f30b42e2b2ca143653acc95449d494Dominik Luecke , resultOutput = ["Parse Error"]
f0cb315452faea6fee8144489629e63e9bd7b303Christian Maeder , timeUsed = midnight
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder-- | call ekrh
3edfc414dcff69e925308383a21d5d6357c82f55Christian MaederrunHyperProcess
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder :: String -- ^ problem
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder -> String -- ^ file name template
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder -> String -- ^ time limit
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder -> String -- ^ extra options
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder -> String -- ^ run text
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder -> IO (String, String, TimeOfDay) -- ^ out, err, diff time
3edfc414dcff69e925308383a21d5d6357c82f55Christian MaederrunHyperProcess prob saveFile tl opts runTxtA = do
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder stpTmpFile <- getTempFile prob saveFile
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder let stpPrelFile = stpTmpFile ++ ".prelude.tme"
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder stpRunFile = stpTmpFile ++ ".run.tme"
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder writeFile stpPrelFile $ prelTxt tl ++ opts
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder writeFile stpRunFile runTxtA
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder t_start <- getHetsTime
7b336a27b56727a0f016ba99abe635a1f488ace9Christian Maeder (_, stdoutC, stderrC) <- executeProcess hyperS
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder [stpPrelFile, stpTmpFile, stpRunFile] ""
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder t_end <- getHetsTime
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder removeFile stpPrelFile
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder removeFile stpRunFile
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder removeFile stpTmpFile
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder return (stdoutC, stderrC, diffHetsTime t_end t_start)
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder-- | Mapping type from SZS to Hets
7c5b9e36788476b052a83f4c815f956a507139abDominik Lueckedata HyperResult = HProved | HDisproved | HTimeout | HError | HMemout
7d786e51d8a65852f2347ff0d8bc720d25313e76Christian MaedergetHyperResult :: [String] -> HyperResult
7d786e51d8a65852f2347ff0d8bc720d25313e76Christian MaedergetHyperResult out = case map (takeWhile isAlpha . dropWhile isSpace)
7d786e51d8a65852f2347ff0d8bc720d25313e76Christian Maeder $ mapMaybe (stripPrefix "% SZS status ") out of
7d786e51d8a65852f2347ff0d8bc720d25313e76Christian Maeder [s] | szsProved s -> HProved
7d786e51d8a65852f2347ff0d8bc720d25313e76Christian Maeder | szsDisproved s -> HDisproved
7d786e51d8a65852f2347ff0d8bc720d25313e76Christian Maeder | szsTimeout s -> HTimeout
7d786e51d8a65852f2347ff0d8bc720d25313e76Christian Maeder | szsMemoryOut s -> HMemout
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder-- | examine SZS output
7c5b9e36788476b052a83f4c815f956a507139abDominik LueckeexamineProof :: SoftFOLProverState
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder -> ProofStatus ProofTree
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder -> (ATPRetval, ProofStatus ProofTree)
3edfc414dcff69e925308383a21d5d6357c82f55Christian MaederexamineProof sps stdoutC stderrC defStatus =
914425f2c2846927aa187964aee6ffb8dad9a2a7Christian Maeder let outText = "\nOutput was:\n\n" ++ stdoutC ++ stderrC
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder provenStat = defStatus
914425f2c2846927aa187964aee6ffb8dad9a2a7Christian Maeder { usedAxioms = getAxioms sps
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder , proofTree = ProofTree stdoutC }
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder in case getHyperResult $ lines stdoutC of
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder HProved -> (ATPSuccess, provenStat { goalStatus = Proved True })
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder HTimeout -> (ATPTLimitExceeded, defStatus)
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder HDisproved -> (ATPSuccess, provenStat { goalStatus = Disproved })
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder HMemout -> (ATPError ("Out of Memory." ++ outText), defStatus)
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder HError -> ( ATPError ("Internal Error in ekrhyper." ++ outText)
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke-- Consistency Checker
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik LueckehyperConsChecker :: ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederhyperConsChecker = (mkUsableConsChecker hyperS hyperS () consCheck)
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke { ccNeedsTimer = False }
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke Runs the krhyper cons-chcker. The tactic script only contains a string for the
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik LueckerunTxtC :: String
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke "% start derivation with the input received so far\n" ++
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke "#(run).\n\n" ++
7b336a27b56727a0f016ba99abe635a1f488ace9Christian Maeder "% print Hyper proof\n" ++
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke "%#(print_proof).\n\n" ++
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke "% print result and proof using SZS terminology;\n" ++
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke "% requires postprocessing with post_szs script for proper legibility\n" ++
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke "%#(print_szs_proof).\n\n" ++
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke "% Show the model\n" ++
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke "#(print_model).\n"
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik LueckeconsCheck :: String
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke -> TacticScript
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke -> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder -> IO (CCStatus ProofTree)
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik LueckeconsCheck thName (TacticScript tl) tm freedefs =
6c6d2a6f4311ec0548fcbbf8b4a77ed05d57fcdaDominik Luecke case tTarget tm of
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder Theory sig nSens -> do
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder let proverStateI = spassProverState sig (toNamedList nSens) freedefs
cfd1a004271309b400e2856c4c4e4cf1a00393b2Christian Maeder saveFile = basename thName ++ ".tptp"
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder prob <- showTPTPProblemM thName proverStateI []
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder (stdoutC, stderrC, t_u) <-
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder runHyperProcess prob saveFile tl "" runTxtC
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder return CCStatus
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder { ccResult = case getHyperResult $ lines stdoutC of
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder HProved -> Just True
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder HDisproved -> Just False
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder , ccProofTree = ProofTree $ stdoutC ++ stderrC
3edfc414dcff69e925308383a21d5d6357c82f55Christian Maeder , ccUsedTime = t_u }