CVC3: CVC3::DatatypeTheoremProducer Class Reference

CVC3

#include <datatype_theorem_producer.h>

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

Collaboration diagram for CVC3::DatatypeTheoremProducer:

Collaboration graph

List of all members.

Public Member Functions

DatatypeTheoremProducer (TheoryDatatype *theoryDatatype)
Constructor.
Theorem dummyTheorem (const CDList< Theorem > &facts, const Expr &e)
Theorem rewriteSelCons (const CDList< Theorem > &facts, const Expr &e)
Theorem rewriteTestCons (const Expr &e)
Theorem decompose (const Theorem &e)
Theorem noCycle (const Expr &e)

Private Attributes

TheoryDatatype * d_theoryDatatype

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

Implements CVC3::DatatypeProofRules.

Definition at line 63 of file datatype_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::getConstructor(), CVC3::Type::getExpr(), CVC3::Expr::getOpExpr(), CVC3::Expr::getType(), CVC3::isConstructor(), CVC3::isSelector(), and CVC3::CDList< T >::size().

Theorem DatatypeTheoremProducer::rewriteTestCons ( const Expr & e ) [virtual]

Implements CVC3::DatatypeProofRules.

Definition at line 99 of file datatype_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::getConstructor(), CVC3::Expr::getOpExpr(), CVC3::isConstructor(), and CVC3::isTester().

Theorem DatatypeTheoremProducer::decompose ( const Theorem & e ) [virtual]

Implements CVC3::DatatypeProofRules.

Definition at line 118 of file datatype_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::eqExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::isApply(), CVC3::isConstructor(), and CVC3::Theorem::isRewrite().

Theorem DatatypeTheoremProducer::noCycle ( const Expr & e ) [virtual]

Implements CVC3::DatatypeProofRules.

Definition at line 147 of file datatype_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Type::arity(), CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getOpExpr(), CVC3::Expr::getType(), CVC3::Expr::isApply(), CVC3::isConstructor(), and CVC3::isDatatype().

Member Data Documentation

TheoryDatatype* CVC3::DatatypeTheoremProducer::d_theoryDatatype [private]

Definition at line 34 of file datatype_theorem_producer.h.

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