From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Mon, 26 Apr 2010 21:37:34 +0000 (+0000)
Subject: Adding the intermediary TypeNode to represent (and separate) the Types at the Node... 
X-Git-Tag: cvc5-1.0.0~9109
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3ee48833fd8cffe897a05a986c08a30d9de57213;p=cvc5.git

Adding the intermediary TypeNode to represent (and separate) the Types at the Node level.
---

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 0abeebb9e..404334199 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -8,9 +8,12 @@ noinst_LTLIBRARIES = libexpr.la
 libexpr_la_SOURCES = \
 	node.h \
 	node.cpp \
+	type_node.h \
+	type_node.cpp \
 	node_builder.h \
 	@srcdir@/expr.h \
 	type.h \
+	type.cpp \
 	node_value.h \
 	node_manager.h \
 	@srcdir@/expr_manager.h \
@@ -22,7 +25,6 @@ libexpr_la_SOURCES = \
 	@srcdir@/expr_manager.cpp \
 	node_value.cpp \
 	@srcdir@/expr.cpp \
-	type.cpp \
 	command.h \
 	command.cpp \
 	declaration_scope.h \
@@ -36,6 +38,8 @@ EXTRA_DIST = \
 	@srcdir@/expr.h \
 	@srcdir@/expr_manager.cpp \
 	@srcdir@/expr.cpp \
+	@srcdir@/type.h \
+	@srcdir@/type.cpp \
 	kind_template.h \
 	metakind_template.h \
 	expr_manager_template.h \
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index e5a50591f..bc724cdd1 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -30,6 +30,7 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   deleteFromTable(d_ints, nv);
   deleteFromTable(d_tnodes, nv);
   deleteFromTable(d_nodes, nv);
+  deleteFromTable(d_types, nv);
   deleteFromTable(d_strings, nv);
   deleteFromTable(d_ptrs, nv);
 
@@ -59,6 +60,7 @@ void AttributeManager::deleteAllAttributes() {
   deleteAllFromTable(d_ints);
   deleteAllFromTable(d_tnodes);
   deleteAllFromTable(d_nodes);
+  deleteAllFromTable(d_types);
   deleteAllFromTable(d_strings);
   deleteAllFromTable(d_ptrs);
 
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 4250bb3ef..f231b701c 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -18,6 +18,7 @@
 /* There are strong constraints on ordering of declarations of
  * attributes and nodes due to template use */
 #include "expr/node.h"
+#include "expr/type_node.h"
 
 #ifndef __CVC4__EXPR__ATTRIBUTE_H
 #define __CVC4__EXPR__ATTRIBUTE_H
@@ -59,6 +60,8 @@ class AttributeManager {
   AttrHash<TNode> d_tnodes;
   /** Underlying hash table for node-valued attributes */
   AttrHash<Node> d_nodes;
+  /** Underlying hash table for types attributes */
+  AttrHash<TypeNode> d_types;
   /** Underlying hash table for string-valued attributes */
   AttrHash<std::string> d_strings;
   /** Underlying hash table for pointer-valued attributes */
@@ -241,6 +244,18 @@ struct getTable<Node, false> {
   }
 };
 
+/** Access the "d_types" member of AttributeManager. */
+template <>
+struct getTable<TypeNode, false> {
+  typedef AttrHash<TypeNode> table_type;
+  static inline table_type& get(AttributeManager& am) {
+    return am.d_types;
+  }
+  static inline const table_type& get(const AttributeManager& am) {
+    return am.d_types;
+  }
+};
+
 /** Access the "d_strings" member of AttributeManager. */
 template <>
 struct getTable<std::string, false> {
@@ -313,7 +328,7 @@ struct getTable<TNode, true> {
   }
 };
 
-/** Access the "d_nodes" member of AttributeManager. */
+/** Access the "d_cdnodes" member of AttributeManager. */
 template <>
 struct getTable<Node, true> {
   typedef CDAttrHash<Node> table_type;
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 7407043d2..5d50dd100 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -48,12 +48,12 @@ ExprManager::~ExprManager() {
 
 BooleanType ExprManager::booleanType() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_nodeManager->booleanType();
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()));
 }
 
 KindType ExprManager::kindType() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_nodeManager->kindType();
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->kindType()));
 }
 
 Expr ExprManager::mkExpr(Kind kind) {
@@ -154,46 +154,58 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
 /** Make a function type from domain to range. */
 FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) {
   NodeManagerScope nms(d_nodeManager);
-  return d_nodeManager->mkFunctionType(domain, range);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode)));
 }
 
 /** Make a function type with input types from argTypes. */
 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);
+  std::vector<TypeNode> argTypeNodes;
+  for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
+    argTypeNodes.push_back(*argTypes[i].d_typeNode);
+  }
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode)));
 }
 
 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
   Assert( sorts.size() >= 2 );
   NodeManagerScope nms(d_nodeManager);
-  return d_nodeManager->mkFunctionType(sorts);
+  std::vector<TypeNode> sortNodes;
+  for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
+     sortNodes.push_back(*sorts[i].d_typeNode);
+  }
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes)));
 }
 
 FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
   Assert( sorts.size() >= 1 );
   NodeManagerScope nms(d_nodeManager);
-  return d_nodeManager->mkPredicateType(sorts);
+  std::vector<TypeNode> sortNodes;
+  for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
+     sortNodes.push_back(*sorts[i].d_typeNode);
+  }
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)));
 }
 
 SortType ExprManager::mkSort(const std::string& name) {
   NodeManagerScope nms(d_nodeManager);
-  return d_nodeManager->mkSort(name);
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)));
 }
 
 Type ExprManager::getType(const Expr& e) {
   NodeManagerScope nms(d_nodeManager);
-  return d_nodeManager->getType(e.getNode());
+  return Type(d_nodeManager, new TypeNode(d_nodeManager->getType(e.getNode())));
 }
 
 Expr ExprManager::mkVar(const std::string& name, const Type& type) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkVarPtr(name, type));
+  return Expr(this, d_nodeManager->mkVarPtr(name, *type.d_typeNode));
 }
 
 Expr ExprManager::mkVar(const Type& type) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkVarPtr(type));
+  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
 }
 
 unsigned ExprManager::minArity(Kind kind) {
diff --git a/src/expr/node.h b/src/expr/node.h
index 27756da5b..f8d9117c7 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -33,7 +33,7 @@
 
 namespace CVC4 {
 
-class Type;
+class TypeNode;
 class NodeManager;
 
 template <bool ref_count>
@@ -229,7 +229,7 @@ public:
    * Returns the unique id of this node
    * @return the ud
    */
-  uint64_t getId() const {
+  unsigned getId() const {
     return d_nv->getId();
   }
 
@@ -247,7 +247,7 @@ public:
    * Returns the type of this node.
    * @return the type
    */
-  Type getType() const;
+  TypeNode getType() const;
 
   /**
    * Returns the kind of this node.
@@ -322,16 +322,16 @@ public:
                            const typename AttrKind::value_type& value);
 
   /** Iterator allowing for scanning through the children. */
-  typedef typename expr::NodeValue::iterator<ref_count> iterator;
+  typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > iterator;
   /** Constant iterator allowing for scanning through the children. */
-  typedef typename expr::NodeValue::iterator<ref_count> const_iterator;
+  typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > const_iterator;
 
   /**
    * Returns the iterator pointing to the first child.
    * @return the iterator
    */
   inline iterator begin() {
-    return d_nv->begin<ref_count>();
+    return d_nv->begin< NodeTemplate<ref_count> >();
   }
 
   /**
@@ -340,7 +340,7 @@ public:
    * @return the end of the children iterator.
    */
   inline iterator end() {
-    return d_nv->end<ref_count>();
+    return d_nv->end< NodeTemplate<ref_count> >();
   }
 
   /**
@@ -348,7 +348,7 @@ public:
    * @return the const_iterator
    */
   inline const_iterator begin() const {
-    return d_nv->begin<ref_count>();
+    return d_nv->begin< NodeTemplate<ref_count> >();
   }
 
   /**
@@ -357,7 +357,7 @@ public:
    * @return the end of the children const_iterator.
    */
   inline const_iterator end() const {
-    return d_nv->end<ref_count>();
+    return d_nv->end< NodeTemplate<ref_count> >();
   }
 
   /**
@@ -814,7 +814,7 @@ inline bool NodeTemplate<ref_count>::hasOperator() const {
 }
 
 template <bool ref_count>
-Type NodeTemplate<ref_count>::getType() const {
+TypeNode 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 09e72660e..cefeb2fe2 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -173,6 +173,7 @@
 
 /* strong dependency; make sure node is included first */
 #include "node.h"
+#include "type_node.h"
 
 #ifndef __CVC4__NODE_BUILDER_H
 #define __CVC4__NODE_BUILDER_H
@@ -410,21 +411,21 @@ public:
   // override this in a derived class.
   inline ~NodeBuilderBase();
 
-  typedef expr::NodeValue::iterator<true> iterator;
-  typedef expr::NodeValue::iterator<true> const_iterator;
+  typedef expr::NodeValue::iterator< NodeTemplate<true>  > iterator;
+  typedef expr::NodeValue::iterator< NodeTemplate<true> > const_iterator;
 
   /** Get the begin-const-iterator of this Node-under-construction. */
   inline const_iterator begin() const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    return d_nv->begin<true>();
+    return d_nv->begin< NodeTemplate<true> >();
   }
 
   /** Get the end-const-iterator of this Node-under-construction. */
   inline const_iterator end() const {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
-    return d_nv->end<true>();
+    return d_nv->end< NodeTemplate<true> >();
   }
 
   /** Get the kind of this Node-under-construction. */
@@ -505,6 +506,14 @@ public:
     return append(n);
   }
 
+  /** Append a sequence of children to this TypeNode-under-construction. */
+  inline Builder&
+  append(const std::vector<TypeNode>& children) {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
+    return append(children.begin(), children.end());
+  }
+
   /** Append a sequence of children to this Node-under-construction. */
   template <bool ref_count>
   inline Builder&
@@ -537,6 +546,18 @@ public:
     return static_cast<Builder&>(*this);
   }
 
+  /** Append a child to this Node-under-construction. */
+  Builder& append(const TypeNode& typeNode) {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
+    Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node");
+    allocateNvIfNecessaryForAppend();
+    expr::NodeValue* nv = typeNode.d_nv;
+    nv->inc();
+    d_nv->d_children[d_nv->d_nchildren++] = nv;
+    return static_cast<Builder&>(*this);
+  }
+
 private:
 
   /** Construct the node value out of the node builder */
@@ -553,6 +574,10 @@ public:
   Node* constructNodePtr();
   Node* constructNodePtr() const;
 
+  /** Construction of the TypeNode out of the node builder */
+  TypeNode constructTypeNode();
+  TypeNode constructTypeNode() const;
+
   // two versions, so we can support extraction from (const)
   // NodeBuilders which are temporaries appearing as rvalues
   operator Node();
@@ -1245,6 +1270,17 @@ void NodeBuilderBase<Builder>::decrRefCounts() {
   d_inlineNv.d_nchildren = 0;
 }
 
+
+template <class Builder>
+TypeNode NodeBuilderBase<Builder>::constructTypeNode() {
+  return TypeNode(constructNV());
+}
+
+template <class Builder>
+TypeNode NodeBuilderBase<Builder>::constructTypeNode() const {
+  return TypeNode(constructNV());
+}
+
 template <class Builder>
 Node NodeBuilderBase<Builder>::constructNode() {
   return Node(constructNV());
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 138a87493..cbfcdd110 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -20,6 +20,7 @@
 /* circular dependency; force node.h first */
 #include "expr/attribute.h"
 #include "expr/node.h"
+#include "expr/type_node.h"
 
 #ifndef __CVC4__NODE_MANAGER_H
 #define __CVC4__NODE_MANAGER_H
@@ -32,7 +33,6 @@
 #include "expr/metakind.h"
 #include "expr/node_value.h"
 #include "context/context.h"
-#include "expr/type.h"
 
 namespace CVC4 {
 
@@ -206,7 +206,7 @@ class NodeManager {
 
   // NodeManager's attributes.  These aren't exposed outside of this
   // class; use the getters.
-  typedef expr::Attribute<TypeTag, Node> TypeAttr;
+  typedef expr::Attribute<TypeTag, TypeNode> TypeAttr;
   typedef expr::Attribute<AtomicTag, bool> AtomicAttr;
 
   /**
@@ -290,12 +290,13 @@ public:
    * 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, const Type& type);
-  Node* mkVarPtr(const std::string& name, const Type& type);
+  Node mkVar(const std::string& name, const TypeNode& type);
+  Node* mkVarPtr(const std::string& name, const TypeNode& type);
 
   /** Create a variable with the given type. */
-  Node mkVar(const Type& type);
-  Node* mkVarPtr(const Type& type);
+  Node mkVar(const TypeNode& type);
+  Node* mkVarPtr(const TypeNode& type);
+
 
   /**
    * Create a constant of type T.  It will have the appropriate
@@ -304,6 +305,19 @@ public:
   template <class T>
   Node mkConst(const T&);
 
+  template <class T>
+  TypeNode mkTypeConst(const T&);
+
+  template <class NodeClass, class T>
+  NodeClass mkConstInternal(const T&);
+
+  /** Create a type-variable */
+  TypeNode mkTypeVar();
+  TypeNode mkTypeVar(const std::string& name);
+
+  /** Create a node with no children. */
+  TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
+
   /**
    * Determine whether Nodes of a particular Kind have operators.
    * @returns true if Nodes of Kind k have operators.
@@ -433,10 +447,10 @@ public:
                            const typename AttrKind::value_type& value);
 
   /** Get the (singleton) type for booleans. */
-  inline BooleanType booleanType();
+  inline TypeNode booleanType();
 
   /** Get the (singleton) type for sorts. */
-  inline KindType kindType();
+  inline TypeNode kindType();
 
   /**
    * Make a function type from domain to range.
@@ -445,7 +459,7 @@ public:
    * @param range the range type
    * @returns the functional type domain -> range
    */
-  inline Type mkFunctionType(const Type& domain, const Type& range);
+  inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
 
   /**
    * Make a function type with input types from
@@ -455,7 +469,7 @@ public:
    * @param range the range type
    * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
    */
-  inline Type mkFunctionType(const std::vector<Type>& argTypes, const Type& range);
+  inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range);
 
   /**
    * Make a function type with input types from
@@ -463,7 +477,7 @@ public:
    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
    * at least 2 elements.
    */
-  inline Type mkFunctionType(const std::vector<Type>& sorts);
+  inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
 
   /**
    * Make a predicate type with input types from
@@ -471,18 +485,18 @@ public:
    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
    * element.
    */
-  inline Type mkPredicateType(const std::vector<Type>& sorts);
+  inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
 
   /** Make a new sort. */
-  inline Type mkSort();
+  inline TypeNode mkSort();
 
   /** Make a new sort with the given name. */
-  inline Type mkSort(const std::string& name);
+  inline TypeNode mkSort(const std::string& name);
 
   /**
    * Get the type for the given node.
    */
-  inline Type getType(TNode n);
+  inline TypeNode getType(TNode n);
 
   /**
    * Returns true if this node is atomic (has no more Boolean structure)
@@ -589,63 +603,64 @@ NodeManager::setAttribute(TNode n, const AttrKind&,
 
 
 /** Get the (singleton) type for booleans. */
-inline BooleanType NodeManager::booleanType() {
-  return Type(this, new Node(mkConst<TypeConstant>(BOOLEAN_TYPE)));
+inline TypeNode NodeManager::booleanType() {
+  return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
 }
 
 /** Get the (singleton) type for sorts. */
-inline KindType NodeManager::kindType() {
-  return Type(this, new Node(mkConst<TypeConstant>(KIND_TYPE)));
+inline TypeNode NodeManager::kindType() {
+  return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
 }
 
-/** Make a function type from domain to range.
- * TODO: Function types should be unique for this manager. */
-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 from domain to range. */
+inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
+  std::vector<TypeNode> sorts;
+  sorts.push_back(domain);
+  sorts.push_back(range);
+  return mkFunctionType(sorts);
 }
 
-inline Type NodeManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
+inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
   Assert(argTypes.size() >= 1);
-  std::vector<Type> sorts(argTypes);
+  std::vector<TypeNode> sorts(argTypes);
   sorts.push_back(range);
   return mkFunctionType(sorts);
 }
 
-
-inline Type
-NodeManager::mkFunctionType(const std::vector<Type>& sorts) {
+inline TypeNode
+NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
   Assert(sorts.size() >= 2);
-  std::vector<Node> sortNodes;
+  std::vector<TypeNode> sortNodes;
   for (unsigned i = 0; i < sorts.size(); ++ i) {
-    sortNodes.push_back(*(sorts[i].d_typeNode));
+    sortNodes.push_back(sorts[i]);
   }
-  return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes));
+  return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
 }
 
-inline Type
-NodeManager::mkPredicateType(const std::vector<Type>& sorts) {
+inline TypeNode
+NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   Assert(sorts.size() >= 1);
-  std::vector<Node> sortNodes;
+  std::vector<TypeNode> sortNodes;
   for (unsigned i = 0; i < sorts.size(); ++ i) {
-    sortNodes.push_back(*(sorts[i].d_typeNode));
+    sortNodes.push_back(sorts[i]);
   }
-  sortNodes.push_back(*(booleanType().d_typeNode));
-  return Type(this, mkNodePtr(kind::FUNCTION_TYPE, sortNodes));
+  sortNodes.push_back(booleanType());
+  return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
 }
 
-inline Type NodeManager::mkSort() {
-  return Type(this, mkVarPtr(kindType()));
+inline TypeNode NodeManager::mkSort() {
+  return mkTypeVar();
 }
 
-inline Type NodeManager::mkSort(const std::string& name) {
-  return Type(this, mkVarPtr(name, kindType()));
+inline TypeNode NodeManager::mkSort(const std::string& name) {
+  return mkTypeVar(name);
 }
 
-inline Type NodeManager::getType(TNode n)  {
-  Node* typeNode = new Node;
-  getAttribute(n, TypeAttr(), *typeNode);
+inline TypeNode NodeManager::getType(TNode n)  {
+  TypeNode typeNode;
+  getAttribute(n, TypeAttr(), typeNode);
   // TODO: Type computation
-  return Type(this, typeNode);
+  return typeNode;
 }
 
 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
@@ -815,34 +830,61 @@ inline Node* NodeManager::mkNodePtr(Kind kind,
   return NodeBuilder<>(this, kind).append(children).constructNodePtr();
 }
 
-inline Node NodeManager::mkVar(const std::string& name, const Type& type) {
+// N-ary version for types
+inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector<TypeNode>& children) {
+  return NodeBuilder<>(this, kind).append(children).constructTypeNode();
+}
+
+
+inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
   Node n = mkVar(type);
   n.setAttribute(expr::VarNameAttr(), name);
   return n;
 }
 
-inline Node* NodeManager::mkVarPtr(const std::string& name, const Type& type) {
+inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) {
   Node* n = mkVarPtr(type);
   n->setAttribute(expr::VarNameAttr(), name);
   return n;
 }
 
-inline Node NodeManager::mkVar(const Type& type) {
+inline Node NodeManager::mkVar(const TypeNode& type) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
-  n.setAttribute(TypeAttr(), *type.d_typeNode);
+  n.setAttribute(TypeAttr(), type);
   return n;
 }
 
-inline Node* NodeManager::mkVarPtr(const Type& type) {
+inline TypeNode NodeManager::mkTypeVar(const std::string& name) {
+  TypeNode type = mkTypeVar();
+  type.setAttribute(expr::VarNameAttr(), name);
+  return type;
+}
+
+inline TypeNode NodeManager::mkTypeVar() {
+  TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode();
+  return type;
+}
+
+inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
-  n->setAttribute(TypeAttr(), *type.d_typeNode);
+  n->setAttribute(TypeAttr(), type);
   return n;
 }
 
 template <class T>
 Node NodeManager::mkConst(const T& val) {
-  // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
+  return mkConstInternal<Node, T>(val);
+}
+
+template <class T>
+TypeNode NodeManager::mkTypeConst(const T& val) {
+  return mkConstInternal<TypeNode, T>(val);
+}
+
+template <class NodeClass, class T>
+NodeClass NodeManager::mkConstInternal(const T& val) {
 
+  // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
   NVStorage<1> nvStorage;
   expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
 
@@ -855,7 +897,7 @@ Node NodeManager::mkConst(const T& val) {
   expr::NodeValue* nv = poolLookup(&nvStack);
 
   if(nv != NULL) {
-    return Node(nv);
+    return NodeClass(nv);
   }
 
   nv = (expr::NodeValue*)
@@ -876,7 +918,7 @@ Node NodeManager::mkConst(const T& val) {
   Debug("gc") << "creating node value " << nv
               << " [" << nv->d_id << "]: " << *nv << "\n";
 
-  return Node(nv);
+  return NodeClass(nv);
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index a998dd8e4..260a9daae 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -34,6 +34,7 @@
 namespace CVC4 {
 
 template <bool ref_count> class NodeTemplate;
+class TypeNode;
 template <class Builder> class NodeBuilderBase;
 template <unsigned N> class NodeBuilder;
 class AndNodeBuilder;
@@ -101,6 +102,7 @@ class NodeValue {
   // todo add exprMgr ref in debug case
 
   template <bool> friend class ::CVC4::NodeTemplate;
+  friend class ::CVC4::TypeNode;
   template <class Builder> friend class ::CVC4::NodeBuilderBase;
   template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder;
   friend class ::CVC4::NodeManager;
@@ -137,13 +139,13 @@ private:
   const_nv_iterator nv_begin() const;
   const_nv_iterator nv_end() const;
 
-  template <bool ref_count>
+  template <typename T>
   class iterator {
     const_nv_iterator d_i;
   public:
     explicit iterator(const_nv_iterator i) : d_i(i) {}
 
-    inline CVC4::NodeTemplate<ref_count> operator*();
+    inline T operator*();
 
     bool operator==(const iterator& i) {
       return d_i == i.d_i;
@@ -172,11 +174,11 @@ private:
 
 public:
 
-  template <bool ref_count>
-  inline iterator<ref_count> begin() const;
+  template <typename T>
+  inline iterator<T> begin() const;
 
-  template <bool ref_count>
-  inline iterator<ref_count> end() const;
+  template <typename T>
+  inline iterator<T> end() const;
 
   /**
    * Hash this NodeValue.  For hash_maps, hash_sets, etc.. but this is
@@ -317,18 +319,18 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
   return d_children + d_nchildren;
 }
 
-template <bool ref_count>
-inline NodeValue::iterator<ref_count> NodeValue::begin() const {
+template <typename T>
+inline NodeValue::iterator<T> NodeValue::begin() const {
   NodeValue* const* firstChild = d_children;
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     ++firstChild;
   }
-  return iterator<ref_count>(firstChild);
+  return iterator<T>(firstChild);
 }
 
-template <bool ref_count>
-inline NodeValue::iterator<ref_count> NodeValue::end() const {
-  return iterator<ref_count>(d_children + d_nchildren);
+template <typename T>
+inline NodeValue::iterator<T> NodeValue::end() const {
+  return iterator<T>(d_children + d_nchildren);
 }
 
 inline bool NodeValue::isBeingDeleted() const {
@@ -349,13 +351,14 @@ inline NodeValue* NodeValue::getChild(int i) const {
 }/* CVC4 namespace */
 
 #include "expr/node.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace expr {
 
-template <bool ref_count>
-inline CVC4::NodeTemplate<ref_count> NodeValue::iterator<ref_count>::operator*() {
-  return NodeTemplate<ref_count>(*d_i);
+template <typename T>
+inline T NodeValue::iterator<T>::operator*() {
+  return T(*d_i);
 }
 
 inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 63d270ac1..98a7e88e7 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_node.h"
 #include "expr/type_constant.h"
 #include "util/Assert.h"
 #include <string>
@@ -26,12 +27,12 @@ std::ostream& operator<<(std::ostream& out, const Type& e) {
   return out;
 }
 
-Type Type::makeType(NodeTemplate<false> typeNode) const
+Type Type::makeType(const TypeNode& typeNode) const
 {
-  return Type(d_nodeManager, new Node(typeNode));
+  return Type(d_nodeManager, new TypeNode(typeNode));
 }
 
-Type::Type(NodeManager* nm, NodeTemplate<true>* node)
+Type::Type(NodeManager* nm, TypeNode* node)
 : d_typeNode(node),
   d_nodeManager(nm)
 {
@@ -43,19 +44,19 @@ Type::~Type() {
 }
 
 Type::Type()
-: d_typeNode(new Node()),
+: d_typeNode(new TypeNode()),
   d_nodeManager(NULL)
 {
 }
 
 Type::Type(uintptr_t n)
-: d_typeNode(new Node()),
+: d_typeNode(new TypeNode()),
   d_nodeManager(NULL) {
   AlwaysAssert(n == 0);
 }
 
 Type::Type(const Type& t)
-: d_typeNode(new Node(*t.d_typeNode)),
+: d_typeNode(new TypeNode(*t.d_typeNode)),
   d_nodeManager(t.d_nodeManager)
 {
 }
@@ -95,8 +96,7 @@ void Type::toStream(std::ostream& out) const {
 /** 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;
+  return d_typeNode->isBoolean();
 }
 
 /** Cast to a Boolean type */
@@ -109,14 +109,14 @@ Type::operator BooleanType() const {
 /** Is this a function type? */
 bool Type::isFunction() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getKind() == kind::FUNCTION_TYPE;
+  return d_typeNode->isFunction();
 }
 
 /** 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();
+  return d_typeNode->isPredicate();
 }
 
 /** Cast to a function type */
@@ -129,8 +129,7 @@ Type::operator FunctionType() const {
 /** Is this a sort kind */
 bool Type::isSort() const {
   NodeManagerScope nms(d_nodeManager);
-  return d_typeNode->getKind() == kind::VARIABLE &&
-      d_typeNode->getType().isKind();
+  return d_typeNode->isSort();
 }
 
 /** Cast to a sort type */
@@ -143,8 +142,7 @@ Type::operator SortType() const {
 /** 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;
+  return d_typeNode->isKind();
 }
 
 /** Cast to a kind type */
@@ -157,15 +155,19 @@ Type::operator KindType() const {
 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]));
+  std::vector<TypeNode> argNodes = d_typeNode->getArgTypes();
+  std::vector<TypeNode>::iterator it = argNodes.begin();
+  std::vector<TypeNode>::iterator it_end = argNodes.end();
+  for(; it != it_end; ++ it) {
+    args.push_back(makeType(*it));
   }
   return args;
 }
 
 Type FunctionType::getRangeType() const {
   NodeManagerScope nms(d_nodeManager);
-  return makeType((*d_typeNode)[d_typeNode->getNumChildren()-1]);
+  Assert(isFunction());
+  return makeType(d_typeNode->getRangeType());
 }
 
 void BooleanType::toStream(std::ostream& out) const {
diff --git a/src/expr/type.h b/src/expr/type.h
index 4f9142698..5cbe0613a 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -29,7 +29,7 @@
 namespace CVC4 {
 
 class NodeManager;
-template <bool ref_count> class NodeTemplate;
+class TypeNode;
 
 class BooleanType;
 class FunctionType;
@@ -41,12 +41,12 @@ class SortType;
  */
 class CVC4_PUBLIC Type {
 
-  friend class NodeManager;
+  friend class ExprManager;
 
 protected:
 
   /** The internal expression representation */
-  NodeTemplate<true>* d_typeNode;
+  TypeNode* d_typeNode;
 
   /** The responsible expression manager */
   NodeManager* d_nodeManager;
@@ -54,14 +54,14 @@ protected:
   /**
    * Construct a new type given the typeNode;
    */
-  Type makeType(NodeTemplate<false> typeNode) const;
+  Type makeType(const TypeNode& 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);
+  Type(NodeManager* em, TypeNode* typeNode);
 
 public:
 
@@ -160,12 +160,6 @@ public:
   /** Get the range type (i.e., the type of the result). */
   Type getRangeType() const;
 
-  /** Is this as function type? (Returns true.) */
-  bool isFunction() const;
-
-  /** Is this as predicate type? (Returns true if range is Boolean.) */
-  bool isPredicate() const;
-
   /**
    * Outputs a string representation of this type to the stream,
    * in the format "D -> R" or "(A, B, C) -> R".
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
new file mode 100644
index 000000000..87b6ed58a
--- /dev/null
+++ b/src/expr/type_node.cpp
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/** node.cpp
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Reference-counted encapsulation of a pointer to node information.
+ **/
+
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+TypeNode TypeNode::s_null(&expr::NodeValue::s_null);
+
+bool TypeNode::isBoolean() const {
+  return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE;
+}
+
+/** Is this a function type? */
+bool TypeNode::isFunction() const {
+  return getKind() == kind::FUNCTION_TYPE;
+}
+
+/** Is this a predicate type? NOTE: all predicate types are also
+    function types. */
+bool TypeNode::isPredicate() const {
+  return isFunction() && getRangeType().isBoolean();
+}
+
+std::vector<TypeNode> TypeNode::getArgTypes() const {
+  Assert(isFunction());
+  std::vector<TypeNode> args;
+  for (unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++ i) {
+    args.push_back((*this)[i]);
+  }
+  return args;
+}
+
+TypeNode TypeNode::getRangeType() const {
+  Assert(isFunction());
+  return (*this)[getNumChildren()-1];
+}
+
+
+/** Is this a sort kind */
+bool TypeNode::isSort() const {
+  return getKind() == kind::VARIABLE;
+}
+
+/** Is this a kind type (i.e., the type of a type)? */
+bool TypeNode::isKind() const {
+  return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == KIND_TYPE;
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
new file mode 100644
index 000000000..7747b93e1
--- /dev/null
+++ b/src/expr/type_node.h
@@ -0,0 +1,437 @@
+/*********************                                                        */
+/** type_node.h
+ ** Original author: dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Reference-counted encapsulation of a pointer to node information.
+ **/
+
+#include "cvc4_private.h"
+
+// circular dependency
+#include "expr/node_value.h"
+
+#ifndef __CVC4__TYPE_NODE_H
+#define __CVC4__TYPE_NODE_H
+
+#include <vector>
+#include <string>
+#include <iostream>
+#include <stdint.h>
+
+#include "expr/kind.h"
+#include "expr/metakind.h"
+#include "util/Assert.h"
+#include "util/output.h"
+
+namespace CVC4 {
+
+class NodeManager;
+
+namespace expr {
+class NodeValue;
+}/* CVC4::expr namespace */
+
+/**
+ * Encapsulation of an NodeValue pointer.  The reference count is
+ * maintained in the NodeValue if ref_count is true.
+ */
+class TypeNode {
+
+  /**
+   * The NodeValue has access to the private constructors, so that the
+   * iterators can can create new nodes.
+   */
+  friend class expr::NodeValue;
+
+  /** A convenient null-valued encapsulated pointer */
+  static TypeNode s_null;
+
+  /** The referenced NodeValue */
+  expr::NodeValue* d_nv;
+
+  /**
+   * This constructor is reserved for use by the TypeNode package.
+   */
+  explicit TypeNode(const expr::NodeValue*);
+
+  friend class NodeManager;
+
+  template <class Builder>
+  friend class NodeBuilderBase;
+
+  /**
+   * Assigns the expression value and does reference counting. No assumptions
+   * are made on the expression, and should only be used if we know what we
+   * are doing.
+   *
+   * @param ev the expression value to assign
+   */
+  void assignNodeValue(expr::NodeValue* ev);
+
+public:
+
+  /** Default constructor, makes a null expression. */
+  TypeNode() : d_nv(&expr::NodeValue::s_null) { }
+
+  /** Copy constructor */
+  TypeNode(const TypeNode& node);
+
+  /**
+   * Assignment operator for nodes, copies the relevant information from node
+   * to this node.
+   * @param node the node to copy
+   * @return reference to this node
+   */
+  TypeNode& operator=(const TypeNode& typeNode);
+
+  /**
+   * Destructor. If ref_count is true it will decrement the reference count
+   * and, if zero, collect the NodeValue.
+   */
+  ~TypeNode() throw(AssertionException);
+
+  /**
+   * Return the null node.
+   * @return the null node
+   */
+  static TypeNode null() {
+    return s_null;
+  }
+
+  /**
+   * Returns true if this type is a null type.
+   * @return true if null
+   */
+  bool isNull() const {
+    return d_nv == &expr::NodeValue::s_null;
+  }
+
+  /**
+   * Structural comparison operator for expressions.
+   * @param typeNode the type node to compare to
+   * @return true if expressions are equal, false otherwise
+   */
+  bool operator==(const TypeNode& typeNode) const {
+    return d_nv == typeNode.d_nv;
+  }
+
+  /**
+   * Structural comparison operator for expressions.
+   * @param typeNode the type node to compare to
+   * @return true if expressions are equal, false otherwise
+   */
+  bool operator!=(const TypeNode& typeNode) const {
+    return d_nv != typeNode.d_nv;
+  }
+
+  /**
+   * We compare by expression ids so, keeping things deterministic and having
+   * that subexpressions have to be smaller than the enclosing expressions.
+   * @param node the node to compare to
+   * @return true if this expression is smaller
+   */
+  inline bool operator<(const TypeNode& typeNode) const {
+    return d_nv->d_id < typeNode.d_nv->d_id;
+  }
+
+  /**
+   * Returns the i-th child of this node.
+   * @param i the index of the child
+   * @return the node representing the i-th child
+   */
+  TypeNode operator[](int i) const {
+    return TypeNode(d_nv->getChild(i));
+  }
+
+  /**
+   * Returns the unique id of this node
+   * @return the id
+   */
+  unsigned getId() const {
+    return d_nv->getId();
+  }
+
+  /**
+   * Returns the kind of this type node.
+   * @return the kind
+   */
+  inline Kind getKind() const {
+    return Kind(d_nv->d_kind);
+  }
+
+  /**
+   * Returns the metakind of this type node.
+   * @return the metakind
+   */
+  inline kind::MetaKind getMetaKind() const {
+    return kind::metaKindOf(getKind());
+  }
+
+  /**
+   * Returns the number of children this node has.
+   * @return the number of children
+   */
+  inline size_t getNumChildren() const;
+
+  /**
+   * If this is a CONST_* TypeNode, extract the constant from it.
+   */
+  template <class T>
+  inline const T& getConst() const;
+
+  /**
+   * Returns the value of the given attribute that this has been attached.
+   * @param attKind the kind of the attribute
+   * @return the value of the attribute
+   */
+  template <class AttrKind>
+  inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
+
+  // Note that there are two, distinct hasAttribute() declarations for
+  // a reason (rather than using a pointer-valued argument with a
+  // default value): they permit more optimized code in the underlying
+  // hasAttribute() implementations.
+
+  /**
+   * Returns true if this node has been associated an attribute of given kind.
+   * Additionaly, if a pointer to the value_kind is give, and the attribute
+   * value has been set for this node, it will be returned.
+   * @param attKind the kind of the attribute
+   * @return true if this node has the requested attribute
+   */
+  template <class AttrKind>
+  inline bool hasAttribute(const AttrKind& attKind) const;
+
+  /**
+   * Returns true if this node has been associated an attribute of given kind.
+   * Additionaly, if a pointer to the value_kind is give, and the attribute
+   * value has been set for this node, it will be returned.
+   * @param attKind the kind of the attribute
+   * @param value where to store the value if it exists
+   * @return true if this node has the requested attribute
+   */
+  template <class AttrKind>
+  inline bool getAttribute(const AttrKind& attKind,
+                           typename AttrKind::value_type& value) const;
+
+  /**
+   * Sets the given attribute of this node to the given value.
+   * @param attKind the kind of the atribute
+   * @param value the value to set the attribute to
+   */
+  template <class AttrKind>
+  inline void setAttribute(const AttrKind& attKind,
+                           const typename AttrKind::value_type& value);
+
+  /** Iterator allowing for scanning through the children. */
+  typedef expr::NodeValue::iterator<TypeNode> iterator;
+  /** Constant iterator allowing for scanning through the children. */
+  typedef expr::NodeValue::iterator<TypeNode> const_iterator;
+
+  /**
+   * Returns the iterator pointing to the first child.
+   * @return the iterator
+   */
+  inline iterator begin() {
+    return d_nv->begin<TypeNode>();
+  }
+
+  /**
+   * Returns the iterator pointing to the end of the children (one beyond the
+   * last one.
+   * @return the end of the children iterator.
+   */
+  inline iterator end() {
+    return d_nv->end<TypeNode>();
+  }
+
+  /**
+   * Returns the const_iterator pointing to the first child.
+   * @return the const_iterator
+   */
+  inline const_iterator begin() const {
+    return d_nv->begin<TypeNode>();
+  }
+
+  /**
+   * Returns the const_iterator pointing to the end of the children (one
+   * beyond the last one.
+   * @return the end of the children const_iterator.
+   */
+  inline const_iterator end() const {
+    return d_nv->end<TypeNode>();
+  }
+
+  /**
+   * Converts this node into a string representation.
+   * @return the string representation of this node.
+   */
+  inline std::string toString() const {
+    return d_nv->toString();
+  }
+
+  /**
+   * Converst this node into a string representation and sends it to the
+   * given stream
+   * @param out the sream to serialise this node to
+   */
+  inline void toStream(std::ostream& out, int toDepth = -1) const {
+    d_nv->toStream(out, toDepth);
+  }
+
+  /**
+   * Very basic pretty printer for Node.
+   * @param o output stream to print to.
+   * @param indent number of spaces to indent the formula by.
+   */
+  void printAst(std::ostream & o, int indent = 0) const;
+
+  /** Is this the Boolean type? */
+  bool isBoolean() const;
+
+  /** Is this a function type? */
+  bool isFunction() const;
+
+  /** Get the argument types */
+  std::vector<TypeNode> getArgTypes() const;
+
+  /** Get the range type (i.e., the type of the result). */
+  TypeNode getRangeType() const;
+
+  /** Is this a predicate type? NOTE: all predicate types are also
+      function types. */
+  bool isPredicate() const;
+
+  /** Is this a sort kind */
+  bool isSort() const;
+
+  /** Is this a kind type (i.e., the type of a type)? */
+  bool isKind() const;
+
+private:
+
+  /**
+   * Indents the given stream a given amount of spaces.
+   * @param out the stream to indent
+   * @param indent the numer of spaces
+   */
+  static void indent(std::ostream& out, int indent) {
+    for(int i = 0; i < indent; i++) {
+      out << ' ';
+    }
+  }
+
+};/* class TypeNode */
+
+/**
+ * Serializes a given node to the given stream.
+ * @param out the output stream to use
+ * @param node the node to output to the stream
+ * @return the changed stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
+  n.toStream(out, Node::setdepth::getDepth(out));
+  return out;
+}
+
+}/* CVC4 namespace */
+
+#include <ext/hash_map>
+
+#include "expr/node_manager.h"
+
+namespace CVC4 {
+
+// for hash_maps, hash_sets..
+struct TypeNodeHashFunction {
+  size_t operator()(const CVC4::TypeNode& node) const {
+    return (size_t) node.getId();
+  }
+};
+
+inline size_t TypeNode::getNumChildren() const {
+  return d_nv->getNumChildren();
+}
+
+template <class T>
+inline const T& TypeNode::getConst() const {
+  return d_nv->getConst<T>();
+}
+
+inline TypeNode::TypeNode(const expr::NodeValue* ev) :
+  d_nv(const_cast<expr::NodeValue*> (ev)) {
+  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  d_nv->inc();
+}
+
+inline TypeNode::TypeNode(const TypeNode& typeNode) {
+  Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value!");
+  d_nv = typeNode.d_nv;
+  d_nv->inc();
+}
+
+inline TypeNode::~TypeNode() throw(AssertionException) {
+  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  d_nv->dec();
+}
+
+inline void TypeNode::assignNodeValue(expr::NodeValue* ev) {
+  d_nv = ev;
+  d_nv->inc();
+}
+
+inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
+  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+  if(EXPECT_TRUE( d_nv != typeNode.d_nv )) {
+    d_nv->dec();
+    d_nv = typeNode.d_nv;
+    d_nv->inc();
+  }
+  return *this;
+}
+
+template <class AttrKind>
+inline typename AttrKind::value_type TypeNode::
+getAttribute(const AttrKind&) 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 ?" );
+  return NodeManager::currentNM()->getAttribute(d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool TypeNode::
+hasAttribute(const AttrKind&) 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 ?" );
+  return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) 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 ?" );
+  return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void TypeNode::
+setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value);
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__NODE_H */
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index d0be9a351..7894743d6 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();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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(){
-    BooleanType booleanType = d_nodeManager->booleanType();
+    TypeNode 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 bfe0ef3cf..43bcc7fe3 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -60,7 +60,7 @@ class AttributeWhite : public CxxTest::TestSuite {
   Context* d_ctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
-  Type* d_booleanType;
+  TypeNode* d_booleanType;
 
 public:
 
@@ -69,7 +69,7 @@ public:
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
 
-    d_booleanType = new Type(d_nm->booleanType());
+    d_booleanType = new TypeNode(d_nm->booleanType());
   }
 
   void tearDown() {
@@ -146,7 +146,7 @@ public:
     lastId = attr::LastAttributeId<TNode, false>::s_id;
     TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId);
 
-    lastId = attr::LastAttributeId<Node, false>::s_id;
+    lastId = attr::LastAttributeId<TypeNode, false>::s_id;
     TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId);
 
   }
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 6469806d6..7e034036a 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;
+  TypeNode *d_booleanType;
 
 public:
 
@@ -44,7 +44,7 @@ public:
     d_ctxt = new Context;
     d_nodeManager = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nodeManager);
-    d_booleanType = new Type(d_nodeManager->booleanType());
+    d_booleanType = new TypeNode(d_nodeManager->booleanType());
   }
 
   void tearDown() {
@@ -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);
+    TypeNode sort = d_nodeManager->mkSort("T");
+    TypeNode booleanType = d_nodeManager->booleanType();
+    TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
 
     Node f = d_nodeManager->mkVar(predType);
     Node a = d_nodeManager->mkVar(booleanType);
@@ -490,7 +490,7 @@ public:
   }
 
   void testToString() {
-    Type booleanType = d_nodeManager->booleanType();
+    TypeNode 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();
+    TypeNode 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 17e1d6f18..a1887118c 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -37,7 +37,7 @@ private:
   Context* d_ctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
-  Type* d_booleanType;
+  TypeNode* d_booleanType;
 
 public:
 
@@ -47,7 +47,7 @@ public:
     d_scope = new NodeManagerScope(d_nm);
 
     specKind = PLUS;
-    d_booleanType = new Type(d_nm->booleanType());
+    d_booleanType = new TypeNode(d_nm->booleanType());
   }
 
   void tearDown() {
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 118ba8173..0e1e09178 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -142,7 +142,7 @@ public:
   }
 
   void testMkVarWithNoName() {
-    Type booleanType = d_nodeManager->booleanType();
+    TypeNode 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 testMkVarWithName() {
-    Type booleanType = d_nodeManager->booleanType();
+    TypeNode booleanType = d_nodeManager->booleanType();
     Node x = d_nodeManager->mkVar("x", booleanType);
     TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
     TS_ASSERT_EQUALS(x.getNumChildren(),0u);
@@ -187,9 +187,9 @@ public:
   }
 
   void testBooleanType() {
-    Type t = d_nodeManager->booleanType();
-    Type t2 = d_nodeManager->booleanType();
-    Type t3 = d_nodeManager->mkSort("T");
+    TypeNode t = d_nodeManager->booleanType();
+    TypeNode t2 = d_nodeManager->booleanType();
+    TypeNode t3 = d_nodeManager->mkSort("T");
     TS_ASSERT( t.isBoolean() );
     TS_ASSERT( !t.isFunction() );
     TS_ASSERT( !t.isKind() );
@@ -199,14 +199,14 @@ public:
     TS_ASSERT_EQUALS(t, t2);
     TS_ASSERT( t != t3 );
 
-    BooleanType bt = t;
+    TypeNode bt = t;
     TS_ASSERT_EQUALS( bt, t);
   }
 
   void testKindType() {
-    Type t = d_nodeManager->kindType();
-    Type t2 = d_nodeManager->kindType();
-    Type t3 = d_nodeManager->mkSort("T");
+    TypeNode t = d_nodeManager->kindType();
+    TypeNode t2 = d_nodeManager->kindType();
+    TypeNode t3 = d_nodeManager->mkSort("T");
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( !t.isFunction() );
@@ -218,15 +218,15 @@ public:
     TS_ASSERT_EQUALS(t, t2);
     TS_ASSERT( t != t3);
 
-    KindType kt = t;
+    TypeNode kt = t;
     TS_ASSERT_EQUALS( kt, t );
     // TODO: Is there a way to get the type of otherType (it should == t)?
   }
 
   void testMkFunctionTypeBoolToBool() {
-    Type booleanType = d_nodeManager->booleanType();
-    Type t = d_nodeManager->mkFunctionType(booleanType,booleanType);
-    Type t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
+    TypeNode booleanType = d_nodeManager->booleanType();
+    TypeNode t = d_nodeManager->mkFunctionType(booleanType,booleanType);
+    TypeNode t2 = d_nodeManager->mkFunctionType(booleanType,booleanType);
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
@@ -237,7 +237,7 @@ public:
 
     TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = t;
+    TypeNode ft = t;
     TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), 1u);
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], booleanType);
@@ -246,16 +246,16 @@ public:
   }
 
   void testMkFunctionTypeVectorOfArgsWithReturnType() {
-    Type a = d_nodeManager->mkSort();
-    Type b = d_nodeManager->mkSort();
-    Type c = d_nodeManager->mkSort();
+    TypeNode a = d_nodeManager->mkSort();
+    TypeNode b = d_nodeManager->mkSort();
+    TypeNode c = d_nodeManager->mkSort();
 
-    std::vector<Type> argTypes;
+    std::vector<TypeNode> argTypes;
     argTypes.push_back(a);
     argTypes.push_back(b);
 
-    Type t = d_nodeManager->mkFunctionType(argTypes,c);
-    Type t2 = d_nodeManager->mkFunctionType(argTypes,c);
+    TypeNode t = d_nodeManager->mkFunctionType(argTypes,c);
+    TypeNode t2 = d_nodeManager->mkFunctionType(argTypes,c);
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
@@ -266,7 +266,7 @@ public:
 
     TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = t;
+    TypeNode ft = t;
     TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
@@ -276,17 +276,17 @@ public:
   }
 
   void testMkFunctionTypeVectorOfArguments() {
-    Type a = d_nodeManager->mkSort();
-    Type b = d_nodeManager->mkSort();
-    Type c = d_nodeManager->mkSort();
+    TypeNode a = d_nodeManager->mkSort();
+    TypeNode b = d_nodeManager->mkSort();
+    TypeNode c = d_nodeManager->mkSort();
 
-    std::vector<Type> types;
+    std::vector<TypeNode> types;
     types.push_back(a);
     types.push_back(b);
     types.push_back(c);
 
-    Type t = d_nodeManager->mkFunctionType(types);
-    Type t2 = d_nodeManager->mkFunctionType(types);
+    TypeNode t = d_nodeManager->mkFunctionType(types);
+    TypeNode t2 = d_nodeManager->mkFunctionType(types);
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
@@ -297,7 +297,7 @@ public:
 
     TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = t;
+    TypeNode ft = t;
     TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), types.size()-1);
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
@@ -306,18 +306,18 @@ public:
   }
 
   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();
+    TypeNode a = d_nodeManager->mkSort("a");
+    TypeNode b = d_nodeManager->mkSort("b");
+    TypeNode c = d_nodeManager->mkSort("c");
+    TypeNode booleanType = d_nodeManager->booleanType();
 
-    std::vector<Type> argTypes;
+    std::vector<TypeNode> argTypes;
     argTypes.push_back(a);
     argTypes.push_back(b);
     argTypes.push_back(c);
 
-    Type t = d_nodeManager->mkPredicateType(argTypes);
-    Type t2 = d_nodeManager->mkPredicateType(argTypes);
+    TypeNode t = d_nodeManager->mkPredicateType(argTypes);
+    TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
 
     TS_ASSERT( !t.isBoolean() );
     TS_ASSERT( t.isFunction() );
@@ -328,7 +328,7 @@ public:
 
     TS_ASSERT_EQUALS( t, t2 );
 
-    FunctionType ft = t;
+    TypeNode ft = t;
     TS_ASSERT_EQUALS( ft, t );
     TS_ASSERT_EQUALS(ft.getArgTypes().size(), argTypes.size());
     TS_ASSERT_EQUALS(ft.getArgTypes()[0], a);
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 25c22f196..e0dfd7aa8 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);
+    TypeNode typeX = d_nm->booleanType();
+    TypeNode 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 44b13c87c..6b14a38d5 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -94,7 +94,7 @@ class TheoryUFWhite : public CxxTest::TestSuite {
 
   TheoryUF* d_euf;
 
-  Type* d_booleanType;
+  TypeNode* d_booleanType;
 
 public:
 
@@ -107,7 +107,7 @@ public:
     d_outputChannel.clear();
     d_euf = new TheoryUF(d_ctxt, d_outputChannel);
 
-    d_booleanType = new Type(d_nm->booleanType());
+    d_booleanType = new TypeNode(d_nm->booleanType());
   }
 
   void tearDown() {