| andCNFRule(const Theorem &thm) | CVC3::SearchEngineTheoremProducer | [virtual] |
| caseSplit(const Expr &a, const Theorem &a_proves_c, const Theorem ¬_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_checkProofs | CVC3::TheoremProducer | [protected] |
| d_commonRules | CVC3::SearchEngineTheoremProducer | [private] |
| d_em | CVC3::TheoremProducer | [protected] |
| d_hole | CVC3::TheoremProducer | [protected] |
| d_pfOp | CVC3::TheoremProducer | [protected] |
| d_tm | CVC3::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 ¬_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] |
