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