CVC3

CVC3::SearchEngineTheoremProducer Member List

This is the complete list of members for CVC3::SearchEngineTheoremProducer, including all inherited members.
andCNFRule(const Theorem &thm)CVC3::SearchEngineTheoremProducer [virtual]
caseSplit(const Expr &a, const Theorem &a_proves_c, const Theorem &not_a_proves_c)CVC3::SearchEngineTheoremProducer [virtual]
checkSoundNoSkolems(const Expr &e, ExprMap< bool > &visited, const ExprMap< bool > &skolems)CVC3::SearchEngineTheoremProducer [private]
checkSoundNoSkolems(const Theorem &t, ExprMap< bool > &visited, const ExprMap< bool > &skolems)CVC3::SearchEngineTheoremProducer [private]
confAndrAF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)CVC3::SearchEngineTheoremProducer [virtual]
confAndrAT(const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)CVC3::SearchEngineTheoremProducer [virtual]
confIffr(const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)CVC3::SearchEngineTheoremProducer [virtual]
confIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)CVC3::SearchEngineTheoremProducer [virtual]
confIterThenElse(const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)CVC3::SearchEngineTheoremProducer [virtual]
conflictClause(const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)CVC3::SearchEngineTheoremProducer [virtual]
conflictRule(const std::vector< Theorem > &thms, const Theorem &clause)CVC3::SearchEngineTheoremProducer [virtual]
convertToCNF(const Expr &v, const Expr &phi)CVC3::SearchEngineTheoremProducer [private]
cutRule(const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)CVC3::SearchEngineTheoremProducer [virtual]
d_checkProofsCVC3::TheoremProducer [protected]
d_commonRulesCVC3::SearchEngineTheoremProducer [private]
d_emCVC3::TheoremProducer [protected]
d_holeCVC3::TheoremProducer [protected]
d_pfOpCVC3::TheoremProducer [protected]
d_tmCVC3::TheoremProducer [protected]
eliminateSkolemAxioms(const Theorem &tFalse, const std::vector< Theorem > &delta)CVC3::SearchEngineTheoremProducer [virtual]
findInLocalCache(const Expr &i, ExprMap< Expr > &localCache, std::vector< Expr > &boundVars)CVC3::SearchEngineTheoremProducer [private]
iffCNFRule(const Theorem &thm)CVC3::SearchEngineTheoremProducer [virtual]
iffToClauses(const Theorem &iff)CVC3::SearchEngineTheoremProducer [virtual]
impCNFRule(const Theorem &thm)CVC3::SearchEngineTheoremProducer [virtual]
iteCNFRule(const Theorem &thm)CVC3::SearchEngineTheoremProducer [virtual]
iteToClauses(const Theorem &ite)CVC3::SearchEngineTheoremProducer [virtual]
negIntro(const Expr &not_a, const Theorem &pfFalse)CVC3::SearchEngineTheoremProducer [virtual]
newAssumption(const Expr &thm, const Proof &pf, int scope=-1)CVC3::TheoremProducer [inline, protected]
newLabel(const Expr &e)CVC3::TheoremProducer
newPf(const std::string &name)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e)CVC3::TheoremProducer
newPf(const std::string &name, const Proof &pf)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e1, const Expr &e2)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e, const Proof &pf)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)CVC3::TheoremProducer
newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)CVC3::TheoremProducer
newPf(const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const std::string &name, const std::vector< Expr > &args)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e, const std::vector< Expr > &args)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const std::string &name, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const std::string &name, const std::vector< Expr > &args, const Proof &pf)CVC3::TheoremProducer
newPf(const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)CVC3::TheoremProducer
newPf(const Proof &label, const Expr &frm, const Proof &pf)CVC3::TheoremProducer
newPf(const Proof &label, const Proof &pf)CVC3::TheoremProducer
newPf(const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)CVC3::TheoremProducer
newPf(const std::vector< Proof > &labels, const Proof &pf)CVC3::TheoremProducer
newReflTheorem(const Expr &e)CVC3::TheoremProducer [inline, protected]
newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducer [inline, protected]
newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducer [inline, protected]
newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducer [inline, protected]
newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducer [inline, protected]
opCNFRule(const Theorem &thm, int kind, const std::string &ruleName)CVC3::SearchEngineTheoremProducer [private]
orCNFRule(const Theorem &thm)CVC3::SearchEngineTheoremProducer [virtual]
proofByContradiction(const Expr &a, const Theorem &pfFalse)CVC3::SearchEngineTheoremProducer [virtual]
propAndrAF(const Theorem &andr_th, bool left, const Theorem &b_th)CVC3::SearchEngineTheoremProducer [virtual]
propAndrAT(const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)CVC3::SearchEngineTheoremProducer [virtual]
propAndrLF(const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)CVC3::SearchEngineTheoremProducer [virtual]
propAndrLRT(const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)CVC3::SearchEngineTheoremProducer [virtual]
propAndrRF(const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)CVC3::SearchEngineTheoremProducer [virtual]
propIffr(const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)CVC3::SearchEngineTheoremProducer [virtual]
propIterIfThen(const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)CVC3::SearchEngineTheoremProducer [virtual]
propIterIte(const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)CVC3::SearchEngineTheoremProducer [virtual]
propIterThen(const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)CVC3::SearchEngineTheoremProducer [virtual]
satProof(const Expr &queryExpr, const Proof &satProof)CVC3::SearchEngineTheoremProducer [virtual]
SearchEngineTheoremProducer(TheoremManager *tm)CVC3::SearchEngineTheoremProducer
soundError(const std::string &file, int line, const std::string &cond, const std::string &msg)CVC3::TheoremProducer [protected]
TheoremProducer(TheoremManager *tm)CVC3::TheoremProducer
unitProp(const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)CVC3::SearchEngineTheoremProducer [virtual]
verifyConflict(const Theorem &thm, TheoremMap &m)CVC3::SearchEngineTheoremProducer [private]
withAssumptions()CVC3::TheoremProducer [inline]
withProof()CVC3::TheoremProducer [inline]
~SearchEngineRules()CVC3::SearchEngineRules [inline, virtual]
~SearchEngineTheoremProducer()CVC3::SearchEngineTheoremProducer [inline, virtual]
~TheoremProducer()CVC3::TheoremProducer [inline, virtual]