* 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

11 files changed, 362 insertions, 148 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
         /*
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.
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 2f84f018b..6f611cf95 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -91,7 +91,7 @@ size_t Expr::getNumChildren() const {
   return d_node->getNumChildren();
 }
 
-const Type* Expr::getType() const {
+Type* Expr::getType() const {
   ExprManagerScope ems(*this);
   return d_node->getType();
 }
diff --git a/src/expr/expr.h b/src/expr/expr.h
index b297be6fb..c5478b1da 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -106,7 +106,7 @@ public:
   /** Returns the type of the expression, if it has been computed.
    * Returns NULL if the type of the expression is not known.
    */
-  const Type* getType() const;
+  Type* getType() const;
 
   /**
    * Returns the string representation of the expression.
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index f0a35e5f1..0b0139118 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -42,12 +42,12 @@ ExprManager::~ExprManager() {
   delete d_ctxt;
 }
 
-const BooleanType* ExprManager::booleanType() const {
+BooleanType* ExprManager::booleanType() const {
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->booleanType();
 }
 
-const KindType* ExprManager::kindType() const {
+KindType* ExprManager::kindType() const {
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->kindType();
 }
@@ -106,32 +106,30 @@ Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
 }
 
 /** Make a function type from domain to range. */
-const FunctionType* 
-ExprManager::mkFunctionType(const Type* domain, 
-                            const Type* range) {
+FunctionType* ExprManager::mkFunctionType(Type* domain,
+                                          Type* range) {
   NodeManagerScope nms(d_nodeManager);
-  return d_nodeManager->mkFunctionType(domain,range);
+  return d_nodeManager->mkFunctionType(domain, range);
 }
 
 /** Make a function type with input types from argTypes. */
-const FunctionType* 
-ExprManager::mkFunctionType(const std::vector<const Type*>& argTypes, 
-                            const Type* range) {
+FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes,
+                                          Type* range) {
   NodeManagerScope nms(d_nodeManager);
-  return d_nodeManager->mkFunctionType(argTypes,range);
+  return d_nodeManager->mkFunctionType(argTypes, range);
 }
 
-const Type* ExprManager::mkSort(const std::string& name) {
+Type* ExprManager::mkSort(const std::string& name) {
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkSort(name);
 }
 
-Expr ExprManager::mkVar(const Type* type, const std::string& name) {
+Expr ExprManager::mkVar(Type* type, const std::string& name) {
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
 }
 
-Expr ExprManager::mkVar(const Type* type) {
+Expr ExprManager::mkVar(Type* type) {
   NodeManagerScope nms(d_nodeManager);
   return Expr(this, new Node(d_nodeManager->mkVar(type)));
 }
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index ff4e0db6b..3c73e1ced 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -51,10 +51,10 @@ public:
   ~ExprManager();
 
   /** Get the type for booleans */
-  const BooleanType* booleanType() const;
+  BooleanType* booleanType() const;
 
   /** Get the type for sorts. */
-  const KindType* kindType() const;
+  KindType* kindType() const;
 
   /**
    * Make a unary expression of a given kind (TRUE, FALSE,...).
@@ -95,21 +95,21 @@ public:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /** Make a function type from domain to range. */
-  const FunctionType*
-    mkFunctionType(const Type* domain,
-                   const Type* range);
+  FunctionType*
+    mkFunctionType(Type* domain,
+                   Type* range);
 
   /** Make a function type with input types from argTypes. */
-  const FunctionType*
-    mkFunctionType(const std::vector<const Type*>& argTypes,
-                   const Type* range);
+  FunctionType*
+    mkFunctionType(const std::vector<Type*>& argTypes,
+                   Type* range);
 
   /** Make a new sort with the given name. */
-  const Type* mkSort(const std::string& name);
+  Type* mkSort(const std::string& name);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(const Type* type, const std::string& name);
-  Expr mkVar(const Type* type);
+  Expr mkVar(Type* type, const std::string& name);
+  Expr mkVar(Type* type);
 
 private:
   /** The context */
diff --git a/src/expr/node.h b/src/expr/node.h
index d1bb8f3b3..25990cedf 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -240,7 +240,7 @@ public:
    * Returns the type of this node.
    * @return the type
    */
-  const Type* getType() const;
+  Type* getType() const;
 
   /**
    * Returns the kind of this node.
@@ -707,7 +707,7 @@ bool NodeTemplate<ref_count>::hasOperator() const {
 }
 
 template <bool ref_count>
-const Type* NodeTemplate<ref_count>::getType() const {
+Type* NodeTemplate<ref_count>::getType() const {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
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);
     }
   }
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index b40ec2978..a3be61e48 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -30,6 +30,7 @@
 #include "expr/expr.h"
 #include "expr/node_value.h"
 #include "context/context.h"
+#include "expr/type.h"
 
 namespace CVC4 {
 
@@ -44,7 +45,7 @@ struct Type {};
 }/* CVC4::expr::attr namespace */
 
 typedef Attribute<attr::VarName, std::string> VarNameAttr;
-typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
+typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupFcn> TypeAttr;
 
 }/* CVC4::expr namespace */
 
@@ -55,12 +56,12 @@ class NodeManager {
 
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
                               expr::NodeValueInternalHashFcn,
-                              expr::NodeValue::NodeValueEq> NodeValueSet;
+                              expr::NodeValue::NodeValueEq> NodeValuePool;
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
                               expr::NodeValueIDHashFcn,
                               expr::NodeValue::NodeValueEq> ZombieSet;
 
-  NodeValueSet d_nodeValueSet;
+  NodeValuePool d_nodeValuePool;
 
   expr::attr::AttributeManager d_attrManager;
 
@@ -108,6 +109,8 @@ public:
     poolInsert( &expr::NodeValue::s_null );
   }
 
+  ~NodeManager();
+
   static NodeManager* currentNM() { return s_current; }
 
   // general expression-builders
@@ -121,8 +124,8 @@ public:
   Node mkNode(Kind kind, const std::vector<Node>& children);
 
   // variables are special, because duplicates are permitted
-  Node mkVar(const Type* type, const std::string& name);
-  Node mkVar(const Type* type);
+  Node mkVar(Type* type, const std::string& name);
+  Node mkVar(Type* type);
   Node mkVar();
 
   template <class AttrKind>
@@ -172,27 +175,26 @@ public:
                            const typename AttrKind::value_type& value);
 
   /** Get the type for booleans. */
-  inline const BooleanType* booleanType() const {
+  inline BooleanType* booleanType() const {
     return BooleanType::getInstance();
   }
 
   /** Get the type for sorts. */
-  inline const KindType* kindType() const {
+  inline KindType* kindType() const {
     return KindType::getInstance();
   }
 
   /** Make a function type from domain to range. */
-  inline const FunctionType*
-  mkFunctionType(const Type* domain, const Type* range) const;
+  inline FunctionType* mkFunctionType(Type* domain, Type* range) const;
 
   /** Make a function type with input types from argTypes. */
-  inline const FunctionType*
-  mkFunctionType(const std::vector<const Type*>& argTypes, const Type* range) const;
+  inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
+                                      Type* range) const;
 
   /** Make a new sort with the given name. */
-  inline const Type* mkSort(const std::string& name) const;
+  inline Type* mkSort(const std::string& name) const;
 
-  inline const Type* getType(TNode n) const;
+  inline Type* getType(TNode n) const;
 };
 
 /**
@@ -308,41 +310,39 @@ inline void NodeManager::setAttribute(TNode n,
 
 /** Make a function type from domain to range.
  * TODO: Function types should be unique for this manager. */
-const FunctionType*
-NodeManager::mkFunctionType(const Type* domain,
-                            const Type* range) const {
-  std::vector<const Type*> argTypes;
+FunctionType* NodeManager::mkFunctionType(Type* domain,
+                                          Type* range) const {
+  std::vector<Type*> argTypes;
   argTypes.push_back(domain);
   return new FunctionType(argTypes, range);
 }
 
 /** Make a function type with input types from argTypes.
  * TODO: Function types should be unique for this manager. */
-const FunctionType*
-NodeManager::mkFunctionType(const std::vector<const Type*>& argTypes,
-                            const Type* range) const {
+FunctionType* NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
+                                          Type* range) const {
   Assert( argTypes.size() > 0 );
   return new FunctionType(argTypes, range);
 }
 
-const Type*
-NodeManager::mkSort(const std::string& name) const {
+Type* NodeManager::mkSort(const std::string& name) const {
   return new SortType(name);
 }
-inline const Type* NodeManager::getType(TNode n) const {
+
+inline Type* NodeManager::getType(TNode n) const {
   return getAttribute(n, CVC4::expr::TypeAttr());
 }
 
 inline void NodeManager::poolInsert(expr::NodeValue* nv) {
-  Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(),
+  Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
          "NodeValue already in the pool!");
-  d_nodeValueSet.insert(nv);// FIXME multithreading
+  d_nodeValuePool.insert(nv);// FIXME multithreading
 }
 
 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
-  Assert(d_nodeValueSet.find(nv) != d_nodeValueSet.end(),
+  Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
          "NodeValue is not in the pool!");
-  d_nodeValueSet.erase(nv);// FIXME multithreading
+  d_nodeValuePool.erase(nv);// FIXME multithreading
 }
 
 }/* CVC4 namespace */
@@ -382,14 +382,15 @@ inline Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
   return NodeBuilder<>(this, kind).append(children);
 }
 
-inline Node NodeManager::mkVar(const Type* type, const std::string& name) {
+inline Node NodeManager::mkVar(Type* type, const std::string& name) {
   Node n = mkVar(type);
   n.setAttribute(expr::VarNameAttr(), name);
   return n;
 }
 
-inline Node NodeManager::mkVar(const Type* type) {
+inline Node NodeManager::mkVar(Type* type) {
   Node n = mkVar();
+  type->inc();// reference-count the type
   n.setAttribute(expr::TypeAttr(), type);
   return n;
 }
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 4bdda6810..2549f02ca 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -26,11 +26,12 @@ std::ostream& operator<<(std::ostream& out, const Type& e) {
 }
 
 Type::Type() :
-  d_name(std::string("<undefined>")) {
+  d_name(std::string("<undefined>")),
+  d_rc(0) {
 }
 
 Type::Type(std::string name) : 
-  d_name(name) { 
+  d_name(name) {
 }
 
 std::string Type::getName() const {
@@ -39,7 +40,9 @@ std::string Type::getName() const {
 
 BooleanType BooleanType::s_instance;
 
-BooleanType::BooleanType() : Type(std::string("BOOLEAN")) {
+BooleanType::BooleanType() :
+  Type(std::string("BOOLEAN")) {
+  d_rc = RC_MAX;// singleton, not heap-allocated
 }
 
 BooleanType::~BooleanType() {
@@ -54,22 +57,23 @@ bool BooleanType::isBoolean() const {
   return true;
 }
 
-FunctionType::FunctionType(const std::vector<const Type*>& argTypes,
-                           const Type* range) 
-  : d_argTypes(argTypes),
-    d_rangeType(range) {
+FunctionType::FunctionType(const std::vector<Type*>& argTypes,
+                           Type* range) :
+  d_argTypes(argTypes),
+  d_rangeType(range) {
+
   Assert( argTypes.size() > 0 );
 }
 
-  // FIXME: What becomes of argument types?
+// FIXME: What becomes of argument types?
 FunctionType::~FunctionType() {
 }
 
-const std::vector<const Type*> FunctionType::getArgTypes() const {
+const std::vector<Type*> FunctionType::getArgTypes() const {
   return d_argTypes;
 }
 
-const Type* FunctionType::getRangeType() const {
+Type* FunctionType::getRangeType() const {
   return d_rangeType;
 }
 
@@ -100,7 +104,9 @@ void FunctionType::toStream(std::ostream& out) const {
 
 KindType KindType::s_instance;
 
-KindType::KindType() : Type(std::string("KIND")) {
+KindType::KindType() :
+  Type(std::string("KIND")) {
+  d_rc = RC_MAX;// singleton, not heap-allocated
 }
 
 KindType::~KindType() {
@@ -115,12 +121,11 @@ KindType::getInstance() {
   return &s_instance;
 }
 
-SortType::SortType(std::string name)
-  : Type(name) {
+SortType::SortType(std::string name) :
+  Type(name) {
 }
 
 SortType::~SortType() {
 }
 
-
 }
diff --git a/src/expr/type.h b/src/expr/type.h
index 7009ed504..fd9ea01d7 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -17,19 +17,32 @@
 #define __CVC4__TYPE_H
 
 #include "cvc4_config.h"
+#include "util/output.h"
+#include "util/Assert.h"
 
 #include <string>
 #include <vector>
+#include <limits.h>
 
 namespace CVC4 {
 
+namespace expr {
+  namespace attr {
+    struct TypeCleanupFcn;
+  }/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+
 class NodeManager;
 
 /**
  * Class encapsulating CVC4 expression types.
  */
 class CVC4_PUBLIC Type {
+protected:
+  static const unsigned RC_MAX = UINT_MAX;
+
 public:
+
   /** Comparision for equality */
   bool operator==(const Type& t) const;
 
@@ -72,11 +85,38 @@ protected:
   /** Create a type with the given name. */
   Type(std::string name);
 
-  /** Destructor */
-  virtual ~Type() { };
-
   /** The name of the type (may be empty). */
   std::string d_name;
+
+  /**
+   * The reference count for this Type (how many times it's referred
+   * to in the Type attribute table)
+   */
+  unsigned d_rc;
+
+  /** Force a virtual destructor for safety. */
+  virtual ~Type() {
+    Assert(d_rc == RC_MAX || d_rc == 0,
+           "illegal ref count %u for destructed Type", d_rc);
+  }
+
+  /** Increment the reference count */
+  void inc() {
+    if(d_rc != RC_MAX) {
+      ++d_rc;
+    }
+  }
+
+  /** Decrement the reference count */
+  void dec() {
+    if(d_rc != RC_MAX) {
+      Assert(d_rc != 0, "illegal ref count %u for dec()", d_rc);
+      --d_rc;
+    }
+  }
+
+  friend class ::CVC4::NodeManager;
+  friend struct ::CVC4::expr::attr::TypeCleanupFcn;
 };
 
 /**
@@ -117,10 +157,10 @@ class FunctionType : public Type {
 
 public:
   /** Retrieve the argument types. The vector will be non-empty. */
-  const std::vector<const Type*> getArgTypes() const;
+  const std::vector<Type*> getArgTypes() const;
 
   /** Get the range type (i.e., the type of the result). */
-  const Type* getRangeType() const;
+  Type* getRangeType() const;
   
   /** Is this as function type? (Returns true.) */
   bool isFunction() const;
@@ -141,17 +181,17 @@ private:
    * @param argTypes a non-empty vector of input types
    * @param range the result type
    */
-  FunctionType(const std::vector<const Type*>& argTypes,
-               const Type* range);
+  FunctionType(const std::vector<Type*>& argTypes,
+               Type* range);
 
   /** Destructor */
   ~FunctionType();
   
   /** The list of input types. */
-  const std::vector<const Type*> d_argTypes;
+  const std::vector<Type*> d_argTypes;
 
   /** The result type. */
-  const Type* d_rangeType;
+  Type* d_rangeType;
 
   friend class NodeManager;
 };
@@ -211,6 +251,22 @@ private:
  */
 std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
 
-}
+namespace expr {
+namespace attr {
+
+struct TypeCleanupFcn {
+  static void cleanup(Type* t) {
+    // reference-count the Type
+    t->dec();
+    if(t->d_rc == 0) {
+      delete t;
+    }
+  }
+};
+
+}/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+
+}/* CVC4 namespace */
 
 #endif /* __CVC4__TYPE_H */