CVC3::ContextObj Class Reference
[Context Management]

#include <context.h>

Inherited by CVC3::CDList< Clause >, CVC3::CDList< ClauseOwner >, CVC3::CDList< dynTrig >, CVC3::CDList< Expr >, CVC3::CDList< Ineq >, CVC3::CDList< Literal >, CVC3::CDList< ProcessKinds >, CVC3::CDList< size_t >, CVC3::CDList< SmartCDO< Theorem > >, CVC3::CDList< Splitter >, CVC3::CDList< std::vector< Expr > >, CVC3::CDList< Theorem >, CVC3::CDList< Theory * >, CVC3::CDList< Trigger >, CVC3::CDMap< Expr, bool >, CVC3::CDMap< Expr, bool, HashFcn >, CVC3::CDMap< Expr, BoundInfo >, CVC3::CDMap< Expr, BoundInfo, HashFcn >, CVC3::CDMap< Expr, CDList< dynTrig > * >, CVC3::CDMap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< Expr, EpsRational >, CVC3::CDMap< Expr, EpsRational, HashFcn >, CVC3::CDMap< Expr, Expr >, CVC3::CDMap< Expr, Expr, HashFcn >, CVC3::CDMap< Expr, FreeConst >, CVC3::CDMap< Expr, FreeConst, HashFcn >, CVC3::CDMap< Expr, int >, CVC3::CDMap< Expr, int, HashFcn >, CVC3::CDMap< Expr, Literal >, CVC3::CDMap< Expr, Literal, HashFcn >, CVC3::CDMap< Expr, Rational >, CVC3::CDMap< Expr, Rational, HashFcn >, CVC3::CDMap< Expr, SmartCDO< Unsigned > >, CVC3::CDMap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDMap< Expr, std::set< std::vector< Expr > > >, CVC3::CDMap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDMap< Expr, std::vector< Expr > >, CVC3::CDMap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDMap< Expr, Theorem >, CVC3::CDMap< Expr, Theorem, HashFcn >, CVC3::CDMap< Expr, UserAssertion >, CVC3::CDMap< Expr, UserAssertion, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDO< bool >, CVC3::CDO< Clause >, CVC3::CDO< Expr >, CVC3::CDO< int >, CVC3::CDO< QueryResult >, CVC3::CDO< Rational >, CVC3::CDO< size_t >, CVC3::CDO< std::set< LitPriorityPair >::const_iterator >, CVC3::CDO< Theorem >, CVC3::CDO< U >, CVC3::CDO< unsigned >, CVC3::CDO< Unsigned >, CVC3::CDO< unsigned int >, CVC3::CDOmap< Expr, bool, HashFcn >, CVC3::CDOmap< Expr, BoundInfo, HashFcn >, CVC3::CDOmap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDOmap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< Expr, EpsRational, HashFcn >, CVC3::CDOmap< Expr, Expr, HashFcn >, CVC3::CDOmap< Expr, FreeConst, HashFcn >, CVC3::CDOmap< Expr, int, HashFcn >, CVC3::CDOmap< Expr, Literal, HashFcn >, CVC3::CDOmap< Expr, Rational, HashFcn >, CVC3::CDOmap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDOmap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDOmap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDOmap< Expr, Theorem, HashFcn >, CVC3::CDOmap< Expr, UserAssertion, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDFlags, CVC3::CDList< T >, CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDMapData, CVC3::CDMapOrdered< Key, Data >, CVC3::CDMapOrderedData, CVC3::CDO< T >, CVC3::CDOmap< Key, Data, HashFcn >, and CVC3::CDOmapOrdered< Key, Data >.

Collaboration diagram for CVC3::ContextObj:

Collaboration graph

List of all members.

Public Member Functions

ContextObj (Context *context)
Create a new ContextObj.
virtual ~ContextObj ()
int level () const
bool isCurrent (int scope=-1) const
void makeCurrent (int scope=-1)
void * operator new (size_t size, MemoryManager *mm)
void operator delete (void *pMem, MemoryManager *mm)
void * operator new (size_t size, bool b)
void operator delete (void *pMem, bool b)
void operator delete (void *)

Protected Member Functions

ContextObj (const ContextObj &co)
Copy constructor (defined mainly for debugging purposes).
ContextObj & operator= (const ContextObj &co)
Assignment operator (defined mainly for debugging purposes).
virtual ContextObj * makeCopy (ContextMemoryManager *cmm)=0
Make a copy of the current object so it can be restored to its current state.
virtual void restoreData (ContextObj *data)
Restore the current object from the given data.
const ContextObj * getRestore ()
virtual void setNull (void)=0
Set the current object to be invalid.
ContextMemoryManager * getCMM ()
Return our name (for debugging).

Private Member Functions

void update (int scope=-1)
Update on the given scope, on the current scope if 'scope' == -1.

Private Attributes

Scope * d_scope
Last scope in which this object was modified.
ContextObjChain * d_restore
The list of values on previous scopes; our destructor should clean up those.

Friends

class Scope
class ContextObjChain
class CDFlags

Detailed Description

Description: This is a generic class from which all objects that are context-dependent should inherit. Subclasses need to implement makeCopy, restoreData, and setNull.

Definition at line 200 of file context.h.

Constructor & Destructor Documentation

CVC3::ContextObj::ContextObj ( const ContextObj & co ) [inline, protected]

Copy constructor (defined mainly for debugging purposes).

Definition at line 220 of file context.h.

References DebugAssert, and IF_DEBUG.

ContextObj::~ContextObj ( ) [virtual]

Definition at line 179 of file context.cpp.

References d_restore, FatalAssert, and IF_DEBUG.

Member Function Documentation

void ContextObj::update ( int scope = -1 ) [private]

Update on the given scope, on the current scope if 'scope' == -1.

Definition at line 153 of file context.cpp.

References CVC3::Scope::addToChain(), ContextObjChain, d_restore, d_scope, DebugAssert, getCMM(), IF_DEBUG, CVC3::int2string(), CVC3::Scope::level(), level(), makeCopy(), CVC3::Scope::prevScope(), and CVC3::Scope::topScope().

ContextObj& CVC3::ContextObj::operator= ( const ContextObj & co ) [inline, protected]

Assignment operator (defined mainly for debugging purposes).

Definition at line 229 of file context.h.

References DebugAssert.

virtual ContextObj* CVC3::ContextObj::makeCopy ( ContextMemoryManager * cmm ) [protected, pure virtual]

Make a copy of the current object so it can be restored to its current state.

Implemented in CVC3::CDFlags, CVC3::CDList< T >, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDMapData, CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDMapOrderedData, CVC3::CDMapOrdered< Key, Data >, CVC3::CDO< T >, CVC3::CDList< Theory * >, CVC3::CDList< Theorem >, CVC3::CDList< Literal >, CVC3::CDList< Splitter >, CVC3::CDList< ProcessKinds >, CVC3::CDList< dynTrig >, CVC3::CDList< Expr >, CVC3::CDList< size_t >, CVC3::CDList< ClauseOwner >, CVC3::CDList< Clause >, CVC3::CDList< Trigger >, CVC3::CDList< std::vector< Expr > >, CVC3::CDList< Ineq >, CVC3::CDList< SmartCDO< Theorem > >, CVC3::CDOmap< Expr, EpsRational, HashFcn >, CVC3::CDOmap< Expr, bool, HashFcn >, CVC3::CDOmap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDOmap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< Expr, Rational, HashFcn >, CVC3::CDOmap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDOmap< Expr, UserAssertion, HashFcn >, CVC3::CDOmap< Expr, int, HashFcn >, CVC3::CDOmap< Expr, FreeConst, HashFcn >, CVC3::CDOmap< Expr, Theorem, HashFcn >, CVC3::CDOmap< Expr, BoundInfo, HashFcn >, CVC3::CDOmap< Expr, Literal, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDOmap< Expr, Expr, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< Expr, EpsRational, HashFcn >, CVC3::CDMap< Expr, bool, HashFcn >, CVC3::CDMap< Expr, SmartCDO< Unsigned > >, CVC3::CDMap< Expr, CDList< dynTrig > * >, CVC3::CDMap< Expr, EpsRational >, CVC3::CDMap< Expr, std::set< std::vector< Expr > > >, CVC3::CDMap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDMap< Expr, int >, CVC3::CDMap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDMap< Expr, Rational, HashFcn >, CVC3::CDMap< Expr, FreeConst >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDMap< Expr, Literal >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational >, CVC3::CDMap< Expr, UserAssertion, HashFcn >, CVC3::CDMap< Expr, int, HashFcn >, CVC3::CDMap< Expr, FreeConst, HashFcn >, CVC3::CDMap< Expr, Theorem, HashFcn >, CVC3::CDMap< Expr, bool >, CVC3::CDMap< Expr, BoundInfo, HashFcn >, CVC3::CDMap< Expr, Literal, HashFcn >, CVC3::CDMap< Expr, BoundInfo >, CVC3::CDMap< Expr, Rational >, CVC3::CDMap< Expr, std::vector< Expr > >, CVC3::CDMap< Expr, Expr >, CVC3::CDMap< Expr, Theorem >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< Expr, UserAssertion >, CVC3::CDMap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< Expr, Expr, HashFcn >, CVC3::CDO< int >, CVC3::CDO< Theorem >, CVC3::CDO< unsigned int >, CVC3::CDO< U >, CVC3::CDO< std::set< LitPriorityPair >::const_iterator >, CVC3::CDO< Expr >, CVC3::CDO< QueryResult >, CVC3::CDO< size_t >, CVC3::CDO< Unsigned >, CVC3::CDO< Clause >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, and CVC3::CDO< Rational >.

Referenced by update().

virtual void CVC3::ContextObj::restoreData ( ContextObj * data ) [inline, protected, virtual]

Restore the current object from the given data.

Reimplemented in CVC3::CDFlags, CVC3::CDList< T >, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDMapData, CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDMapOrderedData, CVC3::CDMapOrdered< Key, Data >, CVC3::CDO< T >, CVC3::CDList< Theory * >, CVC3::CDList< Theorem >, CVC3::CDList< Literal >, CVC3::CDList< Splitter >, CVC3::CDList< ProcessKinds >, CVC3::CDList< dynTrig >, CVC3::CDList< Expr >, CVC3::CDList< size_t >, CVC3::CDList< ClauseOwner >, CVC3::CDList< Clause >, CVC3::CDList< Trigger >, CVC3::CDList< std::vector< Expr > >, CVC3::CDList< Ineq >, CVC3::CDList< SmartCDO< Theorem > >, CVC3::CDOmap< Expr, EpsRational, HashFcn >, CVC3::CDOmap< Expr, bool, HashFcn >, CVC3::CDOmap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDOmap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< Expr, Rational, HashFcn >, CVC3::CDOmap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDOmap< Expr, UserAssertion, HashFcn >, CVC3::CDOmap< Expr, int, HashFcn >, CVC3::CDOmap< Expr, FreeConst, HashFcn >, CVC3::CDOmap< Expr, Theorem, HashFcn >, CVC3::CDOmap< Expr, BoundInfo, HashFcn >, CVC3::CDOmap< Expr, Literal, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDOmap< Expr, Expr, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< Expr, EpsRational, HashFcn >, CVC3::CDMap< Expr, bool, HashFcn >, CVC3::CDMap< Expr, SmartCDO< Unsigned > >, CVC3::CDMap< Expr, CDList< dynTrig > * >, CVC3::CDMap< Expr, EpsRational >, CVC3::CDMap< Expr, std::set< std::vector< Expr > > >, CVC3::CDMap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDMap< Expr, int >, CVC3::CDMap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDMap< Expr, Rational, HashFcn >, CVC3::CDMap< Expr, FreeConst >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDMap< Expr, Literal >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational >, CVC3::CDMap< Expr, UserAssertion, HashFcn >, CVC3::CDMap< Expr, int, HashFcn >, CVC3::CDMap< Expr, FreeConst, HashFcn >, CVC3::CDMap< Expr, Theorem, HashFcn >, CVC3::CDMap< Expr, bool >, CVC3::CDMap< Expr, BoundInfo, HashFcn >, CVC3::CDMap< Expr, Literal, HashFcn >, CVC3::CDMap< Expr, BoundInfo >, CVC3::CDMap< Expr, Rational >, CVC3::CDMap< Expr, std::vector< Expr > >, CVC3::CDMap< Expr, Expr >, CVC3::CDMap< Expr, Theorem >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< Expr, UserAssertion >, CVC3::CDMap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< Expr, Expr, HashFcn >, CVC3::CDO< int >, CVC3::CDO< Theorem >, CVC3::CDO< unsigned int >, CVC3::CDO< U >, CVC3::CDO< std::set< LitPriorityPair >::const_iterator >, CVC3::CDO< Expr >, CVC3::CDO< QueryResult >, CVC3::CDO< size_t >, CVC3::CDO< Unsigned >, CVC3::CDO< Clause >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, and CVC3::CDO< Rational >.

Definition at line 239 of file context.h.

References FatalAssert.

Referenced by CVC3::ContextObjChain::restore().

const ContextObj* CVC3::ContextObj::getRestore ( ) [inline, protected]

Definition at line 244 of file context.h.

References CVC3::ContextObjChain::d_data, and CVC3::ContextObjChain::d_restore.

Referenced by CVC3::CDList< SmartCDO< Theorem > >::pop_back().

virtual void CVC3::ContextObj::setNull ( void ) [protected, pure virtual]

Set the current object to be invalid.

Implemented in CVC3::CDFlags, CVC3::CDList< T >, CVC3::CDOmap< Key, Data, HashFcn >, CVC3::CDMapData, CVC3::CDMap< Key, Data, HashFcn >, CVC3::CDOmapOrdered< Key, Data >, CVC3::CDMapOrderedData, CVC3::CDMapOrdered< Key, Data >, CVC3::CDO< T >, CVC3::CDList< Theory * >, CVC3::CDList< Theorem >, CVC3::CDList< Literal >, CVC3::CDList< Splitter >, CVC3::CDList< ProcessKinds >, CVC3::CDList< dynTrig >, CVC3::CDList< Expr >, CVC3::CDList< size_t >, CVC3::CDList< ClauseOwner >, CVC3::CDList< Clause >, CVC3::CDList< Trigger >, CVC3::CDList< std::vector< Expr > >, CVC3::CDList< Ineq >, CVC3::CDList< SmartCDO< Theorem > >, CVC3::CDOmap< Expr, EpsRational, HashFcn >, CVC3::CDOmap< Expr, bool, HashFcn >, CVC3::CDOmap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDOmap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDOmap< std::string, bool, HashFcn >, CVC3::CDOmap< Expr, Rational, HashFcn >, CVC3::CDOmap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDOmap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDOmap< Expr, UserAssertion, HashFcn >, CVC3::CDOmap< Expr, int, HashFcn >, CVC3::CDOmap< Expr, FreeConst, HashFcn >, CVC3::CDOmap< Expr, Theorem, HashFcn >, CVC3::CDOmap< Expr, BoundInfo, HashFcn >, CVC3::CDOmap< Expr, Literal, HashFcn >, CVC3::CDOmap< Expr, EdgeInfo, HashFcn >, CVC3::CDOmap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDOmap< Expr, Expr, HashFcn >, CVC3::CDMap< std::string, bool >, CVC3::CDMap< Expr, EpsRational, HashFcn >, CVC3::CDMap< Expr, bool, HashFcn >, CVC3::CDMap< Expr, SmartCDO< Unsigned > >, CVC3::CDMap< Expr, CDList< dynTrig > * >, CVC3::CDMap< Expr, EpsRational >, CVC3::CDMap< Expr, std::set< std::vector< Expr > > >, CVC3::CDMap< Expr, std::vector< Expr >, HashFcn >, CVC3::CDMap< Expr, int >, CVC3::CDMap< Expr, CDList< dynTrig > *, HashFcn >, CVC3::CDMap< std::string, bool, HashFcn >, CVC3::CDMap< Expr, Rational, HashFcn >, CVC3::CDMap< Expr, FreeConst >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational, HashFcn >, CVC3::CDMap< Expr, std::set< std::vector< Expr > >, HashFcn >, CVC3::CDMap< Expr, Literal >, CVC3::CDMap< Expr, DifferenceLogicGraph::EpsRational >, CVC3::CDMap< Expr, UserAssertion, HashFcn >, CVC3::CDMap< Expr, int, HashFcn >, CVC3::CDMap< Expr, FreeConst, HashFcn >, CVC3::CDMap< Expr, Theorem, HashFcn >, CVC3::CDMap< Expr, bool >, CVC3::CDMap< Expr, BoundInfo, HashFcn >, CVC3::CDMap< Expr, Literal, HashFcn >, CVC3::CDMap< Expr, BoundInfo >, CVC3::CDMap< Expr, Rational >, CVC3::CDMap< Expr, std::vector< Expr > >, CVC3::CDMap< Expr, Expr >, CVC3::CDMap< Expr, Theorem >, CVC3::CDMap< Expr, EdgeInfo, HashFcn >, CVC3::CDMap< Expr, UserAssertion >, CVC3::CDMap< Expr, SmartCDO< Unsigned >, HashFcn >, CVC3::CDMap< Expr, EdgeInfo >, CVC3::CDMap< Expr, Expr, HashFcn >, CVC3::CDO< int >, CVC3::CDO< Theorem >, CVC3::CDO< unsigned int >, CVC3::CDO< U >, CVC3::CDO< std::set< LitPriorityPair >::const_iterator >, CVC3::CDO< Expr >, CVC3::CDO< QueryResult >, CVC3::CDO< size_t >, CVC3::CDO< Unsigned >, CVC3::CDO< Clause >, CVC3::CDO< unsigned >, CVC3::CDO< bool >, and CVC3::CDO< Rational >.

ContextMemoryManager* CVC3::ContextObj::getCMM ( ) [inline, protected]

Return our name (for debugging).

Get context memory manager

Definition at line 255 of file context.h.

Referenced by update().

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

Definition at line 269 of file context.h.

Referenced by CVC3::Expr::getFindLevel(), update(), and CVC3::CDFlags::update().

bool CVC3::ContextObj::isCurrent ( int scope = -1 ) const [inline]

Definition at line 270 of file context.h.

Referenced by CVC3::CDList< SmartCDO< Theorem > >::pop_back().

void CVC3::ContextObj::makeCurrent ( int scope = -1 ) [inline]

Definition at line 274 of file context.h.

Referenced by CVC3::CDList< SmartCDO< Theorem > >::push_back(), CVC3::CDO< Rational >::set(), CVC3::CDOmapOrdered< Key, Data >::set(), CVC3::CDOmap< Expr, Expr, HashFcn >::set(), and CVC3::CDFlags::update().

void* CVC3::ContextObj::operator new	(	size_t	size,
		MemoryManager *	mm
	)			`[inline]`

Definition at line 277 of file context.h.

References CVC3::MemoryManager::newData().

void CVC3::ContextObj::operator delete	(	void *	pMem,
		MemoryManager *	mm
	)			`[inline]`

Definition at line 280 of file context.h.

References CVC3::MemoryManager::deleteData().

void* CVC3::ContextObj::operator new	(	size_t	size,
		bool	b
	)			`[inline]`

Definition at line 286 of file context.h.

void CVC3::ContextObj::operator delete	(	void *	pMem,
		bool	b
	)			`[inline]`

Definition at line 289 of file context.h.

void CVC3::ContextObj::operator delete ( void * ) [inline]

Definition at line 293 of file context.h.

Friends And Related Function Documentation

friend class Scope [friend]

Definition at line 201 of file context.h.

friend class ContextObjChain [friend]

Definition at line 202 of file context.h.

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

friend class CDFlags [friend]

Definition at line 203 of file context.h.

Member Data Documentation

Scope* CVC3::ContextObj::d_scope [private]

Last scope in which this object was modified.

Definition at line 206 of file context.h.

Referenced by CVC3::Scope::finalize(), CVC3::ContextObjChain::restore(), update(), and CVC3::CDFlags::update().

ContextObjChain* CVC3::ContextObj::d_restore [private]

The list of values on previous scopes; our destructor should clean up those.

Definition at line 210 of file context.h.

Referenced by CVC3::Scope::finalize(), CVC3::ContextObjChain::restore(), update(), CVC3::CDFlags::update(), and ~ContextObj().

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

Generated on Thu Oct 15 22:18:12 2009 for CVC3 by

doxygen

1.5.8