22 #ifndef _cvc3__search__search_theorem_producer_h_
23 #define _cvc3__search__search_theorem_producer_h_
30 class CommonProofRules;
74 const std::vector<Theorem>& delta);
88 const std::vector<Theorem>& lits,
89 const std::vector<Theorem>& gamma);
99 const Theorem& clause,
unsigned i);
198 const std::string& ruleName);
206 std::vector<Expr>& boundVars);
virtual void propAndrLRT(const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)
void verifyConflict(const Theorem &thm, TheoremMap &m)
virtual Theorem proofByContradiction(const Expr &a, const Theorem &pfFalse)
Proof by contradiction: .
Data structure of expressions in CVC3.
virtual Theorem confIterThenElse(const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)
std::map< Theorem, bool, TheoremLess > TheoremMap
virtual Theorem eliminateSkolemAxioms(const Theorem &tFalse, const std::vector< Theorem > &delta)
Expr findInLocalCache(const Expr &i, ExprMap< Expr > &localCache, std::vector< Expr > &boundVars)
checks if phi has v in local cache of opCNFRule, if so reuse v.
Theorem iffToClauses(const Theorem &iff)
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
virtual Theorem propAndrLF(const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)
virtual Theorem cutRule(const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)
Cut rule: .
virtual Theorem propIffr(const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)
virtual Theorem propIterIte(const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)
virtual ~SearchEngineTheoremProducer()
virtual Theorem caseSplit(const Expr &a, const Theorem &a_proves_c, const Theorem ¬_a_proves_c)
Case split: .
Theorem impCNFRule(const Theorem &thm)
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
virtual void propIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)
Abstract proof rules interface to the simple search engine.
virtual Theorem unitProp(const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)
Unit propagation rule: .
SearchEngineTheoremProducer(TheoremManager *tm)
Theorem orCNFRule(const Theorem &thm)
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
virtual Theorem conflictRule(const std::vector< Theorem > &thms, const Theorem &clause)
"Conflict" rule (all literals in a clause become FALSE)
virtual Theorem confIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)
Theorem opCNFRule(const Theorem &thm, int kind, const std::string &ruleName)
Theorem iteToClauses(const Theorem &ite)
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
virtual Theorem confAndrAF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)
virtual Theorem conflictClause(const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)
Conflict clause rule: .
virtual Theorem propAndrRF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)
Theorem iteCNFRule(const Theorem &thm)
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
CommonProofRules * d_commonRules
virtual Theorem confIffr(const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)
API to the proof rules for the Search Engines.
virtual Theorem propIterThen(const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)
Theorem iffCNFRule(const Theorem &thm)
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Theorem satProof(const Expr &queryExpr, const Proof &satProof)
virtual Theorem propAndrAT(const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)
virtual Theorem negIntro(const Expr ¬_a, const Theorem &pfFalse)
Negation introduction: .
virtual Theorem propAndrAF(const Theorem &andr_th, bool left, const Theorem &b_th)
Expr convertToCNF(const Expr &v, const Expr &phi)
produces the CNF for the formula v <==> phi
void checkSoundNoSkolems(const Expr &e, ExprMap< bool > &visited, const ExprMap< bool > &skolems)
Theorem andCNFRule(const Theorem &thm)
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
virtual Theorem confAndrAT(const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)