Context Management

Collaboration diagram for Context Management:

Classes

• class CVC3::Scope
• class CVC3::ContextObjChain
• class CVC3::ContextObj
• class CVC3::Context
• class CVC3::ContextManager

  Manager for multiple contexts. Also holds current context. More...
  

• class CVC3::ContextNotifyObj

Functions

• bool CVC3::Scope::isCurrent (void) const
• void CVC3::Scope::addToChain (ContextObjChain *obj)

  Called by ContextObj when created.
  

• Scope * CVC3::Scope::topScope () const
• void CVC3::Scope::restore (void)

  Restore all the values.
  

• CVC3::ContextObj::ContextObj (Context *context)

  Create a new ContextObj.
  

---

Detailed Description

Infrastructure for backtrackable data structures.

---

Function Documentation

bool CVC3::Scope::isCurrent

(

void

)

const [inline, inherited]

Definition at line 347 of file context.h.

void CVC3::Scope::addToChain

(

ContextObjChain *

obj

)

[inline, private, inherited]

Called by ContextObj when created.

Definition at line 350 of file context.h.

References CVC3::ContextObjChain::d_restoreChainNext, and CVC3::ContextObjChain::d_restoreChainPrev.

Referenced by CVC3::CDFlags::update().

Scope * CVC3::Scope::topScope

(

)

const [inline, inherited]

Definition at line 358 of file context.h.

References CVC3::Scope::topScope().

Referenced by CVC3::Scope::topScope().

void CVC3::Scope::restore

(

void

)

[inline, inherited]

Restore all the values.

Definition at line 360 of file context.h.

References CVC3::ContextObjChain::restore().

Referenced by CVC3::Context::pop().

CVC3::ContextObj::ContextObj

(

Context *

context

)

[inline, inherited]

Create a new ContextObj.

The initial scope is set to the bottom scope by default, to reduce the work of pop() (otherwise, if the object is defined only on a very high scope, its scope will be moved down with each pop). If 'atBottomScope' == false, the scope is set to the current scope.

Definition at line 371 of file context.h.

References CVC3::ContextObjChain::ContextObjChain(), CVC3::ContextObjChain::d_restore, DebugAssert, and IF_DEBUG.