From: Martin <martin.brain@cs.ox.ac.uk>
Date: Thu, 5 Oct 2017 09:08:53 +0000 (+0100)
Subject: Allow CDHashMaps for objects without default constructors (#1092)
X-Git-Tag: cvc5-1.0.0~5577
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c5c0c2287203b61acc94bb83fac1b91ae290007;p=cvc5.git

Allow CDHashMaps for objects without default constructors (#1092)

This is a patch, originally from mdeters/cdhashmap-default-constructibility that allows CDHashMaps to be declared for objects that don't have default constructors.
---

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 5b7a4dab1..82aa90891 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -180,7 +180,7 @@ public:
          bool allocatedInCMM = false) :
     ContextObj(allocatedInCMM, context),
     d_key(key),
-    d_data(),
+    d_data(data),
     d_map(NULL),
     d_noTrash(allocatedInCMM) {
 
@@ -343,7 +343,7 @@ public:
     Element* obj;
     if(i == d_map.end()) {// create new object
       obj = new(true) Element(d_context, this, k, Data());
-      d_map[k] = obj;
+      d_map.insert(std::make_pair(k, obj));
     } else {
       obj = (*i).second;
     }
@@ -355,7 +355,7 @@ public:
 
     if(i == d_map.end()) {// create new object
       Element* obj = new(true) Element(d_context, this, k, d);
-      d_map[k] = obj;
+      d_map.insert(std::make_pair(k, obj));
       return true;
     } else {
       (*i).second->set(d);
@@ -392,7 +392,7 @@ public:
 
     Element* obj = new(true) Element(d_context, this, k, d,
                                      true /* atLevelZero */);
-    d_map[k] = obj;
+    d_map.insert(std::make_pair(k, obj));
   }
 
   // FIXME: no erase(), too much hassle to implement efficiently...