CVC3
CVC3::QuantTheoremProducer Member List

This is the complete list of members for CVC3::QuantTheoremProducer, including all inherited members.

addNewConst(const Expr &e)CVC3::QuantTheoremProducervirtual
adjustVarUniv(const Theorem &t1, const std::vector< Expr > &newBvs)CVC3::QuantTheoremProducervirtual
boundVarElim(const Theorem &t1)CVC3::QuantTheoremProducervirtual
d_checkProofsCVC3::TheoremProducerprotected
d_emCVC3::TheoremProducerprotected
d_holeCVC3::TheoremProducerprotected
d_pfOpCVC3::TheoremProducerprotected
d_theoryQuantCVC3::QuantTheoremProducerprivate
d_tmCVC3::TheoremProducerprotected
d_typeFoundCVC3::QuantTheoremProducerprivate
newAssumption(const Expr &thm, const Proof &pf, int scope=-1)CVC3::TheoremProducerinlineprotected
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::TheoremProducerinlineprotected
newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newRWThm(const Expr &e, const Expr &newE)CVC3::QuantTheoremProducervirtual
newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
normalizeQuant(const Expr &e)CVC3::QuantTheoremProducervirtual
packVar(const Theorem &t1)CVC3::QuantTheoremProducervirtual
partialUniversalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel)CVC3::QuantTheoremProducervirtual
pullVarOut(const Theorem &t1)CVC3::QuantTheoremProducervirtual
QuantTheoremProducer(TheoremManager *tm, TheoryQuant *theoryQuant)CVC3::QuantTheoremProducerinline
recFindBoundVars(const Expr &e, ExprMap< bool > &boundVars, ExprMap< bool > &visited)CVC3::QuantTheoremProducerprivate
rewriteNotExists(const Expr &e)CVC3::QuantTheoremProducervirtual
rewriteNotForall(const Expr &e)CVC3::QuantTheoremProducervirtual
soundError(const std::string &file, int line, const std::string &cond, const std::string &msg)CVC3::TheoremProducerprotected
TheoremProducer(TheoremManager *tm)CVC3::TheoremProducer
universalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel, Expr gterm)CVC3::QuantTheoremProducervirtual
universalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel)CVC3::QuantTheoremProducervirtual
universalInst(const Theorem &t1, const std::vector< Expr > &terms)CVC3::QuantTheoremProducervirtual
withAssumptions()CVC3::TheoremProducerinline
withProof()CVC3::TheoremProducerinline
~QuantProofRules()CVC3::QuantProofRulesinlinevirtual
~TheoremProducer()CVC3::TheoremProducerinlinevirtual