#include <variable.h>

Collaboration diagram for CVC3::VariableManager:

[legend]

List of all members.

Classes

class EqLV
class HashLV

Public Member Functions

VariableManager (ContextManager *cm, SearchEngineRules *rules, const std::string &mmFlag)
~VariableManager ()
void gc (VariableValue *v)
Garbage collect VariableValue pointer.
void postponeGC ()
Postpone garbage collection.
void resumeGC ()
Resume garbage collection.
ContextManager * getCM () const
SearchEngineRules * getRules () const

Private Types

typedef std::hash_set
< VariableValue *, HashLV,
EqLV > VariableValueSet

Private Member Functions

VariableValue * newVariableValue (const Expr &e)

Private Attributes

ContextManager * d_cm
MemoryManager * d_mm
SearchEngineRules * d_rules
VariableManagerNotifyObj * d_notifyObj
bool d_disableGC
Disable the garbage collection.
bool d_postponeGC
Postpone garbage collection.
std::vector< VariableValue * > d_deleted
Vector of variables to be deleted (postponed during pop())
VariableValueSet d_varSet

Friends

class Variable
class VariableValue

Detailed Description

Definition at line 363 of file variable.h.

Member Typedef Documentation

typedef std::hash_set<VariableValue*, HashLV, EqLV> CVC3::VariableManager::VariableValueSet [private]

Definition at line 393 of file variable.h.

Constructor & Destructor Documentation

CVC3::VariableManager::VariableManager	(	ContextManager *	cm,
		SearchEngineRules *	rules,
		const std::string &	mmFlag
	)

Definition at line 368 of file variable.cpp.

References d_cm, d_mm, d_notifyObj, and CVC3::ContextManager::getCurrentContext().

CVC3::VariableManager::~VariableManager ( )

Definition at line 380 of file variable.cpp.

References Hash::hash_set< _Key, _HashFcn, _EqualKey >::begin(), Hash::hash_set< _Key, _HashFcn, _EqualKey >::clear(), d_disableGC, d_mm, d_notifyObj, d_varSet, and Hash::hash_set< _Key, _HashFcn, _EqualKey >::end().

Member Function Documentation

VariableValue * CVC3::VariableManager::newVariableValue ( const Expr & e ) [private]

Definition at line 357 of file variable.cpp.

References CVC3::VariableValue::VariableValue().

void CVC3::VariableManager::gc ( VariableValue * v )

Garbage collect VariableValue pointer.

Definition at line 400 of file variable.cpp.

References d_deleted, d_disableGC, d_mm, d_postponeGC, d_varSet, CVC3::MemoryManager::deleteData(), and Hash::hash_set< _Key, _HashFcn, _EqualKey >::erase().

Referenced by CVC3::Variable::operator=(), and CVC3::Variable::~Variable().

void CVC3::VariableManager::postponeGC ( ) [inline]

Postpone garbage collection.

Definition at line 409 of file variable.h.

References d_postponeGC.

Referenced by CVC3::VariableManagerNotifyObj::notifyPre().

void CVC3::VariableManager::resumeGC ( )

Resume garbage collection.

Definition at line 413 of file variable.cpp.

References d_deleted, d_mm, d_postponeGC, and CVC3::MemoryManager::deleteData().

Referenced by CVC3::VariableManagerNotifyObj::notify().

ContextManager* CVC3::VariableManager::getCM ( ) const [inline]

Definition at line 413 of file variable.h.

References d_cm.

Referenced by CVC3::VariableValue::setAssumpThm(), and CVC3::VariableValue::setValue().

SearchEngineRules* CVC3::VariableManager::getRules ( ) const [inline]

Definition at line 414 of file variable.h.

References d_rules.

Referenced by CVC3::Variable::deriveThmRec().

Friends And Related Function Documentation

friend class Variable [friend]

Definition at line 364 of file variable.h.

friend class VariableValue [friend]

Definition at line 365 of file variable.h.

Member Data Documentation

ContextManager* CVC3::VariableManager::d_cm [private]

Definition at line 367 of file variable.h.

Referenced by getCM(), and VariableManager().

MemoryManager* CVC3::VariableManager::d_mm [private]

Definition at line 368 of file variable.h.

Referenced by gc(), resumeGC(), VariableManager(), and ~VariableManager().

SearchEngineRules* CVC3::VariableManager::d_rules [private]

Definition at line 369 of file variable.h.

Referenced by getRules().

VariableManagerNotifyObj* CVC3::VariableManager::d_notifyObj [private]

Definition at line 370 of file variable.h.

Referenced by VariableManager(), and ~VariableManager().

bool CVC3::VariableManager::d_disableGC [private]

Disable the garbage collection.

Normally, it's set in the destructor, so that we can delete all remaining variables without GC getting in the way

Definition at line 375 of file variable.h.

Referenced by gc(), and ~VariableManager().

bool CVC3::VariableManager::d_postponeGC [private]

Postpone garbage collection.

Definition at line 377 of file variable.h.

Referenced by gc(), postponeGC(), and resumeGC().

std::vector<VariableValue*> CVC3::VariableManager::d_deleted [private]

Vector of variables to be deleted (postponed during pop())

Definition at line 379 of file variable.h.

Referenced by gc(), and resumeGC().

VariableValueSet CVC3::VariableManager::d_varSet [private]

Definition at line 394 of file variable.h.