CVCL::SimulateTheoremProducer Class Reference

#include <simulate_theorem_producer.h>

Inheritance diagram for CVCL::SimulateTheoremProducer:

[legend]Collaboration diagram for CVCL::SimulateTheoremProducer:

[legend]List of all members.

Public Member Functions

• SimulateTheoremProducer (TheoremManager *tm)

  Constructor.
  

• virtual ~SimulateTheoremProducer ()
• virtual Theorem expandSimulate (const Expr &e)

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

---

Detailed Description

Definition at line 38 of file simulate_theorem_producer.h.

---

Constructor & Destructor Documentation

CVCL::SimulateTheoremProducer::SimulateTheoremProducer (  TheoremManager *  tm  )  [inline]

Constructor. Definition at line 42 of file simulate_theorem_producer.h.

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

Definition at line 43 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 CVCL::SimulateProofRules. Definition at line 54 of file simulate_theorem_producer.cpp. References CVCL::Expr::arity(), CVCL::TheoremProducer::d_em, CVCL::Rational::getInt(), CVCL::Expr::getKind(), CVCL::Expr::getRational(), CVCL::int2string(), CVCL::isRational(), CVCL::TheoremProducer::newPf(), CVCL::ExprManager::newRatExpr(), CVCL::TheoremProducer::newRWTheorem(), CVCL::SIMULATE, CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

---

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

• simulate_theorem_producer.h
• simulate_theorem_producer.cpp

---