minor changes to cdmap/cdset interface for detection of duplicate inserts

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 45ff68a2326a7581816869c89b3b5a8e57ccfe76..5e5a07f2fd83edca5a58ac1c12791848c40dc288 100644 (file)
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -363,7 +363,7 @@ public:
     return *obj;
   }
 
-  void insert(const Key& k, const Data& d) {
+  bool insert(const Key& k, const Data& d) {
     emptyTrash();
 
     typename table_type::iterator i = d_map.find(k);
@@ -371,8 +371,10 @@ public:
     if(i == d_map.end()) {// create new object
       Element* obj = new(true) Element(d_context, this, k, d);
       d_map[k] = obj;
+      return true;
     } else {
       (*i).second->set(d);
+      return false;
     }
   }
 

diff --git a/src/context/cdset.h b/src/context/cdset.h
index 40d504cad571335273d93391e063994a920f479c..7032f76ba2ffa65eb27bc11a78f73fa3d9498ef4 100644 (file)
--- a/src/context/cdset.h
+++ b/src/context/cdset.h
@@ -22,6 +22,7 @@
 #define __CVC4__CONTEXT__CDSET_H
 
 #include "context/context.h"
+#include "context/cdmap.h"
 #include "util/Assert.h"
 
 namespace CVC4 {
@@ -45,8 +46,12 @@ public:
     return super::count(v);
   }
 
-  void insert(const V& v) {
-    super::insert(v, v);
+  bool insert(const V& v) {
+    return super::insert(v, v);
+  }
+
+  bool contains(const V& v) {
+    return find(v) != end();
   }
 
   // FIXME: no erase(), too much hassle to implement efficiently...