CVC3::Context Class Reference
[Context Management]

#include <context.h>

Collaboration diagram for CVC3::Context:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Attributes


Detailed Description

Encapsulates the general notion of stack-based saving and restoring of a database.

Definition at line 306 of file context.h.


Constructor & Destructor Documentation

Context::Context ( ContextManager cm,
const std::string &  name,
int  id 
)

Definition at line 208 of file context.cpp.

References d_bottomScope, d_topScope, and CVC3::TRACE.

Context::~Context (  ) 

Definition at line 221 of file context.cpp.

References d_cmmStack, d_notifyObjList, d_topScope, CVC3::Scope::finalize(), CVC3::ContextMemoryManager::garbageCollect(), CVC3::Scope::getCMM(), and CVC3::Scope::prevScope().


Member Function Documentation

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

Access methods.

Definition at line 331 of file context.h.

const std::string& CVC3::Context::name (  )  const [inline]

Definition at line 332 of file context.h.

int CVC3::Context::id (  )  const [inline]

Definition at line 333 of file context.h.

Referenced by CVC3::ContextManager::switchContext().

Scope* CVC3::Context::topScope (  )  const [inline]

Definition at line 334 of file context.h.

Referenced by CVC3::Scope::isCurrent(), popto(), and CVC3::Scope::topScope().

Scope* CVC3::Context::bottomScope (  )  const [inline]

Definition at line 335 of file context.h.

int CVC3::Context::level ( void   )  const [inline]

Definition at line 336 of file context.h.

Referenced by pop(), popto(), and push().

void Context::push (  ) 

Definition at line 244 of file context.cpp.

References d_cmmStack, d_topScope, IF_DEBUG, level(), and CVC3::TRACE.

void Context::pop (  ) 

Definition at line 266 of file context.cpp.

References d_cmmStack, d_notifyObjList, d_topScope, DebugAssert, IF_DEBUG, level(), CVC3::Scope::prevScope(), CVC3::Scope::restore(), and CVC3::TRACE.

Referenced by popto().

void Context::popto ( int  toLevel  ) 

Definition at line 296 of file context.cpp.

References level(), pop(), and topScope().

void CVC3::Context::addNotifyObj ( ContextNotifyObj obj  )  [inline]

Definition at line 341 of file context.h.

Referenced by CVC3::ContextNotifyObj::ContextNotifyObj().

void Context::deleteNotifyObj ( ContextNotifyObj obj  ) 

Definition at line 302 of file context.cpp.

References d_notifyObjList.

Referenced by CVC3::ContextNotifyObj::~ContextNotifyObj().

unsigned long Context::getMemory ( int  verbosity  ) 

Definition at line 312 of file context.cpp.

References d_cmmStack, d_name, d_notifyObjList, d_topScope, and CVC3::Scope::getMemory().


Member Data Documentation

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

Context Manager.

Definition at line 308 of file context.h.

std::string CVC3::Context::d_name [private]

Name of context.

Definition at line 311 of file context.h.

Referenced by getMemory().

int CVC3::Context::d_id [private]

Context ID.

Definition at line 314 of file context.h.

Scope* CVC3::Context::d_topScope [private]

Pointer to top and bottom scopes of context.

Definition at line 317 of file context.h.

Referenced by Context(), getMemory(), pop(), push(), and ~Context().

Scope* CVC3::Context::d_bottomScope [private]

Definition at line 318 of file context.h.

Referenced by Context().

std::vector<ContextNotifyObj*> CVC3::Context::d_notifyObjList [private]

List of objects to notify with every pop.

Definition at line 321 of file context.h.

Referenced by deleteNotifyObj(), getMemory(), pop(), and ~Context().

std::vector<ContextMemoryManager*> CVC3::Context::d_cmmStack [private]

Stack of free ContextMemoryManager's.

Definition at line 324 of file context.h.

Referenced by getMemory(), pop(), push(), and ~Context().


The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:14:41 2009 for CVC3 by  doxygen 1.5.2