CVC3  2.4.1
CVC3::CommonTheoremProducer Member List

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

ackermann(const Expr &e1, const Expr &e2)CVC3::CommonTheoremProducervirtual
andElim(const Theorem &e, int i)CVC3::CommonTheoremProducervirtual
andIntro(const Theorem &e1, const Theorem &e2)CVC3::CommonTheoremProducervirtual
andIntro(const std::vector< Theorem > &es)CVC3::CommonTheoremProducervirtual
assumpRule(const Expr &a, int scope=-1)CVC3::CommonTheoremProducervirtual
clearSkolemAxioms()CVC3::CommonTheoremProducerinlinevirtual
CommonTheoremProducer(TheoremManager *tm)CVC3::CommonTheoremProducer
contradictionRule(const Theorem &e, const Theorem &not_e)CVC3::CommonTheoremProducervirtual
d_checkProofsCVC3::TheoremProducerprotected
d_emCVC3::TheoremProducerprotected
d_holeCVC3::TheoremProducerprotected
d_pfOpCVC3::TheoremProducerprotected
d_skolem_axiomsCVC3::CommonTheoremProducerprivate
d_skolemized_thmsCVC3::CommonTheoremProducerprivate
d_skolemVarsCVC3::CommonTheoremProducerprivate
d_tmCVC3::TheoremProducerprotected
excludedMiddle(const Expr &e)CVC3::CommonTheoremProducervirtual
findITE(const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart)CVC3::CommonTheoremProducerprivate
getSkolemAxioms()CVC3::CommonTheoremProducerinlinevirtual
iffContrapositive(const Theorem &thm)CVC3::CommonTheoremProducervirtual
iffFalseElim(const Theorem &e)CVC3::CommonTheoremProducervirtual
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)CVC3::CommonTheoremProducervirtual
iffNotFalse(const Theorem &e)CVC3::CommonTheoremProducervirtual
iffTrue(const Theorem &e)CVC3::CommonTheoremProducervirtual
iffTrueElim(const Theorem &e)CVC3::CommonTheoremProducervirtual
implContrapositive(const Theorem &thm)CVC3::CommonTheoremProducervirtual
implIntro(const Theorem &phi, const std::vector< Expr > &assump)CVC3::CommonTheoremProducervirtual
implIntro3(const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)CVC3::CommonTheoremProducervirtual
implMP(const Theorem &e1, const Theorem &e1_impl_e2)CVC3::CommonTheoremProducervirtual
liftOneITE(const Expr &e)CVC3::CommonTheoremProducervirtual
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
notNotElim(const Theorem &e)CVC3::CommonTheoremProducervirtual
notToIff(const Theorem &not_e)CVC3::CommonTheoremProducervirtual
queryTCC(const Theorem &phi, const Theorem &D_phi)CVC3::CommonTheoremProducervirtual
reflexivityRule(const Expr &a)CVC3::CommonTheoremProducervirtual
rewriteAnd(const Expr &e)CVC3::CommonTheoremProducervirtual
rewriteAnd(const Theorem &e)CVC3::CommonTheoremProducervirtual
rewriteIff(const Expr &e)CVC3::CommonTheoremProducervirtual
rewriteIteFalse(const Expr &e)CVC3::CommonTheoremProducervirtual
rewriteIteSame(const Expr &e)CVC3::CommonTheoremProducervirtual
rewriteIteTrue(const Expr &e)CVC3::CommonTheoremProducervirtual
rewriteNotExists(const Expr &existsExpr)CVC3::CommonTheoremProducervirtual
rewriteNotFalse(const Expr &e)CVC3::CommonTheoremProducervirtual
rewriteNotForall(const Expr &forallExpr)CVC3::CommonTheoremProducervirtual
rewriteNotNot(const Expr &e)CVC3::CommonTheoremProducervirtual
rewriteNotTrue(const Expr &e)CVC3::CommonTheoremProducervirtual
rewriteOr(const Expr &e)CVC3::CommonTheoremProducervirtual
rewriteOr(const Theorem &e)CVC3::CommonTheoremProducervirtual
rewriteReflexivity(const Expr &t)CVC3::CommonTheoremProducervirtual
rewriteUsingSymmetry(const Expr &a1_eq_a2)CVC3::CommonTheoremProducervirtual
skolemize(const Expr &e)CVC3::CommonTheoremProducervirtual
skolemize(const Theorem &thm)CVC3::CommonTheoremProducervirtual
skolemizeRewrite(const Expr &e)CVC3::CommonTheoremProducervirtual
skolemizeRewriteVar(const Expr &e)CVC3::CommonTheoremProducervirtual
soundError(const std::string &file, int line, const std::string &cond, const std::string &msg)CVC3::TheoremProducerprotected
substitutivityRule(const Expr &e, const Theorem &thm)CVC3::CommonTheoremProducervirtual
substitutivityRule(const Expr &e, const Theorem &thm1, const Theorem &thm2)CVC3::CommonTheoremProducervirtual
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)CVC3::CommonTheoremProducervirtual
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)CVC3::CommonTheoremProducervirtual
substitutivityRule(const Expr &e, const int changed, const Theorem &thm)CVC3::CommonTheoremProducervirtual
symmetryRule(const Theorem &a1_eq_a2)CVC3::CommonTheoremProducervirtual
TheoremProducer(TheoremManager *tm)CVC3::TheoremProducer
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)CVC3::CommonTheoremProducervirtual
trueTheorem()CVC3::CommonTheoremProducervirtual
varIntroRule(const Expr &e)CVC3::CommonTheoremProducervirtual
varIntroSkolem(const Expr &e)CVC3::CommonTheoremProducervirtual
withAssumptions()CVC3::TheoremProducerinline
withProof()CVC3::TheoremProducerinline
xorToIff(const Expr &e)CVC3::CommonTheoremProducervirtual
~CommonProofRules()CVC3::CommonProofRulesinlinevirtual
~CommonTheoremProducer()CVC3::CommonTheoremProducerinlinevirtual
~TheoremProducer()CVC3::TheoremProducerinlinevirtual