* 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, 31 insertions, 12 deletions

diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index e8e93f6ff..be54a973e 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -17,24 +17,43 @@
 #include "expr/node_value.h"
 #include "util/output.h"
 
+#include <utility>
+
+using namespace std;
+
 namespace CVC4 {
 namespace expr {
 namespace attr {
 
+/**
+ * Search for the NodeValue in all attribute tables and remove it,
+ * calling the cleanup function if one is defined.
+ */
+template <class T>
+inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
+                                              NodeValue* nv) {
+  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
+    typedef AttributeTraits<T, false> traits_t;
+    typedef AttrHash<T> hash_t;
+    pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv);
+    if(traits_t::cleanup[id] != NULL) {
+      typename hash_t::iterator i = table.find(pr);
+      if(i != table.end()) {
+        traits_t::cleanup[id]((*i).second);
+        table.erase(pr);
+      }
+    } else {
+      table.erase(pr);
+    }
+  }
+}
+
 void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   d_bools.erase(nv);
-  for(unsigned id = 0; id < attr::LastAttributeId<uint64_t, false>::s_id; ++id) {
-    d_ints.erase(std::make_pair(id, nv));
-  }
-  for(unsigned id = 0; id < attr::LastAttributeId<TNode, false>::s_id; ++id) {
-    d_exprs.erase(std::make_pair(id, nv));
-  }
-  for(unsigned id = 0; id < attr::LastAttributeId<std::string, false>::s_id; ++id) {
-    d_strings.erase(std::make_pair(id, nv));
-  }
-  for(unsigned id = 0; id < attr::LastAttributeId<void*, false>::s_id; ++id) {
-    d_ptrs.erase(std::make_pair(id, nv));
-  }
+  deleteFromTable(d_ints, nv);
+  deleteFromTable(d_exprs, nv);
+  deleteFromTable(d_strings, nv);
+  deleteFromTable(d_ptrs, nv);
 
   // FIXME CD-bools in optimized table
         /*