CVCL::ReflexivityTheoremValue Class Reference

A special subclass for reflexivity theorems: e = e and e <=> e. More...

#include <theorem_value.h>

Inheritance diagram for CVCL::ReflexivityTheoremValue:

[legend]Collaboration diagram for CVCL::ReflexivityTheoremValue:

[legend]List of all members.

Private Member Functions

• ReflexivityTheoremValue (TheoremManager *tm, const Expr &e, const Proof &pf)
• ~ReflexivityTheoremValue ()
• bool isRewrite () const
• const Expr & getLHS () const
• const Expr & getRHS () const
• const Expr & getExpr () const
• MemoryManager * getMM ()
• void * operator new (size_t size, MemoryManager *mm)
• void operator delete (void *d)

Private Attributes

• Expr d_expr

Friends

• class Theorem

---

Detailed Description

A special subclass for reflexivity theorems: e = e and e <=> e.

Such theorems are created extremely often, and do not contain any useful information other than the expression itself.

Definition at line 295 of file theorem_value.h.

---

Constructor & Destructor Documentation

CVCL::ReflexivityTheoremValue::ReflexivityTheoremValue (  TheoremManager *  tm, const Expr &  e, const Proof &  pf )  [inline, private]

Definition at line 301 of file theorem_value.h.

CVCL::ReflexivityTheoremValue::~ReflexivityTheoremValue (   )  [inline, private]

Definition at line 304 of file theorem_value.h.

---

Member Function Documentation

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

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

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

Reimplemented from CVCL::TheoremValue. Definition at line 307 of file theorem_value.h. References d_expr.

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

Reimplemented from CVCL::TheoremValue. Definition at line 308 of file theorem_value.h. References d_expr.

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

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

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

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

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

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

void CVCL::ReflexivityTheoremValue::operator delete (  void *  d  )  [inline, private]

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

---

Friends And Related Function Documentation

friend class Theorem [friend]

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

---

Member Data Documentation

Expr CVCL::ReflexivityTheoremValue::d_expr [private]

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

---

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

• theorem_value.h

---