CVC3  2.4.1
CVC3::CoreTheoremProducer Member List

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

andDistributivityRule(const Expr &e)CVC3::CoreTheoremProducervirtual
AndToIte(const Expr &e)CVC3::CoreTheoremProducervirtual
CoreTheoremProducer(TheoremManager *tm, TheoryCore *core)CVC3::CoreTheoremProducerinline
d_checkProofsCVC3::TheoremProducerprotected
d_coreCVC3::CoreTheoremProducerprivate
d_emCVC3::TheoremProducerprotected
d_holeCVC3::TheoremProducerprotected
d_pfOpCVC3::TheoremProducerprotected
d_tmCVC3::TheoremProducerprotected
dummyTheorem(const Expr &e)CVC3::CoreTheoremProducervirtual
iffAndDistrib(const Expr &iff)CVC3::CoreTheoremProducervirtual
iffOrDistrib(const Expr &iff)CVC3::CoreTheoremProducervirtual
IffToIte(const Expr &e)CVC3::CoreTheoremProducervirtual
ifLiftUnaryRule(const Expr &e)CVC3::CoreTheoremProducervirtual
ImpToIte(const Expr &e)CVC3::CoreTheoremProducervirtual
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
newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)CVC3::TheoremProducerinlineprotected
NotToIte(const Expr &not_e)CVC3::CoreTheoremProducervirtual
orDistributivityRule(const Expr &e)CVC3::CoreTheoremProducervirtual
OrToIte(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteAndSubterms(const Expr &e, int idx)CVC3::CoreTheoremProducervirtual
rewriteDistinct(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteImplies(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteIteBool(const Expr &c, const Expr &e1, const Expr &e2)CVC3::CoreTheoremProducervirtual
rewriteIteCond(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteIteElse(const Expr &e, const Theorem &elseThm)CVC3::CoreTheoremProducervirtual
rewriteIteThen(const Expr &e, const Theorem &thenThm)CVC3::CoreTheoremProducervirtual
rewriteIteToAnd(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteIteToIff(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteIteToImp(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteIteToNot(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteIteToOr(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteLetDecl(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteNotAnd(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteNotIff(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteNotIte(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteNotOr(const Expr &e)CVC3::CoreTheoremProducervirtual
rewriteOrSubterms(const Expr &e, int idx)CVC3::CoreTheoremProducervirtual
soundError(const std::string &file, int line, const std::string &cond, const std::string &msg)CVC3::TheoremProducerprotected
TheoremProducer(TheoremManager *tm)CVC3::TheoremProducer
typePred(const Expr &e)CVC3::CoreTheoremProducervirtual
withAssumptions()CVC3::TheoremProducerinline
withProof()CVC3::TheoremProducerinline
~CoreProofRules()CVC3::CoreProofRulesinlinevirtual
~CoreTheoremProducer()CVC3::CoreTheoremProducerinlinevirtual
~TheoremProducer()CVC3::TheoremProducerinlinevirtual