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

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);
   }