24 #ifndef _cvc3__theory_datatype__datatype_proof_rules_h_
25 #define _cvc3__theory_datatype__datatype_proof_rules_h_
31 template<
class T>
class CDList;
Data structure of expressions in CVC3.
virtual ~DatatypeProofRules()
virtual Theorem rewriteSelCons(const CDList< Theorem > &facts, const Expr &e)=0
virtual Theorem decompose(const Theorem &e)=0
virtual Theorem noCycle(const Expr &e)=0
virtual Theorem dummyTheorem(const CDList< Theorem > &facts, const Expr &e)=0
virtual Theorem rewriteTestCons(const Expr &e)=0