context.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file context.h
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Tue Dec 31 19:07:38 2002
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  */
00019 /*****************************************************************************/
00020 
00021 
00022 #ifndef _cvc3__include__context_h_
00023 #define _cvc3__include__context_h_
00024 
00025 #include <string>
00026 #include <vector>
00027 #include "debug.h"
00028 #include "memory_manager_context.h"
00029 
00030 namespace CVC3 {
00031 
00032 /****************************************************************************/
00033 /*! \defgroup Context Context Management
00034  *  \ingroup BuildingBlocks
00035  * Infrastructure for backtrackable data structures.
00036  * @{
00037  */
00038 /****************************************************************************/
00039 
00040 class Context;
00041 class ContextManager;
00042 class ContextNotifyObj;
00043 class ContextObj;
00044 class ContextObjChain;
00045 
00046 /****************************************************************************/
00047 /*! 
00048  * Author: Clark Barrett
00049  *
00050  * Created: Thu Feb 13 00:19:15 2003
00051  *
00052  * A scope encapsulates the portion of a context which has changed
00053  * since the last call to push().  Thus, when pop() is called,
00054  * everything in this scope is restored to its previous state.
00055  */
00056  /****************************************************************************/
00057 
00058 class Scope {
00059   friend class ContextObj;
00060   friend class ContextObjChain;
00061   friend class CDFlags;
00062   //! Context that created this scope
00063   Context* d_context;
00064 
00065   //! Memory manager for this scope
00066   ContextMemoryManager* d_cmm;
00067 
00068   //! Previous scope in this context
00069   Scope* d_prevScope;
00070 
00071   //! Scope level
00072   int d_level;
00073 
00074   /*! @brief Linked list of objects which are "current" in this scope,
00075     and thus need to be restored when the scope is deleted */
00076   ContextObjChain* d_restoreChain;
00077 
00078   //! Called by ContextObj when created
00079   void addToChain(ContextObjChain* obj);
00080 
00081 public:
00082   //! Constructor
00083   Scope(Context* context, ContextMemoryManager* cmm,
00084         Scope* prevScope = NULL)
00085     : d_context(context), d_cmm(cmm), d_prevScope(prevScope),
00086       d_restoreChain(NULL)
00087     { if (prevScope) d_level = prevScope->level() + 1; else d_level = 0; }
00088   //! Destructor
00089   ~Scope() {}
00090 
00091   //! Access functions
00092   Scope* prevScope() const { return d_prevScope; }
00093   int level(void) const { return d_level; }
00094   bool isCurrent(void) const;
00095   Scope* topScope() const;
00096   Context* getContext() const { return d_context; }
00097   ContextMemoryManager* getCMM() const { return d_cmm; }
00098 
00099   void* operator new(size_t size, MemoryManager* mm)
00100     { return mm->newData(size); }
00101   void operator delete(void* pMem, MemoryManager* mm) {
00102     mm->deleteData(pMem);
00103   }
00104   void operator delete(void*) { }
00105 
00106   //! Restore all the values
00107   void restore(void);
00108 
00109   //! Called by ~ContextManager
00110   void finalize(void);
00111 
00112   //! Check for memory leaks
00113   void check(void);
00114 };
00115 
00116 ///////////////////////////////////////////////////////////////////////////////
00117 //                                                                           //
00118 // Class: ContextObjChain                //
00119 // Author: Sergey Berezin                                                    //
00120 // Created: Wed Mar 12 11:25:22 2003               //
00121 
00122 /*! Description: An element of a doubly linked list holding a copy of
00123  * ContextObj in a scope.  It is made separate from ContextObj to keep
00124  * the list pointers valid in all scopes at all times, so that the
00125  * object can be easily removed from the list when the master
00126  * ContextObj is destroyed. */
00127 ///////////////////////////////////////////////////////////////////////////////
00128 class ContextObjChain {
00129 friend class Scope;
00130 friend class ContextObj;
00131 friend class CDFlags;
00132 private:
00133   //! Next link in chain
00134   ContextObjChain* d_restoreChainNext;
00135 
00136   /*! @brief Pointer to the pointer of the previous object which
00137   points to us.  This makes a doubly-linked list for easy element
00138   deletion */
00139   ContextObjChain** d_restoreChainPrev;
00140 
00141   //! Pointer to the previous copy which belongs to the same master
00142   ContextObjChain* d_restore;
00143 
00144   //! Pointer to copy of master to be restored when restore() is called
00145   ContextObj* d_data;
00146 
00147   //! Pointer to the master object
00148   ContextObj* d_master;
00149 
00150   //! Private constructor (only friends can use it)
00151   ContextObjChain(ContextObj* data, ContextObj* master, 
00152       ContextObjChain* restore)
00153     : d_restoreChainNext(NULL), d_restoreChainPrev(NULL),
00154       d_restore(restore), d_data(data), d_master(master)
00155   { }
00156 
00157   //! Restore from d_data to d_master
00158   ContextObjChain* restore(void);
00159 public:
00160   //! Destructor
00161   ~ContextObjChain() {}
00162 
00163   void* operator new(size_t size, MemoryManager* mm) {
00164     return mm->newData(size);
00165   }
00166   void operator delete(void* pMem, MemoryManager* mm) {
00167     mm->deleteData(pMem);
00168   }
00169 
00170   void operator delete(void*) { }
00171 
00172   // If you use this operator, you have to call free yourself when the memory
00173   // is freed.
00174   void* operator new(size_t size, bool b) {
00175     return malloc(size);
00176   }
00177   void operator delete(void* pMem, bool b) {
00178     free(pMem);
00179   }
00180 
00181   IF_DEBUG(std::string name() const;)
00182 };
00183 
00184 ///////////////////////////////////////////////////////////////////////////////
00185 //                                                                           //
00186 // Class: ContextObj                   //
00187 // Author: Clark Barrett                                                     //
00188 // Created: Thu Feb 13 00:21:13 2003               //
00189 
00190 /*!  Description: This is a generic class from which all objects that
00191  * are context-dependent should inherit.  Subclasses need to implement
00192  * makeCopy, restoreData, and setNull.
00193  */
00194 ///////////////////////////////////////////////////////////////////////////////
00195 class CVC_DLL ContextObj {
00196 friend class Scope;
00197 friend class ContextObjChain;
00198 friend class CDFlags;
00199 private:
00200   //! Last scope in which this object was modified.
00201   Scope* d_scope;
00202 
00203   /*! @brief The list of values on previous scopes; our destructor
00204    *  should clean up those. */
00205   ContextObjChain* d_restore;
00206 
00207   IF_DEBUG(std::string d_name);
00208   IF_DEBUG(bool d_active);
00209 
00210   //! Update on the given scope, on the current scope if 'scope' == -1
00211   void update(int scope = -1);
00212 
00213 protected:
00214   //! Copy constructor (defined mainly for debugging purposes)
00215   ContextObj(const ContextObj& co)
00216     : d_scope(co.d_scope), d_restore(co.d_restore) {
00217     IF_DEBUG(d_name=co.d_name);
00218     DebugAssert(co.d_active, "ContextObj["+co.name()+"] copy constructor");
00219     IF_DEBUG(d_active = co.d_active);
00220     //    TRACE("context verbose", "ContextObj()[", this, "]: copy constructor");
00221   }
00222 
00223   //! Assignment operator (defined mainly for debugging purposes)
00224   ContextObj& operator=(const ContextObj& co) {
00225     DebugAssert(false, "ContextObj::operator=(): shouldn't be called");
00226     return *this;
00227   }
00228 
00229   /*! @brief Make a copy of the current object so it can be restored
00230    * to its current state */
00231   virtual ContextObj* makeCopy(ContextMemoryManager* cmm) = 0;
00232 
00233   //! Restore the current object from the given data
00234   virtual void restoreData(ContextObj* data) {
00235     FatalAssert(false, 
00236                 "ContextObj::restoreData(): call in the base abstract class");
00237   }
00238 
00239   const ContextObj* getRestore() {
00240     return d_restore ? d_restore->d_data : NULL;
00241   }
00242 
00243   //! Set the current object to be invalid
00244   virtual void setNull(void) = 0;
00245 
00246   //! Return our name (for debugging)
00247   IF_DEBUG(virtual std::string name() const { return d_name; });
00248 
00249   //! Get context memory manager
00250   ContextMemoryManager* getCMM() { return d_scope->getCMM(); }
00251 
00252 public:
00253   //! Create a new ContextObj.
00254   /*!
00255    * The initial scope is set to the bottom scope by default, to
00256    * reduce the work of pop() (otherwise, if the object is defined
00257    * only on a very high scope, its scope will be moved down with each
00258    * pop).  If 'atBottomScope' == false, the scope is set to the
00259    * current scope. 
00260    */
00261   ContextObj(Context* context, bool atBottomScope = true);
00262   virtual ~ContextObj();
00263 
00264   int level() const { return (d_scope==NULL)? 0 : d_scope->level(); }
00265   bool isCurrent(int scope = -1) const {
00266     if(scope >= 0) return d_scope->level() == scope;
00267     else return d_scope->isCurrent();
00268   }
00269   void makeCurrent(int scope = -1) { if (!isCurrent(scope)) update(scope); }
00270   IF_DEBUG(void setName(const std::string& name) { d_name=name; });
00271 
00272   void* operator new(size_t size, MemoryManager* mm) {
00273     return mm->newData(size);
00274   }
00275   void operator delete(void* pMem, MemoryManager* mm) {
00276     mm->deleteData(pMem);
00277   }
00278 
00279   // If you use this operator, you have to call free yourself when the memory
00280   // is freed.
00281   void* operator new(size_t size, bool b) {
00282     return malloc(size);
00283   }
00284   void operator delete(void* pMem, bool b) {
00285     free(pMem);
00286   }
00287 
00288   void operator delete(void*) { }
00289 };
00290 
00291 ///////////////////////////////////////////////////////////////////////////////
00292 //                                                                           //
00293 // Class: Context                  //
00294 // Author: Clark Barrett                                                     //
00295 // Created: Thu Feb 13 00:24:59 2003               //
00296 /*!
00297  * Encapsulates the general notion of stack-based saving and restoring
00298  * of a database.
00299  */
00300 ///////////////////////////////////////////////////////////////////////////////
00301 class Context {
00302   //! Context Manager
00303   ContextManager* d_cm;
00304 
00305   //! Name of context
00306   std::string d_name;
00307 
00308   //! Context ID
00309   int d_id;
00310 
00311   //! Pointer to top and bottom scopes of context
00312   Scope* d_topScope;
00313   Scope* d_bottomScope;
00314 
00315   //! List of objects to notify with every pop
00316   std::vector<ContextNotifyObj*> d_notifyObjList;
00317 
00318   //! Stack of free ContextMemoryManager's
00319   std::vector<ContextMemoryManager*> d_cmmStack;
00320 
00321 public:
00322   Context(ContextManager* cm, const std::string& name, int id);
00323   ~Context();
00324 
00325   //! Access methods
00326   ContextManager* getCM() const { return d_cm; }
00327   const std::string& name() const { return d_name; }
00328   int id() const { return d_id; }
00329   Scope* topScope() const { return d_topScope; }
00330   Scope* bottomScope() const { return d_bottomScope; }
00331   int level() const { return d_topScope->level(); }
00332 
00333   void push();
00334   void pop();
00335   void popto(int toLevel);
00336   void addNotifyObj(ContextNotifyObj* obj) { d_notifyObjList.push_back(obj); }
00337   void deleteNotifyObj(ContextNotifyObj* obj);
00338   unsigned long getMemory();
00339 };
00340 
00341 // Have to define after Context class
00342 inline bool Scope::isCurrent(void) const
00343   { return this == d_context->topScope(); }
00344 
00345 inline void Scope::addToChain(ContextObjChain* obj) {
00346   if(d_restoreChain != NULL)
00347     d_restoreChain->d_restoreChainPrev = &(obj->d_restoreChainNext);
00348   obj->d_restoreChainNext = d_restoreChain;
00349   obj->d_restoreChainPrev = &d_restoreChain;
00350   d_restoreChain = obj;
00351 }
00352 
00353 inline Scope* Scope::topScope() const { return d_context->topScope(); }
00354 
00355 inline void Scope::restore(void) {
00356   //  TRACE_MSG("context verbose", "Scope::restore() {");
00357   while (d_restoreChain != NULL) d_restoreChain = d_restoreChain->restore();
00358   //  TRACE_MSG("context verbose", "Scope::restore() }");
00359 }
00360 
00361 // Create a new ContextObj.  The initial scope is set to the bottom
00362 // scope by default, to reduce the work of pop() (otherwise, if the
00363 // object is defined only on a very high scope, its scope will be
00364 // moved down with each pop).  If 'atBottomScope' == false, the
00365 // scope is set to the current scope.
00366 inline ContextObj::ContextObj(Context* context, bool atBottomScope)
00367   IF_DEBUG(: d_name("ContextObj"))
00368 {
00369   IF_DEBUG(d_active=true);
00370   DebugAssert(context != NULL, "NULL context pointer");
00371   if (atBottomScope) d_scope = context->bottomScope();
00372   else d_scope = context->topScope();
00373   d_restore = new(true) ContextObjChain(NULL, this, NULL);
00374   d_scope->addToChain(d_restore);
00375   //  if (atBottomScope) d_scope->addSpecialObject(d_restore);
00376   //  TRACE("context verbose", "ContextObj()[", this, "]");
00377 }
00378 
00379 
00380 /****************************************************************************/
00381 //! Manager for multiple contexts.  Also holds current context.
00382 /*!
00383  * Author: Clark Barrett
00384  *
00385  * Created: Thu Feb 13 00:26:29 2003
00386  */
00387 /****************************************************************************/
00388 
00389 class ContextManager {
00390   Context* d_curContext;
00391   std::vector<Context*> d_contexts;
00392 
00393 public:
00394   ContextManager();
00395   ~ContextManager();
00396 
00397   void push() { d_curContext->push(); }
00398   void pop() { d_curContext->pop(); }
00399   void popto(int toLevel) { d_curContext->popto(toLevel); }
00400   int scopeLevel() { return d_curContext->level(); }
00401   Context* createContext(const std::string& name="");
00402   Context* getCurrentContext() { return d_curContext; }
00403   Context* switchContext(Context* context);
00404   unsigned long getMemory();
00405 };
00406 
00407 /****************************************************************************/
00408 /*! Author: Clark Barrett                                                     
00409  *
00410  * Created: Sat Feb 22 16:21:47 2003               
00411  *
00412  * Lightweight version of ContextObj: objects are simply notified
00413  * every time there's a pop. notifyPre() is called right before the
00414  * context is restored, and notify() is called after the context is
00415  * restored.
00416  */
00417 /****************************************************************************/
00418  
00419 class ContextNotifyObj {
00420   friend class Context;
00421 protected:
00422   Context* d_context;
00423 public:
00424   ContextNotifyObj(Context* context): d_context(context)
00425     { context->addNotifyObj(this); }
00426   virtual ~ContextNotifyObj() {
00427     // If we are being deleted before the context, remove ourselves
00428     // from the notify list.  However, if the context is deleted
00429     // before we are, then our d_context will be cleared from ~Context()
00430     if(d_context!=NULL) d_context->deleteNotifyObj(this);
00431   }
00432   virtual void notifyPre(void) {}
00433   virtual void notify(void) {}
00434 };
00435 
00436 /*@}*/  // end of group Context
00437 
00438 }
00439 
00440 #endif

Generated on Tue Jul 3 14:33:36 2007 for CVC3 by  doxygen 1.5.1