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