Marging from types 404:415, changes: Massive

* Types are now represented as nodes in the attribute table and are managed, i.e. you can say
    Type booleanType = d_nodeManager->booleanType();
    Type t = d_nodeManager->mkFunctionType(booleanType, booleanType);
    FunctionType ft = (FunctionType)t;
    Assert(ft.getArgTypes()[0], booleanType);
* The attributes now have a table for Nodes and a table for TNodes (both should be used with caution)
* Changes the way nodes are extracted from NodeBuilder, added several methods to
  extract a Node, NodeValue, or Node*, with corresponding methods for extraction
* Used the above in the construction of Expr and Type objects
* The NodeManager now destroys the attributes in the destructor by pausing the
  garbage collection
* To achive destruction a flag d_inDesctruction has been added to loosen the assertion
  in NodeValue::dec() (there might be -refcount TNodes leftover)
* Beginnings of the Bitvector constants using GMP

Not yet in tiptop phase, needs more documentation, and Types should be pulled out to TypeNodes eventually. Also, the types are currently defined in the builting_kinds, and I need to add these to the theory specific definitions with special 'type' constructs.

I hate branching and merging.

20 files changed, 912 insertions, 431 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index a9480723f..0abeebb9e 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -26,7 +26,8 @@ libexpr_la_SOURCES = \
 	command.h \
 	command.cpp \
 	declaration_scope.h \
-	declaration_scope.cpp
+	declaration_scope.cpp \
+	expr_manager_scope.h 
 
 EXTRA_DIST = \
 	@srcdir@/kind.h \
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 1eeec68af..e5a50591f 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -28,7 +28,8 @@ namespace attr {
 void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   d_bools.erase(nv);
   deleteFromTable(d_ints, nv);
-  deleteFromTable(d_exprs, nv);
+  deleteFromTable(d_tnodes, nv);
+  deleteFromTable(d_nodes, nv);
   deleteFromTable(d_strings, nv);
   deleteFromTable(d_ptrs, nv);
 
@@ -40,7 +41,10 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
     d_cdints.obliterate(std::make_pair(id, nv));
   }
   for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) {
-    d_cdexprs.obliterate(std::make_pair(id, nv));
+    d_cdtnodes.obliterate(std::make_pair(id, nv));
+  }
+  for(unsigned id = 0; id < attr::LastAttributeId<TNode, true>::s_id; ++id) {
+    d_cdnodes.obliterate(std::make_pair(id, nv));
   }
   for(unsigned id = 0; id < attr::LastAttributeId<std::string, true>::s_id; ++id) {
     d_cdstrings.obliterate(std::make_pair(id, nv));
@@ -50,6 +54,24 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   }
 }
 
+void AttributeManager::deleteAllAttributes() {
+  d_bools.clear();
+  deleteAllFromTable(d_ints);
+  deleteAllFromTable(d_tnodes);
+  deleteAllFromTable(d_nodes);
+  deleteAllFromTable(d_strings);
+  deleteAllFromTable(d_ptrs);
+
+  // FIXME CD-bools in optimized table
+  d_cdbools.clear();
+  d_cdints.clear();
+  d_cdtnodes.clear();
+  d_cdnodes.clear();
+  d_cdstrings.clear();
+  d_cdptrs.clear();
+}
+
+
 }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 27cddf299..4250bb3ef 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -29,7 +29,6 @@
 
 #include "context/cdmap.h"
 #include "expr/node.h"
-#include "expr/type.h"
 #include "util/output.h"
 
 // include supporting templates
@@ -57,7 +56,9 @@ class AttributeManager {
   /** Underlying hash table for integral-valued attributes */
   AttrHash<uint64_t> d_ints;
   /** Underlying hash table for node-valued attributes */
-  AttrHash<TNode> d_exprs;
+  AttrHash<TNode> d_tnodes;
+  /** Underlying hash table for node-valued attributes */
+  AttrHash<Node> d_nodes;
   /** Underlying hash table for string-valued attributes */
   AttrHash<std::string> d_strings;
   /** Underlying hash table for pointer-valued attributes */
@@ -71,7 +72,9 @@ class AttributeManager {
   /** Underlying hash table for context-dependent integral-valued attributes */
   CDAttrHash<uint64_t> d_cdints;
   /** Underlying hash table for context-dependent node-valued attributes */
-  CDAttrHash<TNode> d_cdexprs;
+  CDAttrHash<TNode> d_cdtnodes;
+  /** Underlying hash table for context-dependent node-valued attributes */
+  CDAttrHash<Node> d_cdnodes;
   /** Underlying hash table for context-dependent string-valued attributes */
   CDAttrHash<std::string> d_cdstrings;
   /** Underlying hash table for context-dependent pointer-valued attributes */
@@ -80,6 +83,9 @@ class AttributeManager {
   template <class T>
   void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
 
+  template <class T>
+  void deleteAllFromTable(AttrHash<T>& table);
+
   /**
    * getTable<> is a helper template that gets the right table from an
    * AttributeManager given its type.
@@ -93,7 +99,8 @@ public:
   AttributeManager(context::Context* ctxt) :
     d_cdbools(ctxt),
     d_cdints(ctxt),
-    d_cdexprs(ctxt),
+    d_cdtnodes(ctxt),
+    d_cdnodes(ctxt),
     d_cdstrings(ctxt),
     d_cdptrs(ctxt) {
   }
@@ -166,6 +173,11 @@ public:
    * @param nv the node from which to delete attributes
    */
   void deleteAllAttributes(NodeValue* nv);
+
+  /**
+   * Remove all attributes from the tables.
+   */
+  void deleteAllAttributes();
 };
 
 }/* CVC4::expr::attr namespace */
@@ -205,15 +217,27 @@ struct getTable<uint64_t, false> {
   }
 };
 
-/** Access the "d_exprs" member of AttributeManager. */
+/** Access the "d_tnodes" member of AttributeManager. */
 template <>
 struct getTable<TNode, false> {
   typedef AttrHash<TNode> table_type;
   static inline table_type& get(AttributeManager& am) {
-    return am.d_exprs;
+    return am.d_tnodes;
   }
   static inline const table_type& get(const AttributeManager& am) {
-    return am.d_exprs;
+    return am.d_tnodes;
+  }
+};
+
+/** Access the "d_nodes" member of AttributeManager. */
+template <>
+struct getTable<Node, false> {
+  typedef AttrHash<Node> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_nodes;
+  }
+  static inline const table_type& get(const AttributeManager& am) {
+    return am.d_nodes;
   }
 };
 
@@ -277,15 +301,27 @@ struct getTable<uint64_t, true> {
   }
 };
 
-/** Access the "d_cdexprs" member of AttributeManager. */
+/** Access the "d_tnodes" member of AttributeManager. */
 template <>
 struct getTable<TNode, true> {
   typedef CDAttrHash<TNode> table_type;
   static inline table_type& get(AttributeManager& am) {
-    return am.d_cdexprs;
+    return am.d_cdtnodes;
+  }
+  static inline const table_type& get(const AttributeManager& am) {
+    return am.d_cdtnodes;
+  }
+};
+
+/** Access the "d_nodes" member of AttributeManager. */
+template <>
+struct getTable<Node, true> {
+  typedef CDAttrHash<Node> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_cdnodes;
   }
   static inline const table_type& get(const AttributeManager& am) {
-    return am.d_cdexprs;
+    return am.d_cdnodes;
   }
 };
 
@@ -499,6 +535,27 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
   }
 }
 
+/**
+ * Remove all attributes from the table calling the cleanup function if one is defined.
+ */
+template <class T>
+inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
+  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
+    typedef AttributeTraits<T, false> traits_t;
+    typedef AttrHash<T> hash_t;
+    if(traits_t::cleanup[id] != NULL) {
+      typename hash_t::iterator it = table.begin();
+      typename hash_t::iterator it_end = table.end();
+      while (it != it_end) {
+        traits_t::cleanup[id]((*it).second);
+        ++ it;
+      }
+    }
+    table.clear();
+  }
+}
+
+
 }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 0ae2cdc22..4ac89afec 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -341,6 +341,13 @@ public:
     super::erase(nv);
   }
 
+  /**
+   * Clear the hash table.
+   */
+  void clear() {
+    super::clear();
+  }
+
 };/* class AttrHash<bool> */
 
 /**
diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
index c4eb3af1c..eb41c788e 100644
--- a/src/expr/builtin_kinds
+++ b/src/expr/builtin_kinds
@@ -120,3 +120,11 @@ operator DISTINCT 2: "disequality"
 variable SKOLEM "skolem var"
 variable VARIABLE "variable"
 operator TUPLE 2: "a tuple"
+
+constant TYPE_CONSTANT \
+    ::CVC4::TypeConstant \
+    ::CVC4::TypeConstantHashStrategy \
+    "expr/type_constant.h" \
+    "basic types"
+operator FUNCTION_TYPE 2: "function type"
+variable SORT_TYPE "sort type"
diff --git a/src/expr/command.h b/src/expr/command.h
index 6a4bb67ed..bb295a662 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -27,6 +27,7 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "expr/type.h"
 #include "util/result.h"
 
 namespace CVC4 {
@@ -92,10 +93,11 @@ public:
 
 class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
 public:
-  DeclarationCommand(const std::vector<std::string>& ids, const Type* t);
+  DeclarationCommand(const std::vector<std::string>& ids, const Type& t);
   void toStream(std::ostream& out) const;
 protected:
   std::vector<std::string> d_declaredSymbols;
+  Type d_type;
 };
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -257,8 +259,10 @@ inline void CommandSequence::addCommand(Command* cmd) {
 
 /* class DeclarationCommand */
 
-inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, const Type* t) :
-  d_declaredSymbols(ids) {
+inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids, const Type& t) :
+  d_declaredSymbols(ids),
+  d_type(t)
+{
 }
 
 /* class SetBenchmarkStatusCommand */
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index c326817ad..6dc9453d2 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -27,11 +27,12 @@ using namespace context;
 DeclarationScope::DeclarationScope() :
   d_context(new Context()),
   d_exprMap(new (true) CDMap<std::string,Expr,StringHashFunction>(d_context)),
-  d_typeMap(new (true) CDMap<std::string,Type*,StringHashFunction>(d_context)) {
+  d_typeMap(new (true) CDMap<std::string,Type,StringHashFunction>(d_context)) {
 }
 
 DeclarationScope::~DeclarationScope() {
   d_exprMap->deleteSelf();
+  d_typeMap->deleteSelf();
   delete d_context;
 }
 
@@ -47,7 +48,7 @@ Expr DeclarationScope::lookup(const std::string& name) const throw () {
   return (*d_exprMap->find(name)).second;
 }
 
-void DeclarationScope::bindType(const std::string& name, Type* t) throw () {
+void DeclarationScope::bindType(const std::string& name, const Type& t) throw () {
   d_typeMap->insert(name,t);
 }
 
@@ -55,7 +56,7 @@ bool DeclarationScope::isBoundType(const std::string& name) const throw () {
   return d_typeMap->find(name) != d_typeMap->end();
 }
 
-Type* DeclarationScope::lookupType(const std::string& name) const throw () {
+Type DeclarationScope::lookupType(const std::string& name) const throw () {
   return (*d_typeMap->find(name)).second;
 }
 
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index e08c25173..7d0f2b787 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -56,7 +56,7 @@ class CVC4_PUBLIC DeclarationScope {
   context::CDMap<std::string,Expr,StringHashFunction> *d_exprMap;
 
   /** A map for types. */
-  context::CDMap<std::string,Type*,StringHashFunction> *d_typeMap;
+  context::CDMap<std::string,Type,StringHashFunction> *d_typeMap;
 
 public:
   /** Create a declaration scope. */
@@ -85,7 +85,7 @@ public:
    * @param name an identifier
    * @param t the type to bind to <code>name</code>
    */
-  void bindType(const std::string& name, Type* t) throw ();
+  void bindType(const std::string& name, const Type& t) throw ();
 
   /** Check whether a name is bound to an expression.
    *
@@ -113,7 +113,7 @@ public:
    * @param name the identifier to lookup
    * @returns the type bound to <code>name</code> in the current scope.
    */
-  Type* lookupType(const std::string& name) const throw ();
+  Type lookupType(const std::string& name) const throw ();
 
   /** Pop a scope level. Deletes all bindings since the last call to
    * <code>pushScope</code>. Calls to <code>pushScope</code> and
diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
new file mode 100644
index 000000000..38f8fc787
--- /dev/null
+++ b/src/expr/expr_manager_scope.h
@@ -0,0 +1,52 @@
+/*
+ * expr_manager_scope.h
+ *
+ *  Created on: Apr 7, 2010
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__EXPR_MANAGER_SCOPE_H
+#define __CVC4__EXPR_MANAGER_SCOPE_H
+
+#include "expr/expr.h"
+#include "expr/node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * Creates a <code>NodeManagerScope</code> with the underlying
+ * <code>NodeManager</code> of a given <code>Expr</code> or
+ * <code>ExprManager</code>.  The <code>NodeManagerScope</code> is
+ * destroyed when the <code>ExprManagerScope</code> is destroyed. See
+ * <code>NodeManagerScope</code> for more information.
+ */
+// NOTE: Here, it seems ExprManagerScope is redundant, since we have
+// NodeManagerScope already.  However, without this class, we'd need
+// Expr to be a friend of ExprManager, because in the implementation
+// of Expr functions, it needs to set the current NodeManager
+// correctly (and to do that it needs access to
+// ExprManager::getNodeManager()).  So, we make ExprManagerScope a
+// friend of ExprManager's, since its implementation is simple to
+// read and understand (and verify that it doesn't do any mischief).
+//
+// ExprManager::getNodeManager() can't just be made public, since
+// ExprManager is exposed to clients of the library and NodeManager is
+// not.  Similarly, ExprManagerScope shouldn't go in expr_manager.h,
+// since that's a public header.
+class ExprManagerScope {
+  NodeManagerScope d_nms;
+public:
+  inline ExprManagerScope(const Expr& e) :
+    d_nms(e.getExprManager() == NULL
+          ? NodeManager::currentNM()
+          : e.getExprManager()->getNodeManager()) {
+  }
+  inline ExprManagerScope(const ExprManager& exprManager) :
+    d_nms(exprManager.getNodeManager()) {
+  }
+};
+
+}
+
+
+#endif /* __CVC4__EXPR_MANAGER_SCOPE_H */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index a8d957c91..7407043d2 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -46,12 +46,12 @@ ExprManager::~ExprManager() {
   delete d_ctxt;
 }
 
-BooleanType* ExprManager::booleanType() const {
+BooleanType ExprManager::booleanType() const {
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->booleanType();
 }
 
-KindType* ExprManager::kindType() const {
+KindType ExprManager::kindType() const {
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->kindType();
 }
@@ -64,7 +64,7 @@ Expr ExprManager::mkExpr(Kind kind) {
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkNode(kind)));
+  return Expr(this, d_nodeManager->mkNodePtr(kind));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
@@ -75,7 +75,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode())));
+  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode()));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
@@ -86,8 +86,8 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
-                                          child2.getNode())));
+  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(),
+                                             child2.getNode()));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
@@ -99,8 +99,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
-                                          child2.getNode(), child3.getNode())));
+  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(), child2.getNode(), child3.getNode()));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
@@ -112,9 +111,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
+  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
-                                          child4.getNode())));
+                                          child4.getNode()));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
@@ -127,9 +126,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
                 kind::kindToString(kind).c_str(),
                 minArity(kind), maxArity(kind), n);
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkNode(kind, child1.getNode(),
+  return Expr(this, d_nodeManager->mkNodePtr(kind, child1.getNode(),
                                           child2.getNode(), child3.getNode(),
-                                          child5.getNode())));
+                                          child5.getNode()));
 }
 
 Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
@@ -149,49 +148,52 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
     nodes.push_back(it->getNode());
     ++it;
   }
-  return Expr(this, new Node(d_nodeManager->mkNode(kind, nodes)));
+  return Expr(this, d_nodeManager->mkNodePtr(kind, nodes));
 }
 
 /** Make a function type from domain to range. */
-FunctionType* ExprManager::mkFunctionType(Type* domain,
-                                          Type* range) {
+FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) {
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkFunctionType(domain, range);
 }
 
 /** Make a function type with input types from argTypes. */
-FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes,
-                                          Type* range) {
+FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
   Assert( argTypes.size() >= 1 );
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkFunctionType(argTypes, range);
 }
 
-FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& sorts) {
+FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
   Assert( sorts.size() >= 2 );
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkFunctionType(sorts);
 }
 
-FunctionType* ExprManager::mkPredicateType(const std::vector<Type*>& sorts) {
+FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
   Assert( sorts.size() >= 1 );
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkPredicateType(sorts);
 }
 
-Type* ExprManager::mkSort(const std::string& name) {
+SortType ExprManager::mkSort(const std::string& name) {
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkSort(name);
 }
 
-Expr ExprManager::mkVar(const std::string& name, Type* type) {
+Type ExprManager::getType(const Expr& e) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkVar(name, type)));
+  return d_nodeManager->getType(e.getNode());
 }
 
-Expr ExprManager::mkVar(Type* type) {
+Expr ExprManager::mkVar(const std::string& name, const Type& type) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkVar(type)));
+  return Expr(this, d_nodeManager->mkVarPtr(name, type));
+}
+
+Expr ExprManager::mkVar(const Type& type) {
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, d_nodeManager->mkVarPtr(type));
 }
 
 unsigned ExprManager::minArity(Kind kind) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 82698732c..df5190af6 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -85,10 +85,10 @@ public:
   ~ExprManager();
 
   /** Get the type for booleans */
-  BooleanType* booleanType() const;
+  BooleanType booleanType() const;
 
   /** Get the type for sorts. */
-  KindType* kindType() const;
+  KindType kindType() const;
 
   /**
    * Make a unary expression of a given kind (TRUE, FALSE,...).
@@ -162,15 +162,13 @@ public:
   Expr mkConst(const T&);
 
   /** Make a function type from domain to range. */
-  FunctionType* mkFunctionType(Type* domain,
-                               Type* range);
+  FunctionType mkFunctionType(const Type& domain, const Type& range);
 
   /**
    * Make a function type with input types from argTypes.
    * <code>argTypes</code> must have at least one element.
    */
-  FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
-                               Type* range);
+  FunctionType mkFunctionType(const std::vector<Type>& argTypes, const Type& range);
 
   /**
    * Make a function type with input types from
@@ -178,7 +176,7 @@ public:
    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
    * at least 2 elements.
    */
-  FunctionType* mkFunctionType(const std::vector<Type*>& sorts);
+  FunctionType mkFunctionType(const std::vector<Type>& sorts);
 
   /**
    * Make a predicate type with input types from
@@ -186,14 +184,17 @@ public:
    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
    * element.
    */
-  FunctionType* mkPredicateType(const std::vector<Type*>& sorts);
+  FunctionType mkPredicateType(const std::vector<Type>& sorts);
 
   /** Make a new sort with the given name. */
-  Type* mkSort(const std::string& name);
+  SortType mkSort(const std::string& name);
+
+  /** Get the type of an expression */
+  Type getType(const Expr& e);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(const std::string& name, Type* type);
-  Expr mkVar(Type* type);
+  Expr mkVar(const std::string& name, const Type& type);
+  Expr mkVar(const Type& type);
 
   /** Returns the minimum arity of the given kind. */
   static unsigned minArity(Kind kind);
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 7c723d338..ba7032e34 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -18,6 +18,7 @@
 #include "util/Assert.h"
 
 #include "util/output.h"
+#include "expr/expr_manager_scope.h"
 
 ${includes}
 
@@ -25,7 +26,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 29 "${template}"
+#line 30 "${template}"
 
 using namespace CVC4::kind;
 
@@ -128,10 +129,10 @@ Expr Expr::getOperator() const {
   return Expr(d_exprManager, new Node(d_node->getOperator()));
 }
 
-Type* Expr::getType() const {
+Type Expr::getType() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  return d_node->getType();
+  return d_exprManager->getType(*this);
 }
 
 std::string Expr::toString() const {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 2fa10ceb8..0e960358f 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -144,7 +144,7 @@ public:
   /** Returns the type of the expression, if it has been computed.
    * Returns NULL if the type of the expression is not known.
    */
-  Type* getType() const;
+  Type getType() const;
 
   /**
    * Returns the string representation of the expression.
diff --git a/src/expr/node.h b/src/expr/node.h
index 3a2aca571..27756da5b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -28,7 +28,6 @@
 
 #include "expr/kind.h"
 #include "expr/metakind.h"
-#include "expr/type.h"
 #include "util/Assert.h"
 #include "util/output.h"
 
@@ -248,7 +247,7 @@ public:
    * Returns the type of this node.
    * @return the type
    */
-  Type* getType() const;
+  Type getType() const;
 
   /**
    * Returns the kind of this node.
@@ -640,7 +639,7 @@ NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
   if(ref_count) {
     d_nv->dec();
   } else {
-    Assert(d_nv->d_rc > 0 || d_nv->isBeingDeleted(),
+    Assert(d_nv->d_rc > 0 || d_nv->isBeingDeleted() || NodeManager::currentNM()->inDestruction(),
            "TNode pointing to an expired NodeValue at destruction time");
   }
 }
@@ -815,7 +814,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const {
 }
 
 template <bool ref_count>
-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_builder.h b/src/expr/node_builder.h
index c854b6b80..a093fc954 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -537,7 +537,26 @@ public:
     return static_cast<Builder&>(*this);
   }
 
+private:
+
+  /** Construct the node value out of the node builder */
+  expr::NodeValue* constructNV();
+  expr::NodeValue* constructNV() const;
+
+public:
+
+  /** Construct the Node out of the node builder */
+  Node constructNode();
+  Node constructNode() const;
+
+  /** Construct a Node on the heap out of the node builder */
+  Node* constructNodePtr();
+  Node* constructNodePtr() const;
+
+  // two versions, so we can support extraction from (const)
+  // NodeBuilders which are temporaries appearing as rvalues
   operator Node();
+  operator Node() const;
 
   inline void toStream(std::ostream& out, int depth = -1) const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
@@ -1227,7 +1246,17 @@ void NodeBuilderBase<Builder>::decrRefCounts() {
 }
 
 template <class Builder>
-NodeBuilderBase<Builder>::operator Node() {
+Node* NodeBuilderBase<Builder>::constructNodePtr() {
+  return new Node(constructNV());
+}
+
+template <class Builder>
+Node* NodeBuilderBase<Builder>::constructNodePtr() const {
+  return new Node(constructNV());
+}
+
+template <class Builder>
+expr::NodeValue* NodeBuilderBase<Builder>::constructNV() {
   Assert(!isUsed(), "NodeBuilder is one-shot only; "
          "attempt to access it after conversion");
   Assert(getKind() != kind::UNDEFINED_KIND,
@@ -1265,7 +1294,7 @@ NodeBuilderBase<Builder>::operator Node() {
     setUsed();
     Debug("gc") << "creating node value " << nv
                 << " [" << nv->d_id << "]: " << nv->toString() << "\n";
-    return Node(nv);
+    return nv;
   }
 
   // check that there are the right # of children for this kind
@@ -1309,7 +1338,7 @@ NodeBuilderBase<Builder>::operator Node() {
       decrRefCounts();
       d_inlineNv.d_nchildren = 0;
       setUsed();
-      return Node(poolNv);
+      return poolNv;
     } else {
       /* Subcase (b): The Node under construction is NOT already in
        * the NodeManager's pool. */
@@ -1347,7 +1376,7 @@ NodeBuilderBase<Builder>::operator Node() {
       d_nm->poolInsert(nv);
       Debug("gc") << "creating node value " << nv
                   << " [" << nv->d_id << "]: " << *nv << "\n";
-      return Node(nv);
+      return nv;
     }
   } else {
     /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
@@ -1369,7 +1398,7 @@ NodeBuilderBase<Builder>::operator Node() {
 
       dealloc();
       setUsed();
-      return Node(poolNv);
+      return poolNv;
     } else {
       /* Subcase (b) The Node under construction is NOT already in the
        * NodeManager's pool. */
@@ -1392,11 +1421,198 @@ NodeBuilderBase<Builder>::operator Node() {
       d_nm->poolInsert(nv);
       Debug("gc") << "creating node value " << nv
                   << " [" << nv->d_id << "]: " << *nv << "\n";
-      return Node(nv);
+      return nv;
     }
   }
 }
 
+// CONST VERSION OF NODE EXTRACTOR
+template <class Builder>
+expr::NodeValue* NodeBuilderBase<Builder>::constructNV() const {
+  Assert(!isUsed(), "NodeBuilder is one-shot only; "
+         "attempt to access it after conversion");
+  Assert(getKind() != kind::UNDEFINED_KIND,
+         "Can't make an expression of an undefined kind!");
+
+  // NOTE: The comments in this function refer to the cases in the
+  // file comments at the top of this file.
+
+  // Case 0: If a VARIABLE
+  if(getMetaKind() == kind::metakind::VARIABLE) {
+    /* 0. If a VARIABLE, treat similarly to 1(b), except that we know
+     * there are no children (no reference counts to reason about),
+     * and we don't keep VARIABLE-kinded Nodes in the NodeManager
+     * pool. */
+
+    Assert( ! nvIsAllocated(),
+            "internal NodeBuilder error: "
+            "VARIABLE-kinded NodeBuilder is heap-allocated !?" );
+    Assert( d_inlineNv.d_nchildren == 0,
+            "improperly-formed VARIABLE-kinded NodeBuilder: "
+            "no children permitted" );
+
+    // we have to copy the inline NodeValue out
+    expr::NodeValue* nv = (expr::NodeValue*)
+      std::malloc(sizeof(expr::NodeValue));
+    if(nv == NULL) {
+      throw std::bad_alloc();
+    }
+    // there are no children, so we don't have to worry about
+    // reference counts in this case.
+    nv->d_nchildren = 0;
+    nv->d_kind = d_nv->d_kind;
+    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+    nv->d_rc = 0;
+    Debug("gc") << "creating node value " << nv
+                << " [" << nv->d_id << "]: " << *nv << "\n";
+    return nv;
+  }
+
+  // check that there are the right # of children for this kind
+  Assert(getMetaKind() != kind::metakind::CONSTANT,
+         "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
+  Assert(d_nv->d_nchildren >= kind::metakind::getLowerBoundForKind(getKind()),
+         "Nodes with kind %s must have at least %u children (the one under "
+         "construction has %u)",
+         kind::kindToString(getKind()).c_str(),
+         kind::metakind::getLowerBoundForKind(getKind()),
+         getNumChildren());
+  Assert(d_nv->d_nchildren <= kind::metakind::getUpperBoundForKind(getKind()),
+         "Nodes with kind %s must have at most %u children (the one under "
+         "construction has %u)",
+         kind::kindToString(getKind()).c_str(),
+         kind::metakind::getUpperBoundForKind(getKind()),
+         getNumChildren());
+
+  // Implementation differs depending on whether the NodeValue was
+  // malloc'ed or not and whether or not it's in the already-been-seen
+  // NodeManager pool of Nodes.  See implementation notes at the top
+  // of this file.
+
+  if(EXPECT_TRUE( ! nvIsAllocated() )) {
+    /** Case 1.  d_nv points to d_inlineNv: it is the backing store
+     ** supplied by the user (or derived class) **/
+
+    // Lookup the expression value in the pool we already have
+    expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
+    // If something else is there, we reuse it
+    if(poolNv != NULL) {
+      /* Subcase (a): The Node under construction already exists in
+       * the NodeManager's pool. */
+
+      /* 1(a). The existing NodeManager pool entry is returned; we
+       * leave child reference counts alone and get them at
+       * NodeBuilder destruction time. */
+
+      return poolNv;
+    } else {
+      /* Subcase (b): The Node under construction is NOT already in
+       * the NodeManager's pool. */
+
+      /* 1(b). A new heap-allocated NodeValue must be constructed and
+       * all settings and children from d_inlineNv copied into it.
+       * This new NodeValue is put into the NodeManager's pool.  The
+       * NodeBuilder cannot be marked as "used", so we increment all
+       * child reference counts (which will be decremented to match on
+       * destruction of the NodeBuilder).  We return a Node wrapper
+       * for this new NodeValue, which increments its reference
+       * count. */
+
+      // create the canonical expression value for this node
+      expr::NodeValue* nv = (expr::NodeValue*)
+        std::malloc(sizeof(expr::NodeValue) +
+                    ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
+      if(nv == NULL) {
+        throw std::bad_alloc();
+      }
+      nv->d_nchildren = d_inlineNv.d_nchildren;
+      nv->d_kind = d_inlineNv.d_kind;
+      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_rc = 0;
+
+      std::copy(d_inlineNv.d_children,
+                d_inlineNv.d_children + d_inlineNv.d_nchildren,
+                nv->d_children);
+
+      for(expr::NodeValue::nv_iterator i = nv->nv_begin();
+          i != nv->nv_end();
+          ++i) {
+        (*i)->inc();
+      }
+
+      //poolNv = nv;
+      d_nm->poolInsert(nv);
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << *nv << "\n";
+      return nv;
+    }
+  } else {
+    /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger
+     ** buffer that was heap-allocated by this NodeBuilder. **/
+
+    // Lookup the expression value in the pool we already have (with insert)
+    expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
+    // If something else is there, we reuse it
+    if(poolNv != NULL) {
+      /* Subcase (a): The Node under construction already exists in
+       * the NodeManager's pool. */
+
+      /* 2(a). The existing NodeManager pool entry is returned; we
+       * leave child reference counts alone and get them at
+       * NodeBuilder destruction time. */
+
+      return poolNv;
+    } else {
+      /* Subcase (b) The Node under construction is NOT already in the
+       * NodeManager's pool. */
+
+      /* 2(b). The heap-allocated d_nv cannot be "cropped" to the
+       * correct size; we create a copy, increment child reference
+       * counts, place this copy into the NodeManager pool, and return
+       * a Node wrapper around it.  The child reference counts will be
+       * decremented to match at NodeBuilder destruction time. */
+
+      // create the canonical expression value for this node
+      expr::NodeValue* nv = (expr::NodeValue*)
+        std::malloc(sizeof(expr::NodeValue) +
+                    ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
+      if(nv == NULL) {
+        throw std::bad_alloc();
+      }
+      nv->d_nchildren = d_nv->d_nchildren;
+      nv->d_kind = d_nv->d_kind;
+      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_rc = 0;
+
+      std::copy(d_nv->d_children,
+                d_nv->d_children + d_nv->d_nchildren,
+                nv->d_children);
+
+      for(expr::NodeValue::nv_iterator i = nv->nv_begin();
+          i != nv->nv_end();
+          ++i) {
+        (*i)->inc();
+      }
+
+      //poolNv = nv;
+      d_nm->poolInsert(nv);
+      Debug("gc") << "creating node value " << nv
+                  << " [" << nv->d_id << "]: " << *nv << "\n";
+      return nv;
+    }
+  }
+}
+
+template <class Builder>
+NodeBuilderBase<Builder>::operator Node() {
+  return Node(constructNV());
+}
+
+template <class Builder>
+NodeBuilderBase<Builder>::operator Node() const {
+  return Node(constructNV());
+}
+
 template <unsigned nchild_thresh>
 template <unsigned N>
 void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 708bd16b2..4f0e0ff76 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -27,55 +27,23 @@ namespace CVC4 {
 
 __thread NodeManager* NodeManager::s_current = 0;
 
-NodeManager::NodeManager(context::Context* ctxt) :
-  d_attrManager(ctxt),
-  d_nodeUnderDeletion(NULL),
-  d_reclaiming(false) {
-  poolInsert( &expr::NodeValue::s_null );
-
-  for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
-    Kind k = Kind(i);
-
-    if(hasOperator(k)) {
-      d_operators[i] = mkConst(Kind(k));
-    }
-  }
-}
-
-NodeManager::~NodeManager() {
-  // have to ensure "this" is the current NodeManager during
-  // destruction of operators, because they get GCed.
-
-  NodeManagerScope nms(this);
-
-  for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
-    d_operators[i] = Node::null();
-  }
-
-  while(!d_zombies.empty()) {
-    reclaimZombies();
-  }
-
-  poolRemove( &expr::NodeValue::s_null );
-}
-
 /**
  * This class ensures that NodeManager::d_reclaiming gets set to false
  * even on exceptional exit from NodeManager::reclaimZombies().
  */
-struct Reclaim {
-  bool& d_reclaimField;
+struct ScopedBool {
+  bool& d_value;
 
-  Reclaim(bool& reclaim) :
-    d_reclaimField(reclaim) {
+  ScopedBool(bool& reclaim) :
+    d_value(reclaim) {
 
     Debug("gc") << ">> setting RECLAIM field\n";
-    d_reclaimField = true;
+    d_value = true;
   }
 
-  ~Reclaim() {
+  ~ScopedBool() {
     Debug("gc") << "<< clearing RECLAIM field\n";
-    d_reclaimField = false;
+    d_value = false;
   }
 };
 
@@ -98,17 +66,57 @@ struct NVReclaim {
   }
 };
 
+
+NodeManager::NodeManager(context::Context* ctxt) :
+  d_attrManager(ctxt),
+  d_nodeUnderDeletion(NULL),
+  d_dontGC(false),
+  d_inDestruction(false) {
+  poolInsert( &expr::NodeValue::s_null );
+
+  for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
+    Kind k = Kind(i);
+
+    if(hasOperator(k)) {
+      d_operators[i] = mkConst(Kind(k));
+    }
+  }
+}
+
+NodeManager::~NodeManager() {
+  // have to ensure "this" is the current NodeManager during
+  // destruction of operators, because they get GCed.
+
+  NodeManagerScope nms(this);
+  ScopedBool inDestruction(d_inDestruction);
+
+  {
+    ScopedBool dontGC(d_dontGC);
+    d_attrManager.deleteAllAttributes();
+  }
+
+  for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
+    d_operators[i] = Node::null();
+  }
+
+  while(!d_zombies.empty()) {
+    reclaimZombies();
+  }
+
+  poolRemove( &expr::NodeValue::s_null );
+}
+
 void NodeManager::reclaimZombies() {
   // FIXME multithreading
 
   Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
 
   // during reclamation, reclaimZombies() is never supposed to be called
-  Assert(! d_reclaiming, "NodeManager::reclaimZombies() not re-entrant!");
+  Assert(! d_dontGC, "NodeManager::reclaimZombies() not re-entrant!");
 
   // whether exit is normal or exceptional, the Reclaim dtor is called
   // and ensures that d_reclaiming is set back to false.
-  Reclaim r(d_reclaiming);
+  ScopedBool r(d_dontGC);
 
   // We copy the set away and clear the NodeManager's set of zombies.
   // This is because reclaimZombie() decrements the RC of the
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index c3f5238d6..3a6b6e15a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -30,7 +30,6 @@
 
 #include "expr/kind.h"
 #include "expr/metakind.h"
-#include "expr/expr.h"
 #include "expr/node_value.h"
 #include "context/context.h"
 #include "expr/type.h"
@@ -86,7 +85,12 @@ class NodeManager {
    * NodeValues, but these shouldn't trigger a (recursive) call to
    * reclaimZombies().
    */
-  bool d_reclaiming;
+  bool d_dontGC;
+
+  /**
+   * Marks that we are in the Destructor currently.
+   */
+  bool d_inDestruction;
 
   /**
    * The set of zombie nodes.  We may want to revisit this design, as
@@ -164,11 +168,11 @@ class NodeManager {
     // reclaimZombies(), because it's already running.
     Debug("gc") << "zombifying node value " << nv
                 << " [" << nv->d_id << "]: " << *nv
-                << (d_reclaiming ? " [CURRENTLY-RECLAIMING]" : "")
+                << (d_dontGC ? " [CURRENTLY-RECLAIMING]" : "")
                 << std::endl;
     d_zombies.insert(nv);// FIXME multithreading
 
-    if(!d_reclaiming) {// FIXME multithreading
+    if(!d_dontGC) {// FIXME multithreading
       // for now, collect eagerly.  can add heuristic here later..
       reclaimZombies();
     }
@@ -202,9 +206,7 @@ class NodeManager {
 
   // NodeManager's attributes.  These aren't exposed outside of this
   // class; use the getters.
-  typedef expr::ManagedAttribute<TypeTag,
-                                 CVC4::Type*,
-                                 expr::attr::TypeCleanupStrategy> TypeAttr;
+  typedef expr::Attribute<TypeTag, Node> TypeAttr;
   typedef expr::Attribute<AtomicTag, bool> AtomicAttr;
 
   /**
@@ -239,6 +241,11 @@ public:
   NodeManager(context::Context* ctxt);
   ~NodeManager();
 
+  /**
+   * Return true if we are in destruction.
+   */
+  bool inDestruction() const { return d_inDestruction; }
+
   /** The node manager in the current context. */
   static NodeManager* currentNM() { return s_current; }
 
@@ -246,37 +253,49 @@ public:
 
   /** Create a node with no children. */
   Node mkNode(Kind kind);
+  Node* mkNodePtr(Kind kind);
 
   /** Create a node with one child. */
   Node mkNode(Kind kind, TNode child1);
+  Node* mkNodePtr(Kind kind, TNode child1);
 
   /** Create a node with two children. */
   Node mkNode(Kind kind, TNode child1, TNode child2);
+  Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
 
   /** Create a node with three children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
+  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
 
   /** Create a node with four children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
               TNode child4);
+  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
+              TNode child4);
 
   /** Create a node with five children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
               TNode child4, TNode child5);
+  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
+              TNode child4, TNode child5);
 
   /** Create a node with an arbitrary number of children. */
   template <bool ref_count>
   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
+  template <bool ref_count>
+  Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
   /**
    * Create a variable with the given name and type.  NOTE that no
    * lookup is done on the name.  If you mkVar("a", type) and then
    * mkVar("a", type) again, you have two variables.
    */
-  Node mkVar(const std::string& name, Type* type);
+  Node mkVar(const std::string& name, const Type& type);
+  Node* mkVarPtr(const std::string& name, const Type& type);
 
   /** Create a variable with the given type. */
-  Node mkVar(Type* type);
+  Node mkVar(const Type& type);
+  Node* mkVarPtr(const Type& type);
 
   /**
    * Create a constant of type T.  It will have the appropriate
@@ -414,14 +433,10 @@ public:
                            const typename AttrKind::value_type& value);
 
   /** Get the (singleton) type for booleans. */
-  inline BooleanType* booleanType() const {
-    return BooleanType::getInstance();
-  }
+  inline BooleanType booleanType();
 
   /** Get the (singleton) type for sorts. */
-  inline KindType* kindType() const {
-    return KindType::getInstance();
-  }
+  inline KindType kindType();
 
   /**
    * Make a function type from domain to range.
@@ -430,7 +445,7 @@ public:
    * @param range the range type
    * @returns the functional type domain -> range
    */
-  inline FunctionType* mkFunctionType(Type* domain, Type* range) const;
+  inline Type mkFunctionType(const Type& domain, const Type& range);
 
   /**
    * Make a function type with input types from
@@ -440,8 +455,7 @@ public:
    * @param range the range type
    * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
    */
-  inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
-                                      Type* range) const;
+  inline Type mkFunctionType(const std::vector<Type>& argTypes, const Type& range);
 
   /**
    * Make a function type with input types from
@@ -449,7 +463,7 @@ public:
    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
    * at least 2 elements.
    */
-  inline FunctionType* mkFunctionType(const std::vector<Type*>& sorts) const;
+  inline Type mkFunctionType(const std::vector<Type>& sorts);
 
   /**
    * Make a predicate type with input types from
@@ -457,16 +471,15 @@ public:
    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
    * element.
    */
-  inline FunctionType* mkPredicateType(const std::vector<Type*>& sorts) const;
+  inline Type mkPredicateType(const std::vector<Type>& sorts);
 
   /** Make a new sort with the given name. */
-  inline Type* mkSort(const std::string& name) const;
+  inline Type mkSort(const std::string& name);
 
-  /** Get the type for the given node.
-   *
-   * TODO: Does this call compute the type if it's not already available?
+  /**
+   * Get the type for the given node.
    */
-  inline Type* getType(TNode n) const;
+  inline Type getType(TNode n);
 
   /**
    * Returns true if this node is atomic (has no more Boolean structure)
@@ -518,38 +531,6 @@ public:
   }
 };
 
-/**
- * Creates a <code>NodeManagerScope</code> with the underlying
- * <code>NodeManager</code> of a given <code>Expr</code> or
- * <code>ExprManager</code>.  The <code>NodeManagerScope</code> is
- * destroyed when the <code>ExprManagerScope</code> is destroyed. See
- * <code>NodeManagerScope</code> for more information.
- */
-// NOTE: Here, it seems ExprManagerScope is redundant, since we have
-// NodeManagerScope already.  However, without this class, we'd need
-// Expr to be a friend of ExprManager, because in the implementation
-// of Expr functions, it needs to set the current NodeManager
-// correctly (and to do that it needs access to
-// ExprManager::getNodeManager()).  So, we make ExprManagerScope a
-// friend of ExprManager's, since its implementation is simple to
-// read and understand (and verify that it doesn't do any mischief).
-//
-// ExprManager::getNodeManager() can't just be made public, since
-// ExprManager is exposed to clients of the library and NodeManager is
-// not.  Similarly, ExprManagerScope shouldn't go in expr_manager.h,
-// since that's a public header.
-class ExprManagerScope {
-  NodeManagerScope d_nms;
-public:
-  inline ExprManagerScope(const Expr& e) :
-    d_nms(e.getExprManager() == NULL
-          ? NodeManager::currentNM()
-          : e.getExprManager()->getNodeManager()) {
-  }
-  inline ExprManagerScope(const ExprManager& exprManager) :
-    d_nms(exprManager.getNodeManager()) {
-  }
-};
 
 template <class AttrKind>
 inline typename AttrKind::value_type
@@ -603,45 +584,61 @@ NodeManager::setAttribute(TNode n, const AttrKind&,
   d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
 }
 
+
+/** Get the (singleton) type for booleans. */
+inline BooleanType NodeManager::booleanType() {
+  return Type(this, new Node(mkConst<TypeConstant>(BOOLEAN_TYPE)));
+}
+
+/** Get the (singleton) type for sorts. */
+inline KindType NodeManager::kindType() {
+  return Type(this, new Node(mkConst<TypeConstant>(KIND_TYPE)));
+}
+
 /** Make a function type from domain to range.
  * TODO: Function types should be unique for this manager. */
-inline FunctionType* NodeManager::mkFunctionType(Type* domain,
-                                                 Type* range) const {
-  std::vector<Type*> argTypes;
-  argTypes.push_back(domain);
-  return new FunctionType(argTypes, range);
+inline Type NodeManager::mkFunctionType(const Type& domain, const Type& range) {
+  return Type(this, mkNodePtr(kind::FUNCTION_TYPE, *domain.d_typeNode, *range.d_typeNode));
 }
 
-/** Make a function type with input types from argTypes.
- * TODO: Function types should be unique for this manager. */
-inline FunctionType*
-NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
-                            Type* range) const {
-  Assert( argTypes.size() > 0 );
-  return new FunctionType(argTypes, range);
+inline Type NodeManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
+  Assert(argTypes.size() >= 1);
+  std::vector<Type> sorts(argTypes);
+  sorts.push_back(range);
+  return mkFunctionType(sorts);
 }
 
-inline FunctionType*
-NodeManager::mkFunctionType(const std::vector<Type*>& sorts) const {
-  Assert( sorts.size() >= 2 );
-  std::vector<Type*> argTypes(sorts);
-  Type* rangeType = argTypes.back();
-  argTypes.pop_back();
-  return mkFunctionType(argTypes,rangeType);
+
+inline Type
+NodeManager::mkFunctionType(const std::vector<Type>& sorts) {
+  Assert(sorts.size() >= 2);
+  std::vector<Node> sortNodes;
+  for (unsigned i = 0; i < sorts.size(); ++ i) {
+    sortNodes.push_back(*(sorts[i].d_typeNode));
+  }
+  return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes));
 }
 
-inline FunctionType*
-NodeManager::mkPredicateType(const std::vector<Type*>& sorts) const {
-  Assert( sorts.size() >= 1 );
-  return mkFunctionType(sorts,booleanType());
+inline Type
+NodeManager::mkPredicateType(const std::vector<Type>& sorts) {
+  Assert(sorts.size() >= 1);
+  std::vector<Node> sortNodes;
+  for (unsigned i = 0; i < sorts.size(); ++ i) {
+    sortNodes.push_back(*(sorts[i].d_typeNode));
+  }
+  sortNodes.push_back(*(booleanType().d_typeNode));
+  return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes));
 }
 
-inline Type* NodeManager::mkSort(const std::string& name) const {
-  return new SortType(name);
+inline Type NodeManager::mkSort(const std::string& name) {
+  return Type(this, mkVarPtr(name, kindType()));
 }
 
-inline Type* NodeManager::getType(TNode n) const {
-  return getAttribute(n, TypeAttr());
+inline Type NodeManager::getType(TNode n)  {
+  Node* typeNode = new Node;
+  getAttribute(n, TypeAttr(), *typeNode);
+  // TODO: Type computation
+  return Type(this, typeNode);
 }
 
 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
@@ -731,33 +728,71 @@ inline bool NodeManager::hasOperator(Kind k) {
 }
 
 inline Node NodeManager::mkNode(Kind kind) {
-  return NodeBuilder<>(this, kind);
+  return NodeBuilder<0>(this, kind);
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind) {
+  NodeBuilder<0> nb(this, kind);
+  return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
-  return NodeBuilder<>(this, kind) << child1;
+  return NodeBuilder<1>(this, kind) << child1;
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
+  NodeBuilder<1> nb(this, kind);
+  nb << child1;
+  return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
-  return NodeBuilder<>(this, kind) << child1 << child2;
+  return NodeBuilder<2>(this, kind) << child1 << child2;
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
+  NodeBuilder<2> nb(this, kind);
+  nb << child1 << child2;
+  return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3) {
-  return NodeBuilder<>(this, kind) << child1 << child2 << child3;
+  return NodeBuilder<3>(this, kind) << child1 << child2 << child3;
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
+                                TNode child3) {
+  NodeBuilder<3> nb(this, kind);
+  nb << child1 << child2 << child3;
+  return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4) {
-  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
+  return NodeBuilder<4>(this, kind) << child1 << child2 << child3 << child4;
+}
+
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
+                                TNode child3, TNode child4) {
+  NodeBuilder<4> nb(this, kind);
+  nb << child1 << child2 << child3 << child4;
+  return nb.constructNodePtr();
 }
 
 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
                                 TNode child3, TNode child4, TNode child5) {
-  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4
+  return NodeBuilder<5>(this, kind) << child1 << child2 << child3 << child4
                                    << child5;
 }
 
+inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
+                                TNode child3, TNode child4, TNode child5) {
+  NodeBuilder<5> nb(this, kind);
+  nb << child1 << child2 << child3 << child4 << child5;
+  return nb.constructNodePtr();
+}
+
 // N-ary version
 template <bool ref_count>
 inline Node NodeManager::mkNode(Kind kind,
@@ -766,16 +801,34 @@ inline Node NodeManager::mkNode(Kind kind,
   return NodeBuilder<>(this, kind).append(children);
 }
 
-inline Node NodeManager::mkVar(const std::string& name, Type* type) {
+template <bool ref_count>
+inline Node* NodeManager::mkNodePtr(Kind kind,
+                                const std::vector<NodeTemplate<ref_count> >&
+                                children) {
+  return NodeBuilder<>(this, kind).append(children).constructNodePtr();
+}
+
+inline Node NodeManager::mkVar(const std::string& name, const Type& type) {
   Node n = mkVar(type);
   n.setAttribute(expr::VarNameAttr(), name);
   return n;
 }
 
-inline Node NodeManager::mkVar(Type* type) {
-  Node n = Node(NodeBuilder<>(this, kind::VARIABLE));
-  type->inc();// reference-count the type
-  n.setAttribute(TypeAttr(), type);
+inline Node* NodeManager::mkVarPtr(const std::string& name, const Type& type) {
+  Node* n = mkVarPtr(type);
+  n->setAttribute(expr::VarNameAttr(), name);
+  return n;
+}
+
+inline Node NodeManager::mkVar(const Type& type) {
+  Node n = NodeBuilder<0>(this, kind::VARIABLE);
+  n.setAttribute(TypeAttr(), *type.d_typeNode);
+  return n;
+}
+
+inline Node* NodeManager::mkVarPtr(const Type& type) {
+  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
+  n->setAttribute(TypeAttr(), *type.d_typeNode);
   return n;
 }
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 851c440b6..63d270ac1 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -15,6 +15,7 @@
 
 #include "expr/node_manager.h"
 #include "expr/type.h"
+#include "expr/type_constant.h"
 #include "util/Assert.h"
 #include <string>
 
@@ -25,106 +26,187 @@ std::ostream& operator<<(std::ostream& out, const Type& e) {
   return out;
 }
 
-Type::Type() :
-  d_name(std::string("<undefined>")),
-  d_rc(0) {
+Type Type::makeType(NodeTemplate<false> typeNode) const
+{
+  return Type(d_nodeManager, new Node(typeNode));
 }
 
-Type::Type(std::string name) : 
-  d_name(name),
-  d_rc(0) {
+Type::Type(NodeManager* nm, NodeTemplate<true>* node)
+: d_typeNode(node),
+  d_nodeManager(nm)
+{
 }
 
-std::string Type::getName() const {
-  return d_name;
+Type::~Type() {
+  NodeManagerScope nms(d_nodeManager);
+  delete d_typeNode;
 }
 
-BooleanType BooleanType::s_instance;
+Type::Type()
+: d_typeNode(new Node()),
+  d_nodeManager(NULL)
+{
+}
 
-BooleanType::BooleanType() :
-  Type(std::string("BOOLEAN")) {
-  d_rc = RC_MAX;// singleton, not heap-allocated
+Type::Type(uintptr_t n)
+: d_typeNode(new Node()),
+  d_nodeManager(NULL) {
+  AlwaysAssert(n == 0);
 }
 
-BooleanType::~BooleanType() {
+Type::Type(const Type& t)
+: d_typeNode(new Node(*t.d_typeNode)),
+  d_nodeManager(t.d_nodeManager)
+{
 }
 
-BooleanType* BooleanType::getInstance() {
-  return &s_instance;
+bool Type::isNull() const {
+  return d_typeNode->isNull();
 }
 
-bool BooleanType::isBoolean() const {
-  return true;
+Type& Type::operator=(const Type& t) {
+  NodeManagerScope nms(d_nodeManager);
+  if (this != &t) {
+    *d_typeNode = *t.d_typeNode;
+    d_nodeManager = t.d_nodeManager;
+  }
+  return *this;
 }
 
-FunctionType::FunctionType(const std::vector<Type*>& argTypes,
-                           Type* range) :
-  d_argTypes(argTypes),
-  d_rangeType(range) {
+bool Type::operator==(const Type& t) const {
+  return *d_typeNode == *t.d_typeNode;
+}
 
-  Assert( argTypes.size() > 0 );
+bool Type::operator!=(const Type& t) const {
+  return *d_typeNode != *t.d_typeNode;
 }
 
-// FIXME: What becomes of argument types?
-FunctionType::~FunctionType() {
+void Type::toStream(std::ostream& out) const {
+  NodeManagerScope nms(d_nodeManager);
+  // Do the cast by hand
+  if (isBoolean()) { out << (BooleanType)*this; return; }
+  if (isFunction()) { out << (FunctionType)*this; return; }
+  if (isKind()) { out << (KindType)*this; return; }
+  if (isSort()) { out << (SortType)*this; return; }
+  // We should not get here
+  Unreachable("Type not implemented completely");
 }
 
-const std::vector<Type*> FunctionType::getArgTypes() const {
-  return d_argTypes;
+/** Is this the Boolean type? */
+bool Type::isBoolean() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getKind() == kind::TYPE_CONSTANT
+      && d_typeNode->getConst<TypeConstant>() == BOOLEAN_TYPE;
 }
 
-Type* FunctionType::getRangeType() const {
-  return d_rangeType;
+/** Cast to a Boolean type */
+Type::operator BooleanType() const {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isBoolean());
+  return BooleanType(*this);
 }
 
-bool FunctionType::isFunction() const {
-  return true;
+/** Is this a function type? */
+bool Type::isFunction() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getKind() == kind::FUNCTION_TYPE;
 }
 
-bool FunctionType::isPredicate() const {
-  return d_rangeType->isBoolean();
+/** Is this a predicate type? NOTE: all predicate types are also
+    function types. */
+bool Type::isPredicate() const {
+  NodeManagerScope nms(d_nodeManager);
+  return isFunction() && ((FunctionType)*this).getRangeType().isBoolean();
 }
 
-void FunctionType::toStream(std::ostream& out) const {
-  if( d_argTypes.size() > 1 ) {
-    out << "(";
-  }
-  for( unsigned int i=0; i < d_argTypes.size(); ++i ) {
-    if( i > 0 ) {
-      out << ",";
-    }
-    d_argTypes[i]->toStream(out);
-  }
-  if( d_argTypes.size() > 1 ) {
-    out << ")";
-  }
-  out << " -> ";
-  d_rangeType->toStream(out);
+/** Cast to a function type */
+Type::operator FunctionType() const {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isFunction());
+  return FunctionType(*this);
+}
+
+/** Is this a sort kind */
+bool Type::isSort() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getKind() == kind::VARIABLE &&
+      d_typeNode->getType().isKind();
+}
+
+/** Cast to a sort type */
+Type::operator SortType() const {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isSort());
+  return SortType(*this);
 }
 
-KindType KindType::s_instance;
+/** Is this a kind type (i.e., the type of a type)? */
+bool Type::isKind() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getKind() == kind::TYPE_CONSTANT
+      && d_typeNode->getConst<TypeConstant>() == KIND_TYPE;
+}
+
+/** Cast to a kind type */
+Type::operator KindType() const {
+  NodeManagerScope nms(d_nodeManager);
+  Assert(isKind());
+  return KindType(*this);
+}
 
-KindType::KindType() :
-  Type(std::string("KIND")) {
-  d_rc = RC_MAX;// singleton, not heap-allocated
+std::vector<Type> FunctionType::getArgTypes() const {
+  NodeManagerScope nms(d_nodeManager);
+  std::vector<Type> args;
+  for (unsigned i = 0, i_end = d_typeNode->getNumChildren() - 1; i < i_end; ++ i) {
+    args.push_back(makeType((*d_typeNode)[i]));
+  }
+  return args;
 }
 
-KindType::~KindType() {
+Type FunctionType::getRangeType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return makeType((*d_typeNode)[d_typeNode->getNumChildren()-1]);
 }
 
-bool KindType::isKind() const {
-  return true;
+void BooleanType::toStream(std::ostream& out) const {
+  out << "BOOLEAN";
 }
 
-KindType* KindType::getInstance() {
-  return &s_instance;
+std::string SortType::getName() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->getAttribute(expr::VarNameAttr());
 }
 
-SortType::SortType(std::string name) :
-  Type(name) {
+void SortType::toStream(std::ostream& out) const {
+  NodeManagerScope nms(d_nodeManager);
+  out << getName();
 }
 
-SortType::~SortType() {
+void FunctionType::toStream(std::ostream& out) const {
+  NodeManagerScope nms(d_nodeManager);
+  unsigned arity = d_typeNode->getNumChildren();
+
+  if(arity > 2) {
+    out << "(";
+  }
+  unsigned int i;
+  for(i=0; i < arity - 1; ++i) {
+    if(i > 0) {
+      out << ",";
+    }
+    out << makeType((*d_typeNode)[i]);
+  }
+  if(arity > 2) {
+    out << ")";
+  }
+  out << " -> ";
+  (*d_typeNode)[i].toStream(out);
 }
 
+BooleanType::BooleanType(const Type& t) : Type(t) {}
+FunctionType::FunctionType(const Type& t) : Type(t) {}
+KindType::KindType(const Type& t) : Type(t) {}
+SortType::SortType(const Type& t) : Type(t) {}
+
+
 }/* CVC4 namespace */
diff --git a/src/expr/type.h b/src/expr/type.h
index 8a9d6cd70..4f9142698 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -24,153 +24,146 @@
 #include <string>
 #include <vector>
 #include <limits.h>
+#include <stdint.h>
 
 namespace CVC4 {
 
-namespace expr {
-  namespace attr {
-    struct TypeCleanupStrategy;
-  }/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-
 class NodeManager;
+template <bool ref_count> class NodeTemplate;
+
+class BooleanType;
+class FunctionType;
+class KindType;
+class SortType;
 
 /**
  * Class encapsulating CVC4 expression types.
  */
 class CVC4_PUBLIC Type {
+
+  friend class NodeManager;
+
 protected:
-  static const unsigned RC_MAX = UINT_MAX;
+
+  /** The internal expression representation */
+  NodeTemplate<true>* d_typeNode;
+
+  /** The responsible expression manager */
+  NodeManager* d_nodeManager;
+
+  /**
+   * Construct a new type given the typeNode;
+   */
+  Type makeType(NodeTemplate<false> typeNode) const;
+
+  /**
+   * Constructor for internal purposes.
+   * @param em the expression manager that handles this expression
+   * @param node the actual expression node pointer for this type
+   */
+  Type(NodeManager* em, NodeTemplate<true>* typeNode);
 
 public:
 
+  /**
+   * Initialize from an integer. Fails if the integer is not 0.
+   * NOTE: This is here purely to support the auto-initialization
+   * behavior of the ANTLR3 C backend. Should be removed if future
+   * versions of ANTLR fix the problem.
+   */
+  Type(uintptr_t n);
+
+  /** Force a virtual destructor for safety. */
+  virtual ~Type();
+
+  /** Default constructor */
+  Type();
+
+  /** Copy constructor */
+  Type(const Type& t);
+
+  /** Check whether this is a null type */
+  bool isNull() const;
+
+  /** Assignment operator */
+  Type& operator=(const Type& t);
+
   /** Comparison for equality */
-  //bool operator==(const Type& t) const;
+  bool operator==(const Type& t) const;
 
   /** Comparison for disequality */
-  //bool operator!=(const Type& e) const;
+  bool operator!=(const Type& t) const;
 
-  /** Get the name of this type. May be empty for composite types. */
-  std::string getName() const;
+  /** Is this the Boolean type? */
+  bool isBoolean() const;
 
-  /** Is this the boolean type? */
-  virtual bool isBoolean() const {
-    return false;
-  }
+  /** Cast to a Boolean type */
+  operator BooleanType() const;
 
   /** Is this a function type? */
-  virtual bool isFunction() const {
-    return false;
-  }
+  bool isFunction() const;
 
   /** Is this a predicate type? NOTE: all predicate types are also
       function types. */
-  virtual bool isPredicate() const {
-    return false;
-  }
+  bool isPredicate() const;
 
-  /** Is this a kind type (i.e., the type of a type)? */
-  virtual bool isKind() const {
-    return false;
-  }
+  /** Cast to a function type */
+  operator FunctionType() const;
 
-  /** Outputs a string representation of this type to the stream. */
-  virtual void toStream(std::ostream& out) const {
-    out << getName();
-  }
+  /** Is this a sort kind */
+  bool isSort() const;
 
-protected:
-  /** Create an un-named type. */
-  Type();
+  /** Cast to a sort type */
+  operator SortType() const;
 
-  /** Create a type with the given name. */
-  Type(std::string name);
+  /** Is this a kind type (i.e., the type of a type)? */
+  bool isKind() const;
 
-  /** The name of the type (may be empty). */
-  std::string d_name;
+  /** Cast to a kind type */
+  operator KindType() const;
 
-  /**
-   * The reference count for this Type (how many times it's referred
-   * to in the Type attribute table)
-   */
-  unsigned d_rc;
+  /** Outputs a string representation of this type to the stream. */
+  virtual void toStream(std::ostream& out) const;
 
-  /** 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::TypeCleanupStrategy;
 };
 
 /**
  * Singleton class encapsulating the boolean type.
  */
-class BooleanType : public Type {
+class CVC4_PUBLIC BooleanType : public Type {
 
 public:
-  /** Is this the boolean type? (Returns true.) */
-  bool isBoolean() const;
 
-  static BooleanType* getInstance();
-private:
+  /** Construct from the base type */
+  BooleanType(const Type& type);
 
-  /** Create a type associated with nodeManager. */
-  BooleanType();
-
-  /**
-   * Do-nothing private copy constructor operator, to prevent
-   * copy-construction.
-   */
-  BooleanType(const BooleanType&);
-
-  /** Destructor */
-  ~BooleanType();
-
-  /**
-   * Do-nothing private assignment operator, to prevent assignment.
-   */
-  BooleanType& operator=(const BooleanType&);
+  /** Is this the boolean type? (Returns true.) */
+  bool isBoolean() const;
 
-  /** The singleton instance */
-  static BooleanType s_instance;
+  /** Just outputs BOOLEAN */
+  void toStream(std::ostream& out) const;
 };
 
 /**
  * Class encapsulating a function type.
- * TODO: Override == to check component types?
  */
-class FunctionType : public Type {
+class CVC4_PUBLIC FunctionType : public Type {
 
 public:
-  /** Retrieve the argument types. The vector will be non-empty. */
-  const std::vector<Type*> getArgTypes() const;
+
+  /** Construct from the base type */
+  FunctionType(const Type& type);
+
+  /** Get the argument types */
+  std::vector<Type> getArgTypes() const;
 
   /** Get the range type (i.e., the type of the result). */
-  Type* getRangeType() const;
+  Type getRangeType() const;
 
   /** Is this as function type? (Returns true.) */
   bool isFunction() const;
 
-  /** Is this as predicate type? (Returns true if range is
-      boolean.) */
+  /** Is this as predicate type? (Returns true if range is Boolean.) */
   bool isPredicate() const;
 
   /**
@@ -179,74 +172,38 @@ public:
    */
   void toStream(std::ostream& out) const;
 
-private:
-
-  /**
-   * Construct a function type associated with nodeManager, given a
-   * vector of argument types and the range type.
-
-   * @param argTypes a non-empty vector of input types
-   * @param range the result type
-   */
-  FunctionType(const std::vector<Type*>& argTypes,
-               Type* range);
-
-  /** Destructor */
-  ~FunctionType();
-
-  /** The list of input types. */
-  const std::vector<Type*> d_argTypes;
-
-  /** The result type. */
-  Type* d_rangeType;
-
-  friend class NodeManager;
 };
 
-
-/** Class encapsulating the kind type (the type of types).
-*/
-class KindType : public Type {
+/**
+ * Class encapsulating a user-defined sort.
+ */
+class CVC4_PUBLIC SortType : public Type {
 
 public:
-  /** Is this the kind type? (Returns true.) */
-  bool isKind() const;
-
-  /** Get an instance of the kind type. */
-  static KindType* getInstance();
-
-private:
-
-  KindType();
-
-  /* Do-nothing private copy constructor, to prevent copy
-     construction. */
-  KindType(const KindType&);
 
-  /** Destructor */
-  ~KindType();
+  /** Construct from the base type */
+  SortType(const Type& type);
 
-  /* Do-nothing private assignment operator, to prevent assignment. */
-  KindType& operator=(const KindType&);
+  /** Get the name of the sort */
+  std::string getName() const;
 
-  /** The singleton instance */
-  static KindType s_instance;
+  /** Outouts the name of the sort */
+  void toStream(std::ostream& out) const;
 };
 
-/** Class encapsulating a user-defined sort.
-    TODO: Should sort be uniquely named per-nodeManager and not conflict
-    with any builtins? */
-class SortType : public Type {
+/**
+ * Class encapsulating the kind type (the type of types).
+ */
+class CVC4_PUBLIC KindType : public Type {
 
 public:
-  /** Destructor */
-  ~SortType();
 
-private:
-  /** Create a sort with the given name. */
-  SortType(std::string name);
+  /** Construct from the base type */
+  KindType(const Type& type);
+
+  /** Is this the kind type? (Returns true.) */
+  bool isKind() const;
 
-  friend class NodeManager;
 };
 
 /**
@@ -257,22 +214,6 @@ private:
  */
 std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
 
-namespace expr {
-namespace attr {
-
-struct TypeCleanupStrategy {
-  static void cleanup(Type* t) {
-    // reference-count the Type
-    t->dec();
-    if(t->d_rc == 0) {
-      delete t;
-    }
-  }
-};/* struct TypeCleanupStrategy */
-
-}/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__TYPE_H */
diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h
new file mode 100644
index 000000000..86698459b
--- /dev/null
+++ b/src/expr/type_constant.h
@@ -0,0 +1,26 @@
+/*
+ * type_constant.h
+ *
+ *  Created on: Apr 5, 2010
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__TYPE_CONSTANT_H_
+#define __CVC4__TYPE_CONSTANT_H_
+
+namespace CVC4 {
+
+enum TypeConstant {
+  BOOLEAN_TYPE,
+  KIND_TYPE
+};
+
+struct TypeConstantHashStrategy {
+  static inline size_t hash(TypeConstant tc) {
+    return tc;
+  }
+};/* struct BoolHashStrategy */
+
+}
+
+#endif /* __CVC4__TYPE_CONSTANT_H_ */