CVC3::UFProofRules Class Reference

#include <uf_proof_rules.h>

Inheritance diagram for CVC3::UFProofRules:

Inheritance graph
[legend]
List of all members.

Public Member Functions


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:
Generated on Wed Nov 18 16:18:35 2009 for CVC3 by  doxygen 1.5.2