CVC3
2.4.1
|
#include <context.h>
Description: This is a generic class from which all objects that are context-dependent should inherit. Subclasses need to implement makeCopy, restoreData, and setNull.
CVC3::ContextObj::ContextObj | ( | const ContextObj & | co | ) | [inline, protected] |
Copy constructor (defined mainly for debugging purposes)
Definition at line 220 of file context.h.
References IF_DEBUG, and DebugAssert.
ContextObj::~ContextObj | ( | ) | [virtual] |
Definition at line 179 of file context.cpp.
References IF_DEBUG, FatalAssert, CVC3::ContextObjChain::d_restore, CVC3::ContextObjChain::d_restoreChainNext, CVC3::ContextObjChain::d_restoreChainPrev, and CVC3::ContextObjChain::d_master.
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 DebugAssert, CVC3::int2string(), d_scope, d_restore, and IF_DEBUG.
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::CDMap, CVC3::CDMapOrdered, CVC3::CDMapData, CVC3::CDMapOrderedData, CVC3::CDOmap, CVC3::CDOmapOrdered, CVC3::CDList, CVC3::CDO, and CVC3::CDFlags.
virtual void CVC3::ContextObj::restoreData | ( | ContextObj * | data | ) | [inline, protected, virtual] |
Restore the current object from the given data.
Reimplemented in CVC3::CDMap, CVC3::CDMapOrdered, CVC3::CDMapData, CVC3::CDMapOrderedData, CVC3::CDOmap, CVC3::CDOmapOrdered, CVC3::CDList, CVC3::CDO, and CVC3::CDFlags.
Definition at line 239 of file context.h.
References FatalAssert.
const ContextObj* CVC3::ContextObj::getRestore | ( | ) | [inline, protected] |
Definition at line 244 of file context.h.
References CVC3::ContextObjChain::d_restore, and CVC3::ContextObjChain::d_data.
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::CDMap, CVC3::CDMapOrdered, CVC3::CDMapData, CVC3::CDMapOrderedData, CVC3::CDOmap, CVC3::CDOmapOrdered, CVC3::CDList, CVC3::CDO, and CVC3::CDFlags.
ContextMemoryManager* CVC3::ContextObj::getCMM | ( | ) | [inline, protected] |
int CVC3::ContextObj::level | ( | void | ) | const [inline] |
Definition at line 269 of file context.h.
Referenced by 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::CDOmap< Key, Data, HashFcn >::set(), CVC3::CDOmapOrdered< Key, Data >::set(), and CVC3::CDO< Rational >::set().
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] |
void CVC3::ContextObj::operator delete | ( | void * | pMem, |
bool | b | ||
) | [inline] |
void CVC3::ContextObj::operator delete | ( | void * | ) | [inline] |
friend class ContextObjChain [friend] |
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(), and 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::CDFlags::update(), CVC3::Scope::finalize(), and update().