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] |