* 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, 177 insertions, 50 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 4dc050648..62619e2b6 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -389,28 +389,139 @@ public:
 namespace attr {
 
 /** Default cleanup for unmanaged Attribute<> */
-template <class T>
-struct AttributeCleanupFcn {
-  static inline void cleanup(const T&) {}
-};
+struct NullCleanupFcn {
+};/* struct NullCleanupFcn */
 
 /** Default cleanup for ManagedAttribute<> */
 template <class T>
 struct ManagedAttributeCleanupFcn {
-};
+};/* struct ManagedAttributeCleanupFcn<> */
 
 /** Specialization for T* */
 template <class T>
 struct ManagedAttributeCleanupFcn<T*> {
   static inline void cleanup(T* p) { delete p; }
-};
+};/* struct ManagedAttributeCleanupFcn<T*> */
 
 /** Specialization for const T* */
 template <class T>
 struct ManagedAttributeCleanupFcn<const T*> {
   static inline void cleanup(const T* p) { delete p; }
+};/* struct ManagedAttributeCleanupFcn<const T*> */
+
+/**
+ * Helper for Attribute<> class below to determine whether a cleanup
+ * is defined or not.
+ */
+template <class T, class C>
+struct getCleanupFcn {
+  typedef T value_type;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void fn(typename mapping::table_value_type t) {
+    C::cleanup(mapping::convertBack(t));
+  }
+};/* struct getCleanupFcn<> */
+
+/**
+ * Specialization for NullCleanupFcn.
+ */
+template <class T>
+struct getCleanupFcn<T, NullCleanupFcn> {
+  typedef T value_type;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupFcn<T, NullCleanupFcn> */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupFcn<T, NullCleanupFcn>::fn)(typename getCleanupFcn<T, NullCleanupFcn>::mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupFcn<T>.
+ */
+template <class T>
+struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > {
+  typedef T value_type;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::fn)(typename getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupFcn<T*>.
+ */
+template <class T>
+struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > {
+  typedef T* value_type;
+  typedef ManagedAttributeCleanupFcn<value_type> C;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void fn(typename mapping::table_value_type t) {
+    C::cleanup(mapping::convertBack(t));
+  }
+};/* struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > */
+
+/**
+ * Specialization for ManagedAttributeCleanupFcn<const T*>.
+ */
+template <class T>
+struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > {
+  typedef const T* value_type;
+  typedef ManagedAttributeCleanupFcn<value_type> C;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void fn(typename mapping::table_value_type t) {
+    C::cleanup(mapping::convertBack(t));
+  }
+};/* struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > */
+
+/**
+ * Cause compile-time error for improperly-instantiated
+ * getCleanupFcn<>.
+ */
+template <class T, class U>
+struct getCleanupFcn<T, ManagedAttributeCleanupFcn<U> >;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
+
+namespace attr {
+
+/**
+ * This is the last-attribute-assigner.  IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
+template <class T, bool context_dep>
+struct LastAttributeId {
+  static uint64_t s_id;
+};
+
+/** Initially zero. */
+template <class T, bool context_dep>
+uint64_t LastAttributeId<T, context_dep>::s_id = 0;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE TRAITS ============================================================
+
+namespace attr {
+
+/**
+ * This is the last-attribute-assigner.  IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
+template <class T, bool context_dep>
+struct AttributeTraits {
+  typedef void (*cleanup_t)(T);
+  static std::vector<cleanup_t> cleanup;
 };
 
+template <class T, bool context_dep>
+std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
+  AttributeTraits<T, context_dep>::cleanup;
+
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE DEFINITION ========================================================
@@ -431,9 +542,16 @@ struct ManagedAttributeCleanupFcn<const T*> {
  */
 template <class T,
           class value_t,
-          class CleanupFcn = attr::AttributeCleanupFcn<value_t>,
+          class CleanupFcn = attr::NullCleanupFcn,
           bool context_dep = false>
-struct Attribute {
+class Attribute {
+  /**
+   * The unique ID associated to this attribute.  Assigned statically,
+   * at load time.
+   */
+  static const uint64_t s_id;
+
+public:
 
   /** The value type for this attribute. */
   typedef value_t value_type;
@@ -454,20 +572,43 @@ struct Attribute {
    */
   static const bool context_dependent = context_dep;
 
-private:
-
   /**
-   * The unique ID associated to this attribute.  Assigned statically,
-   * at load time.
+   * Register this attribute kind and check that the ID is a valid ID
+   * for bool-valued attributes.  Fail an assert if not.  Otherwise
+   * return the id.
    */
-  static const uint64_t s_id;
+  static inline uint64_t registerAttribute() {
+    typedef typename attr::KindValueToTableValueMapping<value_t>::table_value_type table_value_type;
+    typedef attr::AttributeTraits<table_value_type, context_dep> traits;
+    uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
+    Assert(traits::cleanup.size() == id);// sanity check
+    traits::cleanup.push_back(attr::getCleanupFcn<value_t, CleanupFcn>::fn);
+    return id;
+  }
+};/* class Attribute<> */
+
+/**
+ * An "attribute type" structure for boolean flags (special).  The
+ * full one is below; the existence of this one disallows for boolean
+ * flag attributes with a specialized cleanup function.
+ */
+/* -- doesn't work; other specialization is "more specific" ??
+template <class T, class CleanupFcn, bool context_dep>
+class Attribute<T, bool, CleanupFcn, context_dep> {
+  template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
+  ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
 };
+*/
 
 /**
  * An "attribute type" structure for boolean flags (special).
  */
-template <class T, class CleanupFcn, bool context_dep>
-struct Attribute<T, bool, CleanupFcn, context_dep> {
+template <class T, bool context_dep>
+class Attribute<T, bool, attr::NullCleanupFcn, context_dep> {
+  /** IDs for bool-valued attributes are actually bit assignments. */
+  static const uint64_t s_id;
+
+public:
 
   /** The value type for this attribute; here, bool. */
   typedef bool value_type;
@@ -495,21 +636,18 @@ struct Attribute<T, bool, CleanupFcn, context_dep> {
   static const bool context_dependent = context_dep;
 
   /**
-   * Check that the ID is a valid ID for bool-valued attributes.  Fail
-   * an assert if not.  Otherwise return the id.
+   * Register this attribute kind and check that the ID is a valid ID
+   * for bool-valued attributes.  Fail an assert if not.  Otherwise
+   * return the id.
    */
-  static inline uint64_t checkID(uint64_t id) {
+  static inline uint64_t registerAttribute() {
+    uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++;
     AlwaysAssert( id <= 63,
                   "Too many boolean node attributes registered "
                   "during initialization !" );
     return id;
   }
-
-private:
-
-  /** IDs for bool-valued attributes are actually bit assignments. */
-  static const uint64_t s_id;
-};
+};/* class Attribute<..., bool, ...> */
 
 /**
  * This is a context-dependent attribute kind (the only difference
@@ -520,7 +658,7 @@ private:
 template <class T,
           class value_type>
 struct CDAttribute :
-    public Attribute<T, value_type, attr::AttributeCleanupFcn<value_type>, true> {};
+    public Attribute<T, value_type, attr::NullCleanupFcn, true> {};
 
 /**
  * This is a managed attribute kind (the only difference between
@@ -541,35 +679,21 @@ struct ManagedAttribute :
 
 // ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
 
-namespace attr {
-
-/**
- * This is the last-attribute-assigner.  IDs are not globally
- * unique; rather, they are unique for each table_value_type.
- */
-template <class T, bool context_dep>
-struct LastAttributeId {
-  static uint64_t s_id;
-};
-
-/** Initially zero. */
-template <class T, bool context_dep>
-uint64_t LastAttributeId<T, context_dep>::s_id = 0;
-
-}/* CVC4::expr::attr namespace */
-
 /** Assign unique IDs to attributes at load time. */
+// Use of the comma-operator here forces instantiation (and
+// initialization) of the AttributeTraits<> structure and its
+// "cleanup" vector before registerAttribute() is called.  This is
+// important because otherwise the vector is initialized later,
+// clearing the first-pushed cleanup function.
 template <class T, class value_t, class CleanupFcn, bool context_dep>
 const uint64_t Attribute<T, value_t, CleanupFcn, context_dep>::s_id =
-  attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::s_id++;
+  ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::cleanup.size(),
+    Attribute<T, value_t, CleanupFcn, context_dep>::registerAttribute() );
 
-/**
- * Assign unique IDs to bool-valued attributes at load time, checking
- * that they are in range.
- */
-template <class T, class CleanupFcn, bool context_dep>
-const uint64_t Attribute<T, bool, CleanupFcn, context_dep>::s_id =
-  Attribute<T, bool, CleanupFcn, context_dep>::checkID(attr::LastAttributeId<bool, context_dep>::s_id++);
+/** Assign unique IDs to attributes at load time. */
+template <class T, bool context_dep>
+const uint64_t Attribute<T, bool, attr::NullCleanupFcn, context_dep>::s_id =
+  Attribute<T, bool, attr::NullCleanupFcn, context_dep>::registerAttribute();
 
 // ATTRIBUTE MANAGER ===========================================================
 
@@ -609,6 +733,9 @@ class AttributeManager {
   /** Underlying hash table for context-dependent pointer-valued attributes */
   CDAttrHash<void*> d_cdptrs;
 
+  template <class T>
+  void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
+
   /**
    * getTable<> is a helper template that gets the right table from an
    * AttributeManager given its type.