CVC3::SimulateTheoremProducer Class Reference

#include <simulate_theorem_producer.h>

Inheritance diagram for CVC3::SimulateTheoremProducer:

[legend]

Collaboration diagram for CVC3::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 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::int2string(), 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:

• simulate_theorem_producer.h
• simulate_theorem_producer.cpp