CVC3::UFTheoremProducer Class Reference

#include <uf_theorem_producer.h>

Inheritance diagram for CVC3::UFTheoremProducer:

Inheritance graph
[legend]
Collaboration diagram for CVC3::UFTheoremProducer:

Collaboration graph
[legend]
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]

Implements CVC3::UFProofRules.

Definition at line 54 of file uf_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, d_theoryUF, CVC3::Theorem::getAssumptionsRef(), CVC3::Op::getExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getName(), CVC3::Expr::getOp(), CVC3::Theorem::getProof(), CVC3::Expr::isApply(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::TheoryUF::transClosureExpr(), and CVC3::TheoremProducer::withProof().

Theorem UFTheoremProducer::relTrans ( const Theorem t1,
const Theorem t2 
) [virtual]

Implements CVC3::UFProofRules.

Definition at line 76 of file uf_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CLASS_NAME, CVC3::Theorem::getExpr(), CVC3::Expr::getName(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::TRANS_CLOSURE, and CVC3::TheoremProducer::withProof().

Theorem UFTheoremProducer::applyLambda ( const Expr e  )  [virtual]

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

Implements CVC3::UFProofRules.

Definition at line 114 of file uf_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), CVC3::LAMBDA, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem UFTheoremProducer::rewriteOpDef ( const Expr e  )  [virtual]

Replace LETDECL in the operator with the definition.

Implements CVC3::UFProofRules.

Definition at line 149 of file uf_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getOpExpr(), CVC3::Expr::isApply(), CVC3::LETDECL, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().


Member Data Documentation

TheoryUF* CVC3::UFTheoremProducer::d_theoryUF [private]

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