CVC3::SimulateTheoremProducer Class Reference

#include <simulate_theorem_producer.h>

Inheritance diagram for CVC3::SimulateTheoremProducer:

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

Collaboration graph
[legend]
List of all members.

Public Member Functions


Detailed Description

Definition at line 30 of file simulate_theorem_producer.h.


Constructor & Destructor Documentation

CVC3::SimulateTheoremProducer::SimulateTheoremProducer ( TheoremManager tm  )  [inline]

Constructor.

Definition at line 34 of file simulate_theorem_producer.h.

virtual CVC3::SimulateTheoremProducer::~SimulateTheoremProducer (  )  [inline, virtual]

Definition at line 35 of file simulate_theorem_producer.h.


Member Function Documentation

Theorem SimulateTheoremProducer::expandSimulate ( const Expr e  )  [virtual]

SIMULATE(f, s_0, i_1, ..., i_k, N) <=> f(...f(f(s_0, i_1), i_2), ... i_k).

Implements CVC3::SimulateProofRules.

Definition at line 46 of file simulate_theorem_producer.cpp.

References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Rational::getInt(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::TheoremProducer::newRWTheorem(), CVC3::SIMULATE, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().


The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:18:35 2009 for CVC3 by  doxygen 1.5.2