05bf9cbe382548c2665dd01a6a402640c9ec3813Christian Maeder{-# LANGUAGE FlexibleInstances #-}
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiDescription : QuickCheck model checker for CASL.CFOL
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiMaintainer : till@informatik.uni-bremen.de
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiStability : provisional
44f39faa8e6beccd718e09cb41a6bd667db14be7Christian MaederPortability : non-portable (via GUI imports, FlexibleInstances)
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiQuickCheck model checker for CASL.CFOL.
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiInitially, only finite enumeration domains are supported
1bd72434378dac9262c5af0f204e87c674998d71Christian Maedermodule CASL.QuickCheck (quickCheckProver) where
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowskiimport qualified Common.AS_Annotation as AS_Anno
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowskiimport qualified Common.Result as Result
a81a6e924a0a027f48823b0a09cf51ad807c2e5bChristian Maederimport Common.Utils (timeoutSecs)
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowskiimport qualified Data.Map as Map
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski-- a qmodel is a certain term model used by QuickCheck
56c56b2181e76c239929ddade2925ba5c3f3fffdChristian Maederdata QModel = QModel
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer { sign :: CASLSign
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer -- sentences determining the set of terms for a sort
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , carrierSens :: Map.Map SORT [CASLFORMULA]
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer -- definitions of predicates and operations
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , predDefs :: Map.Map PRED_SYMB [([CASLTERM], CASLFORMULA)]
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , opDefs :: Map.Map OP_SYMB [([CASLTERM], CASLTERM)]
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer -- currently evaluated items, for avoiding infinite recursion
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , evaluatedPreds :: [(PRED_SYMB, [CASLTERM])]
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , evaluatedOps :: [(OP_SYMB, [CASLTERM])]
5708367a1e4f8c55364c82495262bcd7ad406d8bChristian Maeder } deriving Show
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Run the QuickCheck service.
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskirunQuickCheck :: QModel
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder {- ^ logical part containing the input Sign and axioms and possibly
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder goals that have been proved earlier as additional axioms -}
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder -> GenericConfig ProofTree -- ^ configuration to use
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -> Bool -- ^ True means save theory file
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -> String -- ^ name of the theory in the DevGraph
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -> AS_Anno.Named CASLFORMULA -- ^ goal to prove
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder -> IO (ATPRetval, GenericConfig ProofTree)
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- ^ (retval, configuration with proof status and complete output)
0c69f08a7017e47517265f974ed045f5b4134b02Till MossakowskirunQuickCheck qm cfg _saveFile _thName nGoal = do
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder (stat, Result d res) <- case timeLimit cfg of
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer Nothing -> return (ATPSuccess, quickCheck qm nGoal)
a81a6e924a0a027f48823b0a09cf51ad807c2e5bChristian Maeder mRes <- timeoutSecs t $ return $ quickCheck qm nGoal
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder return $ maybe (ATPTLimitExceeded, fail "time limit exceeded")
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder (\ x -> (ATPSuccess, x)) mRes
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder let fstr = show (printTheoryFormula $ AS_Anno.mapNamed
b983a1c05057154ba9839cc8034c41871598c7f9Christian Maeder (simplifyCASLSen $ sign qm) nGoal)
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer showDiagStrings = intercalate "\n" . map diagString -- no final newline
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder diagstr = case (res, d) of
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder (Just True, _) -> showDiagStrings (take 10 d)
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer _ -> unlines ["Formula failed: ", fstr, " some Counterexamples: "]
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder ++ showDiagStrings (take 10 d)
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer gstat = case res of
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer Just True -> Proved True
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer Just False -> Disproved
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer Nothing -> openGoalStatus
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer setStatus pstat = pstat { goalStatus = gstat
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , usedProver = "QuickCheck"
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , proofTree = ProofTree diagstr }
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer cfg' = cfg { proofStatus = setStatus (proofStatus cfg)
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , resultOutput = [diagstr] }
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer return (stat, cfg')
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer -- return ATPError if time is up???
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski-- | initial QModel
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskimakeQm :: CASLSign -> QModel
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo WiedemeyermakeQm sig = QModel { sign = sig
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , carrierSens = Map.empty
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , evaluatedPreds = []
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer , evaluatedOps = []
0c69f08a7017e47517265f974ed045f5b4134b02Till MossakowskiinsertSens :: QModel -> [AS_Anno.Named CASLFORMULA] -> QModel
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiinsertSens = foldl insertSen
1f6c89020cf4aff3421850b9f422523b1d542fb8Christian Maeder-- | insert sentences into a QModel
1f6c89020cf4aff3421850b9f422523b1d542fb8Christian MaederinsertSen :: QModel -> AS_Anno.Named CASLFORMULA -> QModel
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo WiedemeyerinsertSen qm sen = if not $ AS_Anno.isAxiom sen then qm else
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski qm1 = case f of
4da70bec38acda1694ac5e854fd7aff20425c208Till Mossakowski -- sort generation constraint?
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski Sort_gen_ax cs _ ->
1f6c89020cf4aff3421850b9f422523b1d542fb8Christian Maeder let s = map (\ c -> (newSort c, [f])) cs
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski ins = foldr $ uncurry $ Map.insertWith (++)
de2f13b8310de00ca228385b1530660e036054c2Christian Maeder in qm { carrierSens = ins (carrierSens qm) s }
4da70bec38acda1694ac5e854fd7aff20425c208Till Mossakowski -- axiom forcing empty carrier?
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Quantification Universal [Var_decl [_] s _] (Atom False _) _ ->
4da70bec38acda1694ac5e854fd7aff20425c208Till Mossakowski qm { carrierSens = Map.insertWith (++) s [f] (carrierSens qm) }
5432628486104961a32558db978860320bd2a37bTill Mossakowski insertPred p args body q =
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder q { predDefs = Map.insertWith (++) p [(args, body)] (predDefs q)}
5432628486104961a32558db978860320bd2a37bTill Mossakowski insertOp op args body q =
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder q { opDefs = Map.insertWith (++) op [(args, body)] (opDefs q) }
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski in case stripAllQuant f of
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski -- insert a predicate or operation definition into a QModel
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski Predication predsymb args _ ->
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder insertPred predsymb args trueForm qm1
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski Negation (Predication predsymb args _) _ ->
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder insertPred predsymb args falseForm qm1
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Relation (Predication predsymb args _) Equivalence body _ ->
5432628486104961a32558db978860320bd2a37bTill Mossakowski insertPred predsymb args body qm1
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Equation (Application opsymb args _) _ body _ ->
5432628486104961a32558db978860320bd2a37bTill Mossakowski insertOp opsymb args body qm1
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder {- treat equality as special predicate symbol, for detecting inequalities
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder also exploit that inequality is symmetric -}
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Negation (Equation t1 _ t2 _) _ ->
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder insertPred eqSymb [t1, t2] falseForm $
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder insertPred eqSymb [t2, t1] falseForm qm1
5432628486104961a32558db978860320bd2a37bTill Mossakowski-- | predicate symbol for equality (with dummy type)
5432628486104961a32558db978860320bd2a37bTill MossakowskieqSymb :: PRED_SYMB
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian MaedereqSymb = mkQualPred eqId (Pred_type [] nullRange)
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski-- * Variable assignments
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyerdata VariableAssignment = VariableAssignment QModel [(VAR, CASLTERM)]
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maederinstance Show VariableAssignment where
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer show (VariableAssignment qm assignList) = showAssignments qm assignList
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskishowAssignments :: QModel -> [(VAR, CASLTERM)] -> String
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskishowAssignments qm xs =
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo Wiedemeyer '[' : intercalate ", " (map (showSingleAssignment qm) xs) ++ "]"
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskishowSingleAssignment :: QModel -> (VAR, CASLTERM) -> String
56c56b2181e76c239929ddade2925ba5c3f3fffdChristian MaedershowSingleAssignment qm (v, t) =
b983a1c05057154ba9839cc8034c41871598c7f9Christian Maeder show v ++ "->" ++ showDoc (rmTypesT (const return) (const id) (sign qm) t) ""
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederemptyAssignment :: QModel -> VariableAssignment
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederemptyAssignment qm = VariableAssignment qm []
970835ca7cec4085ba84151d5b901cde934ec8f6Thiemo WiedemeyerinsertAssignment :: VariableAssignment -> (VAR, CASLTERM) -> VariableAssignment
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederinsertAssignment (VariableAssignment qm ass) (v, t) =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder VariableAssignment qm ((v, t) : ass)
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederconcatAssignment :: VariableAssignment -> VariableAssignment
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder -> VariableAssignment
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederconcatAssignment (VariableAssignment qm l1) (VariableAssignment _ l2) =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder VariableAssignment qm $ l1 ++ l2
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski-- * The quickcheck model checker
0c69f08a7017e47517265f974ed045f5b4134b02Till MossakowskiquickCheck :: QModel -> AS_Anno.Named CASLFORMULA -> Result Bool
72a99654d0be685fadb285be4c7f1bdb414bd271Christian MaederquickCheck qm =
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maeder calculateFormula True qm (emptyAssignment qm) . AS_Anno.sentence
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaedercalculateTerm :: QModel -> VariableAssignment -> CASLTERM -> Result CASLTERM
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskicalculateTerm qm ass trm = case trm of
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Qual_var var _ _ -> lookupVar var ass
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Application opSymb terms _ ->
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski applyOperation qm ass opSymb terms
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Sorted_term term _ _ -> calculateTerm qm ass term
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Conditional t1 fo t2 _ -> do
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski res <- calculateFormula False qm ass fo
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder calculateTerm qm ass $ if res then t1 else t2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder _ -> fail $ "QuickCheck.calculateTerm: unsupported: " ++ showDoc trm ""
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederlookupVar :: VAR -> VariableAssignment -> Result CASLTERM
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederlookupVar v (VariableAssignment _ ass) = case lookup v ass of
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder Nothing -> fail ("no value for variable " ++ show v ++ " found")
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Just val -> return val
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederapplyOperation :: QModel -> VariableAssignment -> OP_SYMB -> [CASLTERM]
77d3bde11c45c6ea9ec237dec6ed733bcde3ca14Christian Maeder -> Result CASLTERM
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiapplyOperation qm ass opsymb terms = do
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- block infinite recursion
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder when ((opsymb, terms) `elem` evaluatedOps qm)
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder (fail ("infinite recursion when calculating"
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder ++ show (mkAppl opsymb terms)))
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder let qm' = qm { evaluatedOps = (opsymb, terms) : evaluatedOps qm }
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- evaluate argument terms
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski args <- mapM (calculateTerm qm' ass) terms
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- find appropriate operation definition
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski case Map.lookup opsymb (opDefs qm) of
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- no operation definition? Then return unevaluated term
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder return (mkAppl opsymb terms)
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski Just bodies -> do
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- bind formal to actual arguments
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder (body, m) <- match bodies args $
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder showDoc (mkAppl opsymb args) ""
77d3bde11c45c6ea9ec237dec6ed733bcde3ca14Christian Maeder let ass' = foldl insertAssignment ass m
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- evaluate body of operation definition
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski calculateTerm qm' ass' body
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder{- | match a list of arguments (second parameter) against a
1bd72434378dac9262c5af0f204e87c674998d71Christian Maedera a list of bodies (first argument), each coming with a
1bd72434378dac9262c5af0f204e87c674998d71Christian Maederlist of formal parameters and a body term or formula -}
1bd72434378dac9262c5af0f204e87c674998d71Christian Maedermatch :: [([CASLTERM], a)] -> [CASLTERM] -> String
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder -> Result (a, [(VAR, CASLTERM)])
56c56b2181e76c239929ddade2925ba5c3f3fffdChristian Maedermatch bodies args msg =
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski case mapMaybe (match1 args) bodies of
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder [] -> fail ("no matching found for " ++ msg)
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder subst : _ -> return subst
6f485a7c411a3a411673a43aadd6293975f1b029Till Mossakowski-- match against a single body
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maedermatch1 :: [CASLTERM] -> ([CASLTERM], a) -> Maybe (a, [(VAR, CASLTERM)])
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maedermatch1 args (vars, body) = do
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder subst <- fmap concat $ zipWithM match2 vars args
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder if consistent subst then return (body, subst) else Nothing
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maedermatch2 :: CASLTERM -> CASLTERM -> Maybe [(VAR, CASLTERM)]
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maedermatch2 (Qual_var v _ _) t = Just [(v, t)]
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maedermatch2 (Application opsymb1 terms1 _) (Application opsymb2 terms2 _) =
6f485a7c411a3a411673a43aadd6293975f1b029Till Mossakowski -- direct match of operation symbols?
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder if opsymb1 == opsymb2 then
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder fmap concat $ zipWithM match2 terms1 terms2
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder -- if not, try to exploit overloading relation
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maeder let (opsymb1', terms1', w1) = stripInj opsymb1 terms1
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maeder (opsymb2', terms2', w2) = stripInj opsymb2 terms2
6f485a7c411a3a411673a43aadd6293975f1b029Till Mossakowski when (opSymbName opsymb1' /= opSymbName opsymb2' || w1 /= w2) Nothing
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder fmap concat $ zipWithM match2 terms1' terms2'
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowskimatch2 (Sorted_term t1 _ _) t2 = match2 t1 t2
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowskimatch2 t1 (Sorted_term t2 _ _) = match2 t1 t2
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowskimatch2 _ _ = Nothing
6f485a7c411a3a411673a43aadd6293975f1b029Till Mossakowski-- | strip off the injections of an application
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederstripInj :: OP_SYMB -> [CASLTERM] -> (OP_SYMB, [CASLTERM], [SORT])
9cda5e432971e59b79484cc5921fe76c04891e98Christian MaederstripInj opsymb terms =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder let (opsymb', terms') =
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maeder case (isInjName $ opSymbName opsymb, terms) of
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder (True, [Application o ts _]) -> (o, ts)
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder _ -> (opsymb, terms)
6f485a7c411a3a411673a43aadd6293975f1b029Till Mossakowski strip1 t1@(Application o [t2] _) =
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maeder if isInjName $ opSymbName o then t2 else t1
6f485a7c411a3a411673a43aadd6293975f1b029Till Mossakowski strip1 t1 = t1
6f485a7c411a3a411673a43aadd6293975f1b029Till Mossakowski terms'' = map strip1 terms'
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder in (opsymb', terms'', map sortOfTerm terms'')
6f485a7c411a3a411673a43aadd6293975f1b029Till Mossakowski-- | is a substitution consistent with itself?
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maederconsistent :: [(VAR, CASLTERM)] -> Bool
56c56b2181e76c239929ddade2925ba5c3f3fffdChristian Maederconsistent ass =
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski isJust $ foldM insertAss Map.empty ass
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder insertAss m (v, t) =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder Just t1 -> if t == t1 then return m else Nothing
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski Nothing -> Just $ Map.insert v t m
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederternaryAnd :: (Result Bool, a) -> (Result Bool, a) -> (Result Bool, a)
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederternaryAnd b1@(Result _ (Just False), _) _ = b1
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederternaryAnd (Result d1 (Just True), _) (b2, x2) =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder (Result d1 (Just ()) >> b2, x2)
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederternaryAnd (Result d1 Nothing, _) (b2@(Result _ (Just False)), x2) =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder (Result d1 (Just ()) >> b2, x2)
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederternaryAnd (Result d1 Nothing, _) (b2, x2) =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder (Result d1 (Just ()) >> b2 >> Result [] Nothing, x2)
4da70bec38acda1694ac5e854fd7aff20425c208Till MossakowskiternaryOr :: Result Bool -> Result Bool -> Result Bool
4da70bec38acda1694ac5e854fd7aff20425c208Till MossakowskiternaryOr b1@(Result _ (Just True)) _ = b1
ceef5f7843a1f96fe5a62e0f6880e38b3d5f4708Christian MaederternaryOr (Result d1 (Just False)) b2 = Result d1 (Just ()) >> b2
9cda5e432971e59b79484cc5921fe76c04891e98Christian MaederternaryOr (Result d1 Nothing) b2@(Result _ (Just True)) =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder Result d1 (Just ()) >> b2
9cda5e432971e59b79484cc5921fe76c04891e98Christian MaederternaryOr (Result d1 Nothing) b2 =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder Result d1 (Just ()) >> b2 >> Result [] Nothing
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaedercalculateFormula :: Bool -> QModel -> VariableAssignment -> CASLFORMULA
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder -> Result Bool
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till MossakowskicalculateFormula isOuter qm varass f = case f of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Quantification {} ->
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski calculateQuantification isOuter qm varass f
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Junction j formulas _ ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let newFs = map (calculateFormula False qm varass) formulas
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder in if j == Dis then foldl ternaryOr (return False) newFs else do
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder let (res, f1) =
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder foldl ternaryAnd (return True, f)
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski (zip (map (calculateFormula False qm varass) formulas) formulas)
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder when isOuter $ case maybeResult res of
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder Just False ->
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder justWarn () $ "Conjunction not fulfilled\n"
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder ++ "Formula that failed: " ++ showDoc f1 ""
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder _ -> return ()
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Relation f1 c f2 _ ->
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let res1 = calculateFormula False qm varass f1
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder res2 = calculateFormula False qm varass f2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder in if c == Equivalence then liftM2 (==) res1 res2 else
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder ternaryOr (fmap not res1) res2
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maeder Negation f1 _ ->
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maeder fmap not $ calculateFormula False qm varass f1
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Atom b _ -> return b
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Equation term1 _ term2 _ -> do
56c56b2181e76c239929ddade2925ba5c3f3fffdChristian Maeder t1 <- calculateTerm qm varass term1
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski t2 <- calculateTerm qm varass term2
5432628486104961a32558db978860320bd2a37bTill Mossakowski equalElements qm t1 t2
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Predication predsymb terms _ ->
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski applyPredicate qm varass predsymb terms
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski _ -> fail $ "formula evaluation not implemented for: " ++ showDoc f ""
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaedercalculateQuantification :: Bool -> QModel -> VariableAssignment -> CASLFORMULA
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski -> Result Bool
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till MossakowskicalculateQuantification isOuter qm varass qf = case qf of
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski Quantification quant vardecls f _ -> do
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski assments <- generateVariableAssignments qm vardecls
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder let assments' = map (`concatAssignment` varass) assments
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski case quant of
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski Universal -> do
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski let resList = map (flip (calculateFormula False qm) f) assments'
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder (res, fass) = foldl ternaryAnd (return True, emptyAssignment qm)
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski (zip resList assments')
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder when isOuter $ case maybeResult res of
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder Just False ->
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder justWarn () ("Universal quantification not fulfilled\n"
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder ++ "Counterexample: " ++ show fass)
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder _ -> return ()
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski Existential ->
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski foldl ternaryOr (return False)
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski (map (flip (calculateFormula False qm) f) assments')
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder Unique_existential ->
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder {- scan the assingments, stop scanning once the result is clear,
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder using the Left constructor of the Either monad -}
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder let combineEx1 state ass2 = case state of
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder Right (msgsSoFar, ass1) ->
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder let Result msgs res = calculateFormula False qm ass2 f
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder in case (res, ass1) of
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski -- the first fulfilment
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder (Just True, Nothing) -> Right (msgsSoFar ++ msgs, Just ass2)
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski -- the second fulfilment
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder (Just True, Just ass1') ->
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder Left (msgsSoFar ++ msgs, Just (ass1', ass2))
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski -- not fulfilled? Then nothing changes
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder (Just False, _) -> Right (msgsSoFar ++ msgs, ass1)
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski -- don't know? Then we don't know either
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder (Nothing, _) -> Left (msgsSoFar ++ msgs, Nothing)
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder Left _ -> state
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder in case foldl combineEx1 (Right ([], Nothing)) assments' of
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder Right (msgs, Just _) -> Result msgs (Just True)
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder Right (msgs, Nothing) -> do
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski Result msgs (Just ())
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder (justWarn () ("Unique Existential quantification"
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder ++ " not fulfilled: no assignment found"))
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder Left (msgs, Just (ass1, ass2)) -> do
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski Result msgs (Just ())
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder (justWarn () ("Unique Existential quantification"
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder ++ " not fulfilled: at least two assignments found:\n"
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder ++ show ass1 ++ "\n" ++ show ass2 ++ "\n"))
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maeder Left (msgs, Nothing) ->
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski Result msgs Nothing
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski _ -> fail "calculateQuantification wrongly applied"
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaederapplyPredicate :: QModel -> VariableAssignment -> PRED_SYMB -> [CASLTERM]
77d3bde11c45c6ea9ec237dec6ed733bcde3ca14Christian Maeder -> Result Bool
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiapplyPredicate qm ass predsymb terms = do
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- block infinite recursion
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder when (elem (predsymb, terms) $ evaluatedPreds qm)
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder (fail ("infinite recursion when calculating"
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder ++ show (mkPredication predsymb terms)))
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder let qm' = qm { evaluatedPreds = (predsymb, terms) : evaluatedPreds qm }
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- evaluate argument terms
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski args <- mapM (calculateTerm qm' ass) terms
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- find appropriate predicate definition
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski case Map.lookup predsymb (predDefs qm) of
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder Nothing -> fail ("no predicate definition for " ++ showDoc predsymb "")
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski Just bodies -> do
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- bind formal to actual arguments
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder (body, m) <- match bodies args $
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder showDoc (mkPredication predsymb args) ""
77d3bde11c45c6ea9ec237dec6ed733bcde3ca14Christian Maeder let ass' = foldl insertAssignment ass m
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- evaluate body of predicate definition
73e3f6eaf0c13ddf88f86d7dbf524595be91e022Till Mossakowski calculateFormula False qm' ass' body
5432628486104961a32558db978860320bd2a37bTill MossakowskiequalElements :: QModel -> CASLTERM -> CASLTERM -> Result Bool
5432628486104961a32558db978860320bd2a37bTill MossakowskiequalElements qm t1 t2 =
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder if t1 == t2 then return True
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder else applyPredicate qm (emptyAssignment qm) eqSymb [t1, t2]
56c56b2181e76c239929ddade2925ba5c3f3fffdChristian MaedergenerateVariableAssignments :: QModel -> [VAR_DECL]
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder -> Result [VariableAssignment]
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskigenerateVariableAssignments qm vardecls = do
facec64191b1f2aab74c4baa5f8ead0693c7813aChristian Maeder let vars = flatVAR_DECLs vardecls
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder carriers <- mapM (getCarrier qm . snd) vars
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski let varsCarriers = zip (map fst vars) carriers
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder return $ map (VariableAssignment qm) (gVAs varsCarriers)
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaedergVAs :: [(VAR, [CASLTERM])] -> [[(VAR, CASLTERM)]]
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskigVAs [] = [[]]
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaedergVAs ((v, carrier) : vs) = let
093ef39e87d41dc823b174aba9d24039d00da037Christian Maeder fs = map (\ b -> (v, b)) carrier
093ef39e87d41dc823b174aba9d24039d00da037Christian Maeder in [f : r | f <- fs, r <- rs]
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski-- | check whether some formula leads to term generation of a sort
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian MaedertermSort :: CASLFORMULA -> Maybe (SORT, [CASLTERM])
4da70bec38acda1694ac5e854fd7aff20425c208Till Mossakowski-- sort generation constraint
4da70bec38acda1694ac5e854fd7aff20425c208Till MossakowskitermSort (Sort_gen_ax constr _) =
4da70bec38acda1694ac5e854fd7aff20425c208Till Mossakowski case sorts of
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- at the moment, we only treat one-sort constraints with constants
56c56b2181e76c239929ddade2925ba5c3f3fffdChristian Maeder [s] -> if all constant ops
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder then Just (s, map mkTerm ops)
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder where (sorts, ops, _) = recover_Sort_gen_ax constr
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski constant (Qual_op_name _ (Op_type _ [] _ _) _) = True
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski constant _ = False
8975e88a732e0c50a6b95c4ad18808c49a643fc5Christian Maeder mkTerm op = mkAppl op []
4da70bec38acda1694ac5e854fd7aff20425c208Till Mossakowski-- axiom forcing empty carrier
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedertermSort (Quantification Universal [Var_decl [_] s _] (Atom False _) _) =
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskitermSort _ = Nothing
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski-- | get the carrier set for a specific sort
1bd72434378dac9262c5af0f204e87c674998d71Christian MaedergetCarrier :: QModel -> SORT -> Result [CASLTERM]
56c56b2181e76c239929ddade2925ba5c3f3fffdChristian MaedergetCarrier qm s =
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski case Map.lookup s (carrierSens qm) of
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder Nothing -> fail ("sort " ++ show s ++ " is not generated")
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Just sens -> case mapMaybe termSort sens of
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder [] -> fail ("sort " ++ show s ++ " is not generated by constants")
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder (_, terms) : _ -> return terms
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- todo: generalise this
0c69f08a7017e47517265f974ed045f5b4134b02Till Mossakowski-- * Interfacing to Hets prover interface
77d3bde11c45c6ea9ec237dec6ed733bcde3ca14Christian Maeder{- | The Prover implementation. First runs the batch prover (with
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder graphical feedback), then starts the GUI prover. -}
433bb7cb49200f4e6c7341101da25309e423c0e2Christian MaederquickCheckProver :: Prover CASLSign CASLFORMULA CASLMor CASL_Sublogics ProofTree
e24ad3f655daa60ddabe690e4b11de3187996c16cmaederquickCheckProver = (mkProverTemplate "QuickCheck"
e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder (SL.top { has_part = False, which_logic = SL.FOL }) quickCheckGUI)
e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder { proveCMDLautomaticBatch = Just quickCheckCMDLautomaticBatch }
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Record for prover specific functions. This is used by both GUI and command
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski line interface.
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiatpFun :: String -- ^ theory name
f094a7999dfa79cad2eb34ce15f1939c0d6b9e39Till Mossakowski -> ATPFunctions CASLSign CASLFORMULA CASLMor ProofTree QModel
0c69f08a7017e47517265f974ed045f5b4134b02Till MossakowskiatpFun _thName = ATPFunctions
f094a7999dfa79cad2eb34ce15f1939c0d6b9e39Till Mossakowski { initialProverState = \ sig sens _ -> insertSens (makeQm sig) sens,
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski atpTransSenName = id,
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski atpInsertSentence = insertSen,
d7e0a19c6dc518f6257015fa88f925c7bbee79e5Christian Maeder goalOutput = \ _ _ _ -> do
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski putStrLn "No display of output yet"
77d3bde11c45c6ea9ec237dec6ed733bcde3ca14Christian Maeder proverHelpText =
77d3bde11c45c6ea9ec237dec6ed733bcde3ca14Christian Maeder "QuickCheck tries to evaluate sentences in term generated models. " ++
77d3bde11c45c6ea9ec237dec6ed733bcde3ca14Christian Maeder "This only works if your theory contains enough generated or " ++
77d3bde11c45c6ea9ec237dec6ed733bcde3ca14Christian Maeder "freely generated datatypes.",
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski batchTimeEnv = "HETS_SPASS_BATCH_TIME_LIMIT",
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder fileExtensions = FileExtensions {problemOutput = ".none1",
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski proverOutput = ".none2",
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski theoryConfiguration = ".none3"},
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski runProver = runQuickCheck,
72a99654d0be685fadb285be4c7f1bdb414bd271Christian Maeder createProverOptions = const [] }
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Invokes the generic prover GUI. SPASS specific functions are omitted by
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski data type ATPFunctions.
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiquickCheckGUI :: String -- ^ theory name
a14767aeac3e78ed100f5b75e210ba563ee10dbaChristian Maeder -> Theory CASLSign CASLFORMULA ProofTree
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder {- ^ theory consisting of a signature
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder and a list of named sentences -}
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski -> [FreeDefMorphism CASLFORMULA CASLMor] -- ^ freeness constraints
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder -> IO [ProofStatus ProofTree] -- ^ proof status for each goal
f094a7999dfa79cad2eb34ce15f1939c0d6b9e39Till MossakowskiquickCheckGUI thName th freedefs = genericATPgui (atpFun thName) True
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder (proverName quickCheckProver) thName th freedefs emptyProofTree
f30f834d81e1c294aff8eb2752fd864f6488820dChristian Maeder-- ** command line function
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Implementation of 'Logic.Prover.proveCMDLautomaticBatch' which provides an
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski automatic command line interface to the QuickCheck prover via MathServe.
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski QuickCheck specific functions are omitted by data type ATPFunctions.
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiquickCheckCMDLautomaticBatch ::
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski Bool -- ^ True means include proved theorems
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -> Bool -- ^ True means save problem file
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder -> MVar (Result.Result [ProofStatus ProofTree])
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -- ^ used to store the result of the batch run
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski -> String -- ^ theory name
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder -> TacticScript -- ^ default tactic script
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder -> Theory CASLSign CASLFORMULA ProofTree {- ^ theory consisting of a
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder signature and a list of named sentences -}
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski -> [FreeDefMorphism CASLFORMULA CASLMor] -- ^ freeness constraints
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder -> IO (ThreadId, MVar ())
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder {- ^ fst: identifier of the batch thread for killing it
1bd72434378dac9262c5af0f204e87c674998d71Christian Maeder snd: MVar to wait for the end of the thread -}
afae8493e1c904789e3352f6daae63bd66cf057dTill MossakowskiquickCheckCMDLautomaticBatch inclProvedThs saveProblem_batch resultMVar
f094a7999dfa79cad2eb34ce15f1939c0d6b9e39Till Mossakowski thName defTS th freedefs =
afae8493e1c904789e3352f6daae63bd66cf057dTill Mossakowski genericCMDLautomaticBatch (atpFun thName) inclProvedThs saveProblem_batch
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder resultMVar (proverName quickCheckProver) thName
3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder (parseTacticScript batchTimeLimit [] defTS) th freedefs emptyProofTree