* 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, 10 insertions, 4 deletions

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index d4de88daf..75f6eb2ae 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -71,6 +71,7 @@ class CDOmap : public ContextObj {
       }
       d_next->d_prev = d_prev;
       d_prev->d_next = d_next;
+      Debug("gc") << "CDMap<> trash push_back " << this << std::endl;
       d_map->d_trash.push_back(this);
     } else {
       d_data = p->d_data;
@@ -155,7 +156,7 @@ public:
 
   CDMapData(Context* context) : ContextObj(context) {}
   CDMapData(const ContextObj& co) : ContextObj(co) {}
-  ~CDMapData() { destroy(); }
+  ~CDMapData() throw(AssertionException) { destroy(); }
 };
 
 /**
@@ -192,7 +193,7 @@ class CDMap : public ContextObj {
         i != d_trash.end();
         ++i) {
       Debug("gc") << "emptyTrash(): " << *i << std::endl;
-      //(*i)->deleteSelf();
+      (*i)->deleteSelf();
     }
     d_trash.clear();
   }
@@ -201,21 +202,26 @@ public:
 
   CDMap(Context* context) :
     ContextObj(context),
+    d_map(),
     d_first(NULL),
     d_context(context),
     d_trash() {
   }
 
   ~CDMap() throw(AssertionException) {
+    Debug("gc") << "cdmap " << this
+                << " disappearing, destroying..." << std::endl;
     destroy();
+    Debug("gc") << "cdmap " << this
+                << " disappearing, done destroying" << std::endl;
     for(typename table_type::iterator i = d_map.begin();
         i != d_map.end();
         ++i) {
       (*i).second->deleteSelf();
     }
-    //d_map.clear();
-    Debug("gc") << "cdmap gone, emptying trash" << std::endl;
+    Debug("gc") << "cdmap " << this << " gone, emptying trash" << std::endl;
     emptyTrash();
+    Debug("gc") << "done emptying trash for " << this << std::endl;
   }
 
   // The usual operators of map