* 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().

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