1 files changed, 44 insertions, 41 deletions

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 83a8f22c4..94b507a7e 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -100,8 +100,15 @@ template <class Key, class Data, class HashFcn = std::hash<Key> >
 class CDOhash_map : public ContextObj {
   friend class CDHashMap<Key, Data, HashFcn>;
 
-  Key d_key;
-  Data d_data;
+ public:
+  // The type of the <Key, Data> value mapped to by this class.
+  using value_type = std::pair<Key, Data>;
+
+ private:
+  value_type d_value;
+  Key& mutable_key() { return d_value.first; }
+  Data& mutable_data() { return d_value.second; }
+
   CDHashMap<Key, Data, HashFcn>* d_map;
 
   /** never put this cdhashmapelement on the trash */
@@ -121,10 +128,10 @@ class CDOhash_map : public ContextObj {
     CDOhash_map* p = static_cast<CDOhash_map*>(data);
     if(d_map != NULL) {
       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);
+        Assert(d_map->d_map.find(getKey()) != d_map->d_map.end()
+               && (*d_map->d_map.find(getKey())).second == this);
         // no longer in map (popped beyond first level in which it was)
-        d_map->d_map.erase(d_key);
+        d_map->d_map.erase(getKey());
         // If we call deleteSelf() here, it re-enters restore().  So,
         // put it on a "trash heap" instead, for later deletion.
         //
@@ -150,42 +157,40 @@ class CDOhash_map : public ContextObj {
           enqueueToGarbageCollect();
         }
       } else {
-        d_data = p->d_data;
+        mutable_data() = p->get();
       }
     }
     // Explicitly call destructors for the key and the data as they will not
     // otherwise get called.
-    p->d_key.~Key();
-    p->d_data.~Data();
+    p->mutable_key().~Key();
+    p->mutable_data().~Data();
   }
 
   /** ensure copy ctor is only called by us */
-  CDOhash_map(const CDOhash_map& other) :
-    ContextObj(other),
-    // don't need to save the key---and if we do we can get
-    // refcounts for Node keys messed up and leak memory
-    d_key(),
-    d_data(other.d_data),
-    d_map(other.d_map),
-    d_prev(NULL),
-    d_next(NULL) {
+  CDOhash_map(const CDOhash_map& other)
+      : ContextObj(other),
+        // don't need to save the key---and if we do we can get
+        // refcounts for Node keys messed up and leak memory
+        d_value(Key(), other.d_value.second),
+        d_map(other.d_map),
+        d_prev(NULL),
+        d_next(NULL)
+  {
   }
   CDOhash_map& operator=(const CDOhash_map&) CVC4_UNDEFINED;
 
-public:
-
+ public:
   CDOhash_map(Context* context,
-         CDHashMap<Key, Data, HashFcn>* map,
-         const Key& key,
-         const Data& data,
-         bool atLevelZero = false,
-         bool allocatedInCMM = false) :
-    ContextObj(allocatedInCMM, context),
-    d_key(key),
-    d_data(data),
-    d_map(NULL),
-    d_noTrash(allocatedInCMM) {
-
+              CDHashMap<Key, Data, HashFcn>* map,
+              const Key& key,
+              const Data& data,
+              bool atLevelZero = false,
+              bool allocatedInCMM = false)
+      : ContextObj(allocatedInCMM, context),
+        d_value(key, data),
+        d_map(NULL),
+        d_noTrash(allocatedInCMM)
+  {
     // untested, probably unsafe.
     Assert(!(atLevelZero && allocatedInCMM));
 
@@ -194,7 +199,7 @@ public:
       // removed from the map, it's inserted at level 0 as an
       // "initializing" element.  See
       // CDHashMap<>::insertAtContextLevelZero().
-      d_data = data;
+      mutable_data() = data;
     } else {
       // Normal map insertion: first makeCurrent(), then set the data
       // and then, later, the map.  Order is important; we can't
@@ -232,16 +237,14 @@ public:
 
   void set(const Data& data) {
     makeCurrent();
-    d_data = data;
+    mutable_data() = data;
   }
 
-  const Key& getKey() const {
-    return d_key;
-  }
+  const Key& getKey() const { return d_value.first; }
 
-  const Data& get() const {
-    return d_data;
-  }
+  const Data& get() const { return d_value.second; }
+
+  const value_type& getValue() const { return d_value; }
 
   operator Data() {
     return get();
@@ -395,6 +398,8 @@ public:
 
   // FIXME: no erase(), too much hassle to implement efficiently...
 
+  using value_type = typename CDOhash_map<Key, Data, HashFcn>::value_type;
+
   class iterator {
     const Element* d_it;
 
@@ -415,9 +420,7 @@ public:
     }
 
     // Dereference operators.
-    std::pair<const Key, const Data> operator*() const {
-      return std::pair<const Key, const Data>(d_it->getKey(), d_it->get());
-    }
+    const value_type& operator*() const { return d_it->getValue(); }
 
     // Prefix increment
     iterator& operator++() {