CVC3::UFProofRules Class Reference

#include <uf_proof_rules.h>

Inherited by CVC3::UFTheoremProducer.

List of all members.

Public Member Functions

• virtual ~UFProofRules ()
• virtual Theorem relToClosure (const Theorem &rel)=0
• virtual Theorem relTrans (const Theorem &t1, const Theorem &t2)=0
• virtual Theorem applyLambda (const Expr &e)=0

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

• virtual Theorem rewriteOpDef (const Expr &e)=0

  Replace LETDECL in the operator with the definition.
  

---

Detailed Description

Definition at line 32 of file uf_proof_rules.h.

---

Constructor & Destructor Documentation

virtual CVC3::UFProofRules::~UFProofRules

(

)

[inline, virtual]

Definition at line 35 of file uf_proof_rules.h.

---

Member Function Documentation

virtual Theorem CVC3::UFProofRules::relToClosure

(

const Theorem &

rel

)

[pure virtual]

Implemented in CVC3::UFTheoremProducer.

Referenced by CVC3::TheoryUF::assertFact(), and CVC3::TheoryUF::update().

virtual Theorem CVC3::UFProofRules::relTrans	(	const Theorem &	t1,
		const Theorem &	t2
	)		[pure virtual]

Implemented in CVC3::UFTheoremProducer.

Referenced by CVC3::TheoryUF::assertFact().

virtual Theorem CVC3::UFProofRules::applyLambda

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::UFTheoremProducer.

Referenced by CVC3::TheoryUF::checkSat(), and CVC3::TheoryUF::rewrite().

virtual Theorem CVC3::UFProofRules::rewriteOpDef

(

const Expr &

e

)

[pure virtual]

Replace LETDECL in the operator with the definition.

Implemented in CVC3::UFTheoremProducer.

---

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

• uf_proof_rules.h