CVCL::RWTheoremValue Class Reference

#include <theorem_value.h>

Inheritance diagram for CVCL::RWTheoremValue:

[legend]Collaboration diagram for CVCL::RWTheoremValue:

[legend]List of all members.

Public Member Functions

• ~RWTheoremValue ()
• bool isRewrite () const
• MemoryManager * getMM ()
• void * operator new (size_t size, MemoryManager *mm)
• void operator delete (void *d)

Protected Attributes

• Expr d_lhs
• Expr d_rhs

Private Member Functions

• RWTheoremValue (TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
• RWTheoremValue (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
• const Expr & getExpr () const
• const Expr & getLHS () const
• const Expr & getRHS () const

Friends

• class Theorem

---

Detailed Description

Definition at line 235 of file theorem_value.h.

---

Constructor & Destructor Documentation

CVCL::RWTheoremValue::RWTheoremValue (  TheoremManager *  tm, const Expr &  lhs, const Expr &  rhs, const Assumptions &  assump, const Proof &  pf, bool  isAssump, int  scope = -1 )  [inline, private]

Definition at line 247 of file theorem_value.h.

CVCL::RWTheoremValue::RWTheoremValue (  TheoremManager *  tm, const Expr &  thm, const Assumptions &  assump, const Proof &  pf, bool  isAssump, int  scope = -1 )  [inline, private]

Definition at line 254 of file theorem_value.h.

CVCL::RWTheoremValue::~RWTheoremValue (   )  [inline]

Definition at line 276 of file theorem_value.h.

---

Member Function Documentation

const Expr& CVCL::RWTheoremValue::getExpr (   )  const [inline, private, virtual]

Reimplemented from CVCL::TheoremValue. Definition at line 260 of file theorem_value.h. References d_lhs, d_rhs, CVCL::TheoremValue::d_thm, CVCL::Expr::eqExpr(), CVCL::Expr::getType(), CVCL::Expr::iffExpr(), CVCL::Type::isBool(), and CVCL::Expr::isNull().

const Expr& CVCL::RWTheoremValue::getLHS (   )  const [inline, private, virtual]

Reimplemented from CVCL::TheoremValue. Definition at line 271 of file theorem_value.h. References d_lhs.

const Expr& CVCL::RWTheoremValue::getRHS (   )  const [inline, private, virtual]

Reimplemented from CVCL::TheoremValue. Definition at line 272 of file theorem_value.h. References d_rhs.

bool CVCL::RWTheoremValue::isRewrite (   )  const [inline, virtual]

Reimplemented from CVCL::TheoremValue. Definition at line 278 of file theorem_value.h.

MemoryManager* CVCL::RWTheoremValue::getMM (   )  [inline, virtual]

Reimplemented from CVCL::TheoremValue. Definition at line 281 of file theorem_value.h. References CVCL::TheoremValue::d_tm, and CVCL::TheoremManager::getRWMM().

void* CVCL::RWTheoremValue::operator new (  size_t  size, MemoryManager *  mm )  [inline]

Reimplemented from CVCL::TheoremValue. Definition at line 283 of file theorem_value.h. References CVCL::MemoryManager::newData().

void CVCL::RWTheoremValue::operator delete (  void *  d  )  [inline]

Reimplemented from CVCL::TheoremValue. Definition at line 287 of file theorem_value.h.

---

Friends And Related Function Documentation

friend class Theorem [friend]

Reimplemented from CVCL::TheoremValue. Definition at line 237 of file theorem_value.h.

---

Member Data Documentation

Expr CVCL::RWTheoremValue::d_lhs [protected]

Definition at line 242 of file theorem_value.h. Referenced by getExpr(), and getLHS().

Expr CVCL::RWTheoremValue::d_rhs [protected]

Definition at line 243 of file theorem_value.h. Referenced by getExpr(), and getRHS().

---

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

• theorem_value.h

---