1 files changed, 35 insertions, 16 deletions

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 523c5387b..bd74fd4d4 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -24,7 +24,7 @@
 
 #include "cvc4_config.h"
 #include <stdint.h>
-#include "kind.h"
+#include "expr/kind.h"
 
 #include <string>
 #include <iterator>
@@ -98,7 +98,7 @@ class NodeValue {
   NodeValue(int);
 
   /** Destructor decrements the ref counts of its children */
-  ~NodeValue() throw();
+  ~NodeValue();
 
   typedef NodeValue** nv_iterator;
   typedef NodeValue const* const* const_nv_iterator;
@@ -150,16 +150,19 @@ public:
   }
 
   /**
-   * Hash this expression.
+   * Hash this NodeValue.  For hash_maps, hash_sets, etc.. but this is
+   * for expr package internal use only at present!  This is likely to
+   * be POORLY PERFORMING for other uses!  For example, this gives
+   * collisions for all VARIABLEs.
    * @return the hash value of this expression.
    */
-  size_t hash() const {
+  size_t internalHash() const {
     size_t hash = d_kind;
     const_nv_iterator i = nv_begin();
     const_nv_iterator i_end = nv_end();
-    while (i != i_end) {
+    while(i != i_end) {
       hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
-      ++ i;
+      ++i;
     }
     return hash;
   }
@@ -209,7 +212,27 @@ public:
   static inline Kind dKindToKind(unsigned d) {
     return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
   }
-};
+};/* class NodeValue */
+
+/**
+ * For hash_maps, hash_sets, etc.. but this is for expr package
+ * internal use only at present!  This is likely to be POORLY
+ * PERFORMING for other uses!  NodeValue::internalHash() will lead to
+ * collisions for all VARIABLEs.
+ */
+struct NodeValueInternalHashFcn {
+  inline size_t operator()(const NodeValue* nv) const {
+    return (size_t) nv->internalHash();
+  }
+};/* struct NodeValueHashFcn */
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#include "node_manager.h"
+
+namespace CVC4 {
+namespace expr {
 
 inline NodeValue::NodeValue() :
   d_id(0),
@@ -225,7 +248,7 @@ inline NodeValue::NodeValue(int) :
   d_nchildren(0) {
 }
 
-inline NodeValue::~NodeValue() throw() {
+inline NodeValue::~NodeValue() {
   for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
     (*i)->dec();
   }
@@ -243,7 +266,10 @@ inline void NodeValue::dec() {
   if(EXPECT_TRUE( d_rc < MAX_RC )) {
     --d_rc;
     if(EXPECT_FALSE( d_rc == 0 )) {
-      // FIXME gc
+      Assert(NodeManager::currentNM() != NULL,
+             "No current NodeManager on destruction of NodeValue: "
+             "maybe a public CVC4 interface function is missing a NodeManagerScope ?");
+      NodeManager::currentNM()->gc(this);
     }
   }
 }
@@ -264,13 +290,6 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
   return d_children + d_nchildren;
 }
 
-// for hash_maps, hash_sets, ...
-struct NodeValueHashFcn {
-  size_t operator()(const CVC4::expr::NodeValue* nv) const {
-    return (size_t)nv->hash();
-  }
-};/* struct NodeValueHashFcn */
-
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */