CVCL::DatatypeTheoremProducer Class Reference

#include <datatype_theorem_producer.h>

Inheritance diagram for CVCL::DatatypeTheoremProducer:

[legend]Collaboration diagram for CVCL::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 41 of file datatype_theorem_producer.h.

---

Constructor & Destructor Documentation

CVCL::DatatypeTheoremProducer::DatatypeTheoremProducer (  TheoryDatatype *  theoryDatatype  )  [inline]

Constructor. Definition at line 46 of file datatype_theorem_producer.h.

---

Member Function Documentation

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

Implements CVCL::DatatypeProofRules. Definition at line 60 of file datatype_theorem_producer.cpp. References CVCL::TheoremProducer::newTheorem(), and CVCL::CDList< T >::size().

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

Implements CVCL::DatatypeProofRules. Definition at line 71 of file datatype_theorem_producer.cpp. References CVCL::Expr::arity(), CVCL::TheoryDatatype::canCollapse(), d_theoryDatatype, CVCL::TheoryDatatype::getConstant(), CVCL::getConstructor(), CVCL::Type::getExpr(), CVCL::Expr::getOpExpr(), CVCL::TheoryDatatype::getSelectorInfo(), CVCL::Expr::getType(), CVCL::isConstructor(), CVCL::isSelector(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::CDList< T >::size(), and CVCL::TheoremProducer::withProof().

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

Implements CVCL::DatatypeProofRules. Definition at line 108 of file datatype_theorem_producer.cpp. References d_theoryDatatype, CVCL::Theory::falseExpr(), CVCL::TheoryDatatype::getConsForTester(), CVCL::getConstructor(), CVCL::Expr::getOpExpr(), CVCL::isConstructor(), CVCL::isTester(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Theory::trueExpr(), and CVCL::TheoremProducer::withProof().

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

Implements CVCL::DatatypeProofRules. Definition at line 128 of file datatype_theorem_producer.cpp. References CVCL::andExpr(), CVCL::Expr::arity(), CVCL::Expr::eqExpr(), CVCL::Theorem::getLHS(), CVCL::Expr::getOpExpr(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Expr::isApply(), CVCL::isConstructor(), CVCL::Theorem::isRewrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), and CVCL::TheoremProducer::withProof().

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

Implements CVCL::DatatypeProofRules. Definition at line 157 of file datatype_theorem_producer.cpp. References CVCL::andExpr(), CVCL::Expr::arity(), CVCL::Type::arity(), d_theoryDatatype, CVCL::Expr::getOpExpr(), CVCL::TheoryDatatype::getReachablePredicate(), CVCL::Expr::getType(), CVCL::isConstructor(), CVCL::isDatatype(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), and CVCL::TheoremProducer::withProof().

---

Member Data Documentation

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

Definition at line 42 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

---