| andElim(const Theorem &e, int i)=0 | CVCL::CommonProofRules | [pure virtual] |
| andIntro(const Theorem &e1, const Theorem &e2)=0 | CVCL::CommonProofRules | [pure virtual] |
| andIntro(const std::vector< Theorem > &es)=0 | CVCL::CommonProofRules | [pure virtual] |
| assumpRule(const Expr &a, int scope=-1)=0 | CVCL::CommonProofRules | [pure virtual] |
| clearSkolemAxioms()=0 | CVCL::CommonProofRules | [pure virtual] |
| contradictionRule(const Theorem &e, const Theorem ¬_e)=0 | CVCL::CommonProofRules | [pure virtual] |
| getSkolemAxioms()=0 | CVCL::CommonProofRules | [pure virtual] |
| iffContrapositive(const Theorem &thm)=0 | CVCL::CommonProofRules | [pure virtual] |
| iffFalseElim(const Theorem &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0 | CVCL::CommonProofRules | [pure virtual] |
| iffNotFalse(const Theorem &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| iffTrue(const Theorem &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| iffTrueElim(const Theorem &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| implContrapositive(const Theorem &thm)=0 | CVCL::CommonProofRules | [pure virtual] |
| implIntro(const Theorem &phi, const std::vector< Expr > &assump)=0 | CVCL::CommonProofRules | [pure virtual] |
| implMP(const Theorem &e1, const Theorem &e1_impl_e2)=0 | CVCL::CommonProofRules | [pure virtual] |
| notNotElim(const Theorem ¬_not_e)=0 | CVCL::CommonProofRules | [pure virtual] |
| notToIff(const Theorem ¬_e)=0 | CVCL::CommonProofRules | [pure virtual] |
| reflexivityRule(const Expr &a)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteAnd(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteAnd(const Theorem &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteIff(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteNotExists(const Expr &existsExpr)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteNotFalse(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteNotForall(const Expr &forallExpr)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteNotNot(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteNotTrue(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteOr(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteOr(const Theorem &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteReflexivity(const Expr &a_eq_a)=0 | CVCL::CommonProofRules | [pure virtual] |
| rewriteUsingSymmetry(const Expr &a1_eq_a2)=0 | CVCL::CommonProofRules | [pure virtual] |
| skolemize(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| skolemize(const Theorem &thm)=0 | CVCL::CommonProofRules | [pure virtual] |
| skolemizeRewrite(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| skolemizeRewriteVar(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| substitutivityRule(const Op &op, const std::vector< Theorem > &thms)=0 | CVCL::CommonProofRules | [pure virtual] |
| substitutivityRule(const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)=0 | CVCL::CommonProofRules | [pure virtual] |
| symmetryRule(const Theorem &a1_eq_a2)=0 | CVCL::CommonProofRules | [pure virtual] |
| transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0 | CVCL::CommonProofRules | [pure virtual] |
| trueTheorem()=0 | CVCL::CommonProofRules | [pure virtual] |
| varIntroRule(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| varIntroSkolem(const Expr &e)=0 | CVCL::CommonProofRules | [pure virtual] |
| ~CommonProofRules() | CVCL::CommonProofRules | [inline, virtual] |
