CVCL::UFTheoremProducer Class Reference

#include <uf_theorem_producer.h>

Inheritance diagram for CVCL::UFTheoremProducer:

[legend]Collaboration diagram for CVCL::UFTheoremProducer:

[legend]List of all members.

Public Member Functions

• UFTheoremProducer (TheoremManager *tm, TheoryUF *theoryUF)

  Constructor.
  

• Theorem relToClosure (const Theorem &rel)
• Theorem relTrans (const Theorem &t1, const Theorem &t2)
• Theorem applyLambda (const Expr &e)

  Beta reduction: |- (lambda x. f(x))(arg) = f(arg).
  

• Theorem rewriteOpDef (const Expr &e)

  Replace CONSTDEF and LETDECL in the operator with the definition.
  

Private Attributes

• TheoryUF * d_theoryUF

---

Detailed Description

Definition at line 41 of file uf_theorem_producer.h.

---

Constructor & Destructor Documentation

CVCL::UFTheoremProducer::UFTheoremProducer (  TheoremManager *  tm, TheoryUF *  theoryUF )  [inline]

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

---

Member Function Documentation

Theorem UFTheoremProducer::relToClosure (  const Theorem &  rel  )  [virtual]

Implements CVCL::UFProofRules. Definition at line 62 of file uf_theorem_producer.cpp. References CVCL::Expr::arity(), CVCL::Assumptions::copy(), d_theoryUF, CVCL::Theorem::getAssumptions(), CVCL::Op::getExpr(), CVCL::Theorem::getExpr(), CVCL::Expr::getName(), CVCL::Expr::getOp(), CVCL::Theorem::getProof(), CVCL::Expr::isApply(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::TheoryUF::transClosureExpr(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem UFTheoremProducer::relTrans (  const Theorem &  t1, const Theorem &  t2 )  [virtual]

Implements CVCL::UFProofRules. Definition at line 87 of file uf_theorem_producer.cpp. References CVCL::Expr::arity(), CVCL::Theorem::getExpr(), CVCL::Expr::getName(), CVCL::Expr::getOp(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Theorem::getProof(), CVCL::merge(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::TRANS_CLOSURE, CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem UFTheoremProducer::applyLambda (  const Expr &  e  )  [virtual]

Beta reduction: |- (lambda x. f(x))(arg) = f(arg). Implements CVCL::UFProofRules. Definition at line 128 of file uf_theorem_producer.cpp. References CVCL::Expr::arity(), CVCL::Expr::getBody(), CVCL::Expr::getKids(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::Expr::getVars(), CVCL::Expr::isApply(), CVCL::Expr::isLambda(), CVCL::LAMBDA, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::substExpr(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

Theorem UFTheoremProducer::rewriteOpDef (  const Expr &  e  )  [virtual]

Replace CONSTDEF and LETDECL in the operator with the definition. Implements CVCL::UFProofRules. Definition at line 167 of file uf_theorem_producer.cpp. References CVCL::Expr::arity(), CVCL::CONSTDEF, CVCL::Expr::getKids(), CVCL::Expr::getKind(), CVCL::Expr::getOpExpr(), CVCL::Expr::isApply(), CVCL::LETDECL, CVCL::Expr::mkOp(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

---

Member Data Documentation

TheoryUF* CVCL::UFTheoremProducer::d_theoryUF [private]

Definition at line 42 of file uf_theorem_producer.h. Referenced by relToClosure().

---

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

• uf_theorem_producer.h
• uf_theorem_producer.cpp

---