| andDistributivityRule(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| AndToIte(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| iffAndDistrib(const Expr &iff)=0 | CVC3::CoreProofRules | [pure virtual] |
| iffOrDistrib(const Expr &iff)=0 | CVC3::CoreProofRules | [pure virtual] |
| IffToIte(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| ifLiftUnaryRule(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| ImpToIte(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| NotToIte(const Expr ¬_e)=0 | CVC3::CoreProofRules | [pure virtual] |
| orDistributivityRule(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| OrToIte(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteAndSubterms(const Expr &e, int idx)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteDistinct(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteImplies(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteBool(const Expr &c, const Expr &e1, const Expr &e2)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteCond(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteElse(const Expr &e, const Theorem &elseThm)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteFalse(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteSame(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteThen(const Expr &e, const Theorem &thenThm)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteToAnd(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteToIff(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteToImp(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteToNot(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteToOr(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteIteTrue(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteLetDecl(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteNotAnd(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteNotIff(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteNotIte(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteNotOr(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| rewriteOrSubterms(const Expr &e, int idx)=0 | CVC3::CoreProofRules | [pure virtual] |
| typePred(const Expr &e)=0 | CVC3::CoreProofRules | [pure virtual] |
| ~CoreProofRules() | CVC3::CoreProofRules | [inline, virtual] |
1.5.1