CVCL::TheoremValue Class Reference

#include <theorem_value.h>

Inheritance diagram for CVCL::TheoremValue:

[legend]Collaboration diagram for CVCL::TheoremValue:

[legend]List of all members.

Public Member Functions

virtual ~TheoremValue ()
std::string toString () const
virtual MemoryManager * getMM ()
void * operator new (size_t size, MemoryManager *mm)
void operator delete (void *d)

Protected Attributes

TheoremManager * d_tm
Theorem Manager.
Expr d_thm
The expression representing a theorem.
Assumptions d_assump
The assumptions for the theorem.
Proof d_proof
Proof of the theorem.
int d_refcount: 16
How many pointers to this theorem value.
int d_scopeLevel: 16
Largest scope level of the assumptions.
unsigned d_flag
Temporary flag used during traversals.
int d_cachedValue: 29
Temporary cache used during traversals.
bool d_isAssump: 1
bool d_expand: 1
whether it should this be expanded in graph traversal
bool d_clauselit: 1
whether it belongs to the conflict clause

Private Member Functions

TheoremValue (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump, int scope=-1)
TheoremValue (const TheoremValue &t)
TheoremValue & operator= (const TheoremValue &t)
bool isFlagged () const
void clearAllFlags ()
void setFlag ()
void setCachedValue (int value)
int getCachedValue () const
void setExpandFlag (bool val)
bool getExpandFlag ()
void setLitFlag (bool val)
bool getLitFlag ()
int getScope ()
virtual bool isRewrite () const
virtual const Expr & getExpr () const
virtual const Expr & getLHS () const
virtual const Expr & getRHS () const
const Assumptions & getAssumptionsRef () const
bool isAssump () const
const Proof & getProof ()

Friends

Detailed Description

Definition at line 61 of file theorem_value.h.

Constructor & Destructor Documentation

CVCL::TheoremValue::TheoremValue ( TheoremManager * tm,

const Expr & thm,

const Assumptions & assump,

const Proof & pf,

bool isAssump,

int scope = -1

) [inline, private]

NOTE: it is private; only friend classes can call it.
If the assumptions refer to only one theorem, grab the assumptions of that theorem instead.
Definition at line 106 of file theorem_value.h.
References CVCL::Assumptions::begin(), d_assump, d_scopeLevel, d_tm, CVCL::Assumptions::empty(), CVCL::Assumptions::end(), CVCL::TheoremManager::getCM(), CVCL::TheoremManager::isActive(), CVCL::Assumptions::isNull(), CVCL::ContextManager::scopeLevel(), and CVCL::Assumptions::setConst().

CVCL::TheoremValue::TheoremValue ( const TheoremValue & t ) [inline, private]

Definition at line 130 of file theorem_value.h.

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

Definition at line 204 of file theorem_value.h.
References d_refcount.

Member Function Documentation

TheoremValue& CVCL::TheoremValue::operator= ( const TheoremValue & t ) [inline, private]

Definition at line 133 of file theorem_value.h.

bool CVCL::TheoremValue::isFlagged ( ) const [inline, private]

Definition at line 138 of file theorem_value.h.
References d_flag, d_tm, and CVCL::TheoremManager::getFlag().
Referenced by CVCL::Theorem::isFlagged().

void CVCL::TheoremValue::clearAllFlags ( ) [inline, private]

Definition at line 142 of file theorem_value.h.
References CVCL::TheoremManager::clearAllFlags(), and d_tm.
Referenced by CVCL::Theorem::clearAllFlags().

void CVCL::TheoremValue::setFlag ( ) [inline, private]

Definition at line 146 of file theorem_value.h.
References d_flag, d_tm, and CVCL::TheoremManager::getFlag().
Referenced by CVCL::Theorem::setFlag().

void CVCL::TheoremValue::setCachedValue ( int value ) [inline, private]

Definition at line 150 of file theorem_value.h.
References d_cachedValue.
Referenced by CVCL::Theorem::setCachedValue().

int CVCL::TheoremValue::getCachedValue ( ) const [inline, private]

Definition at line 154 of file theorem_value.h.
References d_cachedValue.
Referenced by CVCL::Theorem::getCachedValue().

void CVCL::TheoremValue::setExpandFlag ( bool val ) [inline, private]

Definition at line 158 of file theorem_value.h.
References d_expand.
Referenced by CVCL::Theorem::setExpandFlag().

bool CVCL::TheoremValue::getExpandFlag ( ) [inline, private]

Definition at line 162 of file theorem_value.h.
References d_expand.
Referenced by CVCL::Theorem::getExpandFlag().

void CVCL::TheoremValue::setLitFlag ( bool val ) [inline, private]

Definition at line 166 of file theorem_value.h.
References d_clauselit.
Referenced by CVCL::Theorem::setLitFlag().

bool CVCL::TheoremValue::getLitFlag ( ) [inline, private]

Definition at line 170 of file theorem_value.h.
References d_clauselit.
Referenced by CVCL::Theorem::getLitFlag().

int CVCL::TheoremValue::getScope ( ) [inline, private]

Definition at line 174 of file theorem_value.h.
References d_scopeLevel.
Referenced by CVCL::Theorem::getScope().

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

Reimplemented in CVCL::RWTheoremValue, and CVCL::ReflexivityTheoremValue.
Definition at line 179 of file theorem_value.h.
Referenced by getLHS(), getRHS(), and CVCL::Theorem::isRewrite().

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

Reimplemented in CVCL::RWTheoremValue, and CVCL::ReflexivityTheoremValue.
Definition at line 181 of file theorem_value.h.
References d_thm.
Referenced by CVCL::Theorem::getExpr(), and toString().

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

Reimplemented in CVCL::RWTheoremValue, and CVCL::ReflexivityTheoremValue.
Definition at line 182 of file theorem_value.h.
References d_thm, isRewrite(), and toString().
Referenced by CVCL::Theorem::getLHS().

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

Reimplemented in CVCL::RWTheoremValue, and CVCL::ReflexivityTheoremValue.
Definition at line 189 of file theorem_value.h.
References d_thm, isRewrite(), and toString().
Referenced by CVCL::Theorem::getRHS().

const Assumptions& CVCL::TheoremValue::getAssumptionsRef ( ) const [inline, private]

Definition at line 197 of file theorem_value.h.
References d_assump.
Referenced by CVCL::Theorem::getAssumptionsRef().

bool CVCL::TheoremValue::isAssump ( ) const [inline, private]

Definition at line 199 of file theorem_value.h.
References d_isAssump.
Referenced by CVCL::Theorem::getAssumptions(), and CVCL::Theorem::isAssump().

const Proof& CVCL::TheoremValue::getProof ( ) [inline, private]

Definition at line 200 of file theorem_value.h.
References d_proof.
Referenced by CVCL::Theorem::getProof().

std::string CVCL::TheoremValue::toString ( ) const [inline]

Definition at line 209 of file theorem_value.h.
References d_assump, getExpr(), CVCL::Expr::toString(), and CVCL::Assumptions::toString().
Referenced by getLHS(), and getRHS().

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

Reimplemented in CVCL::RWTheoremValue, and CVCL::ReflexivityTheoremValue.
Definition at line 214 of file theorem_value.h.
References d_tm, and CVCL::TheoremManager::getMM().
Referenced by CVCL::Theorem::operator=(), and CVCL::Theorem::~Theorem().

void* CVCL::TheoremValue::operator new ( size_t size,

MemoryManager * mm

) [inline]

Reimplemented in CVCL::RWTheoremValue, and CVCL::ReflexivityTheoremValue.
Definition at line 216 of file theorem_value.h.
References CVCL::MemoryManager::newData().

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

Reimplemented in CVCL::RWTheoremValue, and CVCL::ReflexivityTheoremValue.
Definition at line 220 of file theorem_value.h.

Friends And Related Function Documentation

friend class Theorem [friend]

Reimplemented in CVCL::RWTheoremValue, and CVCL::ReflexivityTheoremValue.
Definition at line 64 of file theorem_value.h.

friend class RWTheoremValue [friend]

Definition at line 65 of file theorem_value.h.

friend class ReflexivityTheoremValue [friend]

Definition at line 66 of file theorem_value.h.

Member Data Documentation

TheoremManager* CVCL::TheoremValue::d_tm [protected]

Theorem Manager.

Definition at line 70 of file theorem_value.h.
Referenced by clearAllFlags(), CVCL::ReflexivityTheoremValue::getMM(), CVCL::RWTheoremValue::getMM(), getMM(), isFlagged(), setFlag(), TheoremValue(), CVCL::Theorem::withAssumptions(), and CVCL::Theorem::withProof().

Expr CVCL::TheoremValue::d_thm [protected]

The expression representing a theorem.

Definition at line 73 of file theorem_value.h.
Referenced by CVCL::ReflexivityTheoremValue::getExpr(), CVCL::RWTheoremValue::getExpr(), getExpr(), getLHS(), and getRHS().

Assumptions CVCL::TheoremValue::d_assump [protected]

The assumptions for the theorem.

Definition at line 76 of file theorem_value.h.
Referenced by CVCL::Theorem::getAssumptions(), getAssumptionsRef(), TheoremValue(), and toString().

Proof CVCL::TheoremValue::d_proof [protected]

Proof of the theorem.

Definition at line 79 of file theorem_value.h.
Referenced by getProof().

int CVCL::TheoremValue::d_refcount [protected]

How many pointers to this theorem value.

Definition at line 82 of file theorem_value.h.
Referenced by CVCL::Theorem::operator=(), CVCL::Theorem::Theorem(), CVCL::Theorem::~Theorem(), and ~TheoremValue().

int CVCL::TheoremValue::d_scopeLevel [protected]

Largest scope level of the assumptions.

Definition at line 85 of file theorem_value.h.
Referenced by getScope(), and TheoremValue().

unsigned CVCL::TheoremValue::d_flag [protected]

Temporary flag used during traversals.

Definition at line 88 of file theorem_value.h.
Referenced by isFlagged(), and setFlag().

int CVCL::TheoremValue::d_cachedValue [protected]

Temporary cache used during traversals.

Definition at line 91 of file theorem_value.h.
Referenced by getCachedValue(), and setCachedValue().

bool CVCL::TheoremValue::d_isAssump [protected]

Definition at line 93 of file theorem_value.h.
Referenced by isAssump().

bool CVCL::TheoremValue::d_expand [protected]

whether it should this be expanded in graph traversal

Definition at line 94 of file theorem_value.h.
Referenced by getExpandFlag(), and setExpandFlag().

bool CVCL::TheoremValue::d_clauselit [protected]

whether it belongs to the conflict clause

Definition at line 95 of file theorem_value.h.
Referenced by getLitFlag(), and setLitFlag().

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

theorem_value.h

Generated on Thu Apr 13 16:57:45 2006 for CVC Lite by

1.4.4