From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 29 Jun 2010 00:49:38 +0000 (+0000)
Subject: * Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"
X-Git-Tag: cvc5-1.0.0~8976
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e7e9c10006b5b243a73832ed97c5dec79df6c90a;p=cvc5.git

* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"
  data into a CDMap.  Such a key doesn't disappear from the map on pop,
  but rather returns to its "initializing" state, set by
  insertAtContextLevelZero().  This can be used for lazy assignment,
  among other things, and has been added to support some exploratory
  coding by Tim in arithmetic.

* Made internal CDOmap<> copy constructor private (it should always have
  been).  This is necessary to avoid CxxTest (or others) doing nasty
  generic programming things that cause context invariants to be broken.

* Added unit testing for this feature, and in general beef up the unit
  testing for CDMap<>.

* src/expr/node_manager.cpp: Better output for unhandled cases in getType().
---

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 28be629c4..b981628c5 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -161,21 +161,41 @@ class CDOmap : public ContextObj {
     }
   }
 
+  /** ensure copy ctor is only called by us */
+  CDOmap(const CDOmap& other) :
+    ContextObj(other),
+    d_key(other.d_key),
+    d_data(other.d_data),
+    d_map(other.d_map),
+    d_prev(NULL),
+    d_next(NULL) {
+  }
+
 public:
 
   CDOmap(Context* context,
          CDMap<Key, Data, HashFcn>* map,
 	 const Key& key,
-         const Data& data) :
+         const Data& data,
+         bool atLevelZero = false) :
     ContextObj(context),
     d_key(key),
     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);
+    if(atLevelZero) {
+      // "Initializing" map insertion: this entry will never be
+      // removed from the map, it's inserted at level 0 as an
+      // "initializing" element.  See
+      // CDMap<>::insertAtContextLevelZero().
+      d_data = data;
+    } else {
+      // Normal map insertion: first makeCurrent(), then set the data
+      // and then, later, 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*& first = d_map->d_first;
@@ -361,6 +381,40 @@ public:
     }
   }
 
+  /**
+   * Version of insert() for CDMap<> that inserts data value d at
+   * context level zero.  This is a special escape hatch for inserting
+   * "initializing" data into the map.  Imagine something happens at a
+   * deep context level L that causes insertion into a map, such that
+   * the object should have an "initializing" value v1 below context
+   * level L, and a "current" value v2 at context level L.  Then you
+   * can (assuming key k):
+   *
+   *   map.insertAtContextLevelZero(k, v1);
+   *   map.insert(k, v2);
+   *
+   * The justification for this "escape hatch" has to do with
+   * variables and assignments in theories (e.g., in arithmetic).
+   * Let's say you introduce a new variable x at some deep decision
+   * level (thanks to lazy registration, or a splitting lemma, or
+   * whatever).  x might be mapped to something, but for theory
+   * implementation simplicity shouldn't disappear from the map on
+   * backjump; rather, it can take another (legal) value, or a special
+   * value to indicate it needs to be recomputed.
+   *
+   * It is an error (checked via AlwaysAssert()) to
+   * insertAtContextLevelZero() a key that already is in the map.
+   */
+  void insertAtContextLevelZero(const Key& k, const Data& d) {
+    emptyTrash();
+
+    AlwaysAssert(d_map.find(k) == d_map.end());
+
+    Element* obj = new(true) Element(d_context, this, k, d,
+                                     true /* atLevelZero */);
+    d_map[k] = obj;
+  }
+
   // FIXME: no erase(), too much hassle to implement efficiently...
 
   /**
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index b67f42dfa..6e2141351 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -362,7 +362,7 @@ TypeNode NodeManager::getType(TNode n) throw (TypeCheckingExceptionPrivate) {
       typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n);
       break;
     default:
-     Unimplemented();
+      Unhandled(n.getKind());
     }
     setAttribute(n, TypeAttr(), typeNode);
   }
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 93316da76..b4370e93c 100644
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -32,7 +32,7 @@ public:
 
   void setUp() {
     d_context = new Context;
-    //Debug.on("cdmap");
+    //Debug.on("context");
     //Debug.on("gc");
     //Debug.on("pushpop");
   }
@@ -44,12 +44,20 @@ public:
   void testSimpleSequence() {
     CDMap<int, int> map(d_context);
 
+    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());
+    TS_ASSERT(map.find(23) == map.end());
+
     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());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
 
     {
       d_context->push();
@@ -58,6 +66,8 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) == map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
 
       map.insert(5, 6);
       map.insert(9, 8);
@@ -66,6 +76,10 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       {
         d_context->push();
@@ -74,6 +88,10 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
         map.insert(1, 2);
 
@@ -81,6 +99,11 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         {
           d_context->push();
@@ -89,13 +112,38 @@ public:
           TS_ASSERT(map.find(5) != map.end());
           TS_ASSERT(map.find(9) != map.end());
           TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) == map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
 
+          map.insertAtContextLevelZero(23, 317);
           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());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 45);
+          TS_ASSERT(map[23] == 317);
+
+          map.insert(23, 324);
+
+          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());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 45);
+          TS_ASSERT(map[23] == 324);
 
           d_context->pop();
         }
@@ -104,6 +152,12 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
 
         d_context->pop();
       }
@@ -112,6 +166,11 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) != map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(map[23] == 317);
 
       d_context->pop();
     }
@@ -120,6 +179,9 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) != map.end());
+    TS_ASSERT(map[3] == 4);
+    TS_ASSERT(map[23] == 317);
   }
 
   // no intervening find() in this one
@@ -144,6 +206,10 @@ public:
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(7) == map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[5] == 6);
 
         {
           d_context->push();
@@ -167,6 +233,8 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
 
     {
       d_context->push();
@@ -175,6 +243,8 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) == map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
 
       map.insert(5, 6);
       map.insert(9, 8);
@@ -183,6 +253,10 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       {
         d_context->push();
@@ -191,13 +265,24 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
+        map.insertAtContextLevelZero(23, 317);
         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());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
 
         map.obliterate(5);
 
@@ -205,6 +290,11 @@ public:
         TS_ASSERT(map.find(5) == map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
 
         {
           d_context->push();
@@ -213,6 +303,11 @@ public:
           TS_ASSERT(map.find(5) == map.end());
           TS_ASSERT(map.find(9) != map.end());
           TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 317);
 
           d_context->pop();
         }
@@ -221,6 +316,22 @@ public:
         TS_ASSERT(map.find(5) == map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
+
+        map.obliterate(23);
+
+        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());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         d_context->pop();
       }
@@ -229,6 +340,9 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[9] == 8);
 
       d_context->pop();
     }
@@ -237,6 +351,8 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
   }
 
   void testObliteratePrimordial() {
@@ -248,6 +364,7 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map[3] == 4);
 
     {
       d_context->push();
@@ -256,6 +373,7 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) == map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
 
       map.insert(5, 6);
       map.insert(9, 8);
@@ -264,6 +382,9 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       {
         d_context->push();
@@ -272,13 +393,19 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
-
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
         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());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         map.obliterate(3);
 
@@ -286,6 +413,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         {
           d_context->push();
@@ -294,6 +424,9 @@ public:
           TS_ASSERT(map.find(5) != map.end());
           TS_ASSERT(map.find(9) != map.end());
           TS_ASSERT(map.find(1) != map.end());
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
 
           d_context->pop();
         }
@@ -302,6 +435,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         d_context->pop();
       }
@@ -310,6 +446,8 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       d_context->pop();
     }
@@ -329,6 +467,7 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map[3] == 4);
 
     {
       d_context->push();
@@ -337,6 +476,7 @@ public:
       TS_ASSERT(map.find(5) == map.end());
       TS_ASSERT(map.find(9) == map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
 
       map.insert(5, 6);
       map.insert(9, 8);
@@ -345,6 +485,9 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
 
       {
         d_context->push();
@@ -353,6 +496,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
         map.insert(1, 2);
 
@@ -360,6 +506,10 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
 
         map.obliterate(1);
 
@@ -367,6 +517,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
         {
           d_context->push();
@@ -375,6 +528,9 @@ public:
           TS_ASSERT(map.find(5) != map.end());
           TS_ASSERT(map.find(9) != map.end());
           TS_ASSERT(map.find(1) == map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
 
           d_context->pop();
         }
@@ -383,6 +539,9 @@ public:
         TS_ASSERT(map.find(5) != map.end());
         TS_ASSERT(map.find(9) != map.end());
         TS_ASSERT(map.find(1) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
 
         d_context->pop();
       }
@@ -391,6 +550,362 @@ public:
       TS_ASSERT(map.find(5) != map.end());
       TS_ASSERT(map.find(9) != map.end());
       TS_ASSERT(map.find(1) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+
+      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());
+    TS_ASSERT(map[3] == 4);
+  }
+
+  void testInsertAtContextLevelZero() {
+    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());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
+
+    {
+      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());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+
+      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());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+
+      {
+        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());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+
+        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());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+
+        map.insertAtContextLevelZero(23, 317);
+
+        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());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
+
+        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
+                         AssertionException);
+        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472),
+                         AssertionException);
+        map.insert(23, 472);
+
+        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());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 472);
+
+        {
+          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());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 472);
+
+          TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
+                           AssertionException);
+          map.insert(23, 1024);
+
+          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());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 1024);
+
+          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());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        std::cout << "map[23] is " << map[23] << std::endl;
+        TS_ASSERT(map[23] == 472);
+
+        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());
+      TS_ASSERT(map.find(23) != map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(map[23] == 317);
+
+      TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
+                       AssertionException);
+      map.insert(23, 477);
+
+      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());
+      TS_ASSERT(map.find(23) != map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(map[23] == 477);
+
+      d_context->pop();
+    }
+
+    TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
+                     AssertionException);
+
+    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());
+    TS_ASSERT(map.find(23) != map.end());
+    TS_ASSERT(map[3] == 4);
+    TS_ASSERT(map[23] == 317);
+  }
+
+  void testObliterateInsertedAtContextLevelZero() {
+    cout << "\nobliteratCL0\n";
+    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());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
+
+    {
+      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());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+
+      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());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+
+      {
+        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());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+
+        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());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+
+        map.insertAtContextLevelZero(23, 317);
+
+        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());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 317);
+
+        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
+                         AssertionException);
+        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472),
+                         AssertionException);
+        map.insert(23, 472);
+
+        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());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 472);
+
+        {
+          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());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 472);
+
+          TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
+                           AssertionException);
+          map.insert(23, 1024);
+
+          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());
+          TS_ASSERT(map.find(23) != map.end());
+          TS_ASSERT(map[3] == 4);
+          TS_ASSERT(map[5] == 6);
+          TS_ASSERT(map[9] == 8);
+          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(map[23] == 1024);
+
+          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());
+        TS_ASSERT(map.find(23) != map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(map[23] == 472);
+
+        map.obliterate(23);
+
+        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());
+        TS_ASSERT(map.find(23) == map.end());
+        TS_ASSERT(map[3] == 4);
+        TS_ASSERT(map[5] == 6);
+        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(map[1] == 2);
+
+        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());
+      TS_ASSERT(map.find(23) == map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+
+      // reinsert as a normal map entry
+      map.insert(23, 477);
+
+      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());
+      TS_ASSERT(map.find(23) != map.end());
+      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(map[5] == 6);
+      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(map[23] == 477);
 
       d_context->pop();
     }
@@ -399,5 +914,7 @@ public:
     TS_ASSERT(map.find(5) == map.end());
     TS_ASSERT(map.find(9) == map.end());
     TS_ASSERT(map.find(1) == map.end());
+    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(map[3] == 4);
   }
 };