1 files changed, 60 insertions, 6 deletions

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...
 
   /**