CVC3::UFTheoremProducer Class Reference

#include <uf_theorem_producer.h>

Inheritance diagram for CVC3::UFTheoremProducer:
CVC3::UFProofRules CVC3::TheoremProducer

List of all members.

Public Member Functions

Private Attributes


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]
Theorem UFTheoremProducer::relTrans ( const Theorem t1,
const Theorem t2 
) [virtual]
Theorem UFTheoremProducer::applyLambda ( const Expr e  )  [virtual]
Theorem UFTheoremProducer::rewriteOpDef ( const Expr e  )  [virtual]

Member Data Documentation

Definition at line 34 of file uf_theorem_producer.h.

Referenced by relToClosure().


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

Generated on 19 Nov 2009 for CVC3 by  doxygen 1.6.1