, including all inherited members.
ackermann(const Expr &e1, const Expr &e2) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::ackermann(const Expr &e1, const Expr &e2)=0 | CVC3::CommonProofRules | [pure virtual] |
andElim(const Theorem &e, int i) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::andElim(const Theorem &e, int i)=0 | CVC3::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)=0 | CVC3::CommonProofRules | [pure virtual] |
CVC3::CommonProofRules::andIntro(const std::vector< Theorem > &es)=0 | CVC3::CommonProofRules | [pure virtual] |
assumpRule(const Expr &a, int scope=-1) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::assumpRule(const Expr &a, int scope=-1)=0 | CVC3::CommonProofRules | [pure virtual] |
clearSkolemAxioms() | CVC3::CommonTheoremProducer | [inline] |
CVC3::CommonProofRules::clearSkolemAxioms()=0 | CVC3::CommonProofRules | [pure virtual] |
CommonTheoremProducer(TheoremManager *tm) | CVC3::CommonTheoremProducer | |
contradictionRule(const Theorem &e, const Theorem ¬_e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::contradictionRule(const Theorem &e, const Theorem ¬_e)=0 | CVC3::CommonProofRules | [pure virtual] |
d_checkProofs | CVC3::TheoremProducer | [protected] |
d_em | CVC3::TheoremProducer | [protected] |
d_hole | CVC3::TheoremProducer | [protected] |
d_pfOp | CVC3::TheoremProducer | [protected] |
d_skolem_axioms | CVC3::CommonTheoremProducer | [private] |
d_skolemized_thms | CVC3::CommonTheoremProducer | [private] |
d_skolemVars | CVC3::CommonTheoremProducer | [private] |
d_tm | CVC3::TheoremProducer | [protected] |
excludedMiddle(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::excludedMiddle(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
findITE(const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart) | CVC3::CommonTheoremProducer | [private] |
getSkolemAxioms() | CVC3::CommonTheoremProducer | [inline] |
CVC3::CommonProofRules::getSkolemAxioms()=0 | CVC3::CommonProofRules | [pure virtual] |
iffContrapositive(const Theorem &thm) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::iffContrapositive(const Theorem &thm)=0 | CVC3::CommonProofRules | [pure virtual] |
iffFalseElim(const Theorem &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::iffFalseElim(const Theorem &e)=0 | CVC3::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)=0 | CVC3::CommonProofRules | [pure virtual] |
iffNotFalse(const Theorem &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::iffNotFalse(const Theorem &e)=0 | CVC3::CommonProofRules | [pure virtual] |
iffTrue(const Theorem &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::iffTrue(const Theorem &e)=0 | CVC3::CommonProofRules | [pure virtual] |
iffTrueElim(const Theorem &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::iffTrueElim(const Theorem &e)=0 | CVC3::CommonProofRules | [pure virtual] |
implContrapositive(const Theorem &thm) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::implContrapositive(const Theorem &thm)=0 | CVC3::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)=0 | CVC3::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)=0 | CVC3::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)=0 | CVC3::CommonProofRules | [pure virtual] |
liftOneITE(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::liftOneITE(const Expr &e)=0 | CVC3::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_e)=0 | CVC3::CommonProofRules | [pure virtual] |
notToIff(const Theorem ¬_e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::notToIff(const Theorem ¬_e)=0 | CVC3::CommonProofRules | [pure virtual] |
queryTCC(const Theorem &phi, const Theorem &D_phi) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::queryTCC(const Theorem &phi, const Theorem &D_phi)=0 | CVC3::CommonProofRules | [pure virtual] |
reflexivityRule(const Expr &a) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::reflexivityRule(const Expr &a)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteAnd(const Expr &e) | CVC3::CommonTheoremProducer | |
rewriteAnd(const Theorem &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteAnd(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
CVC3::CommonProofRules::rewriteAnd(const Theorem &e)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteIff(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteIff(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteIteFalse(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteIteFalse(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteIteSame(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteIteSame(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteIteTrue(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteIteTrue(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteNotExists(const Expr &existsExpr) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteNotExists(const Expr &existsExpr)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteNotFalse(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteNotFalse(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteNotForall(const Expr &forallExpr) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteNotForall(const Expr &forallExpr)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteNotNot(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteNotNot(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteNotTrue(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteNotTrue(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteOr(const Expr &e) | CVC3::CommonTheoremProducer | |
rewriteOr(const Theorem &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteOr(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
CVC3::CommonProofRules::rewriteOr(const Theorem &e)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteReflexivity(const Expr &t) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteReflexivity(const Expr &a_eq_a)=0 | CVC3::CommonProofRules | [pure virtual] |
rewriteUsingSymmetry(const Expr &a1_eq_a2) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::rewriteUsingSymmetry(const Expr &a1_eq_a2)=0 | CVC3::CommonProofRules | [pure virtual] |
skolemize(const Expr &e) | CVC3::CommonTheoremProducer | |
skolemize(const Theorem &thm) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::skolemize(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
CVC3::CommonProofRules::skolemize(const Theorem &thm)=0 | CVC3::CommonProofRules | [pure virtual] |
skolemizeRewrite(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::skolemizeRewrite(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
skolemizeRewriteVar(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::skolemizeRewriteVar(const Expr &e)=0 | CVC3::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)=0 | CVC3::CommonProofRules | [pure virtual] |
CVC3::CommonProofRules::substitutivityRule(const Expr &e, const Theorem &thm1, const Theorem &thm2)=0 | CVC3::CommonProofRules | [pure virtual] |
CVC3::CommonProofRules::substitutivityRule(const Op &op, const std::vector< Theorem > &thms)=0 | CVC3::CommonProofRules | [pure virtual] |
CVC3::CommonProofRules::substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)=0 | CVC3::CommonProofRules | [pure virtual] |
CVC3::CommonProofRules::substitutivityRule(const Expr &e, const int changed, const Theorem &thm)=0 | CVC3::CommonProofRules | [pure virtual] |
symmetryRule(const Theorem &a1_eq_a2) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::symmetryRule(const Theorem &a1_eq_a2)=0 | CVC3::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)=0 | CVC3::CommonProofRules | [pure virtual] |
trueTheorem() | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::trueTheorem()=0 | CVC3::CommonProofRules | [pure virtual] |
varIntroRule(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::varIntroRule(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
varIntroSkolem(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::varIntroSkolem(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
withAssumptions() | CVC3::TheoremProducer | [inline] |
withProof() | CVC3::TheoremProducer | [inline] |
xorToIff(const Expr &e) | CVC3::CommonTheoremProducer | |
CVC3::CommonProofRules::xorToIff(const Expr &e)=0 | CVC3::CommonProofRules | [pure virtual] |
~CommonProofRules() | CVC3::CommonProofRules | [inline, virtual] |
~CommonTheoremProducer() | CVC3::CommonTheoremProducer | [inline, virtual] |
~TheoremProducer() | CVC3::TheoremProducer | [inline, virtual] |