CVC3::CommonProofRules Member List

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

ackermann(const Expr &e1, const Expr &e2)=0CVC3::CommonProofRules [pure virtual]
andElim(const Theorem &e, int i)=0CVC3::CommonProofRules [pure virtual]
andIntro(const Theorem &e1, const Theorem &e2)=0CVC3::CommonProofRules [pure virtual]
andIntro(const std::vector< Theorem > &es)=0CVC3::CommonProofRules [pure virtual]
assumpRule(const Expr &a, int scope=-1)=0CVC3::CommonProofRules [pure virtual]
clearSkolemAxioms()=0CVC3::CommonProofRules [pure virtual]
contradictionRule(const Theorem &e, const Theorem &not_e)=0CVC3::CommonProofRules [pure virtual]
excludedMiddle(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
getSkolemAxioms()=0CVC3::CommonProofRules [pure virtual]
iffContrapositive(const Theorem &thm)=0CVC3::CommonProofRules [pure virtual]
iffFalseElim(const Theorem &e)=0CVC3::CommonProofRules [pure virtual]
iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0CVC3::CommonProofRules [pure virtual]
iffNotFalse(const Theorem &e)=0CVC3::CommonProofRules [pure virtual]
iffTrue(const Theorem &e)=0CVC3::CommonProofRules [pure virtual]
iffTrueElim(const Theorem &e)=0CVC3::CommonProofRules [pure virtual]
implContrapositive(const Theorem &thm)=0CVC3::CommonProofRules [pure virtual]
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)=0CVC3::CommonProofRules [pure virtual]
implMP(const Theorem &e1, const Theorem &e1_impl_e2)=0CVC3::CommonProofRules [pure virtual]
liftOneITE(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
notNotElim(const Theorem &not_not_e)=0CVC3::CommonProofRules [pure virtual]
notToIff(const Theorem &not_e)=0CVC3::CommonProofRules [pure virtual]
queryTCC(const Theorem &phi, const Theorem &D_phi)=0CVC3::CommonProofRules [pure virtual]
reflexivityRule(const Expr &a)=0CVC3::CommonProofRules [pure virtual]
rewriteAnd(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
rewriteAnd(const Theorem &e)=0CVC3::CommonProofRules [pure virtual]
rewriteIff(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
rewriteIteFalse(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
rewriteIteSame(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
rewriteIteTrue(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
rewriteNotExists(const Expr &existsExpr)=0CVC3::CommonProofRules [pure virtual]
rewriteNotFalse(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
rewriteNotForall(const Expr &forallExpr)=0CVC3::CommonProofRules [pure virtual]
rewriteNotNot(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
rewriteNotTrue(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
rewriteOr(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
rewriteOr(const Theorem &e)=0CVC3::CommonProofRules [pure virtual]
rewriteReflexivity(const Expr &a_eq_a)=0CVC3::CommonProofRules [pure virtual]
rewriteUsingSymmetry(const Expr &a1_eq_a2)=0CVC3::CommonProofRules [pure virtual]
skolemize(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
skolemize(const Theorem &thm)=0CVC3::CommonProofRules [pure virtual]
skolemizeRewrite(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
skolemizeRewriteVar(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
substitutivityRule(const Expr &e, const Theorem &thm)=0CVC3::CommonProofRules [pure virtual]
substitutivityRule(const Expr &e, const Theorem &thm1, const Theorem &thm2)=0CVC3::CommonProofRules [pure virtual]
substitutivityRule(const Op &op, const std::vector< Theorem > &thms)=0CVC3::CommonProofRules [pure virtual]
substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)=0CVC3::CommonProofRules [pure virtual]
substitutivityRule(const Expr &e, const int changed, const Theorem &thm)=0CVC3::CommonProofRules [pure virtual]
symmetryRule(const Theorem &a1_eq_a2)=0CVC3::CommonProofRules [pure virtual]
transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0CVC3::CommonProofRules [pure virtual]
trueTheorem()=0CVC3::CommonProofRules [pure virtual]
varIntroRule(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
varIntroSkolem(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
xorToIff(const Expr &e)=0CVC3::CommonProofRules [pure virtual]
~CommonProofRules()CVC3::CommonProofRules [inline, virtual]


Generated on Thu Oct 15 22:18:11 2009 for CVC3 by  doxygen 1.5.8