842ae4bd224140319ae7feec1872b93dfd491143fielding{- |

842ae4bd224140319ae7feec1872b93dfd491143fieldingModule : $Header$

842ae4bd224140319ae7feec1872b93dfd491143fieldingDescription : Interface to the TPTP theorem prover via Darwin.

842ae4bd224140319ae7feec1872b93dfd491143fieldingCopyright : (c) Heng Jiang, Uni Bremen 2004-2007

842ae4bd224140319ae7feec1872b93dfd491143fieldingLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

842ae4bd224140319ae7feec1872b93dfd491143fieldingMaintainer : jiang@informatik.uni-bremen.de

7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffieldingStability : provisional

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndPortability : needs POSIX

7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndInterface for the Darwin service, uses GUI.GenericATP.

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndSee <http://spass.mpi-sb.mpg.de/> for details on SPASS, and

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd<http://combination.cs.uiowa.edu/Darwin/> for Darwin.

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd-}

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd

7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffieldingmodule SoftFOL.ProveDarwin

7e79e8fd53348f9fc6e8009a4a2522425ab6f08ffielding ( darwinProver

92ae63a7151376cfb024555195deb4860af1a90afuankg , darwinCMDLautomaticBatch

92ae63a7151376cfb024555195deb4860af1a90afuankg , darwinConsChecker

92ae63a7151376cfb024555195deb4860af1a90afuankg ) where

92ae63a7151376cfb024555195deb4860af1a90afuankg

92ae63a7151376cfb024555195deb4860af1a90afuankg-- preliminary hacks for display of CASL models

92ae63a7151376cfb024555195deb4860af1a90afuankgimport Logic.Prover

92ae63a7151376cfb024555195deb4860af1a90afuankg

92ae63a7151376cfb024555195deb4860af1a90afuankgimport SoftFOL.Sign

92ae63a7151376cfb024555195deb4860af1a90afuankgimport SoftFOL.Translate

92ae63a7151376cfb024555195deb4860af1a90afuankgimport SoftFOL.ProverState

92ae63a7151376cfb024555195deb4860af1a90afuankg

92ae63a7151376cfb024555195deb4860af1a90afuankgimport Common.AS_Annotation as AS_Anno

cccd31fa4a72fe23cc3249c06db181b274a55a69gsteinimport qualified Common.Result as Result

cccd31fa4a72fe23cc3249c06db181b274a55a69gsteinimport Common.ProofTree

cccd31fa4a72fe23cc3249c06db181b274a55a69gsteinimport Common.ProverTools

92ae63a7151376cfb024555195deb4860af1a90afuankg

92ae63a7151376cfb024555195deb4860af1a90afuankgimport Data.Char (isDigit)

a50ebe9ca7a0a8e3e9b3f0abd3b9ef55b8dc36c5fuankgimport Data.List (isPrefixOf)

a50ebe9ca7a0a8e3e9b3f0abd3b9ef55b8dc36c5fuankgimport Data.Time (timeToTimeOfDay)

92ae63a7151376cfb024555195deb4860af1a90afuankgimport Data.Time.Clock (UTCTime(..), secondsToDiffTime, getCurrentTime)

92ae63a7151376cfb024555195deb4860af1a90afuankg

cccd31fa4a72fe23cc3249c06db181b274a55a69gsteinimport Control.Monad (when)

cccd31fa4a72fe23cc3249c06db181b274a55a69gsteinimport qualified Control.Concurrent as Concurrent

cccd31fa4a72fe23cc3249c06db181b274a55a69gstein

14262dee6334e2315a7293c40c3d7b20d62e838btrawickimport System.Exit

14262dee6334e2315a7293c40c3d7b20d62e838btrawickimport System.IO

14262dee6334e2315a7293c40c3d7b20d62e838btrawickimport System.Process

cccd31fa4a72fe23cc3249c06db181b274a55a69gstein

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingimport GUI.GenericATP

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingimport Interfaces.GenericATPState

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingimport GUI.Utils (infoDialog)

2261031aa94be82d7e6b1b8c367afc1b282317f5ianhimport Proofs.BatchProcessing

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh-- * Prover implementation

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh

3de8d8649277a02f53aa4f06121420985e8eee08nd{- | The Prover implementation. First runs the batch prover (with

10db6c4117794cbb76695f8b81b02a82bcf986e1ben graphical feedback), then starts the GUI prover. -}

81cc440ca73845f44dc589db106d3feb7a36f33bminfrindarwinProver :: Prover Sign Sentence SoftFOLMorphism () ProofTree

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingdarwinProver = mkAutomaticProver "Darwin" () darwinGUI darwinCMDLautomaticBatch

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingdarwinConsChecker :: ConsChecker Sign Sentence () SoftFOLMorphism ProofTree

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fieldingdarwinConsChecker = (mkConsChecker "darwin" () consCheck)

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding { ccNeedsTimer = False }

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh{- |

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh Record for prover specific functions. This is used by both GUI and command

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh line interface.

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh-}

2261031aa94be82d7e6b1b8c367afc1b282317f5ianhatpFun :: String -- ^ theory name

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh -> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState

3de8d8649277a02f53aa4f06121420985e8eee08ndatpFun thName = ATPFunctions

10db6c4117794cbb76695f8b81b02a82bcf986e1ben { initialProverState = spassProverState

81cc440ca73845f44dc589db106d3feb7a36f33bminfrin , atpTransSenName = transSenName

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh , atpInsertSentence = insertSentenceGen

8b64441666c2d3894744886fc5eda2e9ee15605eben , goalOutput = showTPTPProblem thName

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh , proverHelpText = "no help for darwin available"

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh , batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT"

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh , fileExtensions = FileExtensions

3de8d8649277a02f53aa4f06121420985e8eee08nd { problemOutput = ".tptp"

10db6c4117794cbb76695f8b81b02a82bcf986e1ben , proverOutput = ".spass"

81cc440ca73845f44dc589db106d3feb7a36f33bminfrin , theoryConfiguration = ".spcf" }

81cc440ca73845f44dc589db106d3feb7a36f33bminfrin , runProver = runDarwin

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding , createProverOptions = extraOpts }

8b64441666c2d3894744886fc5eda2e9ee15605eben

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh-- ** GUI

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh{- |

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding Invokes the generic prover GUI. SPASS specific functions are omitted by

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh data type ATPFunctions.

36e56bad6e9dff97dce981cd7543e81d814b5e35fuankg-}

4a13940dc2990df0a798718d3a3f9cf1566c2217bjhdarwinGUI :: String -- ^ theory name

8b9a4881f960811c0804bd11e13f7341be5bace8wrowe -> Theory Sign Sentence ProofTree

8b9a4881f960811c0804bd11e13f7341be5bace8wrowe -- ^ theory consisting of a SoftFOL.Sign.Sign

4a13940dc2990df0a798718d3a3f9cf1566c2217bjh -- and a list of Named SoftFOL.Sign.Sentence

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

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

4a13940dc2990df0a798718d3a3f9cf1566c2217bjhdarwinGUI thName th freedefs =

85c4a4d5ba3751702855fd9b1a78daed874941dcwrowe genericATPgui (atpFun thName) True (proverName darwinProver) thName th

85c4a4d5ba3751702855fd9b1a78daed874941dcwrowe freedefs emptyProofTree

8b9a4881f960811c0804bd11e13f7341be5bace8wrowe

fdf0370f05f77efd6e8f7e888dc21afc1fc79cbfben-- ** command line function

85c4a4d5ba3751702855fd9b1a78daed874941dcwrowe

85c4a4d5ba3751702855fd9b1a78daed874941dcwrowe{- |

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

fdf0370f05f77efd6e8f7e888dc21afc1fc79cbfben automatic command line interface to the Darwin prover via MathServe.

85c4a4d5ba3751702855fd9b1a78daed874941dcwrowe Darwin specific functions are omitted by data type ATPFunctions.

85c4a4d5ba3751702855fd9b1a78daed874941dcwrowe-}

8b9a4881f960811c0804bd11e13f7341be5bace8wrowedarwinCMDLautomaticBatch ::

8b9a4881f960811c0804bd11e13f7341be5bace8wrowe Bool -- ^ True means include proved theorems

85c4a4d5ba3751702855fd9b1a78daed874941dcwrowe -> Bool -- ^ True means save problem file

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

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

85c4a4d5ba3751702855fd9b1a78daed874941dcwrowe -> String -- ^ theory name

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh -> TacticScript -- ^ default tactic script

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh -> Theory Sign Sentence ProofTree -- ^ theory consisting of a

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh -- 'SoftFOL.Sign.Sign' and a list of Named 'SoftFOL.Sign.Sentence'

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

81cc440ca73845f44dc589db106d3feb7a36f33bminfrin -> IO (Concurrent.ThreadId,Concurrent.MVar ())

81cc440ca73845f44dc589db106d3feb7a36f33bminfrin -- ^ fst: identifier of the batch thread for killing it

81cc440ca73845f44dc589db106d3feb7a36f33bminfrin -- snd: MVar to wait for the end of the thread

81cc440ca73845f44dc589db106d3feb7a36f33bminfrindarwinCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar

c7b8ebf28db0c79631ddcc97aaf7ea7d3e029d2ffielding thName defTS th freedefs =

c7b8ebf28db0c79631ddcc97aaf7ea7d3e029d2ffielding genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh resultMVar (proverName darwinProver) thName

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh

3de8d8649277a02f53aa4f06121420985e8eee08nd-- * Main prover functions

3de8d8649277a02f53aa4f06121420985e8eee08nd{- |

3de8d8649277a02f53aa4f06121420985e8eee08nd Runs the Darwin service. The tactic script only contains a string for the

3de8d8649277a02f53aa4f06121420985e8eee08nd time limit.

3de8d8649277a02f53aa4f06121420985e8eee08nd-}

fdf0370f05f77efd6e8f7e888dc21afc1fc79cbfben

3de8d8649277a02f53aa4f06121420985e8eee08ndconsCheck :: String

3de8d8649277a02f53aa4f06121420985e8eee08nd -> TacticScript

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding -> TheoryMorphism Sign Sentence SoftFOLMorphism ProofTree

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

10db6c4117794cbb76695f8b81b02a82bcf986e1ben -> IO(CCStatus ProofTree)

10db6c4117794cbb76695f8b81b02a82bcf986e1benconsCheck thName (TacticScript tl) tm freedefs = case tTarget tm of

10db6c4117794cbb76695f8b81b02a82bcf986e1ben Theory sig nSens -> let

8b64441666c2d3894744886fc5eda2e9ee15605eben saveTPTP = False

10db6c4117794cbb76695f8b81b02a82bcf986e1ben proverStateI = spassProverState sig (toNamedList nSens) freedefs

10db6c4117794cbb76695f8b81b02a82bcf986e1ben problem = showTPTPProblemM thName proverStateI []

10db6c4117794cbb76695f8b81b02a82bcf986e1ben extraOptions = "-pc false -pmtptp true -fd true -to "

3de8d8649277a02f53aa4f06121420985e8eee08nd ++ tl

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding saveFileName = reverse $ fst $ span (/= '/') $ reverse thName

2261031aa94be82d7e6b1b8c367afc1b282317f5ianh runDarwinRealM :: IO(CCStatus ProofTree)

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding runDarwinRealM = do

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding probl <- problem

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding noProg <- missingExecutableInPath "darwin"

09fe0b69d3d1e8c8041c9ce99ee77b8b44b5e3b1fielding if noProg then do

infoDialog "Darwin prover" "Darwin not found"

return CCStatus

{ ccResult = Nothing

, ccProofTree = ProofTree "Darwin not found"

, ccUsedTime = timeToTimeOfDay $ secondsToDiffTime 0 }

else do

when saveTPTP $ writeFile (saveFileName ++ ".tptp") probl

t <- getCurrentTime

let timeTmpFile = "/tmp/" ++ saveFileName ++ show (utctDay t)

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

writeFile timeTmpFile probl

let command = "darwin " ++ extraOptions ++ " " ++ timeTmpFile

(_, outh, errh, proch) <- runInteractiveCommand command

(exCode, output, tUsed) <- parseDarwinOut outh errh proch

let outState = proofStatM exCode output tUsed

return outState

proofStatM :: ExitCode -> [String] -> Int -> CCStatus ProofTree

proofStatM exitCode out tUsed = let

outState = CCStatus

{ ccResult = Just True

, ccProofTree = ProofTree $ unlines $ show exitCode : out

, ccUsedTime = timeToTimeOfDay $ secondsToDiffTime

$ toInteger tUsed }

in case exitCode of

ExitSuccess -> outState

ExitFailure i -> outState

{ ccResult = if elem i [2, 105, 112]

then Nothing else Just False }

in runDarwinRealM

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

runDarwin sps cfg saveTPTP thName nGoal = do

-- putStrLn ("running Darwin...")

runDarwinReal

where

simpleOptions = extraOpts cfg

extraOptions = maybe "-pc false"

( \ tl -> "-pc false" ++ " -to " ++ show tl) $ timeLimit cfg

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

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

'_':AS_Anno.senAttr nGoal

-- tLimit = maybe (guiDefaultTimeLimit) id $ timeLimit cfg

runDarwinReal = do

noProg <- missingExecutableInPath "darwin"

if noProg then

return

(ATPError "Could not start Darwin. Is Darwin in your $PATH?",

emptyConfig (proverName darwinProver)

(AS_Anno.senAttr nGoal) emptyProofTree)

else do

prob <- showTPTPProblem thName sps nGoal $

simpleOptions ++ ["Requested prover: Darwin"]

when saveTPTP

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

t <- getCurrentTime

let timeTmpFile = "/tmp/" ++ tmpFileName ++ (show $ utctDay t) ++

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

writeFile timeTmpFile prob

let command = "darwin " ++ extraOptions ++ " " ++ timeTmpFile

-- putStrLn command

(_, outh, errh, proch) <- runInteractiveCommand command

(exCode, output, tUsed) <- parseDarwinOut outh errh proch

let (err, retval) = proofStat exCode simpleOptions output tUsed

return (err,

cfg{proofStatus = retval,

resultOutput = output,

timeUsed = timeToTimeOfDay $

secondsToDiffTime $ toInteger tUsed})

proofStat exitCode options out tUsed =

case exitCode of

ExitSuccess -> (ATPSuccess, provedStatus options tUsed)

ExitFailure 2 -> (ATPError (unlines ("Internal error.":out)),

defaultProofStatus options)

ExitFailure 112 ->

(ATPTLimitExceeded, defaultProofStatus options)

ExitFailure 105 ->

(ATPBatchStopped, defaultProofStatus options)

ExitFailure _ ->

(ATPSuccess, disProvedStatus options)

defaultProofStatus opts =

(openProofStatus

(AS_Anno.senAttr nGoal) (proverName darwinProver) $

emptyProofTree)

{tacticScript = TacticScript $ show $ ATPTacticScript

{tsTimeLimit = configTimeLimit cfg,

tsExtraOpts = opts} }

disProvedStatus opts = (defaultProofStatus opts)

{goalStatus = Disproved}

provedStatus opts ut = ProofStatus

{ goalName = AS_Anno.senAttr nGoal

, goalStatus = Proved True

, usedAxioms = getAxioms

, usedProver = proverName darwinProver

, proofTree = emptyProofTree

, usedTime = timeToTimeOfDay $ secondsToDiffTime $ toInteger ut

, tacticScript = TacticScript $ show $ ATPTacticScript

{ tsTimeLimit = configTimeLimit cfg, tsExtraOpts = opts }}

getAxioms = let

fl = formulaLists $ initialLogicalPart sps

fs = concatMap formulae $ filter isAxiomFormula fl

in map AS_Anno.senAttr fs

isAxiomFormula :: SPFormulaList -> Bool

isAxiomFormula fl =

case originType fl of

SPOriginAxioms -> True

_ -> False

parseDarwinOut :: Handle -- ^ handel of stdout

-> Handle -- ^ handel of stderr

-> ProcessHandle -- ^ handel of process

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

-- ^ (exit code, complete output, used time)

parseDarwinOut outh _ procHndl = do

--darwin does not write to stderr here, so ignore output

--err <- hGetLine errh

--if null err then

readLineAndParse (ExitFailure 1, [], -1) False

where

readLineAndParse (exCode, output, to) stateFound = do

procState <- isProcessRun

case procState of

ExitSuccess -> do

iseof <- hIsEOF outh

if iseof then

do -- ec <- isProcessRun proc

waitForProcess procHndl

return (exCode, reverse output, to)

else do

line <- hGetLine outh

if "Couldn't find eprover" `isPrefixOf` line

then do

waitForProcess procHndl

return (ExitFailure 2, line : output, to)

else if "Try darwin -h for further information" `isPrefixOf` line

-- error by running darwin.

then do

waitForProcess procHndl

return (ExitFailure 2, line : output, to)

else if "SZS status" `isPrefixOf` line && not stateFound

then let state' = words line !! 2 in

readLineAndParse (checkSZSState state', line : output, to)

True

else if "CPU Time" `isPrefixOf` line -- get cup time

then let time = case takeWhile isDigit $ last (words line) of

ds@(_ : _) -> read ds

_ -> to

in readLineAndParse (exCode, line : output, time)

stateFound

else readLineAndParse (exCode, line : output, to)

stateFound

failure -> do

waitForProcess procHndl

return (failure, output, to)

checkSZSState szsState =

(\ i -> if i == 0 then ExitSuccess else ExitFailure i) $

case szsState of

"Unsolved" -> 101

"Open" -> 102

"Unknown" -> 103

"Assumed" -> 104

"Stopped" -> 105

"Error" -> 106

"InputError" -> 107

"OSError" -> 108

"Forced" -> 109

"User" -> 110

"ResourceOut" -> 111

"Timeout" -> 112

"MemoryOut" -> 113

"Gaveup" -> 114

"Incomplete" -> 115

"Inappropriate" -> 116

"NotTested" -> 117

"NotTestedYet" -> 118

"CounterSatisfiable" -> 119

"CounterTheorem" -> 120

"CounterEquivalent" -> 121

"WeakerCounterTheorem" -> 122

"UnsatisfiableConclusion" -> 123

"EquivalentCounterTheorem" -> 124

"Unsatisfiable" -> 125

"SatisfiableCounterConclusionContradictoryAxioms" -> 126

"UnsatisfiableConclusionContradictoryAxioms" -> 127

"NoConsequence" -> 128

"CounterSatisfiabilityPreserving" -> 129

"CounterSatisfiabilityPartialMapping" -> 130

"CounterSatisfiabilityMapping" -> 131

"CounterSatisfiabilityBijection" -> 132

_ -> 0

-- check if darwin running

isProcessRun = do

exitcode <- getProcessExitCode procHndl

case exitcode of

Nothing -> return ExitSuccess

Just (ExitFailure i) -> return (ExitFailure i)

Just ExitSuccess -> return ExitSuccess