CVC3::DatatypeTheoremProducer Class Reference

#include <datatype_theorem_producer.h>

Inheritance diagram for CVC3::DatatypeTheoremProducer:

[legend]Collaboration diagram for CVC3::DatatypeTheoremProducer:

[legend]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::TheoremProducer::newTheorem(), and 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(), CVC3::TheoryDatatype::canCollapse(), CHECK_PROOFS, CHECK_SOUND, d_theoryDatatype, CVC3::Assumptions::emptyAssump(), CVC3::TheoryDatatype::getConstant(), CVC3::getConstructor(), CVC3::Type::getExpr(), CVC3::Expr::getOpExpr(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::Expr::getType(), CVC3::isConstructor(), CVC3::isSelector(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::CDList< T >::size(), and CVC3::TheoremProducer::withProof().

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, d_theoryDatatype, CVC3::Assumptions::emptyAssump(), CVC3::Theory::falseExpr(), CVC3::TheoryDatatype::getConsForTester(), CVC3::getConstructor(), CVC3::Expr::getOpExpr(), CVC3::isConstructor(), CVC3::isTester(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theory::trueExpr(), and CVC3::TheoremProducer::withProof().

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::Theorem::getLHS(), CVC3::Expr::getOpExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::isApply(), CVC3::isConstructor(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

Theorem DatatypeTheoremProducer::noCycle

(

const Expr &

e

)

[virtual]

Implements CVC3::DatatypeProofRules.

Definition at line 147 of file datatype_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::Type::arity(), CHECK_PROOFS, CHECK_SOUND, d_theoryDatatype, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOpExpr(), CVC3::TheoryDatatype::getReachablePredicate(), CVC3::Expr::getType(), CVC3::isConstructor(), CVC3::isDatatype(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().

---

Member Data Documentation

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

Definition at line 34 of file datatype_theorem_producer.h.

Referenced by noCycle(), rewriteSelCons(), and rewriteTestCons().

---

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

• datatype_theorem_producer.h
• datatype_theorem_producer.cpp

---