I think this finishes off the CDMap<>/Attribute leaks

10 files changed, 588 insertions, 101 deletions

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 1dc44d087..4adf90e4f 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -25,73 +25,76 @@
 #include "context/context.h"
 #include "util/Assert.h"
 
+#include <vector>
 #include <iterator>
 #include <ext/hash_map>
 
 namespace CVC4 {
 namespace context {
 
-// Auxiliary class: almost the same as CDO (see cdo.h), but on
-// setNull() call it erases itself from the map.
+// Auxiliary class: almost the same as CDO (see cdo.h)
 
 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
 
+template <class T, class U>
+inline std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
+  return out << "[" << p.first << "," << p.second << "]";
+}
+
 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
 class CDOmap : public ContextObj {
   Key d_key;
   Data d_data;
-  bool d_inMap; // whether the data must be in the map
-  CDMap<Key, Data, HashFcn>* d_cdmap;
+  CDMap<Key, Data, HashFcn>* d_map;
 
   // Doubly-linked list for keeping track of elements in order of insertion
-  CDOmap<Key, Data, HashFcn>* d_prev;
-  CDOmap<Key, Data, HashFcn>* d_next;
+  CDOmap* d_prev;
+  CDOmap* d_next;
 
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDOmap<Key, Data, HashFcn>(*this);
+    return new(pCMM) CDOmap(*this);
   }
 
   virtual void restore(ContextObj* data) {
-    CDOmap<Key, Data, HashFcn>* p((CDOmap<Key, Data, HashFcn>*) data);
-    if(p->d_inMap) {
-      d_data = p->d_data;
-      d_inMap = true;
-    } else {
-      // Erase itself from the map and put itself into trash.  We cannot
-      // "delete this" here, because it will break context operations in
-      // a non-trivial way.
-      if(d_cdmap->d_map.count(d_key) > 0) {
-        d_cdmap->d_map.erase(d_key);
-        d_cdmap->d_trash.push_back(this);
+    CDOmap* p = static_cast<CDOmap*>(data);
+    if(p->d_map == NULL) {
+      Assert(d_map->d_map.find(d_key) != d_map->d_map.end() &&
+             (*d_map->d_map.find(d_key)).second == this);
+      // no longer in map (popped beyond first level in which it was)
+      d_map->d_map.erase(d_key);
+      // If we call deleteSelf() here, it re-enters restore().  So,
+      // put it on a "trash heap" instead, for later deletion.
+      //
+      // FIXME multithreading
+      if(d_map->d_first == this) {
+        d_map->d_first = d_next;
       }
-
-      d_prev->d_next = d_next;
       d_next->d_prev = d_prev;
-
-      if(d_cdmap->d_first == this) {
-        d_cdmap->d_first = d_next;
-
-        if(d_next == this) {
-          d_cdmap->d_first = NULL;
-        }
-      }
+      d_prev->d_next = d_next;
+      d_map->d_trash.push_back(this);
+    } else {
+      d_data = p->d_data;
     }
   }
 
 public:
 
   CDOmap(Context* context,
-         CDMap<Key, Data, HashFcn>* cdmap,
+         CDMap<Key, Data, HashFcn>* map,
 	 const Key& key,
          const Data& data) :
     ContextObj(context),
     d_key(key),
-    d_inMap(false),
-    d_cdmap(cdmap) {
+    d_map(NULL) {
 
+    // makeCurrent(), then set the data and then the map.  Order is
+    // important; we can't initialize d_map in the constructor init
+    // list above, because we want the restore of d_map to NULL to
+    // signal us to remove the element from the map.
     set(data);
+    d_map = map;
 
-    CDOmap<Key, Data, HashFcn>*& first = d_cdmap->d_first;
+    CDOmap*& first = d_map->d_first;
     if(first == NULL) {
       first = d_next = d_prev = this;
     } else {
@@ -101,12 +104,13 @@ public:
     }
   }
 
-  ~CDOmap() throw(AssertionException) { destroy(); }
+  ~CDOmap() throw(AssertionException) {
+    destroy();
+  }
 
   void set(const Data& data) {
     makeCurrent();
     d_data = data;
-    d_inMap = true;
   }
 
   const Key& getKey() const {
@@ -121,19 +125,19 @@ public:
     return get();
   }
 
-  CDOmap<Key, Data, HashFcn>& operator=(const Data& data) {
+  CDOmap& operator=(const Data& data) {
     set(data);
     return *this;
   }
 
-  CDOmap<Key, Data, HashFcn>* next() const {
-    if(d_next == d_cdmap->d_first) {
+  CDOmap* next() const {
+    if(d_next == d_map->d_first) {
       return NULL;
     } else {
       return d_next;
     }
   }
-};/* class CDOmap */
+};/* class CDOmap<> */
 
 // Dummy subclass of ContextObj to serve as our data class
 class CDMapData : public ContextObj {
@@ -151,6 +155,7 @@ public:
 
   CDMapData(Context* context) : ContextObj(context) {}
   CDMapData(const ContextObj& co) : ContextObj(co) {}
+  ~CDMapData() { destroy(); }
 };
 
 /**
@@ -161,16 +166,18 @@ public:
 template <class Key, class Data, class HashFcn>
 class CDMap : public ContextObj {
 
+  typedef CDOmap<Key, Data, HashFcn> Element;
+  typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
+
   friend class CDOmap<Key, Data, HashFcn>;
 
-  typedef __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> table_type;
   table_type d_map;
 
-  // The vector of CDOmap objects to be destroyed
-  std::vector<CDOmap<Key, Data, HashFcn>*> d_trash;
-  CDOmap<Key, Data, HashFcn>* d_first;
+  Element* d_first;
   Context* d_context;
 
+  std::vector<Element*> d_trash;
+
   // Nothing to save; the elements take care of themselves
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
     return new(pCMM) CDMapData(*this);
@@ -179,14 +186,12 @@ class CDMap : public ContextObj {
   // Similarly, nothing to restore
   virtual void restore(ContextObj* data) {}
 
-  // Destroy stale CDOmap objects from trash
   void emptyTrash() {
-    for(typename std::vector<CDOmap<Key, Data, HashFcn>*>::iterator
-          i = d_trash.begin(), iend = d_trash.end(); i != iend; ++i) {
-      /*
-        delete *i;
-        free(*i);
-      */
+    //FIXME multithreading
+    for(typename std::vector<Element*>::iterator i = d_trash.begin();
+        i != d_trash.end();
+        ++i) {
+      (*i)->deleteSelf();
     }
     d_trash.clear();
   }
@@ -196,19 +201,19 @@ public:
   CDMap(Context* context) :
     ContextObj(context),
     d_first(NULL),
-    d_context(context) {
+    d_context(context),
+    d_trash() {
   }
 
   ~CDMap() throw(AssertionException) {
-    // Delete all the elements and clear the map
-    /*for(typename table_type::iterator
-          i = d_map.begin(), iend = d_map.end(); i != iend; ++i) {
-
-        delete (*i).second;
-        free((*i).second);
-
-    }*/
-    d_map.clear();
+    destroy();
+    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;
     emptyTrash();
   }
 
@@ -222,17 +227,15 @@ public:
     return d_map.count(k);
   }
 
-  typedef CDOmap<Key, Data, HashFcn>& ElementReference;
-
   // If a key is not present, a new object is created and inserted
-  CDOmap<Key, Data, HashFcn>& operator[](const Key& k) {
+  Element& operator[](const Key& k) {
     emptyTrash();
 
     typename table_type::iterator i = d_map.find(k);
 
-    CDOmap<Key, Data, HashFcn>* obj;
+    Element* obj;
     if(i == d_map.end()) {// create new object
-      obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, Data());
+      obj = new(true) Element(d_context, this, k, Data());
       d_map[k] = obj;
     } else {
       obj = (*i).second;
@@ -246,8 +249,7 @@ public:
     typename table_type::iterator i = d_map.find(k);
 
     if(i == d_map.end()) {// create new object
-      CDOmap<Key, Data, HashFcn>*
-	obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d);
+      Element* obj = new(true) Element(d_context, this, k, d);
       d_map[k] = obj;
     } else {
       (*i).second->set(d);
@@ -256,12 +258,40 @@ public:
 
   // FIXME: no erase(), too much hassle to implement efficiently...
 
+  /**
+   * "Obliterating" is kind of like erasing, except it's not
+   * backtrackable; the key is permanently removed from the map.
+   * (Naturally, it can be re-added as a new element.)
+   */
+  void obliterate(const Key& k) {
+    typename table_type::iterator i = d_map.find(k);
+    if(i != d_map.end()) {
+      Debug("gc") << "key " << k << " obliterated" << std::endl;
+      // We can't call ->deleteSelf() here, because it calls the
+      // ContextObj destructor, which calls CDOmap::destroy(), which
+      // restore()'s, which puts the CDOmap on the trash, which causes
+      // a double-delete.
+      (*i).second->~CDOmap();
+
+      typename table_type::iterator j = d_map.find(k);
+      // This if() succeeds for objects inserted when in the
+      // zero-scope: they were never save()'d there, so restore()
+      // never gets a NULL map and so they leak.
+      if(j != d_map.end()) {
+        Element* elt = (*j).second;
+        d_map.erase(j);//FIXME multithreading
+        // was already destructed, so don't call ->deleteSelf()
+        ::operator delete(elt);
+      }
+    }
+  }
+
   class iterator {
-    const CDOmap<Key, Data, HashFcn>* d_it;
+    const Element* d_it;
 
   public:
 
-    iterator(const CDOmap<Key, Data, HashFcn>* p) : d_it(p) {}
+    iterator(const Element* p) : d_it(p) {}
     iterator(const iterator& i) : d_it(i.d_it) {}
 
     // Default constructor
@@ -302,7 +332,7 @@ public:
 
     // Actual postfix increment: returns Proxy with the old value.
     // Now, an expression like *i++ will return the current *i, and
-    // then advance the orderedIterator.  However, don't try to use
+    // then advance the iterator.  However, don't try to use
     // Proxy for anything else.
     const Proxy operator++(int) {
       Proxy e(*(*this));
@@ -323,6 +353,7 @@ public:
 
   iterator find(const Key& k) const {
     typename table_type::const_iterator i = d_map.find(k);
+
     if(i == d_map.end()) {
       return end();
     } else {
@@ -330,6 +361,11 @@ public:
     }
   }
 
+  iterator find(const Key& k) {
+    emptyTrash();
+    return const_cast<const CDMap*>(this)->find(k);
+  }
+
 };/* class CDMap<> */
 
 }/* CVC4::context namespace */
diff --git a/src/context/context.cpp b/src/context/context.cpp
index d2e2bfa1b..05024430c 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -177,6 +177,10 @@ ContextObj* ContextObj::restoreAndContinue() {
 
 void ContextObj::destroy() throw(AssertionException) {
   for(;;) {
+    // If valgrind reports invalid writes on the next few lines,
+    // here's a hint: make sure all classes derived from ContextObj in
+    // the system properly call destroy() in their destructors.
+    // That's needed to maintain this linked list properly.
     if(next() != NULL) {
       next()->prev() = prev();
     }
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index be54a973e..26cb96646 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -56,23 +56,22 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   deleteFromTable(d_ptrs, nv);
 
   // FIXME CD-bools in optimized table
-        /*
   for(unsigned id = 0; id < attr::LastAttributeId<bool, true>::s_id; ++id) {
-    d_cdbools.erase(std::make_pair(id, nv));
+    Debug("gc") << "looking for " << id << " x " << nv << ":" << *nv << std::endl;
+    d_cdbools.obliterate(std::make_pair(id, nv));
   }
   for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, true>::s_id; ++id) {
-    d_cdints.erase(std::make_pair(id, nv));
+    d_cdints.obliterate(std::make_pair(id, nv));
   }
   for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) {
-    d_cdexprs.erase(std::make_pair(id, nv));
+    d_cdexprs.obliterate(std::make_pair(id, nv));
   }
   for(unsigned id = 0; id < attr::LastAttributeId<std::string, true>::s_id; ++id) {
-    d_cdstrings.erase(std::make_pair(id, nv));
+    d_cdstrings.obliterate(std::make_pair(id, nv));
   }
   for(unsigned id = 0; id < attr::LastAttributeId<void*, true>::s_id; ++id) {
-    d_cdptrs.erase(std::make_pair(id, nv));
+    d_cdptrs.obliterate(std::make_pair(id, nv));
   }
-        */
 }
 
 }/* CVC4::expr::attr namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6e24cce74..c51c7fb77 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -421,8 +421,8 @@ inline void NodeManager::setAttribute(TNode n,
 
 /** Make a function type from domain to range.
  * TODO: Function types should be unique for this manager. */
-FunctionType* NodeManager::mkFunctionType(Type* domain,
-                                          Type* range) const {
+inline FunctionType* NodeManager::mkFunctionType(Type* domain,
+                                                 Type* range) const {
   std::vector<Type*> argTypes;
   argTypes.push_back(domain);
   return new FunctionType(argTypes, range);
@@ -430,13 +430,14 @@ FunctionType* NodeManager::mkFunctionType(Type* domain,
 
 /** Make a function type with input types from argTypes.
  * TODO: Function types should be unique for this manager. */
-FunctionType* NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
-                                          Type* range) const {
+inline FunctionType*
+NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
+                            Type* range) const {
   Assert( argTypes.size() > 0 );
   return new FunctionType(argTypes, range);
 }
 
-Type* NodeManager::mkSort(const std::string& name) const {
+inline Type* NodeManager::mkSort(const std::string& name) const {
   return new SortType(name);
 }
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 2549f02ca..2fa21c8a6 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -31,7 +31,8 @@ Type::Type() :
 }
 
 Type::Type(std::string name) : 
-  d_name(name) {
+  d_name(name),
+  d_rc(0) {
 }
 
 std::string Type::getName() const {
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index 248e1e545..26d957c2e 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -175,7 +175,10 @@ public:
    */
   ECData(context::Context* context, TNode n);
 
-  ~ECData() { Debug("ufgc") << "Calling ECData destructor" << std::endl;}
+  ~ECData() {
+    Debug("ufgc") << "Calling ECData destructor" << std::endl;
+    destroy();
+  }
 
   /**
    * An ECData takes over the watch list of another ECData.
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 214f2ac58..122d92cae 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -10,15 +10,17 @@ UNIT_TESTS = \
 	parser/parser_black \
 	context/context_black \
 	context/context_mm_black \
+	context/cdo_black \
 	context/cdlist_black \
+	context/cdmap_black \
 	theory/theory_black \
 	theory/theory_uf_white \
 	util/assert_white \
 	util/configuration_white \
-	util/output_white \
-	util/integer_black \
-	util/integer_white \
-	util/rational_white
+	util/output_white
+#	util/integer_black \
+#	util/integer_white \
+#	util/rational_white
 
 # Things that aren't tests but that tests rely on and need to
 # go into the distribution
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
new file mode 100644
index 000000000..7040e4cc1
--- /dev/null
+++ b/test/unit/context/cdmap_black.h
@@ -0,0 +1,398 @@
+/*********************                                                        */
+/** cdmap_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::context::CDMap<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/cdmap.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class CDMapBlack : public CxxTest::TestSuite {
+
+  Context* d_context;
+
+public:
+
+  void setUp() {
+    d_context = new Context;
+    //Debug.on("cdmap");
+  }
+
+  void tearDown() {
+    delete d_context;
+  }
+
+  void testSimpleSequence() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+
+          map.insert(1, 45);
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      d_context->pop();
+    }
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+  }
+
+  // no intervening find() in this one
+  // (under the theory that this could trigger a bug)
+  void testSimpleSequenceFewerFinds() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    {
+      d_context->push();
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      {
+        d_context->push();
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(7) == map.end());
+
+        {
+          d_context->push();
+
+          d_context->pop();
+        }
+
+        d_context->pop();
+      }
+
+      d_context->pop();
+    }
+  }
+
+  void testObliterate() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        map.obliterate(5);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) == map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) == map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) == map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      d_context->pop();
+    }
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+  }
+
+  void testObliteratePrimordial() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        map.obliterate(3);
+
+        TS_ASSERT(map.find(3) == map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) == map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) != map.end());
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) == map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) == map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      d_context->pop();
+    }
+
+    TS_ASSERT(map.find(3) == map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+  }
+
+  void testObliterateCurrent() {
+    CDMap<int, int> map(d_context);
+
+    map.insert(3, 4);
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+
+    {
+      d_context->push();
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) == map.end());
+      TS_ASSERT(map.find(9) == map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      map.insert(5, 6);
+      map.insert(9, 8);
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      {
+        d_context->push();
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        map.insert(1, 2);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) != map.end());
+
+        map.obliterate(1);
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        {
+          d_context->push();
+
+          TS_ASSERT(map.find(3) != map.end());
+          TS_ASSERT(map.find(5) != map.end());
+          TS_ASSERT(map.find(9) != map.end());
+          TS_ASSERT(map.find(1) == map.end());
+
+          d_context->pop();
+        }
+
+        TS_ASSERT(map.find(3) != map.end());
+        TS_ASSERT(map.find(5) != map.end());
+        TS_ASSERT(map.find(9) != map.end());
+        TS_ASSERT(map.find(1) == map.end());
+
+        d_context->pop();
+      }
+
+      TS_ASSERT(map.find(3) != map.end());
+      TS_ASSERT(map.find(5) != map.end());
+      TS_ASSERT(map.find(9) != map.end());
+      TS_ASSERT(map.find(1) == map.end());
+
+      d_context->pop();
+    }
+
+    TS_ASSERT(map.find(3) != map.end());
+    TS_ASSERT(map.find(5) == map.end());
+    TS_ASSERT(map.find(9) == map.end());
+    TS_ASSERT(map.find(1) == map.end());
+  }
+};
diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h
new file mode 100644
index 000000000..4cdb8f343
--- /dev/null
+++ b/test/unit/context/cdo_black.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/** cdo_black.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::context::CDO<>.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <vector>
+#include <iostream>
+#include "context/context.h"
+#include "context/cdlist.h"
+#include "context/cdo.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+
+class CDOBlack : public CxxTest::TestSuite {
+private:
+
+  Context* d_context;
+
+public:
+
+  void setUp() {
+    d_context = new Context;
+  }
+
+  void tearDown() {
+    delete d_context;
+  }
+
+  void testIntCDO() {
+    // Test that push/pop maintains the original value
+    CDO<int> a1(d_context);
+    a1 = 5;
+    TS_ASSERT(d_context->getLevel() == 0);
+    d_context->push();
+    a1 = 10;
+    TS_ASSERT(d_context->getLevel() == 1);
+    TS_ASSERT(a1 == 10);
+    d_context->pop();
+    TS_ASSERT(d_context->getLevel() == 0);
+    TS_ASSERT(a1 == 5);
+  }
+};
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index c9b47e400..338c09849 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -41,20 +41,6 @@ public:
     delete d_context;
   }
 
-  void testIntCDO() {
-    // Test that push/pop maintains the original value
-    CDO<int> a1(d_context);
-    a1 = 5;
-    TS_ASSERT(d_context->getLevel() == 0);
-    d_context->push();
-    a1 = 10;
-    TS_ASSERT(d_context->getLevel() == 1);
-    TS_ASSERT(a1 == 10);
-    d_context->pop();
-    TS_ASSERT(d_context->getLevel() == 0);
-    TS_ASSERT(a1 == 5);
-  }
-
   void testContextPushPop() {
     // Test what happens when the context is popped below 0
     // the interface doesn't declare any exceptions