This switches the ZombieSet in the NodeManager to use NodeValue's id for equality comparison. The previously used function NodeValueEq incorrectly identified VARIABLE nodes as being equal. This meant that on hash collisions these nodes could leak memory.

3 files changed, 15 insertions, 10 deletions

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 9025aa02a..75521e901 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -150,13 +150,6 @@ static const unsigned MAX_CHILDREN =
 namespace expr {
 
 // Comparison predicate
-struct NodeValueEq {
-  inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
-    return ::CVC4::kind::metakind::NodeValueCompare::compare<false>(nv1, nv2);
-  }
-};
-
-// Comparison predicate
 struct NodeValuePoolEq {
   inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
     return ::CVC4::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
@@ -345,7 +338,7 @@ ${metakind_operatorKinds}
 
 }/* CVC4::kind namespace */
 
-#line 349 "${template}"
+#line 341 "${template}"
 
 namespace theory {
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 0b3830f4b..aaffeb322 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -96,7 +96,7 @@ class NodeManager {
                               expr::NodeValuePoolEq> NodeValuePool;
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
                               expr::NodeValueIDHashFunction,
-                              expr::NodeValueEq> ZombieSet;
+                              expr::NodeValueIDEquality> ZombieSet;
 
   static CVC4_THREADLOCAL(NodeManager*) s_current;
 
@@ -268,7 +268,7 @@ class NodeManager {
       Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
                   << std::endl;
     }
-    d_zombies.insert(nv);// FIXME multithreading
+    d_zombies.insert(nv);  // FIXME multithreading
 
     if(safeToReclaimZombies()) {
       if(d_zombies.size() > 5000) {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index fbf3ff76e..b403d0c86 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -372,6 +372,18 @@ struct NodeValueIDHashFunction {
   }
 };/* struct NodeValueIDHashFunction */
 
+
+/**
+ * An equality predicate that is applicable between pointers to fully
+ * constructed NodeValues.
+ */
+struct NodeValueIDEquality {
+  inline bool operator()(const NodeValue* a, const NodeValue* b) const {
+    return a->getId() == b->getId();
+  }
+};
+
+
 inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 
 }/* CVC4::expr namespace */