| addNewConst(const Expr &e) | CVC3::QuantTheoremProducer | [virtual] |
| adjustVarUniv(const Theorem &t1, const std::vector< Expr > &newBvs) | CVC3::QuantTheoremProducer | [virtual] |
| boundVarElim(const Theorem &t1) | CVC3::QuantTheoremProducer | [virtual] |
| d_checkProofs | CVC3::TheoremProducer | [protected] |
| d_em | CVC3::TheoremProducer | [protected] |
| d_hole | CVC3::TheoremProducer | [protected] |
| d_pfOp | CVC3::TheoremProducer | [protected] |
| d_theoryQuant | CVC3::QuantTheoremProducer | [private] |
| d_tm | CVC3::TheoremProducer | [protected] |
| d_typeFound | CVC3::QuantTheoremProducer | [private] |
| 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] |
| newRWThm(const Expr &e, const Expr &newE) | CVC3::QuantTheoremProducer | [virtual] |
| 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] |
| normalizeQuant(const Expr &e) | CVC3::QuantTheoremProducer | [virtual] |
| packVar(const Theorem &t1) | CVC3::QuantTheoremProducer | [virtual] |
| partialUniversalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel) | CVC3::QuantTheoremProducer | [virtual] |
| pullVarOut(const Theorem &t1) | CVC3::QuantTheoremProducer | [virtual] |
| QuantTheoremProducer(TheoremManager *tm, TheoryQuant *theoryQuant) | CVC3::QuantTheoremProducer | [inline] |
| recFindBoundVars(const Expr &e, ExprMap< bool > &boundVars, ExprMap< bool > &visited) | CVC3::QuantTheoremProducer | [private] |
| rewriteNotExists(const Expr &e) | CVC3::QuantTheoremProducer | [virtual] |
| rewriteNotForall(const Expr &e) | CVC3::QuantTheoremProducer | [virtual] |
| soundError(const std::string &file, int line, const std::string &cond, const std::string &msg) | CVC3::TheoremProducer | [protected] |
| TheoremProducer(TheoremManager *tm) | CVC3::TheoremProducer | |
| universalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel, Expr gterm) | CVC3::QuantTheoremProducer | [virtual] |
| universalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel) | CVC3::QuantTheoremProducer | [virtual] |
| universalInst(const Theorem &t1, const std::vector< Expr > &terms) | CVC3::QuantTheoremProducer | [virtual] |
| withAssumptions() | CVC3::TheoremProducer | [inline] |
| withProof() | CVC3::TheoremProducer | [inline] |
| ~QuantProofRules() | CVC3::QuantProofRules | [inline, virtual] |
| ~TheoremProducer() | CVC3::TheoremProducer | [inline, virtual] |
