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