CVC3::SimulateTheoremProducer Class Reference

#include <simulate_theorem_producer.h>

Inherits CVC3::SimulateProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::SimulateTheoremProducer:

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::Rational::getInt(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::int2string(), CVC3::isRational(), SIMULATE, and CVC3::Expr::toString().

---

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

• simulate_theorem_producer.h
• simulate_theorem_producer.cpp