|
CVC3
|
This is the complete list of members for CVC3::CoreTheoremProducer, including all inherited members.
| andDistributivityRule(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| AndToIte(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| CoreTheoremProducer(TheoremManager *tm, TheoryCore *core) | CVC3::CoreTheoremProducer | inline |
| d_checkProofs | CVC3::TheoremProducer | protected |
| d_core | CVC3::CoreTheoremProducer | private |
| d_em | CVC3::TheoremProducer | protected |
| d_hole | CVC3::TheoremProducer | protected |
| d_pfOp | CVC3::TheoremProducer | protected |
| d_tm | CVC3::TheoremProducer | protected |
| dummyTheorem(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| iffAndDistrib(const Expr &iff) | CVC3::CoreTheoremProducer | virtual |
| iffOrDistrib(const Expr &iff) | CVC3::CoreTheoremProducer | virtual |
| IffToIte(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| ifLiftUnaryRule(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| ImpToIte(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| newAssumption(const Expr &thm, const Proof &pf, int scope=-1) | CVC3::TheoremProducer | inlineprotected |
| 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 | inlineprotected |
| newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
| newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
| newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
| newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf) | CVC3::TheoremProducer | inlineprotected |
| NotToIte(const Expr ¬_e) | CVC3::CoreTheoremProducer | virtual |
| orDistributivityRule(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| OrToIte(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteAndSubterms(const Expr &e, int idx) | CVC3::CoreTheoremProducer | virtual |
| rewriteDistinct(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteImplies(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteIteBool(const Expr &c, const Expr &e1, const Expr &e2) | CVC3::CoreTheoremProducer | virtual |
| rewriteIteCond(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteIteElse(const Expr &e, const Theorem &elseThm) | CVC3::CoreTheoremProducer | virtual |
| rewriteIteThen(const Expr &e, const Theorem &thenThm) | CVC3::CoreTheoremProducer | virtual |
| rewriteIteToAnd(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteIteToIff(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteIteToImp(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteIteToNot(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteIteToOr(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteLetDecl(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteNotAnd(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteNotIff(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteNotIte(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteNotOr(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| rewriteOrSubterms(const Expr &e, int idx) | CVC3::CoreTheoremProducer | virtual |
| soundError(const std::string &file, int line, const std::string &cond, const std::string &msg) | CVC3::TheoremProducer | protected |
| TheoremProducer(TheoremManager *tm) | CVC3::TheoremProducer | |
| typePred(const Expr &e) | CVC3::CoreTheoremProducer | virtual |
| withAssumptions() | CVC3::TheoremProducer | inline |
| withProof() | CVC3::TheoremProducer | inline |
| ~CoreProofRules() | CVC3::CoreProofRules | inlinevirtual |
| ~CoreTheoremProducer() | CVC3::CoreTheoremProducer | inlinevirtual |
| ~TheoremProducer() | CVC3::TheoremProducer | inlinevirtual |
1.8.2