CVC3  2.4.1
context.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file context.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Tue Dec 31 19:07:38 2002
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 
22 #ifndef _cvc3__include__context_h_
23 #define _cvc3__include__context_h_
24 
25 #include <string>
26 #include <vector>
27 #include <stdlib.h>
28 #include "debug.h"
29 #include "memory_manager_context.h"
30 #include "os.h"
31 
32 namespace CVC3 {
33 
34 /****************************************************************************/
35 /*! \defgroup Context Context Management
36  * \ingroup BuildingBlocks
37  * Infrastructure for backtrackable data structures.
38  * @{
39  */
40 /****************************************************************************/
41 
42 class Context;
43 class ContextManager;
44 class ContextNotifyObj;
45 class ContextObj;
46 class ContextObjChain;
47 
48 /****************************************************************************/
49 /*!
50  * Author: Clark Barrett
51  *
52  * Created: Thu Feb 13 00:19:15 2003
53  *
54  * A scope encapsulates the portion of a context which has changed
55  * since the last call to push(). Thus, when pop() is called,
56  * everything in this scope is restored to its previous state.
57  */
58  /****************************************************************************/
59 
60 class Scope {
61  friend class ContextObj;
62  friend class ContextObjChain;
63  friend class CDFlags;
64  //! Context that created this scope
66 
67  //! Memory manager for this scope
69 
70  //! Previous scope in this context
72 
73  //! Scope level
74  int d_level;
75 
76  /*! @brief Linked list of objects which are "current" in this scope,
77  and thus need to be restored when the scope is deleted */
79 
80  //! Called by ContextObj when created
81  void addToChain(ContextObjChain* obj);
82 
83 public:
84  //! Constructor
86  Scope* prevScope = NULL)
87  : d_context(context), d_cmm(cmm), d_prevScope(prevScope),
88  d_restoreChain(NULL)
89  { if (prevScope) d_level = prevScope->level() + 1; else d_level = 0; }
90  //! Destructor
91  ~Scope() {}
92 
93  //! Access functions
94  Scope* prevScope() const { return d_prevScope; }
95  int level(void) const { return d_level; }
96  bool isCurrent(void) const;
97  Scope* topScope() const;
98  Context* getContext() const { return d_context; }
99  ContextMemoryManager* getCMM() const { return d_cmm; }
100 
101  void* operator new(size_t size, MemoryManager* mm)
102  { return mm->newData(size); }
103  void operator delete(void* pMem, MemoryManager* mm) {
104  mm->deleteData(pMem);
105  }
106  void operator delete(void*) { }
107 
108  //! Restore all the values
109  void restore(void);
110 
111  //! Called by ~ContextManager
112  void finalize(void);
113 
114  //! Check for memory leaks
115  void check(void);
116 
117  //! Compute memory used
118  unsigned long getMemory(int verbosity);
119 };
120 
121 ///////////////////////////////////////////////////////////////////////////////
122 // //
123 // Class: ContextObjChain //
124 // Author: Sergey Berezin //
125 // Created: Wed Mar 12 11:25:22 2003 //
126 
127 /*! Description: An element of a doubly linked list holding a copy of
128  * ContextObj in a scope. It is made separate from ContextObj to keep
129  * the list pointers valid in all scopes at all times, so that the
130  * object can be easily removed from the list when the master
131  * ContextObj is destroyed. */
132 ///////////////////////////////////////////////////////////////////////////////
134 friend class Scope;
135 friend class ContextObj;
136 friend class CDFlags;
137 private:
138  //! Next link in chain
140 
141  /*! @brief Pointer to the pointer of the previous object which
142  points to us. This makes a doubly-linked list for easy element
143  deletion */
145 
146  //! Pointer to the previous copy which belongs to the same master
148 
149  //! Pointer to copy of master to be restored when restore() is called
151 
152  //! Pointer to the master object
154 
155  //! Private constructor (only friends can use it)
158  : d_restoreChainNext(NULL), d_restoreChainPrev(NULL),
159  d_restore(restore), d_data(data), d_master(master)
160  { }
161 
162  //! Restore from d_data to d_master
163  ContextObjChain* restore(void);
164 public:
165  //! Destructor
167 
168  void* operator new(size_t size, MemoryManager* mm) {
169  return mm->newData(size);
170  }
171  void operator delete(void* pMem, MemoryManager* mm) {
172  mm->deleteData(pMem);
173  }
174 
175  void operator delete(void*) { }
176 
177  // If you use this operator, you have to call free yourself when the memory
178  // is freed.
179  void* operator new(size_t size, bool b) {
180  return malloc(size);
181  }
182  void operator delete(void* pMem, bool b) {
183  free(pMem);
184  }
185 
186  IF_DEBUG(std::string name() const;)
187 };
188 
189 ///////////////////////////////////////////////////////////////////////////////
190 // //
191 // Class: ContextObj //
192 // Author: Clark Barrett //
193 // Created: Thu Feb 13 00:21:13 2003 //
194 
195 /*! Description: This is a generic class from which all objects that
196  * are context-dependent should inherit. Subclasses need to implement
197  * makeCopy, restoreData, and setNull.
198  */
199 ///////////////////////////////////////////////////////////////////////////////
201 friend class Scope;
202 friend class ContextObjChain;
203 friend class CDFlags;
204 private:
205  //! Last scope in which this object was modified.
207 
208  /*! @brief The list of values on previous scopes; our destructor
209  * should clean up those. */
211 
212  IF_DEBUG(std::string d_name;)
213  IF_DEBUG(bool d_active;)
214 
215  //! Update on the given scope, on the current scope if 'scope' == -1
216  void update(int scope = -1);
217 
218 protected:
219  //! Copy constructor (defined mainly for debugging purposes)
221  : d_scope(co.d_scope), d_restore(co.d_restore) {
222  IF_DEBUG(d_name=co.d_name;)
223  DebugAssert(co.d_active, "ContextObj["+co.name()+"] copy constructor");
224  IF_DEBUG(d_active = co.d_active;)
225  // TRACE("context verbose", "ContextObj()[", this, "]: copy constructor");
226  }
227 
228  //! Assignment operator (defined mainly for debugging purposes)
230  DebugAssert(false, "ContextObj::operator=(): shouldn't be called");
231  return *this;
232  }
233 
234  /*! @brief Make a copy of the current object so it can be restored
235  * to its current state */
236  virtual ContextObj* makeCopy(ContextMemoryManager* cmm) = 0;
237 
238  //! Restore the current object from the given data
239  virtual void restoreData(ContextObj* data) {
240  FatalAssert(false,
241  "ContextObj::restoreData(): call in the base abstract class");
242  }
243 
245  return d_restore ? d_restore->d_data : NULL;
246  }
247 
248  //! Set the current object to be invalid
249  virtual void setNull(void) = 0;
250 
251  //! Return our name (for debugging)
252  IF_DEBUG(virtual std::string name() const { return d_name; })
253 
254  //! Get context memory manager
255  ContextMemoryManager* getCMM() { return d_scope->getCMM(); }
256 
257 public:
258  //! Create a new ContextObj.
259  /*!
260  * The initial scope is set to the bottom scope by default, to
261  * reduce the work of pop() (otherwise, if the object is defined
262  * only on a very high scope, its scope will be moved down with each
263  * pop). If 'atBottomScope' == false, the scope is set to the
264  * current scope.
265  */
266  ContextObj(Context* context);
267  virtual ~ContextObj();
268 
269  int level() const { return (d_scope==NULL)? 0 : d_scope->level(); }
270  bool isCurrent(int scope = -1) const {
271  if(scope >= 0) return d_scope->level() == scope;
272  else return d_scope->isCurrent();
273  }
274  void makeCurrent(int scope = -1) { if (!isCurrent(scope)) update(scope); }
275  IF_DEBUG(void setName(const std::string& name) { d_name=name; })
276 
277  void* operator new(size_t size, MemoryManager* mm) {
278  return mm->newData(size);
279  }
280  void operator delete(void* pMem, MemoryManager* mm) {
281  mm->deleteData(pMem);
282  }
283 
284  // If you use this operator, you have to call free yourself when the memory
285  // is freed.
286  void* operator new(size_t size, bool b) {
287  return malloc(size);
288  }
289  void operator delete(void* pMem, bool b) {
290  free(pMem);
291  }
292 
293  void operator delete(void*) { }
294 };
295 
296 ///////////////////////////////////////////////////////////////////////////////
297 // //
298 // Class: Context //
299 // Author: Clark Barrett //
300 // Created: Thu Feb 13 00:24:59 2003 //
301 /*!
302  * Encapsulates the general notion of stack-based saving and restoring
303  * of a database.
304  */
305 ///////////////////////////////////////////////////////////////////////////////
307  //! Context Manager
309 
310  //! Name of context
311  std::string d_name;
312 
313  //! Context ID
314  int d_id;
315 
316  //! Pointer to top and bottom scopes of context
319 
320  //! List of objects to notify with every pop
321  std::vector<ContextNotifyObj*> d_notifyObjList;
322 
323  //! Stack of free ContextMemoryManager's
324  std::vector<ContextMemoryManager*> d_cmmStack;
325 
326 public:
327  Context(ContextManager* cm, const std::string& name, int id);
328  ~Context();
329 
330  //! Access methods
331  ContextManager* getCM() const { return d_cm; }
332  const std::string& name() const { return d_name; }
333  int id() const { return d_id; }
334  Scope* topScope() const { return d_topScope; }
335  Scope* bottomScope() const { return d_bottomScope; }
336  int level() const { return d_topScope->level(); }
337 
338  void push();
339  void pop();
340  void popto(int toLevel);
341  void addNotifyObj(ContextNotifyObj* obj) { d_notifyObjList.push_back(obj); }
342  void deleteNotifyObj(ContextNotifyObj* obj);
343  unsigned long getMemory(int verbosity);
344 };
345 
346 // Have to define after Context class
347 inline bool Scope::isCurrent(void) const
348  { return this == d_context->topScope(); }
349 
351  if(d_restoreChain != NULL)
352  d_restoreChain->d_restoreChainPrev = &(obj->d_restoreChainNext);
353  obj->d_restoreChainNext = d_restoreChain;
354  obj->d_restoreChainPrev = &d_restoreChain;
355  d_restoreChain = obj;
356 }
357 
358 inline Scope* Scope::topScope() const { return d_context->topScope(); }
359 
360 inline void Scope::restore(void) {
361  // TRACE_MSG("context verbose", "Scope::restore() {");
362  while (d_restoreChain != NULL) d_restoreChain = d_restoreChain->restore();
363  // TRACE_MSG("context verbose", "Scope::restore() }");
364 }
365 
366 // Create a new ContextObj. The initial scope is set to the bottom
367 // scope by default, to reduce the work of pop() (otherwise, if the
368 // object is defined only on a very high scope, its scope will be
369 // moved down with each pop). If 'atBottomScope' == false, the
370 // scope is set to the current scope.
372  IF_DEBUG(: d_name("ContextObj"))
373 {
374  IF_DEBUG(d_active=true;)
375  DebugAssert(context != NULL, "NULL context pointer");
376  d_scope = context->bottomScope();
377  d_restore = new(true) ContextObjChain(NULL, this, NULL);
378  d_scope->addToChain(d_restore);
379  // if (atBottomScope) d_scope->addSpecialObject(d_restore);
380  // TRACE("context verbose", "ContextObj()[", this, "]");
381 }
382 
383 
384 /****************************************************************************/
385 //! Manager for multiple contexts. Also holds current context.
386 /*!
387  * Author: Clark Barrett
388  *
389  * Created: Thu Feb 13 00:26:29 2003
390  */
391 /****************************************************************************/
392 
395  std::vector<Context*> d_contexts;
396 
397 public:
398  ContextManager();
399  ~ContextManager();
400 
401  void push() { d_curContext->push(); }
402  void pop() { d_curContext->pop(); }
403  void popto(int toLevel) { d_curContext->popto(toLevel); }
404  int scopeLevel() { return d_curContext->level(); }
405  Context* createContext(const std::string& name="");
406  Context* getCurrentContext() { return d_curContext; }
407  Context* switchContext(Context* context);
408  unsigned long getMemory(int verbosity);
409 };
410 
411 /****************************************************************************/
412 /*! Author: Clark Barrett
413  *
414  * Created: Sat Feb 22 16:21:47 2003
415  *
416  * Lightweight version of ContextObj: objects are simply notified
417  * every time there's a pop. notifyPre() is called right before the
418  * context is restored, and notify() is called after the context is
419  * restored.
420  */
421 /****************************************************************************/
422 
424  friend class Context;
425 protected:
427 public:
428  ContextNotifyObj(Context* context): d_context(context)
429  { context->addNotifyObj(this); }
430  virtual ~ContextNotifyObj() {
431  // If we are being deleted before the context, remove ourselves
432  // from the notify list. However, if the context is deleted
433  // before we are, then our d_context will be cleared from ~Context()
434  if(d_context!=NULL) d_context->deleteNotifyObj(this);
435  }
436  virtual void notifyPre(void) {}
437  virtual void notify(void) {}
438  virtual unsigned long getMemory(int verbosity) { return sizeof(ContextNotifyObj); }
439 };
440 
441 /*@}*/ // end of group Context
442 
443 }
444 
445 #endif
ContextObjChain ** d_restoreChainPrev
Pointer to the pointer of the previous object which points to us. This makes a doubly-linked list for...
Definition: context.h:144
Scope(Context *context, ContextMemoryManager *cmm, Scope *prevScope=NULL)
Constructor.
Definition: context.h:85
int level() const
Definition: context.h:269
ExprStream & pop(ExprStream &os)
Restore the indentation.
friend class ContextObj
Definition: context.h:135
int level() const
Definition: context.h:336
ContextObjChain * d_restore
The list of values on previous scopes; our destructor should clean up those.
Definition: context.h:210
ContextMemoryManager * d_cmm
Memory manager for this scope.
Definition: context.h:68
#define CVC_DLL
Definition: type.h:43
void push()
Definition: context.cpp:244
std::string d_name
Name of context.
Definition: context.h:311
int d_level
Scope level.
Definition: context.h:74
ContextObjChain * d_restoreChain
Linked list of objects which are "current" in this scope, and thus need to be restored when the scope...
Definition: context.h:78
ContextNotifyObj(Context *context)
Definition: context.h:428
Description: Collection of debugging macros and functions.
int id() const
Definition: context.h:333
const ContextObj * getRestore()
Definition: context.h:244
Context * d_context
Definition: context.h:426
ContextObjChain * d_restore
Pointer to the previous copy which belongs to the same master.
Definition: context.h:147
ContextManager * getCM() const
Access methods.
Definition: context.h:331
virtual unsigned long getMemory(int verbosity)
Definition: context.h:438
ContextObjChain * d_restoreChainNext
Next link in chain.
Definition: context.h:139
void makeCurrent(int scope=-1)
Definition: context.h:274
virtual void notifyPre(void)
Definition: context.h:436
void pop()
Definition: context.cpp:266
int d_id
Context ID.
Definition: context.h:314
ContextObj * d_data
Pointer to copy of master to be restored when restore() is called.
Definition: context.h:150
std::vector< ContextMemoryManager * > d_cmmStack
Stack of free ContextMemoryManager's.
Definition: context.h:324
#define DebugAssert(cond, str)
Definition: debug.h:408
ContextManager * d_cm
Context Manager.
Definition: context.h:308
void deleteNotifyObj(ContextNotifyObj *obj)
Definition: context.cpp:302
Context * getContext() const
Definition: context.h:98
Scope * topScope() const
Definition: context.h:334
virtual ~ContextNotifyObj()
Definition: context.h:430
Scope * d_prevScope
Previous scope in this context.
Definition: context.h:71
unsigned long getMemory(int verbosity)
Compute memory used.
Definition: context.cpp:82
void popto(int toLevel)
Definition: context.cpp:296
Context * getCurrentContext()
Definition: context.h:406
void popto(int toLevel)
Definition: context.h:403
Scope * topScope() const
Definition: context.h:358
virtual void restoreData(ContextObj *data)
Restore the current object from the given data.
Definition: context.h:239
ContextMemoryManager * getCMM() const
Definition: context.h:99
ContextObj & operator=(const ContextObj &co)
Assignment operator (defined mainly for debugging purposes)
Definition: context.h:229
virtual void notify(void)
Definition: context.h:437
ContextObj(const ContextObj &co)
Copy constructor (defined mainly for debugging purposes)
Definition: context.h:220
~ContextObjChain()
Destructor.
Definition: context.h:166
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
Scope * d_topScope
Pointer to top and bottom scopes of context.
Definition: context.h:317
Abstraction over different operating systems.
std::vector< Context * > d_contexts
Definition: context.h:395
Scope * bottomScope() const
Definition: context.h:335
void restore(void)
Restore all the values.
Definition: context.h:360
std::vector< ContextNotifyObj * > d_notifyObjList
List of objects to notify with every pop.
Definition: context.h:321
bool isCurrent(int scope=-1) const
Definition: context.h:270
ContextObjChain * restore(void)
Restore from d_data to d_master.
Definition: context.cpp:111
#define IF_DEBUG(code)
Definition: debug.h:406
virtual void deleteData(void *d)=0
void finalize(void)
Called by ~ContextManager.
Definition: context.cpp:37
void addToChain(ContextObjChain *obj)
Called by ContextObj when created.
Definition: context.h:350
Scope * d_scope
Last scope in which this object was modified.
Definition: context.h:206
~Scope()
Destructor.
Definition: context.h:91
ContextObj * d_master
Pointer to the master object.
Definition: context.h:153
Scope * prevScope() const
Access functions.
Definition: context.h:94
Scope * d_bottomScope
Definition: context.h:318
bool isCurrent(void) const
Definition: context.h:347
virtual void * newData(size_t size)=0
Stack-based memory manager.
void addNotifyObj(ContextNotifyObj *obj)
Definition: context.h:341
int level(void) const
Definition: context.h:95
Context * d_curContext
Definition: context.h:394
ContextObjChain(ContextObj *data, ContextObj *master, ContextObjChain *restore)
Private constructor (only friends can use it)
Definition: context.h:156
ContextMemoryManager * getCMM()
Return our name (for debugging)
Definition: context.h:255
Manager for multiple contexts. Also holds current context.
Definition: context.h:393
Definition: expr.cpp:35
const std::string & name() const
Definition: context.h:332
void check(void)
Check for memory leaks.
Definition: context.cpp:55
ExprStream & push(ExprStream &os)
Set the indentation to the current position.
Context * d_context
Context that created this scope.
Definition: context.h:65