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.

46 files changed, 1272 insertions, 635 deletions

diff --git a/.cproject b/.cproject
index f759126e8..e8275ea65 100644
--- a/.cproject
+++ b/.cproject
@@ -19,7 +19,7 @@
 <folderInfo id="cdt.managedbuild.toolchain.gnu.base.1461790692.1059214216" name="/" resourcePath="">
 <toolChain id="cdt.managedbuild.toolchain.gnu.base.1311293674" name="cdt.managedbuild.toolchain.gnu.base" superClass="cdt.managedbuild.toolchain.gnu.base">
 <targetPlatform archList="all" binaryParser="org.eclipse.cdt.core.ELF" id="cdt.managedbuild.target.gnu.platform.base.1799734525" name="Debug Platform" osList="linux,hpux,aix,qnx" superClass="cdt.managedbuild.target.gnu.platform.base"/>
-<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="false" parallelizationNumber="-1" superClass="cdt.managedbuild.target.gnu.builder.base">
+<builder buildPath="${workspace_loc/cvc4/}" id="cdt.managedbuild.target.gnu.builder.base.549477204" incrementalBuildTarget="all" keepEnvironmentInBuildfile="false" managedBuildOn="false" name="Gnu Make Builder" parallelBuildOn="true" parallelizationNumber="-1" superClass="cdt.managedbuild.target.gnu.builder.base">
 <outputEntries>
 <entry flags="VALUE_WORKSPACE_PATH|RESOLVED" kind="outputPath" name=""/>
 </outputEntries>
diff --git a/.project b/.project
index 78c44f770..eb382f9ed 100644
--- a/.project
+++ b/.project
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <projectDescription>
-	<name>cvc4-antlr3</name>
+	<name>cvc4</name>
 	<comment></comment>
 	<projects>
 	</projects>
@@ -32,7 +32,7 @@
 				</dictionary>
 				<dictionary>
 					<key>org.eclipse.cdt.make.core.buildArguments</key>
-					<value></value>
+					<value>-j</value>
 				</dictionary>
 				<dictionary>
 					<key>org.eclipse.cdt.make.core.buildCommand</key>
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 4621d7fc5..9be4de19b 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -208,6 +208,20 @@ public:
     Debug("gc") << "done emptying trash for " << this << std::endl;
   }
 
+  void clear() throw(AssertionException) {
+    Debug("gc") << "cdmap " << this
+                << " disappearing, destroying..." << std::endl;
+    for(typename table_type::iterator i = d_map.begin();
+        i != d_map.end();
+        ++i) {
+      (*i).second->deleteSelf();
+    }
+    d_map.clear();
+    emptyTrash();
+    Debug("gc") << "done emptying trash for " << this << std::endl;
+  }
+
+
   // The usual operators of map
 
   size_t size() const {
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_ */
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 16bde1de3..3f4435966 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -123,7 +123,7 @@ command returns [CVC4::Command* cmd = 0]
 declaration[CVC4::Command*& cmd]
 @init {
   std::vector<std::string> ids;
-  Type* t;
+  Type t;
   Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : // FIXME: These could be type or function declarations, if that matters.
@@ -132,7 +132,7 @@ declaration[CVC4::Command*& cmd]
   ;
 
 /** Match the right-hand side of a declaration. Returns the type. */
-declType[CVC4::Type*& t, std::vector<std::string>& idList]
+declType[CVC4::Type& t, std::vector<std::string>& idList]
 @init {
   Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
@@ -148,10 +148,10 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList]
  * Match the type in a declaration and do the declaration binding.
  * TODO: Actually parse sorts into Type objects.
  */
-type[CVC4::Type*& t]
+type[CVC4::Type& t]
 @init {
-  Type* t2;
-  std::vector<Type*> typeList;
+  Type t2;
+  std::vector<Type> typeList;
   Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : /* Simple type */
@@ -199,7 +199,7 @@ identifier[std::string& id,
  * Matches a type.
  * TODO: parse more types
  */
-baseType[CVC4::Type*& t]
+baseType[CVC4::Type& t]
 @init {
   std::string id;
   Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
@@ -211,7 +211,7 @@ baseType[CVC4::Type*& t]
 /**
  * Matches a type identifier
  */
-typeSymbol[CVC4::Type*& t]
+typeSymbol[CVC4::Type& t]
 @init {
   std::string id;
   Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index 5f07b16b7..57914c9de 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -62,38 +62,38 @@ Expr ParserState::getVariable(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
-Type*
+Type
 ParserState::getType(const std::string& var_name,
                      SymbolType type) {
   Assert( isDeclared(var_name, type) );
-  Type* t = getSymbol(var_name,type).getType();
+  Type t = getSymbol(var_name,type).getType();
   return t;
 }
 
-Type* ParserState::getSort(const std::string& name) {
+Type ParserState::getSort(const std::string& name) {
   Assert( isDeclared(name, SYM_SORT) );
-  Type *t = d_declScope.lookupType(name);
+  Type t = d_declScope.lookupType(name);
   return t;
 }
 
 /* Returns true if name is bound to a boolean variable. */
 bool ParserState::isBoolean(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean();
+  return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
 }
 
 /* Returns true if name is bound to a function. */
 bool ParserState::isFunction(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction();
+  return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction();
 }
 
 /* Returns true if name is bound to a function returning boolean. */
 bool ParserState::isPredicate(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate();
+  return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 }
 
 Expr 
-ParserState::mkVar(const std::string& name, Type* type) {
-  Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
+ParserState::mkVar(const std::string& name, const Type& type) {
+  Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type);
   defineVar(name,expr);
   return expr;
@@ -101,7 +101,7 @@ ParserState::mkVar(const std::string& name, Type* type) {
 
 const std::vector<Expr>
 ParserState::mkVars(const std::vector<std::string> names,
-                    Type* type) {
+                    const Type& type) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
     vars.push_back(mkVar(names[i],type));
@@ -134,19 +134,19 @@ ParserState::setLogic(const std::string& name) {
   }
 }
 
-Type*
+Type
 ParserState::mkSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Assert( !isDeclared(name, SYM_SORT) ) ;
-  Type* type = d_exprManager->mkSort(name);
+  Type type = d_exprManager->mkSort(name);
   d_declScope.bindType(name, type);
   Assert( isDeclared(name, SYM_SORT) ) ;
   return type;
 }
 
-const std::vector<Type*>
+const std::vector<Type>
 ParserState::mkSorts(const std::vector<std::string>& names) {
-  std::vector<Type*> types;
+  std::vector<Type> types;
   for(unsigned i = 0; i < names.size(); ++i) {
     types.push_back(mkSort(names[i]));
   }
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index de624e3a0..3ca9c2c0e 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -174,7 +174,7 @@ public:
   /**
    * Returns a sort, given a name
    */
-  Type* getSort(const std::string& sort_name);
+  Type getSort(const std::string& sort_name);
 
   /**
    * Checks if a symbol has been declared.
@@ -216,15 +216,15 @@ public:
    * @param var_name the symbol to lookup
    * @param type the (namespace) type of the symbol
    */
-  Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
+  Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
 
   /** Create a new CVC4 variable expression of the given type. */
-  Expr mkVar(const std::string& name, Type* type);
+  Expr mkVar(const std::string& name, const Type& type);
 
   /** Create a set of new CVC4 variable expressions of the given
    type. */
   const std::vector<Expr>
-  mkVars(const std::vector<std::string> names, Type* type);
+  mkVars(const std::vector<std::string> names, const Type& type);
 
   /** Create a new variable definition (e.g., from a let binding). */
   void defineVar(const std::string& name, const Expr& val);
@@ -234,12 +234,12 @@ public:
   /**
    * Creates a new sort with the given name.
    */
-  Type* mkSort(const std::string& name);
+  Type mkSort(const std::string& name);
 
   /**
    * Creates a new sorts with the given names.
    */
-  const std::vector<Type*>
+  const std::vector<Type>
   mkSorts(const std::vector<std::string>& names);
 
   /** Is the symbol bound to a boolean variable? */
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 25c2fbc89..15f0c8844 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -285,7 +285,7 @@ attribute
 functionDeclaration
 @declarations {
   std::string name;
-  std::vector<Type*> sorts;
+  std::vector<Type> sorts;
 }
   : LPAREN_TOK functionName[name,CHECK_UNDECLARED] 
       t = sortSymbol // require at least one sort
@@ -305,10 +305,10 @@ functionDeclaration
 predicateDeclaration
 @declarations {
   std::string name;
-  std::vector<Type*> p_sorts;
+  std::vector<Type> p_sorts;
 }
   : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
-    { Type *t;
+    { Type t;
       if( p_sorts.empty() ) {
         t = EXPR_MANAGER->booleanType();
       } else { 
@@ -329,7 +329,7 @@ sortDeclaration
 /**
  * Matches a sequence of sort symbols and fills them into the given vector.
  */
-sortList[std::vector<CVC4::Type*>& sorts]
+sortList[std::vector<CVC4::Type>& sorts]
   : ( t = sortSymbol { sorts.push_back(t); })* 
   ;
 
@@ -341,7 +341,7 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check]
   : identifier[name,check,SYM_SORT] 
   ;
 
-sortSymbol returns [CVC4::Type* t]
+sortSymbol returns [CVC4::Type t]
 @declarations {
   std::string name;
 }
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index dc2ad4d35..8a4c6b6f7 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -5,3 +5,9 @@
 #
 
 theory ::CVC4::theory::bv::TheoryBV "theory_bv.h"
+
+constant CONST_BITVECTOR \
+    ::CVC4::BitVector \
+    ::CVC4::BitVectorHashStrategy \
+    "util/bitvector.h" \
+    "a fixed-width bit-vector constant"
\ No newline at end of file
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 37542d952..d9b7a4fa6 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -139,7 +139,7 @@ class TheoryEngine {
     }
     Debug("rewrite") << "rewrote-children of " << in << std::endl
                      << "got " << b << std::endl;
-    return Node(b);
+    return b;
   }
 
   /**
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 6597c8b48..7820acb0a 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -25,4 +25,7 @@ libutil_la_SOURCES = \
 	rational.h \
 	rational.cpp \
 	integer.h \
-	integer.cpp
+	integer.cpp \
+	bitvector.h \
+	bitvector.cpp \
+	gmp_util.h
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
new file mode 100644
index 000000000..bea06f71a
--- /dev/null
+++ b/src/util/bitvector.cpp
@@ -0,0 +1,16 @@
+/*
+ * bitvector.cpp
+ *
+ *  Created on: Apr 5, 2010
+ *      Author: dejan
+ */
+
+#include "bitvector.h"
+
+namespace CVC4 {
+
+std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
+  return os << bv.toString();
+}
+
+}
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
new file mode 100644
index 000000000..3859fa407
--- /dev/null
+++ b/src/util/bitvector.h
@@ -0,0 +1,99 @@
+/*
+ * bitvector.h
+ *
+ *  Created on: Mar 31, 2010
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__BITVECTOR_H_
+#define __CVC4__BITVECTOR_H_
+
+#include <string>
+#include <iostream>
+#include "util/gmp_util.h"
+
+namespace CVC4 {
+
+class BitVector {
+
+private:
+
+  unsigned d_size;
+  mpz_class d_value;
+
+  BitVector(unsigned size, const mpz_class& val) : d_size(size), d_value(val) {}
+
+public:
+
+  BitVector(unsigned size = 0)
+  : d_size(size), d_value(0) {}
+
+  BitVector(unsigned size, unsigned int z)
+  : d_size(size), d_value(z) {}
+
+  BitVector(unsigned size, unsigned long int z)
+  : d_size(size), d_value(z) {}
+
+  BitVector(unsigned size, const BitVector& q)
+  : d_size(size), d_value(q.d_value) {}
+
+  ~BitVector() {}
+
+  BitVector& operator =(const BitVector& x) {
+    if(this == &x)
+      return *this;
+    d_value = x.d_value;
+    return *this;
+  }
+
+  bool operator ==(const BitVector& y) const {
+    if (d_size != y.d_size) return false;
+    return d_value == y.d_value;
+  }
+
+  bool operator !=(const BitVector& y) const {
+    if (d_size == y.d_size) return false;
+    return d_value != y.d_value;
+  }
+
+  BitVector operator +(const BitVector& y) const {
+    return BitVector(std::max(d_size, y.d_size), d_value + y.d_value);
+  }
+
+  BitVector operator -(const BitVector& y) const {
+    return *this + ~y + 1;
+  }
+
+  BitVector operator -() const {
+    return ~(*this) + 1;
+  }
+
+  BitVector operator *(const BitVector& y) const {
+    return BitVector(d_size, d_value * y.d_value);
+  }
+
+  BitVector operator ~() const {
+    return BitVector(d_size, d_value);
+  }
+
+  size_t hash() const {
+    return gmpz_hash(d_value.get_mpz_t());
+  }
+
+  std::string toString(unsigned int base = 2) const {
+    return d_value.get_str(base);
+  }
+};
+
+struct BitVectorHashStrategy {
+  static inline size_t hash(const BitVector& bv) {
+    return bv.hash();
+  }
+};
+
+std::ostream& operator <<(std::ostream& os, const BitVector& bv);
+
+}
+
+
+#endif /* __CVC4__BITVECTOR_H_ */
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
new file mode 100644
index 000000000..1849974cd
--- /dev/null
+++ b/src/util/gmp_util.h
@@ -0,0 +1,28 @@
+/*
+ * gmp.h
+ *
+ *  Created on: Apr 5, 2010
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__GMP_H_
+#define __CVC4__GMP_H_
+
+#include <gmpxx.h>
+
+namespace CVC4 {
+
+  /** Hashes the gmp integer primitive in a word by word fashion. */
+  inline size_t gmpz_hash(const mpz_t toHash) {
+    size_t hash = 0;
+    for (int i=0, n=mpz_size(toHash); i<n; ++i){
+      mp_limb_t limb = mpz_getlimbn(toHash, i);
+      hash = hash * 2;
+      hash = hash xor limb;
+    }
+    return hash;
+  }
+
+}
+
+#endif /* __CVC4__GMP_H_ */
diff --git a/src/util/integer.cpp b/src/util/integer.cpp
index 3a7851eec..a26f2108f 100644
--- a/src/util/integer.cpp
+++ b/src/util/integer.cpp
@@ -23,6 +23,6 @@
 
 using namespace CVC4;
 
-std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n){
+std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
   return os << n.toString();
 }
diff --git a/src/util/integer.h b/src/util/integer.h
index c1e5d90ea..2aa8b711a 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -18,22 +18,12 @@
 #ifndef __CVC4__INTEGER_H
 #define __CVC4__INTEGER_H
 
-#include <gmpxx.h>
 #include <string>
+#include <iostream>
+#include "util/gmp_util.h"
 
 namespace CVC4 {
 
-/** Hashes the gmp integer primitive in a word by word fashion. */
-inline size_t gmpz_hash(const mpz_t toHash){
-  size_t hash = 0;
-  for (int i=0, n=mpz_size(toHash); i<n; ++i){
-    mp_limb_t limb = mpz_getlimbn(toHash, i);
-    hash = hash * 2;
-    hash = hash xor limb;
-  }
-  return hash;
-}
-
 class Rational;
 
 class Integer {
diff --git a/src/util/rational.h b/src/util/rational.h
index 48b00899a..e4f0e2bb7 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -24,9 +24,8 @@
 #ifndef __CVC4__RATIONAL_H
 #define __CVC4__RATIONAL_H
 
-#include <gmpxx.h>
 #include <string>
-#include "integer.h"
+#include "util/integer.h"
 
 namespace CVC4 {
 
@@ -76,20 +75,20 @@ public:
   /**
    * Constructs a canonical Rational from a numerator and denominator.
    */
-  Rational(  signed int n,   signed int d) : d_value(n,d) {
+  Rational(signed int n, signed int d) : d_value(n,d) {
     d_value.canonicalize();
   }
   Rational(unsigned int n, unsigned int d) : d_value(n,d) {
     d_value.canonicalize();
   }
-  Rational(  signed long int n,   signed long int d) : d_value(n,d) {
+  Rational(signed long int n, signed long int d) : d_value(n,d) {
     d_value.canonicalize();
   }
   Rational(unsigned long int n, unsigned long int d) : d_value(n,d) {
     d_value.canonicalize();
   }
 
-  Rational(const Integer& n, const Integer& d):
+  Rational(const Integer& n, const Integer& d) :
     d_value(n.get_mpz(), d.get_mpz())
   {
     d_value.canonicalize();
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 5ae644193..d0be9a351 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -70,7 +70,7 @@ public:
   typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> MyDataAttribute;
 
   void testDeallocation() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
     MyData* data;
     MyData* data1;
@@ -88,7 +88,7 @@ public:
   typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute;
   typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute;
   void testInts(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
     const uint64_t val = 63489;
     uint64_t data0 = 0;
@@ -116,7 +116,7 @@ public:
   typedef expr::Attribute<TNodeAttributeId, TNode> TNodeAttribute;
   typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute;
   void testTNodes(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     Node val(d_nodeManager->mkVar(booleanType));
@@ -151,7 +151,7 @@ public:
   typedef expr::Attribute<PtrAttributeId, Foo*> PtrAttribute;
   typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute;
   void testPtrs(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     Foo* val = new Foo(63489);
@@ -182,7 +182,7 @@ public:
   typedef expr::Attribute<ConstPtrAttributeId, const Foo*> ConstPtrAttribute;
   typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute;
   void testConstPtrs(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     const Foo* val = new Foo(63489);
@@ -212,7 +212,7 @@ public:
   typedef expr::Attribute<StringAttributeId, std::string> StringAttribute;
   typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute;
   void testStrings(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     std::string val("63489");
@@ -241,7 +241,7 @@ public:
   typedef expr::Attribute<BoolAttributeId, bool> BoolAttribute;
   typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute;
   void testBools(){
-    Type* booleanType = d_nodeManager->booleanType();
+    BooleanType booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkVar(booleanType));
 
     bool val = true;
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index e3b7811a4..bfe0ef3cf 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -69,10 +69,11 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
 
-    d_booleanType = d_nm->booleanType();
+    d_booleanType = new Type(d_nm->booleanType());
   }
 
   void tearDown() {
+    delete d_booleanType;
     delete d_scope;
     delete d_nm;
     delete d_ctxt;
@@ -101,9 +102,7 @@ public:
     TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id);
 
     lastId = attr::LastAttributeId<void*, false>::s_id;
-    TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
     TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
-    TS_ASSERT_DIFFERS(NodeManager::TypeAttr::s_id, theory::uf::ECAttr::s_id);
 
     lastId = attr::LastAttributeId<bool, false>::s_id;
     TS_ASSERT_LESS_THAN(NodeManager::AtomicAttr::s_id, lastId);
@@ -146,14 +145,18 @@ public:
 
     lastId = attr::LastAttributeId<TNode, false>::s_id;
     TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId);
+
+    lastId = attr::LastAttributeId<Node, false>::s_id;
+    TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
+
   }
 
   void testCDAttributes() {
     //Debug.on("boolattr");
 
-    Node a = d_nm->mkVar(d_booleanType);
-    Node b = d_nm->mkVar(d_booleanType);
-    Node c = d_nm->mkVar(d_booleanType);
+    Node a = d_nm->mkVar(*d_booleanType);
+    Node b = d_nm->mkVar(*d_booleanType);
+    Node c = d_nm->mkVar(*d_booleanType);
 
     Debug("boolattr", "get flag 1 on a (should be F)\n");
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -279,10 +282,10 @@ public:
   void testAttributes() {
     //Debug.on("boolattr");
 
-    Node a = d_nm->mkVar(d_booleanType);
-    Node b = d_nm->mkVar(d_booleanType);
-    Node c = d_nm->mkVar(d_booleanType);
-    Node unnamed = d_nm->mkVar(d_booleanType);
+    Node a = d_nm->mkVar(*d_booleanType);
+    Node b = d_nm->mkVar(*d_booleanType);
+    Node c = d_nm->mkVar(*d_booleanType);
+    Node unnamed = d_nm->mkVar(*d_booleanType);
 
     a.setAttribute(VarNameAttr(), "a");
     b.setAttribute(VarNameAttr(), "b");
diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h
index f93a3fcc8..67e6d3e98 100644
--- a/test/unit/expr/declaration_scope_black.h
+++ b/test/unit/expr/declaration_scope_black.h
@@ -56,7 +56,7 @@ public:
 
   void testBind() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
     declScope.bind("x",x);
     TS_ASSERT( declScope.isBound("x") );
@@ -65,7 +65,7 @@ public:
 
   void testBind2() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     // var name attribute shouldn't matter
     Expr y = d_exprManager->mkVar("y", booleanType);
     declScope.bind("x",y);
@@ -75,7 +75,7 @@ public:
 
   void testBind3() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
     declScope.bind("x",x);
     Expr y = d_exprManager->mkVar(booleanType);
@@ -87,11 +87,11 @@ public:
 
   void testBind4() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
     declScope.bind("x",x);
 
-    Type *t = d_exprManager->mkSort("T");
+    Type t = d_exprManager->mkSort("T");
     // duplicate binding for type is OK
     declScope.bindType("x",t);
 
@@ -103,7 +103,7 @@ public:
 
   void testBindType() {
     DeclarationScope declScope;
-    Type *s = d_exprManager->mkSort("S");
+    Type s = d_exprManager->mkSort("S");
     declScope.bindType("S",s);
     TS_ASSERT( declScope.isBoundType("S") );
     TS_ASSERT_EQUALS( declScope.lookupType("S"), s );
@@ -112,7 +112,7 @@ public:
   void testBindType2() {
     DeclarationScope declScope;
     // type name attribute shouldn't matter
-    Type *s = d_exprManager->mkSort("S");
+    Type s = d_exprManager->mkSort("S");
     declScope.bindType("T",s);
     TS_ASSERT( declScope.isBoundType("T") );
     TS_ASSERT_EQUALS( declScope.lookupType("T"), s );
@@ -120,9 +120,9 @@ public:
 
   void testBindType3() {
     DeclarationScope declScope;
-    Type *s = d_exprManager->mkSort("S");
+    Type s = d_exprManager->mkSort("S");
     declScope.bindType("S",s);
-    Type *t = d_exprManager->mkSort("T");
+    Type t = d_exprManager->mkSort("T");
     // new binding covers old
     declScope.bindType("S",t);
     TS_ASSERT( declScope.isBoundType("S") );
@@ -131,7 +131,7 @@ public:
 
   void testPushScope() {
     DeclarationScope declScope;
-    Type *booleanType = d_exprManager->booleanType();
+    Type booleanType = d_exprManager->booleanType();
     Expr x = d_exprManager->mkVar(booleanType);
     declScope.bind("x",x);
     declScope.pushScope();
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index fd36a7cfa..f40e32ef9 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -254,22 +254,18 @@ public:
   }
 
   void testGetType() {
-    /* Type* getType() const; */
+    /* Type getType(); */
 
     TS_ASSERT(a->getType() == d_em->booleanType());
     TS_ASSERT(b->getType() == d_em->booleanType());
-    TS_ASSERT(c->getType() == NULL);
-    TS_ASSERT(mult->getType() == NULL);
-    TS_ASSERT(plus->getType() == NULL);
-    TS_ASSERT(d->getType() == NULL);
-#ifdef CVC4_ASSERTIONS
-    TS_ASSERT_THROWS(null->getType(), AssertionException);
-#endif /* CVC4_ASSERTIONS */
-
-    TS_ASSERT(i1->getType() == NULL);
-    TS_ASSERT(i2->getType() == NULL);
-    TS_ASSERT(r1->getType() == NULL);
-    TS_ASSERT(r2->getType() == NULL);
+    TS_ASSERT(c->getType().isNull());
+    TS_ASSERT(mult->getType().isNull());
+    TS_ASSERT(plus->getType().isNull());
+    TS_ASSERT(d->getType().isNull());
+    TS_ASSERT(i1->getType().isNull());
+    TS_ASSERT(i2->getType().isNull());
+    TS_ASSERT(r1->getType().isNull());
+    TS_ASSERT(r2->getType().isNull());
   }
 
   void testToString() {
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 23d1daf4e..6469806d6 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -36,7 +36,7 @@ private:
   Context* d_ctxt;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
-  Type* d_booleanType;
+  Type *d_booleanType;
 
 public:
 
@@ -44,11 +44,11 @@ public:
     d_ctxt = new Context;
     d_nodeManager = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nodeManager);
-
-    d_booleanType = d_nodeManager->booleanType();
+    d_booleanType = new Type(d_nodeManager->booleanType());
   }
 
   void tearDown() {
+    delete d_booleanType;
     delete d_scope;
     delete d_nodeManager;
     delete d_ctxt;
@@ -97,12 +97,12 @@ public:
   void testOperatorEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkVar(d_booleanType);
+    b = d_nodeManager->mkVar(*d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar(d_booleanType);
+    Node d = d_nodeManager->mkVar(*d_booleanType);
 
     TS_ASSERT(a==a);
     TS_ASSERT(a==b);
@@ -137,12 +137,12 @@ public:
 
     Node a, b, c;
 
-    b = d_nodeManager->mkVar(d_booleanType);
+    b = d_nodeManager->mkVar(*d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar(d_booleanType);
+    Node d = d_nodeManager->mkVar(*d_booleanType);
 
     /*structed assuming operator == works */
     TS_ASSERT(iff(a!=a, !(a==a)));
@@ -199,7 +199,7 @@ public:
   /*tests:   Node& operator=(const Node&); */
   void testOperatorAssign() {
     Node a, b;
-    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(d_booleanType));
+    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(*d_booleanType));
 
     b = c;
     TS_ASSERT(b==c);
@@ -320,8 +320,8 @@ public:
   void testIteNode() {
     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
-    Node a = d_nodeManager->mkVar(d_booleanType);
-    Node b = d_nodeManager->mkVar(d_booleanType);
+    Node a = d_nodeManager->mkVar(*d_booleanType);
+    Node b = d_nodeManager->mkVar(*d_booleanType);
 
     Node cnd = d_nodeManager->mkNode(PLUS, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
@@ -383,8 +383,8 @@ public:
   void testGetKind() {
     /*inline Kind getKind() const; */
 
-    Node a = d_nodeManager->mkVar(d_booleanType);
-    Node b = d_nodeManager->mkVar(d_booleanType);
+    Node a = d_nodeManager->mkVar(*d_booleanType);
+    Node b = d_nodeManager->mkVar(*d_booleanType);
 
     Node n = d_nodeManager->mkNode(NOT, a);
     TS_ASSERT(NOT == n.getKind());
@@ -400,9 +400,9 @@ public:
   }
 
   void testGetOperator() {
-    Type* sort = d_nodeManager->mkSort("T");
-    Type* booleanType = d_nodeManager->booleanType();
-    Type* predType = d_nodeManager->mkFunctionType(sort, booleanType);
+    Type sort = d_nodeManager->mkSort("T");
+    Type booleanType = d_nodeManager->booleanType();
+    Type predType = d_nodeManager->mkFunctionType(sort, booleanType);
 
     Node f = d_nodeManager->mkVar(predType);
     Node a = d_nodeManager->mkVar(booleanType);
@@ -466,9 +466,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nodeManager->mkVar(d_booleanType);
-    Node y = d_nodeManager->mkVar(d_booleanType);
-    Node z = d_nodeManager->mkVar(d_booleanType);
+    Node x = d_nodeManager->mkVar(*d_booleanType);
+    Node y = d_nodeManager->mkVar(*d_booleanType);
+    Node z = d_nodeManager->mkVar(*d_booleanType);
     Node n = b << x << y << z << kind::AND;
 
     { // iterator
@@ -490,7 +490,7 @@ public:
   }
 
   void testToString() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
 
     Node w = d_nodeManager->mkVar("w",booleanType);
     Node x = d_nodeManager->mkVar("x",booleanType);
@@ -503,7 +503,7 @@ public:
   }
 
   void testToStream() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
 
     Node w = d_nodeManager->mkVar("w",booleanType);
     Node x = d_nodeManager->mkVar("x",booleanType);
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 4521f3bf6..17e1d6f18 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -47,10 +47,11 @@ public:
     d_scope = new NodeManagerScope(d_nm);
 
     specKind = PLUS;
-    d_booleanType = d_nm->booleanType();
+    d_booleanType = new Type(d_nm->booleanType());
   }
 
   void tearDown() {
+    delete d_booleanType;
     delete d_scope;
     delete d_nm;
     delete d_ctxt;
@@ -212,9 +213,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nm->mkVar(d_booleanType);
-    Node y = d_nm->mkVar(d_booleanType);
-    Node z = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node y = d_nm->mkVar(*d_booleanType);
+    Node z = d_nm->mkVar(*d_booleanType);
     b << x << y << z << AND;
 
     {
@@ -463,9 +464,9 @@ public:
   }
 
   void testAppend() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node y = d_nm->mkVar(d_booleanType);
-    Node z = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node y = d_nm->mkVar(*d_booleanType);
+    Node z = d_nm->mkVar(*d_booleanType);
     Node m = d_nm->mkNode(AND, y, z, x);
     Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
     Node o = d_nm->mkNode(XOR, y, x);
@@ -590,12 +591,12 @@ public:
   }
 
   void testConvenienceBuilders() {
-    Node a = d_nm->mkVar(d_booleanType);
-    Node b = d_nm->mkVar(d_booleanType);
-    Node c = d_nm->mkVar(d_booleanType);
-    Node d = d_nm->mkVar(d_booleanType);
-    Node e = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node a = d_nm->mkVar(*d_booleanType);
+    Node b = d_nm->mkVar(*d_booleanType);
+    Node c = d_nm->mkVar(*d_booleanType);
+    Node d = d_nm->mkVar(*d_booleanType);
+    Node e = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
 
     Node m = a && b;
     Node n = (a && b) || c;
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index e059fa509..873e28bb3 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -142,7 +142,7 @@ public:
   }
 
   void testMkVar1() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar(booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
@@ -150,7 +150,7 @@ public:
   }
 
   void testMkVar2() {
-    Type* booleanType = d_nodeManager->booleanType();
+    Type booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar("x", booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
@@ -187,19 +187,19 @@ public:
   }
 
   void testBooleanType() {
-    Type* booleanType1 = d_nodeManager->booleanType();
-    Type* booleanType2 = d_nodeManager->booleanType();
-    Type* otherType = d_nodeManager->mkSort("T");
-    TS_ASSERT( booleanType1->isBoolean() );
+    Type booleanType1 = d_nodeManager->booleanType();
+    Type booleanType2 = d_nodeManager->booleanType();
+    Type otherType = d_nodeManager->mkSort("T");
+    TS_ASSERT( booleanType1.isBoolean() );
     TS_ASSERT_EQUALS(booleanType1, booleanType2);
     TS_ASSERT( booleanType1 != otherType );
   }
 
   void testKindType() {
-    Type* kindType1 = d_nodeManager->kindType();
-    Type* kindType2 = d_nodeManager->kindType();
-    Type* otherType = d_nodeManager->mkSort("T");
-    TS_ASSERT( kindType1->isKind() );
+    Type kindType1 = d_nodeManager->kindType();
+    Type kindType2 = d_nodeManager->kindType();
+    Type otherType = d_nodeManager->mkSort("T");
+    TS_ASSERT( kindType1.isKind() );
     TS_ASSERT_EQUALS(kindType1, kindType2);
     TS_ASSERT( kindType1 != otherType );
     // TODO: Is there a way to get the type of otherType (it should == kindType)
@@ -213,98 +213,98 @@ public:
    * with the current type implementation it's the best we can do. */
 
   void testMkFunctionType2() {
-    Type *booleanType = d_nodeManager->booleanType();
-    Type *t = d_nodeManager->mkFunctionType(booleanType,booleanType);
+    Type booleanType = d_nodeManager->booleanType();
+    Type t = d_nodeManager->mkFunctionType(booleanType,booleanType);
     TS_ASSERT( t != booleanType );
-    TS_ASSERT( t->isFunction() );
+    TS_ASSERT( t.isFunction() );
 
-    FunctionType* ft = (FunctionType*)t;
-    TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1u);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[0], booleanType);
-    TS_ASSERT_EQUALS(ft->getRangeType(), booleanType);
+    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType);
+    TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
 
 /*    Type *t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
     TS_ASSERT_EQUALS( t, t2 );*/
   }
 
   void testMkFunctionTypeVecType() {
-    Type *a = d_nodeManager->mkSort("a");
-    Type *b = d_nodeManager->mkSort("b");
-    Type *c = d_nodeManager->mkSort("c");
+    Type a = d_nodeManager->mkSort("a");
+    Type b = d_nodeManager->mkSort("b");
+    Type c = d_nodeManager->mkSort("c");
 
-    std::vector<Type*> argTypes;
+    std::vector<Type> argTypes;
     argTypes.push_back(a);
     argTypes.push_back(b);
 
-    Type *t = d_nodeManager->mkFunctionType(argTypes,c);
+    Type t = d_nodeManager->mkFunctionType(argTypes,c);
 
     TS_ASSERT( t != a );
     TS_ASSERT( t != b );
     TS_ASSERT( t != c );
-    TS_ASSERT( t->isFunction() );
+    TS_ASSERT( t.isFunction() );
 
-    FunctionType* ft = (FunctionType*)t;
-    TS_ASSERT_EQUALS(ft->getArgTypes().size(), argTypes.size());
-    TS_ASSERT_EQUALS(ft->getArgTypes()[0], a);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[1], b);
-    TS_ASSERT_EQUALS(ft->getRangeType(), c);
+    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
+    TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
+    TS_ASSERT_EQUALS(ft.getRangeType(), c);
 
 /*    Type *t2 = d_nodeManager->mkFunctionType(argTypes,c);
     TS_ASSERT_EQUALS( t, t2 );*/
   }
 
   void testMkFunctionTypeVec() {
-    Type *a = d_nodeManager->mkSort("a");
-    Type *b = d_nodeManager->mkSort("b");
-    Type *c = d_nodeManager->mkSort("c");
+    Type a = d_nodeManager->mkSort("a");
+    Type b = d_nodeManager->mkSort("b");
+    Type c = d_nodeManager->mkSort("c");
 
-    std::vector<Type*> types;
+    std::vector<Type> types;
     types.push_back(a);
     types.push_back(b);
     types.push_back(c);
 
-    Type *t = d_nodeManager->mkFunctionType(types);
+    Type t = d_nodeManager->mkFunctionType(types);
 
     TS_ASSERT( t != a );
     TS_ASSERT( t != b );
     TS_ASSERT( t != c );
-    TS_ASSERT( t->isFunction() );
+    TS_ASSERT( t.isFunction() );
 
-    FunctionType* ft = (FunctionType*)t;
-    TS_ASSERT_EQUALS(ft->getArgTypes().size(), types.size()-1);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[0], a);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[1], b);
-    TS_ASSERT_EQUALS(ft->getRangeType(), c);
+    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
+    TS_ASSERT_EQUALS(ft.getRangeType(), c);
 
 /*    Type *t2 = d_nodeManager->mkFunctionType(types);
     TS_ASSERT_EQUALS( t, t2 );*/
   }
 
   void testMkPredicateType() {
-    Type *a = d_nodeManager->mkSort("a");
-    Type *b = d_nodeManager->mkSort("b");
-    Type *c = d_nodeManager->mkSort("c");
-    Type *booleanType = d_nodeManager->booleanType();
+    Type a = d_nodeManager->mkSort("a");
+    Type b = d_nodeManager->mkSort("b");
+    Type c = d_nodeManager->mkSort("c");
+    Type booleanType = d_nodeManager->booleanType();
 
-    std::vector<Type*> argTypes;
+    std::vector<Type> argTypes;
     argTypes.push_back(a);
     argTypes.push_back(b);
     argTypes.push_back(c);
 
-    Type *t = d_nodeManager->mkPredicateType(argTypes);
+    Type t = d_nodeManager->mkPredicateType(argTypes);
 
     TS_ASSERT( t != a );
     TS_ASSERT( t != b );
     TS_ASSERT( t != c );
     TS_ASSERT( t != booleanType );
-    TS_ASSERT( t->isFunction() );
-
-    FunctionType* ft = (FunctionType*)t;
-    TS_ASSERT_EQUALS(ft->getArgTypes().size(), argTypes.size());
-    TS_ASSERT_EQUALS(ft->getArgTypes()[0], a);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[1], b);
-    TS_ASSERT_EQUALS(ft->getArgTypes()[2], c);
-    TS_ASSERT_EQUALS(ft->getRangeType(), booleanType);
+    TS_ASSERT( t.isFunction() );
+
+    FunctionType ft = (FunctionType)t;
+    TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
+    TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[1], b);
+    TS_ASSERT_EQUALS(ft.getArgTypes()[2], c);
+    TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
 
 //    Type *t2 = d_nodeManager->mkPredicateType(argTypes);
 //    TS_ASSERT_EQUALS( t, t2 );
diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h
index 653e3a1d7..317817e15 100644
--- a/test/unit/parser/parser_white.h
+++ b/test/unit/parser/parser_white.h
@@ -146,17 +146,17 @@ class ParserWhite : public CxxTest::TestSuite {
 
   void setupContext(ParserState* parserState) {
     /* a, b, c: BOOLEAN */
-    parserState->mkVar("a",(Type*)d_exprManager->booleanType());
-    parserState->mkVar("b",(Type*)d_exprManager->booleanType());
-    parserState->mkVar("c",(Type*)d_exprManager->booleanType());
+    parserState->mkVar("a",d_exprManager->booleanType());
+    parserState->mkVar("b",d_exprManager->booleanType());
+    parserState->mkVar("c",d_exprManager->booleanType());
     /* t, u, v: TYPE */
-    Type *t = parserState->mkSort("t");
-    Type *u = parserState->mkSort("u");
-    Type *v = parserState->mkSort("v");
+    Type t = parserState->mkSort("t");
+    Type u = parserState->mkSort("u");
+    Type v = parserState->mkSort("v");
     /* f : t->u; g: u->v; h: v->t; */
-    parserState->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u));
-    parserState->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v));
-    parserState->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t));
+    parserState->mkVar("f", d_exprManager->mkFunctionType(t,u));
+    parserState->mkVar("g", d_exprManager->mkFunctionType(u,v));
+    parserState->mkVar("h", d_exprManager->mkFunctionType(v,t));
     /* x:t; y:u; z:v; */
     parserState->mkVar("x",t);
     parserState->mkVar("y",u);
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 097724d48..25c22f196 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -211,8 +211,8 @@ public:
   void testRegisterTerm() {
     TS_ASSERT(d_dummy->doneWrapper());
 
-    Type* typeX = d_nm->booleanType();
-    Type* typeF = d_nm->mkFunctionType(typeX, typeX);
+    Type typeX = d_nm->booleanType();
+    Type typeF = d_nm->mkFunctionType(typeX, typeX);
 
     Node x = d_nm->mkVar("x",typeX);
     Node f = d_nm->mkVar("f",typeF);
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index f5da06a0b..44b13c87c 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -107,10 +107,11 @@ public:
     d_outputChannel.clear();
     d_euf = new TheoryUF(d_ctxt, d_outputChannel);
 
-    d_booleanType = d_nm->booleanType();
+    d_booleanType = new Type(d_nm->booleanType());
   }
 
   void tearDown() {
+    delete d_booleanType;
     delete d_euf;
     d_outputChannel.clear();
     delete d_scope;
@@ -119,8 +120,8 @@ public:
   }
 
   void testPushPopChain() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -174,8 +175,8 @@ public:
 
   /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */
   void testSimpleChain() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -199,7 +200,7 @@ public:
 
   /* test that !(x == x) is inconsistent */
   void testSelfInconsistent() {
-    Node x = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
     Node x_neq_x = (x.eqNode(x)).notNode();
 
     d_euf->assertFact(x_neq_x);
@@ -212,7 +213,7 @@ public:
 
   /* test that (x == x) is consistent */
   void testSelfConsistent() {
-    Node x = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_euf->assertFact(x_eq_x);
@@ -228,8 +229,8 @@ public:
       f(x) != x
      } is inconsistent */
   void testChain() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -259,7 +260,7 @@ public:
 
 
   void testPushPopA() {
-    Node x = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_ctxt->push();
@@ -270,8 +271,8 @@ public:
   }
 
   void testPushPopB() {
-    Node x = d_nm->mkVar(d_booleanType);
-    Node f = d_nm->mkVar(d_booleanType);
+    Node x = d_nm->mkVar(*d_booleanType);
+    Node f = d_nm->mkVar(*d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_x_eq_x = f_x.eqNode(x);