CVCL::UFProofRules Class Reference

#include <uf_proof_rules.h>

Inheritance diagram for CVCL::UFProofRules:

[legend]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 CONSTDEF and LETDECL in the operator with the definition.
  

---

Detailed Description

Definition at line 40 of file uf_proof_rules.h.

---

Constructor & Destructor Documentation

virtual CVCL::UFProofRules::~UFProofRules (   )  [inline, virtual]

Definition at line 43 of file uf_proof_rules.h.

---

Member Function Documentation

virtual Theorem CVCL::UFProofRules::relToClosure (  const Theorem &  rel  )  [pure virtual]

Implemented in CVCL::UFTheoremProducer. Referenced by CVCL::TheoryUF::assertFact(), and CVCL::TheoryUF::update().

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

Implemented in CVCL::UFTheoremProducer. Referenced by CVCL::TheoryUF::assertFact().

virtual Theorem CVCL::UFProofRules::applyLambda (  const Expr &  e  )  [pure virtual]

Beta reduction: |- (lambda x. f(x))(arg) = f(arg). Implemented in CVCL::UFTheoremProducer. Referenced by CVCL::TheoryUF::checkSat(), and CVCL::TheoryUF::rewrite().

virtual Theorem CVCL::UFProofRules::rewriteOpDef (  const Expr &  e  )  [pure virtual]

Replace CONSTDEF and LETDECL in the operator with the definition. Implemented in CVCL::UFTheoremProducer. Referenced by CVCL::TheoryUF::rewrite().

---

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

• uf_proof_rules.h

---