Merge pull request #102 from timothy-king/node-id-eq

This switches the ZombieSet in the NodeManager to use NodeValue's id …

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 */