From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 23 Mar 2010 21:30:27 +0000 (+0000)
Subject: Documented that ContextObj::destroy() only restores back to context level 0.
X-Git-Tag: cvc5-1.0.0~9173
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=876993722316c92f6d24525e22c89c215ac90521;p=cvc5.git

Documented that ContextObj::destroy() only restores back to context level 0.
If there is more cleanup to do, it has to be done by the destructor.
---

diff --git a/src/context/context.h b/src/context/context.h
index 87e4e5fa1..455169a62 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -273,10 +273,14 @@ public:
  *    ContextMemoryManager (see item 2 above).
  * 4. In the subclass implementation, any time the state is about to be
  *    changed, first call makeCurrent().
- * 5. In the subclass implementation, the destructor should call destroy().
- *    Unfortunately, the destroy() functionality cannot be in the ContextObj
- *    destructor since it needs to call the subclass-specific restore() method
- *    in order to properly clean up saved copies.
+ * 5. In the subclass implementation, the destructor should call destroy(),
+ *    which repeatedly calls restore() until the object is restored to context
+ *    level 0.  Note, however, that if there is additional cleanup required at
+ *    level 0, destroy() does not do this.  It has to be implemented in the
+ *    destructor of the subclass.  The reason the destroy() functionality
+ *    cannot be in the ContextObj destructor is that it needs to call the
+ *    subclass-specific restore() method in order to properly clean up saved
+ *    copies.
  */
 class ContextObj {
   /**
@@ -358,9 +362,10 @@ protected:
 
   /**
    * Should be called from sub-class 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.
+   * to initial version (version at context level 0).  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.
    */
   void destroy() throw(AssertionException);