CVC3
Public Member Functions | Private Attributes

CVC3::DatatypeTheoremProducer Class Reference

#include <datatype_theorem_producer.h>

Inherits CVC3::DatatypeProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::DatatypeTheoremProducer:
Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Attributes


Detailed Description

Definition at line 33 of file datatype_theorem_producer.h.


Constructor & Destructor Documentation

CVC3::DatatypeTheoremProducer::DatatypeTheoremProducer ( TheoryDatatype theoryDatatype) [inline]

Constructor.

Definition at line 38 of file datatype_theorem_producer.h.


Member Function Documentation

Theorem DatatypeTheoremProducer::dummyTheorem ( const CDList< Theorem > &  facts,
const Expr e 
) [virtual]

Implements CVC3::DatatypeProofRules.

Definition at line 52 of file datatype_theorem_producer.cpp.

References CVC3::CDList< T >::size().

Theorem DatatypeTheoremProducer::rewriteSelCons ( const CDList< Theorem > &  facts,
const Expr e 
) [virtual]
Theorem DatatypeTheoremProducer::rewriteTestCons ( const Expr e) [virtual]
Theorem DatatypeTheoremProducer::decompose ( const Theorem e) [virtual]
Theorem DatatypeTheoremProducer::noCycle ( const Expr e) [virtual]

Member Data Documentation

Definition at line 34 of file datatype_theorem_producer.h.


The documentation for this class was generated from the following files: