* Add some protected ContextObj accessors for ContextObj-derived classes:

  + Context* getContext() -- gets the context
  + ContextMemoryManager* getCMM() -- gets the CMM
  + int getLevel() -- the scope level of the ContextObj's most recent update
  + bool isCurrent() -- true iff the most recent update is the current top level

  In particular, the ContextObj::getCMM() call cleans up by TheoryUF's
  ECData::addPredecessor() function substantially (re: code review bug #64).

* Fix serious bugs in context operations that corrupted the ContextObj
  linked lists.  Closes bug #85.

* Identified a bug in the way objects of the "Link" class are
  allocated; see bug #96.

* Re-enable context white-box tests that ensure proper links in linked
  lists.  Closes bug #86.

* Re-enable CDMap<>::emptyTrash().  Closes bug #87.

* Add a tracing option (-t foo or --trace foo) to the driver to enable
  Trace("foo") output stream.  -d foo implies -t foo.

* Minor clean-up of some TheoryUF code; addition of some documentation
  (re: code review bug #64).

* Address some things that caused Doxygen discomfort.

* Address an issue raised in NodeManager's code review (bug #65).

* Remove an inaccurate comment in Attribute code (re: code review bug #61).

1 files changed, 35 insertions, 3 deletions

diff --git a/src/context/cdo.h b/src/context/cdo.h
index e03156e8a..ead43b2e8 100644
--- a/src/context/cdo.h
+++ b/src/context/cdo.h
@@ -66,11 +66,26 @@ class CDO : public ContextObj {
   CDO<T>& operator=(const CDO<T>& cdo);
 
 public:
+
   /**
    * Main constructor - uses default constructor for T to create the initial
    * value of d_data.
    */
-  CDO(Context* context) : ContextObj(context) {}
+  CDO(Context* context) :
+    ContextObj(context) {
+  }
+
+  /**
+   * Main constructor - uses default constructor for T to create the
+   * initial value of d_data.
+   *
+   * This version takes an argument that specifies whether this CDO<>
+   * was itself allocated in context memory.  If it was, it is linked
+   * with the current scope rather than scope 0.
+   */
+  CDO(bool allocatedInCMM, Context* context) :
+    ContextObj(allocatedInCMM, context) {
+  }
 
   /**
    * Constructor from object of type T.  Creates a ContextObj and sets the data
@@ -78,7 +93,24 @@ public:
    * current Scope.  If the Scope is popped, the value will revert to whatever
    * is assigned by the default constructor for T
    */
-  CDO(Context* context, const T& data) : ContextObj(context) {
+  CDO(Context* context, const T& data) :
+    ContextObj(context) {
+    makeCurrent();
+    d_data = data;
+  }
+
+  /**
+   * Constructor from object of type T.  Creates a ContextObj and sets the data
+   * to the given data value.  Note that this value is only valid in the
+   * current Scope.  If the Scope is popped, the value will revert to whatever
+   * is assigned by the default constructor for T.
+   *
+   * This version takes an argument that specifies whether this CDO<>
+   * was itself allocated in context memory.  If it was, it is linked
+   * with the current scope rather than scope 0.
+   */
+  CDO(bool allocatedInCMM, Context* context, const T& data) :
+    ContextObj(allocatedInCMM, context) {
     makeCurrent();
     d_data = data;
   }
@@ -86,7 +118,7 @@ public:
   /**
    * Destructor - call destroy() method
    */
-  ~CDO() throw() { destroy(); }
+  ~CDO() throw(AssertionException) { destroy(); }
 
   /**
    * Set the data in the CDO.  First call makeCurrent.