Changeset 12778

Timestamp:

03.11.2009 17:54:03 (3 weeks ago)

Author:

maeder

Message:

refactored consistency checker interface

Location:

trunk

Files:

• Isabelle/IsaProve.hs (modified) (1 diff)
• Logic/Prover.hs (modified) (2 diffs)
• OWL/ProvePellet.hs (modified) (1 diff)
• Propositional/Prove.hs (modified) (1 diff)
• Propositional/ProveMinisat.hs (modified) (1 diff)
• Propositional/ProveWithTruthTable.hs (modified) (1 diff)
• SoftFOL/ProveDarwin.hs (modified) (1 diff)

trunk/Isabelle/IsaProve.hs

@@ -58 +58 @@
 
 isabelleConsChecker :: ConsChecker Sign Sentence () (DefaultMorphism Sign) ()
-isabelleConsChecker = ConsChecker "Isabelle-refute" () consCheck
+isabelleConsChecker = (mkConsChecker "Isabelle-refute" () consCheck)
+  { ccBatch = False }
 
 -- | the name of the inconsistent lemma for consistency checks

trunk/Logic/Prover.hs

@@ -326 +326 @@
   { ccName :: String
   , ccSublogic :: sublogics
+  , ccBatch :: Bool -- True for batch checkers
+  , ccNeedsTimer :: Bool -- True for checkers that ignore time limits
   , ccAutomatic :: String -- 1.
                  -> TacticScript  -- 2.
@@ -338 +340 @@
   } deriving Typeable
 
+mkConsChecker :: String -> sublogics
+  -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree
+      -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree))
+  -> ConsChecker sign sentence sublogics morphism proof_tree
+mkConsChecker n sl f = ConsChecker
+  { ccName = n
+  , ccSublogic = sl
+  , ccBatch = True
+  , ccNeedsTimer = True
+  , ccAutomatic = f }

trunk/OWL/ProvePellet.hs

@@ -88 +88 @@
 
 pelletConsChecker :: ConsChecker Sign Axiom OWLSub OWLMorphism ProofTree
-pelletConsChecker = ConsChecker "Pellet" sl_top consCheck
+pelletConsChecker = (mkConsChecker "Pellet" sl_top consCheck)
+  { ccNeedsTimer = False }
+
 
 {- |

trunk/Propositional/Prove.hs

@@ -82 +82 @@
 propConsChecker :: LP.ConsChecker Sig.Sign AS_BASIC.FORMULA PropSL
                                   PMorphism.Morphism ProofTree
-propConsChecker = LP.ConsChecker zchaffS top consCheck
+propConsChecker = LP.mkConsChecker zchaffS top consCheck
 
 consCheck :: String -> LP.TacticScript

trunk/Propositional/ProveMinisat.hs

@@ -79 +79 @@
 minisatConsChecker :: LP.ConsChecker Sig.Sign AS_BASIC.FORMULA PropSL
   PMorphism.Morphism ProofTree
-minisatConsChecker = LP.ConsChecker minisatS top consCheck
+minisatConsChecker = LP.mkConsChecker minisatS top consCheck
 
 consCheck :: String -> LP.TacticScript

trunk/Propositional/ProveWithTruthTable.hs

@@ -241 +241 @@
 ttConsistencyChecker :: LP.ConsChecker Sig.Sign FORMULA PropSL
                                   PMorphism.Morphism ProofTree
-ttConsistencyChecker = LP.ConsChecker ttS top consCheck
+ttConsistencyChecker = LP.mkConsChecker ttS top consCheck
 
 consCheck :: String -> LP.TacticScript

trunk/SoftFOL/ProveDarwin.hs

@@ -60 +60 @@
 
 darwinConsChecker :: ConsChecker Sign Sentence () SoftFOLMorphism ProofTree
-darwinConsChecker = ConsChecker "darwin" () consCheck
+darwinConsChecker = (mkConsChecker "darwin" () consCheck)
+  { ccNeedsTimer = False }
 
 {- |