b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett{- |

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettModule : ./SoftFOL/ProveVampire.hs

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettDescription : Interface to the Vampire theorem prover via MathServe.

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettCopyright : (c) Rene Wagner, Klaus Luettich, Rainer Grabbe,

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett Uni Bremen 2005-2006

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettLicense : GPLv2 or higher, see LICENSE.txt

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettMaintainer : Christian.Maeder@dfki.de

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettStability : provisional

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy GimblettPortability : needs POSIX

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

b95c5b557aadc2211867af804d39950d4c9c1444Andy GimblettInterface for the Vampire service, uses GUI.GenericATP.

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy GimblettSee <http://spass.mpi-sb.mpg.de/> for details on SPASS.

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett-}

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettmodule SoftFOL.ProveVampire (vampire, vampireCMDLautomaticBatch) where

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport Logic.Prover

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport SoftFOL.Sign

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport SoftFOL.Translate

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport SoftFOL.MathServMapping

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport SoftFOL.MathServParsing

d64c27888613a81c9634cd939dd05618175465efAndy Gimblettimport SoftFOL.ProverState

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

d64c27888613a81c9634cd939dd05618175465efAndy Gimblettimport qualified Common.AS_Annotation as AS_Anno

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport qualified Common.Result as Result

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblettimport Common.ProofTree

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblettimport Control.Monad (when)

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblettimport qualified Control.Concurrent as Concurrent

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport qualified Control.Exception as Exception

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport GUI.GenericATP

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport Interfaces.GenericATPState

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettimport Proofs.BatchProcessing

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett-- * Prover implementation

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett

b95c5b557aadc2211867af804d39950d4c9c1444Andy Gimblett{- |

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett The Prover implementation. First runs the batch prover (with graphical

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett feedback), then starts the GUI prover.

c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett-}

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblettvampire :: Prover Sign Sentence SoftFOLMorphism () ProofTree

19ef749a762ef2c09579549715a63b364f0395d5Andy Gimblettvampire = (mkProverTemplate "Vampire" () vampireGUI)

29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett { proveCMDLautomaticBatch = Just vampireCMDLautomaticBatch }

29ac9ecacf0983a565b89f133ff2bdf2ac02b0c4Andy Gimblett

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy GimblettvampireHelpText :: String

vampireHelpText =

"No help yet available.\n" ++

"email hets-devel@informatik.uni-bremen.de " ++

"for more information.\n"

-- * Main prover functions

-- ** Utility functions

{- |

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

line interface.

-}

atpFun :: String -- ^ theory name

-> ATPFunctions Sign Sentence SoftFOLMorphism ProofTree SoftFOLProverState

atpFun thName = ATPFunctions

{ initialProverState = spassProverState,

atpTransSenName = transSenName,

atpInsertSentence = insertSentenceGen,

goalOutput = showTPTPProblem thName,

proverHelpText = vampireHelpText,

batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",

fileExtensions = FileExtensions {problemOutput = ".tptp",

proverOutput = ".vamp",

theoryConfiguration = ".spcf"},

runProver = runVampire,

createProverOptions = extraOpts}

-- ** GUI

{- |

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

data type ATPFunctions.

-}

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

vampireGUI thName th freedefs =

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

freedefs emptyProofTree

-- ** command line function

{- |

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

automatic command line interface to the Vampire prover via MathServe.

Vampire specific functions are omitted by data type ATPFunctions.

-}

vampireCMDLautomaticBatch ::

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 -}

vampireCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar

thName defTS th freedefs =

genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch

resultMVar (proverName vampire) thName

(parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree

{- |

Runs the Vampire service.

-}

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

runVampire sps cfg saveTPTP thName nGoal =

Exception.catch (do

prob <- showTPTPProblem thName sps nGoal $ extraOpts cfg ++

["Requested prover: Vampire"]

when saveTPTP

(writeFile (thName ++ '_' : AS_Anno.senAttr nGoal ++ ".tptp") prob)

mathServOut <- callMathServ

MathServCall { mathServService = VampireService,

mathServOperation = TPTPProblem,

problem = prob,

proverTimeLimit = configTimeLimit cfg,

extraOptions = Just $ unwords $ extraOpts cfg}

msResponse <- parseMathServOut mathServOut

return (mapMathServResponse (getAxioms sps) msResponse cfg nGoal

$ proverName vampire))

$ excepToATPResult (proverName vampire) $ AS_Anno.senAttr nGoal