CVC3::UFTheoremProducer Class Reference

#include <uf_theorem_producer.h>

Inherits CVC3::UFProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::UFTheoremProducer:

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 LETDECL in the operator with the definition.
  

Private Attributes

• TheoryUF * d_theoryUF

---

Detailed Description

Definition at line 33 of file uf_theorem_producer.h.

---

Constructor & Destructor Documentation

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

Constructor.

Definition at line 38 of file uf_theorem_producer.h.

---

Member Function Documentation

Theorem UFTheoremProducer::relToClosure

(

const Theorem &

rel

)

[virtual]

Implements CVC3::UFProofRules.

Definition at line 54 of file uf_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Theorem::getAssumptionsRef(), CVC3::Op::getExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getName(), CVC3::Expr::getOp(), CVC3::Theorem::getProof(), CVC3::Expr::isApply(), and CVC3::Expr::toString().

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

Implements CVC3::UFProofRules.

Definition at line 76 of file uf_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Theorem::getExpr(), CVC3::Expr::getName(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::Expr::toString(), and CVC3::TRANS_CLOSURE.

Theorem UFTheoremProducer::applyLambda

(

const Expr &

e

)

[virtual]

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

Implements CVC3::UFProofRules.

Definition at line 114 of file uf_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getKids(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getVars(), CVC3::Expr::isApply(), LAMBDA, and CVC3::Expr::toString().

Theorem UFTheoremProducer::rewriteOpDef

(

const Expr &

e

)

[virtual]

Replace LETDECL in the operator with the definition.

Implements CVC3::UFProofRules.

Definition at line 149 of file uf_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getOpExpr(), CVC3::Expr::isApply(), LETDECL, CVC3::Expr::mkOp(), and CVC3::Expr::toString().

---

Member Data Documentation

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

Definition at line 34 of file uf_theorem_producer.h.

---

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

• uf_theorem_producer.h
• uf_theorem_producer.cpp