23 #ifndef _cvc3__theory_datatype__datatype_theorem_producer_h_
24 #define _cvc3__theory_datatype__datatype_theorem_producer_h_
40 d_theoryDatatype(theoryDatatype) { }
Data structure of expressions in CVC3.
Theorem noCycle(const Expr &e)
DatatypeTheoremProducer(TheoryDatatype *theoryDatatype)
Constructor.
Theorem rewriteSelCons(const CDList< Theorem > &facts, const Expr &e)
Theorem decompose(const Theorem &e)
Abstract interface for recursive datatype proof rules.
This theory handles datatypes.
Theorem dummyTheorem(const CDList< Theorem > &facts, const Expr &e)
Theorem rewriteTestCons(const Expr &e)
TheoryDatatype * d_theoryDatatype