From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 29 Jan 2010 19:46:26 +0000 (+0000)
Subject: Update of context module
X-Git-Tag: cvc5-1.0.0~9330
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2ca8bf894a2e40e56b9379289e46b0a0d33cf272;p=cvc5.git

Update of context module
---

diff --git a/src/context/context.cpp b/src/context/context.cpp
index 3635d0c07..5729c2283 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -12,5 +12,214 @@
  **
  **/
 
+
 #include "context/context.h"
+#include "util/Assert.h"
+
+
+namespace CVC4 {
+namespace context {
+
+
+Context::Context() : d_pContextNotifyObj(NULL) {
+  // Create new memory manager
+  d_pCMM = new ContextMemoryManager();
+
+  // Create initial Scope
+  d_pScopeTop = new(cmm) Scope(this, cmm);
+  d_pScopeBottom = d_pScopeTop;
+}
+
+
+Context::~Context() {
+  // Delete all Scopes
+  popto(-1);
+
+  // Delete the memory manager
+  delete d_pCMM;
+
+  // Clear ContextNotifyObj lists so there are no dangling pointers
+  ContextNotifyObj* pCNO;
+  while (d_pCNOpre != NULL) {
+    pCNO = d_pCNOpre;
+    pCNO->d_ppCNOprev = NULL;
+    d_pContextNotifyObj = pCNO->d_pCNOnext;
+    pCNO->d_pCNOnext = NULL;
+  }
+  while (d_pCNOpost != NULL) {
+    pCNO = d_pCNOpost;
+    pCNO->d_ppCNOprev = NULL;
+    d_pContextNotifyObj = pCNO->d_pCNOnext;
+    pCNO->d_pCNOnext = NULL;
+  }
+}
+
+
+void Context::push() {
+  // FIXME: TRACE("pushpop", indentStr, "Push", " {");
+
+  // Create a new memory region
+  d_pCMM->push();
+
+  // Create a new top Scope
+  d_pScopeTop = new(d_pCMM) Scope(this, d_pCMM, d_pScopeTop);
+}
+
+
+void Context::pop() {
+  // Notify the (pre-pop) ContextNotifyObj objects
+  ContextNotifyObj* pCNO = d_pCNOPre;
+  while (pCNO != NULL) {
+    pCNO->notify();
+    pCNO = pCNO->d_pCNOnext;
+  }
+
+  // Grab the top Scope
+  Scope* pScope = d_pScopeTop;
+
+  // Restore the previous Scope
+  d_pScopeTop = pScope->getScopePrev();
+
+  // Restore all objects in the top Scope
+  delete(d_pCMM) pScope;
+
+  // Pop the memory region
+  d_pCMM->pop();
+
+  // Notify the (post-pop) ContextNotifyObj objects
+  ContextNotifyObj* pCNO = d_pCNOPost;
+  while (pCNO != NULL) {
+    pCNO->notify();
+    pCNO = pCNO->d_pCNOnext;
+  }
+
+  //FIXME:  TRACE("pushpop", indentStr, "}", " Pop");
+}
+
+
+void Context::popto(int toLevel) {
+  // Pop scopes until there are none left or toLevel is reached
+  while (d_pScopeTop != NULL && toLevel < d_pScopeTop()->getLevel()) pop();
+}
+
+
+void Context::addNotifyObjPre(ContextNotifyObj* pCNO) {
+  // Insert pCNO at *front* of list
+  if(d_pCNOpre != NULL)
+    d_pCNOpre->prev() = &(pCNO->next());
+  pCNO->next() = d_pCNOpre;
+  pCNO->prev() = &d_pCNOpre;
+  d_pCNOpre = pCNO;
+}
+
+
+void Context::addNotifyObjPost(ContextNotifyObj* pCNO) {
+  // Insert pCNO at *front* of list
+  if(d_pCNOpost != NULL)
+    d_pCNOpost->prev() = &(pCNO->next());
+  pCNO->next() = d_pCNOpost;
+  pCNO->prev() = &d_pCNOpost;
+  d_pCNOpost = pCNO;
+}
+
+
+void ContextObj::update() {
+  // Call save() to save the information in the current object
+  ContextObj* pContextObjSaved = save(d_pScope->getCMM());
+
+  // Check that base class data was saved
+  Assert(saved.d_pContextObjNext == d_pContextObjNext &&
+         saved.d_ppContextObjPrev == d_ppContextObjPrev &&
+         saved.d_pContextObjRestore == d_pContextObjRestore &&
+         saved.d_pScope == d_pScope,
+         "save() did not properly copy information in base class");
+
+  // Update Scope pointer to current top Scope
+  d_pScope = d_pScope->getContext()->getTopScope();
+
+  // Store the saved copy in the restore pointer
+  d_pContextObjRestore = pContextObjSaved;
+
+  // Insert object into the list of objects that need to be restored when this
+  // Scope is popped.
+  d_pScope->addToChain(this);
+}
+
+
+ContextObj* ContextObj::restoreAndContinue()
+{
+  // Variable to hold next object in list
+  ContextObj* pContextObjNext;
+
+  // Check the restore pointer.  If NULL, this must be the bottom Scope
+  if (d_pContextObjRestore == NULL) {
+    Assert(d_pScope == d_pScope->getContext()->getBottomScope(),
+           "Expected bottom scope");
+    pContextObjNext = d_pContextObjNext;
+    // Nothing else to do
+  }
+  else {
+    // Call restore to update the subclass data
+    restore(d_pContextObjRestore);
+
+    // Remember the next object in the list
+    pContextObjNext = d_pContextObjNext;
+
+    // Restore the base class data
+    d_pScope = d_pContextObjRestore->d_pScope;
+    next() = d_pContextObjRestore->d_pContextObjNext;
+    prev() = d_pContextObjRestore->d_pContextObjPrev;
+    d_pContextObjRestore = d_pContextObjRestore->d_pContextObjRestore;
+  }
+  // Return the next object in the list
+  return pContextObjNext;
+}
+
+
+ContextObj::ContextObj(Context* pContext)
+  : d_pContextObjRestore(NULL)
+{
+  Assert(pContext != NULL, "NULL context pointer");
+  d_pScope = pContext->getBottomScope();
+  d_pScope->addToChain(this);
+}
+
+
+ContextObj::~ContextObj()
+{
+  for(;;) {
+    if (next() != NULL) {
+      next()->prev() = prev();
+    }
+    *(prev()) = next();
+    if (d_pContextObjRestore == NULL) break;
+    restoreAndContinue();
+  }
+}
+
+
+ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify = false) {
+  if (preNotify) {
+    pContext->addNotifyObjPre(this);
+  }
+  else {
+    pContext->addNotifyObjPost(this);
+  }
+}
+
+
+ContextNotifyObj::~ContextNotifyObj()
+{
+  if (d_pCNOnext != NULL) {
+    d_pCNOnext->d_pCNOprev = d_pCNOprev;
+  }
+  if (d_pCNOprev != NULL) {
+    *(d_pCNOprev) = d_pCNOnext;
+  }
+}
+
+
+} /* CVC4::context namespace */
+
 
+} /* CVC4 namespace */
diff --git a/src/context/context.h b/src/context/context.h
index 68667c223..6c9f01acf 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -20,18 +20,414 @@ namespace CVC4 {
 namespace context {
 
 class Context;
+class Scope;
+class ContextObj;
+class ContextNotifyObj;
+
+  /**
+   * A Context encapsulates all of the dynamic state of the system.  Its main
+   * methods are push() and pop().  A call to push() saves the current state,
+   * and a call to pop() restores the state saved by the most recent call to
+   * push().
+   *
+   * Objects which want to participate in this global save and restore
+   * mechanism must inherit from ContextObj (see below).
+   *
+   * For more flexible context-dependent behavior, objects may implement the
+   * ContextNotifyObj interface and simply get a notification when a pop has
+   * occurred.
+   *
+   * Context also uses a helper class called Scope which stores information
+   * specific to the portion of the Context since the last call to push() (see
+   * below).
+   *
+   * Memory allocation in Contexts is done with the help of the
+   * ContextMemoryManager.  A copy is stored in each Scope object for quick
+   * access.
+   *
+   */
+class Context {
+
+  /**
+   * Pointer to the ContextMemoryManager fot this Context.
+   */
+  ContextMemoryManager* d_pCMM;
+
+  /**
+   * Pointer to the current (top) Scope for this Context.
+   */
+  Scope* d_pScopeTop;
+
+  /**
+   * Pointer to the initial (bottom) Scope for this Context.
+   */
+  Scope* d_pScopeBottom;
+
+  /**
+   * Doubly-linked list of objects to notify before every pop.  See
+   * ContextNotifyObj for sturcture of linked list.
+   */
+  ContextNotifyObj* d_pCNOpre;
+
+  /**
+   * Doubly-linked list of objects to notify after every pop.  See
+   * ContextNotifyObj for sturcture of linked list.
+   */
+  ContextNotifyObj* d_pCNOpost;
 
-class ContextManager {
 public:
-  void switchContext(Context);
-  Context snapshot();
-};/* class ContextManager */
+  /**
+   * Constructor: create ContextMemoryManager and initial Scope
+   */
+  Context();
+
+  /**
+   * Destructor: pop all scopes, delete ContextMemoryManager
+   */
+  ~Context();
+
+  /**
+   * Return the current (top) scope
+   */
+  Scope* getTopScope() const { return d_pScopeTop; }
+
+  /**
+   * Return the initial (bottom) scope
+   */
+  Scope* getBottomScope() const { return d_pScopeBottom; }
+
+  /**
+   * Return the current Scope level.  Implemented as inline function following
+   * declaration of Scope class.
+   */
+  int getLevel() const;
+
+  /**
+   * Save the current state, create a new Scope
+   */
+  void push();
+
+  /**
+   * Restore the previous state, delete the top Scope
+   */
+  void pop();
+
+  /**
+   * Pop all the way back to given level
+   */
+  void popto(int toLevel);
+
+  /**
+   * Add pCNO to the list of objects notified before every pop
+   */
+  void addNotifyObjPre(ContextNotifyObj* pCNO);
+
+  /**
+   * Add pCNO to the list of objects notified after every pop
+   */
+  void addNotifyObjPost(ContextNotifyObj* pCNO);
+
+}; /* class Context */
+
+  /**
+   * Conceptually, a Scope encapsulates that portion of the context that
+   * changes after a call to push() and must be undone on a subsequent call to
+   * pop().  In particular, each call to push() creates a new Scope object .
+   * This new Scope object becomes the top scope and it points (via the
+   * d_pScopePrev member) to the previous top Scope.  Each call to pop()
+   * deletes the current top scope and restores the previous one.  The main
+   * purpose of a Scope is to maintain a linked list of ContexObj objects which
+   * change while the Scope is the top scope and which must be restored when
+   * the Scope is deleted.
+   *
+   * A Scope is also associated with a ContextMemoryManager.  All memory
+   * allocated by the Scope is allocated in a single region using the
+   * ContextMemoryManager and released all at once when the Scope is popped.
+   */
+class Scope {
+
+  /**
+   * Context that created this Scope
+   */
+  Context* d_pContext;
+
+  /**
+   * Memory manager for this Scope.  Same as in Context, but stored here too
+   * for faster access by ContextObj objects.
+   */
+  ContextMemoryManager* d_pCMM;
+
+  /**
+   * Previous Scope in this context
+   */
+  Scope* d_pScopePrev;
+
+  /**
+   * Scope level (total number of outstanding push() calls when this Scope was
+   * created).
+   */
+  int d_level;
+
+  /**
+   * Linked list of objects which changed in this scope,
+   * and thus need to be restored when the scope is deleted.
+   */
+  ContextObj* d_pContextObjList;
 
-class ContextObject {
 public:
-  void snapshot();
-  void restore();
-};/* class ContextObject */
+
+  /**
+   * Constructor: Create a new Scope; set the level and the previous Scope
+   * if any.
+   */
+  Scope(Context* pContext, ContextMemoryManager* pCMM,
+        Scope* pScopePrev = NULL)
+    : d_pContext(context), d_pCMM(pCMM), d_pScopePrev(pScopePrev),
+      d_level(0), d_pContextObjList(NULL)
+    { if (pScopePrev != NULL) d_level = pScopePrev->getLevel() + 1; }
+
+  /**
+   * Destructor: Restore all of the objects in CotextObjList.  Defined inline
+   * below.
+   */
+  ~Scope();
+
+  /**
+   * Get the Context for this Scope
+   */
+  Context* getContext() const { return d_pContext; }
+
+  /**
+   * Get the ContextMemoryManager for this Scope
+   */
+  ContextMemoryManager* getCMM() const { return d_pCMM; }
+
+  /**
+   * Get the pointer to the previous Scope (should be NULL if no previous
+   * scope).
+   */
+  Scope* getScopePrev() const { return d_pScopePrev; }
+
+  /**
+   * Get the level of the current Scope
+   */
+  int getLevel(void) const { return d_level; }
+
+  /**
+   * Return true iff this Scope is the current top Scope
+   */
+  bool isCurrent(void) const { return this == d_pContext->getTopScope(); }
+
+  /**
+   * When a ContextObj object is modified for the first time in this Scope, it
+   * should call this method to add itself to the list of objects that will
+   * need to be restored.  Defined inline below.
+   */
+  void addToChain(ContextObj* pContextObj);
+
+  /**
+   * Overload operator new for use with ContextMemoryManager to allow creation
+   * of new Scope objects in the current memory region.
+   */
+  void* operator new(size_t size, ContextMemoryManager* pCMM)
+    { return pCMM->newData(size); }
+
+  /**
+   * Overload operator delete for Scope objects allocated using
+   * ContextMemoryManager.  No need to do anything because memory is freed
+   * automatically when the ContextMemoryManager pop() method is called.
+   */
+  void operator delete(void* pMem, ContextMemoryManager* pCMM) {}
+
+  //FIXME:  //! Check for memory leaks
+  //  void check(void);
+
+}; /* class Scope */
+
+  /**
+   * This is an abstract base class from which all objects that are context-dependent
+   * should inherit.  For any data structure that you want to have be
+   * automatically backtracked, do the following:
+   * 1. Create a class for the data structure that inherits from ContextObj
+   * 2. Implement save()
+   *    The role of save() is to create a new ContexObj object that contains
+   *    enough information to restore the object to its current state, even if
+   *    it gets changed later.  Note that save should call the (default)
+   *    ContextObj Copy Constructor to copy the information in the base class.
+   *    It is recommended that any memory allocated by save() should be done
+   *    through the ContextMemoryManager.  This way, it does not need to be
+   *    explicitly freed when restore is called.  However, it is only required
+   *    that the ContextObj itself be allocated using the
+   *    ContextMemoryManager.  If other memory is allocated not using the
+   *    ContextMemoryManager, it should be freed when restore() is called.
+   * 3. Implement restore()
+   *    The role of restore() is, given the ContextObj returned by a previous
+   *    call to save(), to restore the current object to the state it was in
+   *    when save() was called.  Note that the implementation of restore does
+   *    *not* need to worry about restoring the base class data.  This is done
+   *    automatically.  restore() should not have to free any memory as any
+   *    memory allocated by save() should have been done using the
+   *    ContextMemoryManager (see item 2 above).
+   * 4. In the subclass implementation, any time the state is about to be
+   *    changed, first call to makeCurrent().
+   */
+class ContextObj {
+  /**
+   * Pointer to Scope in which this object was last modified.
+   */
+  Scope* d_pScope; 
+
+  /**
+   * Pointer to most recent version of same ContextObj in a previous Scope
+   */
+  ContextObj* d_pContextObjRestore;
+
+  /**
+   * Next link in ContextObjList list maintained by Scope class.
+   */
+  ContextObj* d_pContextObjNext;
+
+  /**
+   * Previous link in ContextObjList list maintained by Scope class.  We use
+   * double-indirection here to make element deletion easy.
+   */
+  ContextObj** d_ppContextObjPrev;
+
+  /**
+   * Helper method for makeCurrent (see below).  Separated out to allow common
+   * case to be inlined without making a function call.  It calls save() and
+   * does the necessary bookkeeping to ensure that object can be restored to
+   * its current state when restore is called.
+   */
+  void update();
+
+  // The rest of the private methods are for the benefit of the Scope.  We make
+  // Scope our friend so it is the only one that can use them.
+
+  friend class Scope;
+
+  /**
+   * Return reference to next link in ContextObjList.  Used by
+   * Scope::addToChain method.
+   */
+  ContextObj*& next() { return d_pContextObjNext; }
+
+  /**
+   * Return reference to prev link in ContextObjList.  Used by
+   * Scope::addToChain method.
+   */
+  ContextObj**& prev() { return d_ppContextObjPrev; }
+
+  /**
+   * This method is called by Scope during a pop: it does the necessary work to
+   * restore the object from its saved copy and then returns the next object in
+   * the list that needs to be restored.
+   */
+  ContextObj* restoreAndContinue();
+
+protected:
+  /**
+   * This is a method that must be implemented by all classes inheriting from
+   * ContextObj.  See the comment before the class declaration.
+   */
+  virtual ContextObj* save(ContextMemoryManager* pCMM) = 0;
+
+  /**
+   * This is a method that must be implemented by all classes inheriting from
+   * ContextObj.  See the comment before the class declaration.
+   */
+  virtual void restore(ContextObj* pContextObjRestore) = 0;
+
+  /**
+   * This method checks if the object has been modified in this Scope yet.  If
+   * not, it calls update().
+   */
+  void makeCurrent() { if (!(d_pScope->isCurrent())) update(); }
+
+public:
+  /**
+   * Create a new ContextObj.  The initial scope is set to the bottom
+   * scope of the Context.
+   */
+  ContextObj(Context* context);
+
+  /**
+   * Destructor: Calls restore until restored to initial version.  Also removes
+   * object from all Scope lists.  Note that this doesn't actually free the
+   * memory allocated by the ContextMemoryManager for this object.  This isn't
+   * done until the corresponding Scope is popped.
+   */
+  virtual ~ContextObj();
+
+}; /* class ContextObj */
+
+  /**
+   * For more flexible context-dependent behavior than that provided by
+   * ContextObj, objects may implement the ContextNotifyObj interface and
+   * simply get a notification when a pop has occurred.  See Context class for
+   * how to register a ContextNotifyObj with the Context (you can choose to
+   * have notification come before or after the ContextObj objects have been
+   * restored).
+   */
+class ContextNotifyObj {
+  /**
+   * Context is our friend so that when the Context is deleted, any remaining
+   * ContextNotifyObj can be removed from the Context list.
+   */
+  friend Context;
+
+  /**
+   * Pointer to next ContextNotifyObject in this List
+   */
+  ContextNotifyObj* d_pCNOnext;
+
+  /**
+   * Pointer to previous ContextNotifyObject in this list
+   */
+  ContextNotifyObj** d_ppCNOprev;
+
+public:
+  /**
+   * Constructor for ContextNotifyObj.  Parameters are the context to which
+   * this notify object will be added, and a flag which, if true, tells the
+   * context to notify this object *before* the ContextObj objects are
+   * restored.  Otherwise, the context notifies the object after the ContextObj
+   * objects are restored.  The default is for notification after.
+   */
+  ContextNotifyObj(Context* pContext, bool preNotify = false);
+
+  /**
+   * Destructor: removes object from list
+   */
+  virtual ~ContextNotifyObj();
+
+  /**
+   * This is the method called to notify the object of a pop.  It must be
+   * implemented by the subclass.
+   */
+  virtual void notify() = 0;
+}; /* class ContextNotifyObj */
+
+// Inline functions whose definitions had to be delayed:
+
+inline int Context::getLevel() const { return getTopScope()->getLevel(); }
+
+inline void Scope::~Scope() {
+  // Call restore() method on each ContextObj object in the list.
+  // Note that it is the responsibility of restore() to return the next item in
+  // the list.
+  while (d_pContextObjList != NULL) {
+    d_pContextObjList = d_pContextObjList->restoreAndContinue();
+  }
+}
+
+inline void Scope::addToChain(ContextObjChain* pContextObj) {
+  if(d_pContextObjList != NULL)
+    d_pContextObjList->prev() = &(pContextObj->next());
+  pContextObj->next() = d_pContextObjList;
+  pContextObj->prev() = &d_pContextObjList;
+  d_pContextObjList = pContextObj;
+}
 
 template <class T>
 class CDO;
@@ -49,3 +445,4 @@ class CDSet;
 }/* CVC4 namespace */
 
 #endif /* __CVC4__CONTEXT__CONTEXT_H */
+
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index d772b886f..f282df96d 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -119,5 +119,7 @@ void ContextMemoryManager::pop() {
 }
 
 
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
+} /* CVC4::context namespace */
+
+
+} /* CVC4 namespace */
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index eeaa0a2c8..af524a51f 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -34,9 +34,9 @@ namespace context {
 class ContextMemoryManager {
 
   /**
-   * Memory in regions is allocated in chunks.  This is the minimum chunk size
+   * Memory in regions is allocated in chunks.  This is the chunk size
    */
-  static const unsigned chunkSizeBytes = 16384; // #bytes in each chunk
+  static const unsigned chunkSizeBytes = 16384;
 
   /**
    * A list of free chunks is maintained.  This is the maximum number of