ProveDarwin.hs revision 71b4325b4363a587979f07bccb9c55e02ace168e
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederModule : $Header$
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederDescription : Interface to the TPTP theorem prover via Darwin.
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederCopyright : (c) Heng Jiang, Uni Bremen 2004-2007
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederMaintainer : jiang@informatik.uni-bremen.de
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederStability : provisional
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederPortability : needs POSIX
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederInterface for the Darwin service, uses GUI.GenericATP.
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian MaederSee <http://spass.mpi-sb.mpg.de/> for details on SPASS, and
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder<http://combination.cs.uiowa.edu/Darwin/> for Darwin.
25da71ee832b729e33def344a68f59fe21ce9c07Eugen Kuksa ( darwinProver
950875ac099734b9eaccf4233773e6df00477f22Eugen Kuksa , darwinCMDLautomatic
7d0db235b17b2109cd45fa50e6d1bbc77823f81dEugen Kuksa , darwinCMDLautomaticBatch
25da71ee832b729e33def344a68f59fe21ce9c07Eugen Kuksa , darwinConsChecker
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder-- preliminary hacks for display of CASL models
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaederimport Common.AS_Annotation as AS_Anno
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maederimport qualified Common.Result as Result
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksaimport Data.Char (isDigit)
8723ec450f2e7a024230467c0c28a3f154905483cmaederimport Data.List (isPrefixOf)
eae0d62755147d991cc3e903f74f98ac31a7cd42Christian Maederimport Data.Time (timeToTimeOfDay)
d4263171d0ce2cbc390a7b44bff98e8b3c0f8ce7Christian Maederimport Data.Time.Clock (UTCTime(..), secondsToDiffTime, getCurrentTime)
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maederimport qualified Control.Concurrent as Concurrent
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maederimport GUI.Utils (infoDialog)
7c99a6c982aaf61547de8054296c8055c8d1a13aSimon Ulbricht-- * Prover implementation
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder{- | The Prover implementation. First runs the batch prover (with
d97700a22b2585ece83b05f3fff945fdfd0c44b4Christian Maeder graphical feedback), then starts the GUI prover. -}
275698320a734a6fd647ea6a461d6ce38862da1dChristian MaederdarwinProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree
1d65a799298f6b1253d774c22f61029e6eb99cadcmaederdarwinProver = (mkProverTemplate "Darwin" () darwinGUI)
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder { proveCMDLautomatic = Just darwinCMDLautomatic
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder , proveCMDLautomaticBatch = Just darwinCMDLautomaticBatch }
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian MaederdarwinConsChecker
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder :: ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian MaederdarwinConsChecker = (mkProverTemplate "darwin" ()
f674d7a58db3f991300a708f3799d80c369781f8Eugen Kuksa (\ s -> consCheck s $ Tactic_script "20"))
fd94a6f66ccb5cef99aa42069b61e4b8734dbd3fChristian Maeder { proveCMDLautomatic = Just (\ s ts t -> fmap return . consCheck s ts t) }
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder Record for prover specific functions. This is used by both GUI and command
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder line interface.
473f5af6e4803fbeecc814065952396f2501039bChristian MaederatpFun :: String -- ^ theory name
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaederatpFun thName = ATPFunctions
6a88f8edd881afaf4b865b01bfbb4faaf0e7a3c9Simon Ulbricht { initialProverState = spassProverState
473f5af6e4803fbeecc814065952396f2501039bChristian Maeder , atpTransSenName = transSenName
20bbcc2b693b3040d7b8cc92ba966580637027d9cmaeder , atpInsertSentence = insertSentenceGen
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa , goalOutput = showTPTPProblem thName
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder , proverHelpText = "no help for darwin available"
e42249ec61f50a83525db6e5fc9f5c4dd1b4cf5fcmaeder , batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT"
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder , fileExtensions = FileExtensions
734a5ebd38032798f0ab908e2d52862c71b2c127Simon Ulbricht { problemOutput = ".tptp"
ea5ccb1c6e89486a54e1f4bd95840147e96093edChristian Maeder , proverOutput = ".spass"
c8afa08a8bda589ef6670068dff0108464be4da7Christian Maeder , theoryConfiguration = ".spcf" }
c99b0eb6632087d502dd4269599c5aa68a148eebSimon Ulbricht , runProver = runDarwin
b99c9606f2faafeabb3fa8c596992143a561c787Simon Ulbricht , createProverOptions = extraOpts }
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder Invokes the generic prover GUI. SPASS specific functions are omitted by
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder data type ATPFunctions.
f675b8f0a612e37472640da57b48d795bef4427eChristian MaederdarwinGUI :: String -- ^ theory name
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -> Theory Sign Sentence ProofTree
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder -- ^ theory consisting of a SoftFOL.Sign.Sign
7b21830970250ca6369b0ae60f34c990f9a5c5bfTill Mossakowski -- and a list of Named SoftFOL.Sign.Sentence
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder -> IO([Proof_status ProofTree]) -- ^ proof status for each goal
dae8246f1f55b6a85e946fc1bfb6d32d556395f1Simon UlbrichtdarwinGUI thName th freedefs =
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder genericATPgui (atpFun thName) True (prover_name darwinProver) thName th
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa freedefs emptyProofTree
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder-- ** command line functions
2e2559f894aaa661b199e4fa00609f522bc5482aSimon Ulbricht Implementation of 'Logic.Prover.proveCMDLautomatic' which provides an
df67ddf64192bfcae6ece65255ad796a17cbe532Christian Maeder automatic command line interface for a single goal.
be1ce1c2b2819ef32743136c13101f1927375311Christian Maeder Darwin specific functions are omitted by data type ATPFunctions.
f674d7a58db3f991300a708f3799d80c369781f8Eugen KuksadarwinCMDLautomatic ::
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder String -- ^ theory name
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder -> Tactic_script -- ^ default tactic script
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder -> Theory Sign Sentence ProofTree
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -- ^ theory consisting of a signature and a list of Named sentence
526e7f36639cb58e3c99a54bea082499a6b04a25Christian Maeder -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
3e87e1dc85fa76cc6eaeb8eafbc0bea77af939f4Christian Maeder -> IO (Result.Result ([Proof_status ProofTree]))
275698320a734a6fd647ea6a461d6ce38862da1dChristian Maeder -- ^ Proof status for goals and lemmas
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian MaederdarwinCMDLautomatic thName defTS th freedefs =
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder genericCMDLautomatic (atpFun thName) (prover_name darwinProver) thName
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian Maeder (parseTactic_script batchTimeLimit [] defTS) th freedefs emptyProofTree
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder automatic command line interface to the Darwin prover via MathServe.
8f9ac967da20be8d7782d2fc0a085dd42f79c0cbEugen Kuksa Darwin specific functions are omitted by data type ATPFunctions.
6a6689ad6d4c70af2ce3389f39a50982f20fd939Christian MaederdarwinCMDLautomaticBatch ::
703004db20b23870f080c4d9640729b19b7c2288Eugen Kuksa Bool -- ^ True means include proved theorems
703004db20b23870f080c4d9640729b19b7c2288Eugen Kuksa -> Bool -- ^ True means save problem file
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder -> Concurrent.MVar (Result.Result [Proof_status ProofTree])
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder -- ^ used to store the result of the batch run
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder -> String -- ^ theory name
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder -> Tactic_script -- ^ default tactic script
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder -> Theory Sign Sentence ProofTree -- ^ theory consisting of a
5896f38ba2934056542cb7cb3e6359e88a622547Christian Maeder -- 'SoftFOL.Sign.Sign' and a list of Named 'SoftFOL.Sign.Sentence'
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder -- ^ fst: identifier of the batch thread for killing it
eca54dc24f2c59cc51645115347a89ba2b40de36cmaeder -- snd: MVar to wait for the end of the thread
eca54dc24f2c59cc51645115347a89ba2b40de36cmaederdarwinCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder thName defTS th freedefs =
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
18548c6cc2dff13bf9f5f08b3f6cde6ca914df1dChristian Maeder resultMVar (prover_name darwinProver) thName
5fb6343a5a2b4bbc67bc83479c84a92d23d30edfChristian Maeder (parseTactic_script batchTimeLimit [] defTS) th freedefs emptyProofTree
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder-- * Main prover functions
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder Runs the Darwin service. The tactic script only contains a string for the
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederconsCheck :: String
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -> Tactic_script
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -> [FreeDefMorphism SPTerm SoftFOLMorphism] -- ^ freeness constraints
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder -> IO([Proof_status ProofTree])
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederconsCheck thName tac@(Tactic_script tl) tm freedefs = case t_target tm of
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder Theory sig nSens -> let
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder saveTPTP = False
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder proverStateI = spassProverState sig (toNamedList nSens) freedefs
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder problem = showTPTPProblemM thName proverStateI []
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa simpleOptions = ""
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa extraOptions = "-pc true -pmtptp true -fd true -to "
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa saveFileName = reverse $ fst $ span (/= '/') $ reverse thName
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa runDarwinRealM :: IO([Proof_status ProofTree])
b87fb5d6d5aba8fc6d3c528f7da0af228ca76b02Eugen Kuksa runDarwinRealM = do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder probl <- problem
8723ec450f2e7a024230467c0c28a3f154905483cmaeder hasProgramm <- system ("which darwin > /dev/null 2> /dev/null")
7b21830970250ca6369b0ae60f34c990f9a5c5bfTill Mossakowski case hasProgramm of
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski ExitFailure _ -> do
83ce5f14d356cd62e98f4f674da7f11ea1869eb0Till Mossakowski infoDialog "Darwin prover" "Darwin not found"
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski return [Proof_status
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski { goalName = thName
8723ec450f2e7a024230467c0c28a3f154905483cmaeder , goalStatus = openGoalStatus
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa , usedAxioms = getAxioms
8723ec450f2e7a024230467c0c28a3f154905483cmaeder , proverName = prover_name darwinProver
8723ec450f2e7a024230467c0c28a3f154905483cmaeder , proofTree = ProofTree "Darwin not found"
d3d8d20d41aaaa107cf2dfa4dd0434e6a08b22d5Till Mossakowski , usedTime = timeToTimeOfDay $ secondsToDiffTime 0
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , tacticScript = tac }]
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder ExitSuccess -> do
31a81edf1285dc338211bfe86ba50a1f4128d9d2Christian Maeder when saveTPTP $ writeFile (saveFileName ++ ".tptp") probl
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder t <- getCurrentTime
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder let timeTmpFile = "/tmp/" ++ saveFileName ++ show (utctDay t)
5d3978bb76c33d08d6297f69f10bbc04721ee3a5cmaeder ++ "-" ++ show (utctDayTime t) ++ ".tptp"
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder writeFile timeTmpFile probl
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder let command = "darwin " ++ extraOptions ++ " " ++ timeTmpFile
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder (_, outh, errh, proch) <- runInteractiveCommand command
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder (exCode, output, tUsed) <- parseDarwinOut outh errh proch
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder let outState = proof_statM exCode simpleOptions output tUsed
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder return [outState]
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder proof_statM :: ExitCode -> String -> [String] -> Int
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder -> Proof_status ProofTree
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder proof_statM exitCode _ out tUsed = let
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder outState = Proof_status
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder { goalName = thName
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder , goalStatus = Proved (Just True)
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder , usedAxioms = getAxioms
293abe6af19382a456dbe612aef45054ef76832fcmaeder , proverName = prover_name darwinProver
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder , proofTree = ProofTree (unlines out)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder , usedTime = timeToTimeOfDay $ secondsToDiffTime
7b21830970250ca6369b0ae60f34c990f9a5c5bfTill Mossakowski $ toInteger tUsed
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski , tacticScript = tac }
8e3e7896a1818bb0521674cf4f10403e9f9911b3Till Mossakowski in case exitCode of
e5f71ad96ddbaafd3bf8ae0820df93e0db4b0527cmaeder ExitSuccess -> outState
8723ec450f2e7a024230467c0c28a3f154905483cmaeder ExitFailure i -> outState
1f0483f71bad0707f10293d0b4db4649aa93fb35Christian Maeder { goalStatus = if elem i [2, 105, 112]
8723ec450f2e7a024230467c0c28a3f154905483cmaeder then Open $ Reason [show exitCode]
8723ec450f2e7a024230467c0c28a3f154905483cmaeder else Disproved }
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder getAxioms = let
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder fl = formulaLists $ initialLogicalPart proverStateI
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder fs = concatMap formulae $ filter isAxiomFormula fl
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder in runDarwinRealM
232c13ff6847a6f2bac7163392f80ab692cd7774Christian MaederrunDarwin :: SoftFOLProverState
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder -- ^ logical part containing the input Sign and axioms and possibly
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder -- goals that have been proved earlier as additional axioms
5d93620c37abd9c665d3fe532d4852d62dff4233Christian Maeder -> GenericConfig ProofTree -- ^ configuration to use
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder -> Bool -- ^ True means save TPTP file
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder -> String -- ^ name of the theory in the DevGraph
26acf851cacd7a31bdc9b25a42af9949942fa7c6Christian Maeder -> AS_Anno.Named SPTerm -- ^ goal to prove
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder -> IO (ATPRetval, GenericConfig ProofTree)
c5b8b64377e24bcbf5cc108ca433cfbbd6235ba1Christian Maeder -- ^ (retval, configuration with proof status and complete output)
6f9d360a425bdae3bd15289388e64c14a85eca43cmaederrunDarwin sps cfg saveTPTP thName nGoal = do
99b26e2ab8ba89bc9a050c1524137eb6269e2753Christian Maeder -- putStrLn ("running Darwin...")
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder runDarwinReal
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder simpleOptions = extraOpts cfg
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa extraOptions = maybe "-pc false"
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder ( \ tl -> "-pc false" ++ " -to " ++ show tl) $ timeLimit cfg
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder saveFileName = thName++'_':AS_Anno.senAttr nGoal
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder tmpFileName = (reverse $ fst $ span (/='/') $ reverse thName) ++
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder -- tLimit = maybe (guiDefaultTimeLimit) id $ timeLimit cfg
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder runDarwinReal = do
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder hasProgramm <- system ("which darwin > /dev/null 2> /dev/null")
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder case hasProgramm of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder ExitFailure _ -> return
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa (ATPError "Could not start Darwin. Is Darwin in your $PATH?",
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa emptyConfig (prover_name darwinProver)
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaeder (AS_Anno.senAttr nGoal) emptyProofTree)
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa ExitSuccess -> do
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa prob <- showTPTPProblem thName sps nGoal $
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa simpleOptions ++ ["Requested prover: Darwin"]
df24d7f0c79862ffd8189698645e201bf07a4d9cEugen Kuksa when saveTPTP
feb9227bb5c49d5bea1a112500c3b3eba31abdfbcmaeder (writeFile (saveFileName ++".tptp") prob)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder t <- getCurrentTime
6f9d360a425bdae3bd15289388e64c14a85eca43cmaeder let timeTmpFile = "/tmp/" ++ tmpFileName ++ (show $ utctDay t) ++
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder "-" ++ (show $ utctDayTime t) ++ ".tptp"
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa writeFile timeTmpFile prob
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa let command = "darwin " ++ extraOptions ++ " " ++ timeTmpFile
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa -- putStrLn command
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (_, outh, errh, proch) <- runInteractiveCommand command
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (exCode, output, tUsed) <- parseDarwinOut outh errh proch
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa let (err, retval) = proof_stat exCode simpleOptions output tUsed
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa return (err,
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa cfg{proof_status = retval,
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa resultOutput = output,
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa timeUsed = timeToTimeOfDay $
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa secondsToDiffTime $ toInteger tUsed})
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa proof_stat exitCode options out tUsed =
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa case exitCode of
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa ExitSuccess -> (ATPSuccess, proved_status options tUsed)
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa ExitFailure 2 -> (ATPError (unlines ("Internal error.":out)),
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa defaultProof_status options)
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa ExitFailure 112 ->
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa (ATPTLimitExceeded, defaultProof_status options)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa ExitFailure 105 ->
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa (ATPBatchStopped, defaultProof_status options)
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa ExitFailure _ ->
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa (ATPSuccess, disProved_status options)
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa defaultProof_status opts =
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (openProof_status
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa (AS_Anno.senAttr nGoal) (prover_name darwinProver) $
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa emptyProofTree)
dfa31ad230c88a66a9722c2a5ab23fe82c33f014Eugen Kuksa {tacticScript = Tactic_script $ show $ ATPTactic_script
e99cb5db53054d96bb97c9b8b130bd249802450eTill Mossakowski {ts_timeLimit = configTimeLimit cfg,
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa ts_extraOpts = opts} }
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa disProved_status opts = (defaultProof_status opts)
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa {goalStatus = Disproved}
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa proved_status opts ut = Proof_status
d16243f2fd4825f598eee589b68e324e23eb469dEugen Kuksa { goalName = AS_Anno.senAttr nGoal
d16243f2fd4825f598eee589b68e324e23eb469dEugen Kuksa , goalStatus = Proved (Just True)
d16243f2fd4825f598eee589b68e324e23eb469dEugen Kuksa , usedAxioms = getAxioms -- []
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa , proverName = prover_name darwinProver
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa , proofTree = emptyProofTree
ab38e2fac740c4336afafbe0584053dc2e67002bEugen Kuksa , usedTime = timeToTimeOfDay $ secondsToDiffTime $ toInteger ut
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa , tacticScript = Tactic_script $ show $ ATPTactic_script
728bd6bf3eb21b95a5e83db746a3c6ab5e8a6de1Eugen Kuksa { ts_timeLimit = configTimeLimit cfg, ts_extraOpts = opts }}
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa getAxioms = let
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa fl = formulaLists $ initialLogicalPart sps
64f5f0a8c38d5b2ba33b09e02e92b0e3f812d6d0Eugen Kuksa fs = concatMap formulae $ filter isAxiomFormula fl
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederisAxiomFormula :: SPFormulaList -> Bool
6f9d360a425bdae3bd15289388e64c14a85eca43cmaederisAxiomFormula fl =
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder case originType fl of
8723ec450f2e7a024230467c0c28a3f154905483cmaeder SPOriginAxioms -> True
8723ec450f2e7a024230467c0c28a3f154905483cmaederparseDarwinOut :: Handle -- ^ handel of stdout
8723ec450f2e7a024230467c0c28a3f154905483cmaeder -> Handle -- ^ handel of stderr
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht -> ProcessHandle -- ^ handel of process
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder -> IO (ExitCode, [String], Int)
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht -- ^ (exit code, complete output, used time)
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon UlbrichtparseDarwinOut outh _ procHndl = do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder --darwin does not write to stderr here, so ignore output
8723ec450f2e7a024230467c0c28a3f154905483cmaeder --err <- hGetLine errh
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht --if null err then
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa readLineAndParse (ExitFailure 1, [], -1) False
8723ec450f2e7a024230467c0c28a3f154905483cmaeder readLineAndParse (exCode, output, to) stateFound = do
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder procState <- isProcessRun
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder case procState of
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht ExitSuccess -> do
8723ec450f2e7a024230467c0c28a3f154905483cmaeder iseof <- hIsEOF outh
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht if iseof then
233754e153e665aa748bf8b45bd8b1938b6c21a7Christian Maeder do -- ec <- isProcessRun proc
8723ec450f2e7a024230467c0c28a3f154905483cmaeder waitForProcess procHndl
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht return (exCode, reverse output, to)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht line <- hGetLine outh
8723ec450f2e7a024230467c0c28a3f154905483cmaeder if "Couldn't find eprover" `isPrefixOf` line
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht waitForProcess procHndl
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht return (ExitFailure 2, line : output, to)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder else if "Try darwin -h for further information" `isPrefixOf` line
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder -- error by running darwin.
8723ec450f2e7a024230467c0c28a3f154905483cmaeder waitForProcess procHndl
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder return (ExitFailure 2, line : output, to)
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht else if "SZS status" `isPrefixOf` line && not stateFound
8723ec450f2e7a024230467c0c28a3f154905483cmaeder then let state' = words line !! 2 in
8723ec450f2e7a024230467c0c28a3f154905483cmaeder readLineAndParse (checkSZSState state', line : output, to)
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder else if "CPU Time" `isPrefixOf` line -- get cup time
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht then let time = case takeWhile isDigit $ last (words line) of
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht ds@(_ : _) -> read ds
8723ec450f2e7a024230467c0c28a3f154905483cmaeder in readLineAndParse (exCode, line : output, time)
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht else readLineAndParse (exCode, line : output, to)
8723ec450f2e7a024230467c0c28a3f154905483cmaeder failure -> do
de8983abdf4b35af1ed1fdee2de4dff13c2368bacmaeder waitForProcess procHndl
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht return (failure, output, to)
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder checkSZSState szsState =
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht (\ i -> if i == 0 then ExitSuccess else ExitFailure i) $
12882fa70d12d9b56cbd850ccb4b724feb3c62d5Christian Maeder case szsState of
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht "Unsolved" -> 101
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht "Open" -> 102
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht "Unknown" -> 103
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht "Assumed" -> 104
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht "Stopped" -> 105
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht "Error" -> 106
ccd9cf19d129595770d592d3d0d80c6619f7a141Eugen Kuksa "InputError" -> 107
465c6b72e8e480969b5f08658e394992bcc08bfcSimon Ulbricht "OSError" -> 108
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht "Forced" -> 109
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht "User" -> 110
0a46a4d711eca869ad75b4df84dabd72783ebdd2Simon Ulbricht "ResourceOut" -> 111
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa "Timeout" -> 112
d35249e8b76e34d3cbb6adf7d89e9111226a49d6Eugen Kuksa "MemoryOut" -> 113
0b144823976d79a34bff62f7f9ec032e80b8ce85Simon Ulbricht "Gaveup" -> 114
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa "Incomplete" -> 115
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa "Inappropriate" -> 116
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa "NotTested" -> 117
4f820114168836fb05b720c429866baa5665690eChristian Maeder "NotTestedYet" -> 118
4bd27a2cb9efd5d8ff00b5cf823487403add724ecmaeder "CounterSatisfiable" -> 119
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa "CounterTheorem" -> 120
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht "CounterEquivalent" -> 121
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa "WeakerCounterTheorem" -> 122
4937a0e373f619dc520799923acec42db5da5eb3Eugen Kuksa "UnsatisfiableConclusion" -> 123
1698621aea64f7a2b04a4084984eed1437e22771Christian Maeder "EquivalentCounterTheorem" -> 124
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder "Unsatisfiable" -> 125
1d65a799298f6b1253d774c22f61029e6eb99cadcmaeder "SatisfiableCounterConclusionContradictoryAxioms" -> 126
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder "UnsatisfiableConclusionContradictoryAxioms" -> 127
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder "NoConsequence" -> 128
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder "CounterSatisfiabilityPreserving" -> 129
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder "CounterSatisfiabilityPartialMapping" -> 130
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder "CounterSatisfiabilityMapping" -> 131
6fb590a3747600c145abfd7c3483039fb03af032Christian Maeder "CounterSatisfiabilityBijection" -> 132
1ab66a7e4234c760be9689b05ab4c34ce99dba23Simon Ulbricht -- check if darwin running
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder isProcessRun = do
986888e7f4d8ed681272a79c63f329ce8037063dcmaeder exitcode <- getProcessExitCode procHndl
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder case exitcode of
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder Nothing -> return ExitSuccess
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder Just (ExitFailure i) -> return (ExitFailure i)
fcd8dd6d9029180ae5e777e94a973c5e355a55cfcmaeder Just ExitSuccess -> return ExitSuccess