22 #ifndef _cvc3__include__context_h_
23 #define _cvc3__include__context_h_
44 class ContextNotifyObj;
46 class ContextObjChain;
87 : d_context(context), d_cmm(cmm), d_prevScope(
prevScope),
104 mm->deleteData(pMem);
106 void operator delete(
void*) { }
158 : d_restoreChainNext(NULL), d_restoreChainPrev(NULL),
159 d_restore(restore), d_data(data), d_master(master)
169 return mm->newData(size);
172 mm->deleteData(pMem);
175 void operator delete(
void*) { }
179 void*
operator new(
size_t size,
bool b) {
182 void operator delete(
void* pMem,
bool b) {
216 void update(
int scope = -1);
221 : d_scope(co.d_scope), d_restore(co.d_restore) {
223 DebugAssert(co.d_active,
"ContextObj["+co.name()+
"] copy constructor");
230 DebugAssert(
false,
"ContextObj::operator=(): shouldn't be called");
241 "ContextObj::restoreData(): call in the base abstract class");
245 return d_restore ? d_restore->
d_data : NULL;
249 virtual void setNull(
void) = 0;
252 IF_DEBUG(
virtual std::string name()
const {
return d_name; })
269 int level()
const {
return (d_scope==NULL)? 0 : d_scope->
level(); }
271 if(scope >= 0)
return d_scope->
level() == scope;
274 void makeCurrent(
int scope = -1) {
if (!isCurrent(scope)) update(scope); }
275 IF_DEBUG(
void setName(
const std::string& name) { d_name=name; })
286 void*
operator new(
size_t size,
bool b) {
289 void operator delete(
void* pMem,
bool b) {
293 void operator delete(
void*) { }
332 const std::string&
name()
const {
return d_name; }
333 int id()
const {
return d_id; }
340 void popto(
int toLevel);
343 unsigned long getMemory(
int verbosity);
348 {
return this == d_context->topScope(); }
351 if(d_restoreChain != NULL)
355 d_restoreChain = obj;
362 while (d_restoreChain != NULL) d_restoreChain = d_restoreChain->restore();
375 DebugAssert(context != NULL,
"NULL context pointer");
376 d_scope = context->bottomScope();
405 Context* createContext(
const std::string& name=
"");
408 unsigned long getMemory(
int verbosity);
ContextObjChain ** d_restoreChainPrev
Pointer to the pointer of the previous object which points to us. This makes a doubly-linked list for...
Scope(Context *context, ContextMemoryManager *cmm, Scope *prevScope=NULL)
Constructor.
ExprStream & pop(ExprStream &os)
Restore the indentation.
ContextObjChain * d_restore
The list of values on previous scopes; our destructor should clean up those.
ContextMemoryManager * d_cmm
Memory manager for this scope.
std::string d_name
Name of context.
ContextObjChain * d_restoreChain
Linked list of objects which are "current" in this scope, and thus need to be restored when the scope...
ContextNotifyObj(Context *context)
Description: Collection of debugging macros and functions.
const ContextObj * getRestore()
ContextObjChain * d_restore
Pointer to the previous copy which belongs to the same master.
ContextManager * getCM() const
Access methods.
virtual unsigned long getMemory(int verbosity)
ContextObjChain * d_restoreChainNext
Next link in chain.
void makeCurrent(int scope=-1)
virtual void notifyPre(void)
ContextObj * d_data
Pointer to copy of master to be restored when restore() is called.
std::vector< ContextMemoryManager * > d_cmmStack
Stack of free ContextMemoryManager's.
#define DebugAssert(cond, str)
ContextManager * d_cm
Context Manager.
void deleteNotifyObj(ContextNotifyObj *obj)
Context * getContext() const
void * newData(size_t size)
virtual ~ContextNotifyObj()
Scope * d_prevScope
Previous scope in this context.
unsigned long getMemory(int verbosity)
Compute memory used.
Context * getCurrentContext()
virtual void restoreData(ContextObj *data)
Restore the current object from the given data.
ContextMemoryManager * getCMM() const
ContextObj & operator=(const ContextObj &co)
Assignment operator (defined mainly for debugging purposes)
virtual void notify(void)
ContextObj(const ContextObj &co)
Copy constructor (defined mainly for debugging purposes)
~ContextObjChain()
Destructor.
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Scope * d_topScope
Pointer to top and bottom scopes of context.
Abstraction over different operating systems.
std::vector< Context * > d_contexts
Scope * bottomScope() const
void restore(void)
Restore all the values.
std::vector< ContextNotifyObj * > d_notifyObjList
List of objects to notify with every pop.
bool isCurrent(int scope=-1) const
ContextObjChain * restore(void)
Restore from d_data to d_master.
virtual void deleteData(void *d)=0
void finalize(void)
Called by ~ContextManager.
void addToChain(ContextObjChain *obj)
Called by ContextObj when created.
Scope * d_scope
Last scope in which this object was modified.
ContextObj * d_master
Pointer to the master object.
Scope * prevScope() const
Access functions.
bool isCurrent(void) const
virtual void * newData(size_t size)=0
Stack-based memory manager.
void addNotifyObj(ContextNotifyObj *obj)
ContextObjChain(ContextObj *data, ContextObj *master, ContextObjChain *restore)
Private constructor (only friends can use it)
ContextMemoryManager * getCMM()
Return our name (for debugging)
Manager for multiple contexts. Also holds current context.
const std::string & name() const
void check(void)
Check for memory leaks.
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
Context * d_context
Context that created this scope.