This switches the ZombieSet in the NodeManager to use NodeValue's id for equality...

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 9025aa02a3ac181e5663b39c32d3820da9f11d09..75521e901ae63e573b4e4321a194eeb4128151eb 100644 (file)
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -149,13 +149,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 {
@@ -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 0b3830f4b01e1b7a802427004e9e097de6c9f184..aaffeb322161aa49e682bad7871378b8af017eee 100644 (file)
--- 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 fbf3ff76ed43687fa1d038c447ae03f642961097..b403d0c863df12205bfbc61e5b070a7501fd3a16 100644 (file)
--- 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 */