CVC3::UFTheoremProducer Class Reference

#include <uf_theorem_producer.h>

Inheritance diagram for CVC3::UFTheoremProducer:

[legend]

Collaboration diagram for CVC3::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 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, d_theoryUF, CVC3::Theorem::getAssumptionsRef(), CVC3::Op::getExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getName(), CVC3::Expr::getOp(), CVC3::Theorem::getProof(), CVC3::Expr::isApply(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::TheoryUF::transClosureExpr(), and CVC3::TheoremProducer::withProof().

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::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::TRANS_CLOSURE, and CVC3::TheoremProducer::withProof().

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::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), CVC3::LAMBDA, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

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::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getOpExpr(), CVC3::Expr::isApply(), CVC3::LETDECL, CVC3::Expr::mkOp(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

---

Member Data Documentation

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

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