| decompose(const Theorem &e)=0 | CVC3::DatatypeProofRules | [pure virtual] |
| dummyTheorem(const CDList< Theorem > &facts, const Expr &e)=0 | CVC3::DatatypeProofRules | [pure virtual] |
| noCycle(const Expr &e)=0 | CVC3::DatatypeProofRules | [pure virtual] |
| rewriteSelCons(const CDList< Theorem > &facts, const Expr &e)=0 | CVC3::DatatypeProofRules | [pure virtual] |
| rewriteTestCons(const Expr &e)=0 | CVC3::DatatypeProofRules | [pure virtual] |
| ~DatatypeProofRules() | CVC3::DatatypeProofRules | [inline, virtual] |
1.5.1