* test/unit/Makefile.am, test/unit/expr/attribute_white.h,

  test/unit/expr/node_white.h: add whitebox attribute test (pulled out
  attribute stuff from node_white)

* test/unit/parser/parser_black.h: fix memory leaks uncovered by
  valgrind

* src/theory/interrupted.h: actually make this "lightweight" (not
  derived from CVC4::Exception), as promised in my last commit

* src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match
  the new-style cleanup function definition

* src/expr/attribute.cpp, src/expr/attribute.h: support for attribute
  deletion, custom cleanup functions, clearer cleanup function
  definition.

* src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim
  remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool",
  and enable freeing of NodeValues

* src/expr/type.h, src/expr/type.cpp: reference-counting for types,
  customized cleanup function for types, also code cleanup

* (various): changed "const Type*" to "Type*" (to enable
  reference-counting etc.  Types are still immutable.)

* src/util/output.h: add ::isOn()-- which queries whether a
  Debug/Trace flag is currently on or not.

* src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp,
  src/expr/type.cpp, src/expr/expr_manager.cpp, various others:
  minor code cleanup

1 files changed, 13 insertions, 5 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 7be593575..7b171a48b 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -25,9 +25,18 @@ namespace CVC4 {
 
 __thread NodeManager* NodeManager::s_current = 0;
 
+NodeManager::~NodeManager() {
+  NodeManagerScope nms(this);
+  while(!d_zombies.empty()) {
+    reclaimZombies();
+  }
+
+  poolRemove( &expr::NodeValue::s_null );
+}
+
 NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
-  NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
-  if(find == d_nodeValueSet.end()) {
+  NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
+  if(find == d_nodeValuePool.end()) {
     return NULL;
   } else {
     return *find;
@@ -87,7 +96,7 @@ void NodeManager::reclaimZombies() {
     NodeValue* nv = *i;
 
     // collect ONLY IF still zero
-    if((*i)->d_rc == 0) {
+    if(nv->d_rc == 0) {
       Debug("gc") << "deleting node value " << nv
                   << " [" << nv->d_id << "]: " << nv->toString() << "\n";
 
@@ -101,8 +110,7 @@ void NodeManager::reclaimZombies() {
 
       // decr ref counts of children
       nv->decrRefCounts();
-      //free(nv);
-#warning NOT FREEING NODEVALUES
+      free(nv);
     }
   }
 }