Public Member Functions | Private Attributes

CVC3::UFTheoremProducer Class Reference

#include <uf_theorem_producer.h>

Inherits CVC3::UFProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::UFTheoremProducer:
Collaboration graph

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]


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.

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