Flatten libcvc4 build structure; remove some #include interdependences

12 files changed, 364 insertions, 332 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index bf52da184..16ee454c8 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -15,13 +15,14 @@ libexpr_la_SOURCES = \
 	type.h \
 	type.cpp \
 	node_value.h \
+	node_value.cpp \
 	node_manager.h \
+	node_manager.cpp \
+	node_manager_attributes.h \
 	type_checker.h \
 	attribute.h \
 	attribute_internals.h \
 	attribute.cpp \
-	node_manager.cpp \
-	node_value.cpp \
 	command.h \
 	command.cpp \
 	symbol_table.h \
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 721a09403..f9939fa90 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -587,6 +587,85 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
 
 }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
+
+template <class AttrKind>
+inline typename AttrKind::value_type
+NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
+  return d_attrManager->getAttribute(nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
+                                      const AttrKind&) const {
+  return d_attrManager->hasAttribute(nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&,
+                          typename AttrKind::value_type& ret) const {
+  return d_attrManager->getAttribute(nv, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void
+NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&,
+                          const typename AttrKind::value_type& value) {
+  d_attrManager->setAttribute(nv, AttrKind(), value);
+}
+
+template <class AttrKind>
+inline typename AttrKind::value_type
+NodeManager::getAttribute(TNode n, const AttrKind&) const {
+  return d_attrManager->getAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::hasAttribute(TNode n, const AttrKind&) const {
+  return d_attrManager->hasAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::getAttribute(TNode n, const AttrKind&,
+                          typename AttrKind::value_type& ret) const {
+  return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void
+NodeManager::setAttribute(TNode n, const AttrKind&,
+                          const typename AttrKind::value_type& value) {
+  d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
+}
+
+template <class AttrKind>
+inline typename AttrKind::value_type
+NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
+  return d_attrManager->getAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
+  return d_attrManager->hasAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::getAttribute(TypeNode n, const AttrKind&,
+                          typename AttrKind::value_type& ret) const {
+  return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void
+NodeManager::setAttribute(TypeNode n, const AttrKind&,
+                          const typename AttrKind::value_type& value) {
+  d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR__ATTRIBUTE_H */
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index ad9ec49ac..32a1d73e1 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -19,6 +19,7 @@
 #include "expr/expr_manager_scope.h"
 #include "expr/variable_type_map.h"
 #include "util/cvc4_assert.h"
+#include "expr/node_manager_attributes.h"
 
 #include <vector>
 #include <iterator>
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 30f7ce8b9..b1614f31b 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "expr/node.h"
+#include "expr/attribute.h"
 #include "util/output.h"
 
 #include <iostream>
@@ -51,4 +52,42 @@ UnknownTypeException::UnknownTypeException(TNode n) throw() :
                                " its type cannot be computed until it is substituted away") {
 }
 
+/** Is this node constant? (and has that been computed yet?) */
+struct IsConstTag { };
+struct IsConstComputedTag { };
+typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
+typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
+
+template <bool ref_count>
+bool NodeTemplate<ref_count>::isConst() const {
+  assertTNodeNotExpired();
+  Debug("isConst") << "Node::isConst() for: " << *this << std::endl;
+  if(isNull()) {
+    return false;
+  }
+  switch(getMetaKind()) {
+  case kind::metakind::CONSTANT:
+    Debug("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl;
+    return true;
+  case kind::metakind::VARIABLE:
+    Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
+    return false;
+  default:
+    if(getAttribute(IsConstComputedAttr())) {
+      bool bval = getAttribute(IsConstAttr());
+      Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
+      return bval;
+    } else {
+      bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this);
+      Debug("isConst") << "Node::isConst() computed value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
+      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
+      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
+      return bval;
+    }
+  }
+}
+
+template bool NodeTemplate<true>::isConst() const;
+template bool NodeTemplate<false>::isConst() const;
+
 }/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index e6a163a8b..3c058c924 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -443,7 +443,7 @@ public:
    * Returns true if this node represents a constant
    * @return true if const
    */
-  inline bool isConst() const;
+  bool isConst() const;
 
   /**
    * Returns true if this node represents a constant
@@ -921,7 +921,7 @@ inline std::ostream& operator<<(std::ostream& out,
 
 #include <ext/hash_map>
 
-#include "expr/attribute.h"
+//#include "expr/attribute.h"
 #include "expr/node_manager.h"
 #include "expr/type_checker.h"
 
@@ -1271,42 +1271,6 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const
   return NodeManager::currentNM()->getType(*this, check);
 }
 
-/** Is this node constant? (and has that been computed yet?) */
-struct IsConstTag { };
-struct IsConstComputedTag { };
-typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
-typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
-
-template <bool ref_count>
-inline bool
-NodeTemplate<ref_count>::isConst() const {
-  assertTNodeNotExpired();
-  Debug("isConst") << "Node::isConst() for: " << *this << std::endl;
-  if(isNull()) {
-    return false;
-  }
-  switch(getMetaKind()) {
-  case kind::metakind::CONSTANT:
-    Debug("isConst") << "Node::isConst() returning true, it's a CONSTANT" << std::endl;
-    return true;
-  case kind::metakind::VARIABLE:
-    Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
-    return false;
-  default:
-    if(getAttribute(IsConstComputedAttr())) {
-      bool bval = getAttribute(IsConstAttr());
-      Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
-      return bval;
-    } else {
-      bool bval = expr::TypeChecker::computeIsConst(NodeManager::currentNM(), *this);
-      Debug("isConst") << "Node::isConst() computed value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
-      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstAttr(), bval);
-      const_cast< NodeTemplate<ref_count>* >(this)->setAttribute(IsConstComputedAttr(), true);
-      return bval;
-    }
-  }
-}
-
 template <bool ref_count>
 inline Node
 NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index cc890b9b9..f6424cfe0 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -17,7 +17,9 @@
  **/
 
 #include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
 
+#include "expr/attribute.h"
 #include "util/cvc4_assert.h"
 #include "options/options.h"
 #include "util/statistics_registry.h"
@@ -83,7 +85,7 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_options(new Options()),
   d_statisticsRegistry(new StatisticsRegistry()),
   next_id(0),
-  d_attrManager(ctxt),
+  d_attrManager(new expr::attr::AttributeManager(ctxt)),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
   d_inReclaimZombies(false),
@@ -97,7 +99,7 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_options(new Options(options)),
   d_statisticsRegistry(new StatisticsRegistry()),
   next_id(0),
-  d_attrManager(ctxt),
+  d_attrManager(new expr::attr::AttributeManager(ctxt)),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
   d_inReclaimZombies(false),
@@ -105,7 +107,7 @@ NodeManager::NodeManager(context::Context* ctxt,
   init();
 }
 
-inline void NodeManager::init() {
+void NodeManager::init() {
   poolInsert( &expr::NodeValue::s_null );
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
@@ -125,7 +127,7 @@ NodeManager::~NodeManager() {
 
   {
     ScopedBool dontGC(d_inReclaimZombies);
-    d_attrManager.deleteAllAttributes();
+    d_attrManager->deleteAllAttributes();
   }
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
@@ -153,6 +155,7 @@ NodeManager::~NodeManager() {
   }
 
   delete d_statisticsRegistry;
+  delete d_attrManager;
   delete d_options;
 }
 
@@ -216,7 +219,7 @@ void NodeManager::reclaimZombies() {
       d_nodeUnderDeletion = nv;
 
       // remove attributes
-      d_attrManager.deleteAllAttributes(nv);
+      d_attrManager->deleteAllAttributes(nv);
 
       // decr ref counts of children
       nv->decrRefCounts();
@@ -432,4 +435,155 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
   return dtt;
 }
 
+TypeNode NodeManager::mkSort(uint32_t flags) {
+  NodeBuilder<1> nb(this, kind::SORT_TYPE);
+  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+  nb << sortTag;
+  TypeNode tn = nb.constructTypeNode();
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewSort(tn, flags);
+  }
+  return tn;
+}
+
+TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) {
+  NodeBuilder<1> nb(this, kind::SORT_TYPE);
+  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+  nb << sortTag;
+  TypeNode tn = nb.constructTypeNode();
+  setAttribute(tn, expr::VarNameAttr(), name);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewSort(tn, flags);
+  }
+  return tn;
+}
+
+TypeNode NodeManager::mkSort(TypeNode constructor,
+                                    const std::vector<TypeNode>& children,
+                                    uint32_t flags) {
+  Assert(constructor.getKind() == kind::SORT_TYPE &&
+         constructor.getNumChildren() == 0,
+         "expected a sort constructor");
+  Assert(children.size() > 0, "expected non-zero # of children");
+  Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) &&
+          hasAttribute(constructor.d_nv, expr::VarNameAttr()),
+          "expected a sort constructor" );
+  std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr());
+  Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(),
+         "arity mismatch in application of sort constructor");
+  NodeBuilder<> nb(this, kind::SORT_TYPE);
+  Node sortTag = Node(constructor.d_nv->d_children[0]);
+  nb << sortTag;
+  nb.append(children);
+  TypeNode type = nb.constructTypeNode();
+  setAttribute(type, expr::VarNameAttr(), name);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags);
+  }
+  return type;
+}
+
+TypeNode NodeManager::mkSortConstructor(const std::string& name,
+                                        size_t arity) {
+  Assert(arity > 0);
+  NodeBuilder<> nb(this, kind::SORT_TYPE);
+  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
+  nb << sortTag;
+  TypeNode type = nb.constructTypeNode();
+  setAttribute(type, expr::VarNameAttr(), name);
+  setAttribute(type, expr::SortArityAttr(), arity);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewSortConstructor(type);
+  }
+  return type;
+}
+
+Node NodeManager::mkVar(const std::string& name, const TypeNode& type, uint32_t flags) {
+  Node n = NodeBuilder<0>(this, kind::VARIABLE);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
+  setAttribute(n, expr::VarNameAttr(), name);
+  setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewVar(n, flags);
+  }
+  return n;
+}
+
+Node* NodeManager::mkVarPtr(const std::string& name,
+                            const TypeNode& type, uint32_t flags) {
+  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, TypeCheckedAttr(), true);
+  setAttribute(*n, expr::VarNameAttr(), name);
+  setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewVar(*n, flags);
+  }
+  return n;
+}
+
+Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) {
+  Node n = mkBoundVar(type);
+  setAttribute(n, expr::VarNameAttr(), name);
+  return n;
+}
+
+Node* NodeManager::mkBoundVarPtr(const std::string& name,
+                                 const TypeNode& type) {
+  Node* n = mkBoundVarPtr(type);
+  setAttribute(*n, expr::VarNameAttr(), name);
+  return n;
+}
+
+Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) {
+  Node n = NodeBuilder<0>(this, kind::VARIABLE);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
+  setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewVar(n, flags);
+  }
+  return n;
+}
+
+Node* NodeManager::mkVarPtr(const TypeNode& type, uint32_t flags) {
+  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, TypeCheckedAttr(), true);
+  setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
+  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
+    (*i)->nmNotifyNewVar(*n, flags);
+  }
+  return n;
+}
+
+Node NodeManager::mkBoundVar(const TypeNode& type) {
+  Node n = NodeBuilder<0>(this, kind::BOUND_VARIABLE);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
+  return n;
+}
+
+Node* NodeManager::mkBoundVarPtr(const TypeNode& type) {
+  Node* n = NodeBuilder<0>(this, kind::BOUND_VARIABLE).constructNodePtr();
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, TypeCheckedAttr(), true);
+  return n;
+}
+
+Node NodeManager::mkInstConstant(const TypeNode& type) {
+  Node n = NodeBuilder<0>(this, kind::INST_CONSTANT);
+  n.setAttribute(TypeAttr(), type);
+  n.setAttribute(TypeCheckedAttr(), true);
+  return n;
+}
+
+Node NodeManager::mkAbstractValue(const TypeNode& type) {
+  Node n = mkConst(AbstractValue(++d_abstractValueCount));
+  n.setAttribute(TypeAttr(), type);
+  n.setAttribute(TypeCheckedAttr(), true);
+  return n;
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 31f6d75d9..51ed1f94d 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -19,7 +19,7 @@
 #include "cvc4_private.h"
 
 /* circular dependency; force node.h first */
-#include "expr/attribute.h"
+//#include "expr/attribute.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
 #include "expr/expr.h"
@@ -45,27 +45,11 @@ namespace CVC4 {
 class StatisticsRegistry;
 
 namespace expr {
+  namespace attr {
+    class AttributeManager;
+  }/* CVC4::expr::attr namespace */
 
-class TypeChecker;
-
-// Definition of an attribute for the variable name.
-// TODO: hide this attribute behind a NodeManager interface.
-namespace attr {
-  struct VarNameTag { };
-  struct GlobalVarTag { };
-  struct SortArityTag { };
-  struct DatatypeTupleTag { };
-  struct DatatypeRecordTag { };
-}/* CVC4::expr::attr namespace */
-
-typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
-typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr;
-typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
-/** Attribute true for datatype types that are replacements for tuple types */
-typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr;
-/** Attribute true for datatype types that are replacements for record types */
-typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr;
-
+  class TypeChecker;
 }/* CVC4::expr namespace */
 
 /**
@@ -117,7 +101,7 @@ class NodeManager {
 
   size_t next_id;
 
-  expr::attr::AttributeManager d_attrManager;
+  expr::attr::AttributeManager* d_attrManager;
 
   /** The associated ExprManager */
   ExprManager* d_exprManager;
@@ -274,15 +258,6 @@ class NodeManager {
     expr::NodeValue* child[N];
   };/* struct NodeManager::NVStorage<N> */
 
-  // attribute tags
-  struct TypeTag { };
-  struct TypeCheckedTag { };
-
-  // NodeManager's attributes.  These aren't exposed outside of this
-  // class; use the getters.
-  typedef expr::Attribute<TypeTag, TypeNode> TypeAttr;
-  typedef expr::Attribute<TypeCheckedTag, bool> TypeCheckedAttr;
-
   /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
    *
    * It has been decided for now to hold off on implementations of
@@ -781,18 +756,18 @@ public:
   inline TypeNode mkTesterType(TypeNode domain);
 
   /** Make a new (anonymous) sort of arity 0. */
-  inline TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
+  TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
 
   /** Make a new sort with the given name of arity 0. */
-  inline TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
+  TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
 
   /** Make a new sort by parameterizing the given sort constructor. */
-  inline TypeNode mkSort(TypeNode constructor,
-                         const std::vector<TypeNode>& children,
-                         uint32_t flags = ExprManager::SORT_FLAG_NONE);
+  TypeNode mkSort(TypeNode constructor,
+                  const std::vector<TypeNode>& children,
+                  uint32_t flags = ExprManager::SORT_FLAG_NONE);
 
   /** Make a new sort with the given name and arity. */
-  inline TypeNode mkSortConstructor(const std::string& name, size_t arity);
+  TypeNode mkSortConstructor(const std::string& name, size_t arity);
 
   /**
    * Make a predicate subtype type defined by the given LAMBDA
@@ -933,86 +908,6 @@ public:
   }
 };/* class NodeManagerScope */
 
-
-template <class AttrKind>
-inline typename AttrKind::value_type
-NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
-  return d_attrManager.getAttribute(nv, AttrKind());
-}
-
-template <class AttrKind>
-inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
-                                      const AttrKind&) const {
-  return d_attrManager.hasAttribute(nv, AttrKind());
-}
-
-template <class AttrKind>
-inline bool
-NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&,
-                          typename AttrKind::value_type& ret) const {
-  return d_attrManager.getAttribute(nv, AttrKind(), ret);
-}
-
-template <class AttrKind>
-inline void
-NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&,
-                          const typename AttrKind::value_type& value) {
-  d_attrManager.setAttribute(nv, AttrKind(), value);
-}
-
-template <class AttrKind>
-inline typename AttrKind::value_type
-NodeManager::getAttribute(TNode n, const AttrKind&) const {
-  return d_attrManager.getAttribute(n.d_nv, AttrKind());
-}
-
-template <class AttrKind>
-inline bool
-NodeManager::hasAttribute(TNode n, const AttrKind&) const {
-  return d_attrManager.hasAttribute(n.d_nv, AttrKind());
-}
-
-template <class AttrKind>
-inline bool
-NodeManager::getAttribute(TNode n, const AttrKind&,
-                          typename AttrKind::value_type& ret) const {
-  return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret);
-}
-
-template <class AttrKind>
-inline void
-NodeManager::setAttribute(TNode n, const AttrKind&,
-                          const typename AttrKind::value_type& value) {
-  d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
-}
-
-template <class AttrKind>
-inline typename AttrKind::value_type
-NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
-  return d_attrManager.getAttribute(n.d_nv, AttrKind());
-}
-
-template <class AttrKind>
-inline bool
-NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
-  return d_attrManager.hasAttribute(n.d_nv, AttrKind());
-}
-
-template <class AttrKind>
-inline bool
-NodeManager::getAttribute(TypeNode n, const AttrKind&,
-                          typename AttrKind::value_type& ret) const {
-  return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret);
-}
-
-template <class AttrKind>
-inline void
-NodeManager::setAttribute(TypeNode n, const AttrKind&,
-                          const typename AttrKind::value_type& value) {
-  d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
-}
-
-
 /** Get the (singleton) type for booleans. */
 inline TypeNode NodeManager::booleanType() {
   return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
@@ -1229,69 +1124,6 @@ inline bool NodeManager::hasOperator(Kind k) {
   }
 }
 
-inline TypeNode NodeManager::mkSort(uint32_t flags) {
-  NodeBuilder<1> nb(this, kind::SORT_TYPE);
-  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
-  nb << sortTag;
-  TypeNode tn = nb.constructTypeNode();
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewSort(tn, flags);
-  }
-  return tn;
-}
-
-inline TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) {
-  NodeBuilder<1> nb(this, kind::SORT_TYPE);
-  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
-  nb << sortTag;
-  TypeNode tn = nb.constructTypeNode();
-  setAttribute(tn, expr::VarNameAttr(), name);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewSort(tn, flags);
-  }
-  return tn;
-}
-
-inline TypeNode NodeManager::mkSort(TypeNode constructor,
-                                    const std::vector<TypeNode>& children,
-                                    uint32_t flags) {
-  Assert(constructor.getKind() == kind::SORT_TYPE &&
-         constructor.getNumChildren() == 0,
-         "expected a sort constructor");
-  Assert(children.size() > 0, "expected non-zero # of children");
-  Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) &&
-          hasAttribute(constructor.d_nv, expr::VarNameAttr()),
-          "expected a sort constructor" );
-  std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr());
-  Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(),
-         "arity mismatch in application of sort constructor");
-  NodeBuilder<> nb(this, kind::SORT_TYPE);
-  Node sortTag = Node(constructor.d_nv->d_children[0]);
-  nb << sortTag;
-  nb.append(children);
-  TypeNode type = nb.constructTypeNode();
-  setAttribute(type, expr::VarNameAttr(), name);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags);
-  }
-  return type;
-}
-
-inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
-                                               size_t arity) {
-  Assert(arity > 0);
-  NodeBuilder<> nb(this, kind::SORT_TYPE);
-  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
-  nb << sortTag;
-  TypeNode type = nb.constructTypeNode();
-  setAttribute(type, expr::VarNameAttr(), name);
-  setAttribute(type, expr::SortArityAttr(), arity);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewSortConstructor(type);
-  }
-  return type;
-}
-
 inline Kind NodeManager::operatorToKind(TNode n) {
   return kind::operatorToKind(n.d_nv);
 }
@@ -1540,95 +1372,6 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
   return NodeBuilder<>(this, kind).append(children).constructTypeNode();
 }
 
-
-inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, uint32_t flags) {
-  Node n = NodeBuilder<0>(this, kind::VARIABLE);
-  setAttribute(n, TypeAttr(), type);
-  setAttribute(n, TypeCheckedAttr(), true);
-  setAttribute(n, expr::VarNameAttr(), name);
-  setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n, flags);
-  }
-  return n;
-}
-
-inline Node* NodeManager::mkVarPtr(const std::string& name,
-                                   const TypeNode& type, uint32_t flags) {
-  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
-  setAttribute(*n, TypeAttr(), type);
-  setAttribute(*n, TypeCheckedAttr(), true);
-  setAttribute(*n, expr::VarNameAttr(), name);
-  setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n, flags);
-  }
-  return n;
-}
-
-inline Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) {
-  Node n = mkBoundVar(type);
-  setAttribute(n, expr::VarNameAttr(), name);
-  return n;
-}
-
-inline Node* NodeManager::mkBoundVarPtr(const std::string& name,
-                                        const TypeNode& type) {
-  Node* n = mkBoundVarPtr(type);
-  setAttribute(*n, expr::VarNameAttr(), name);
-  return n;
-}
-
-inline Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) {
-  Node n = NodeBuilder<0>(this, kind::VARIABLE);
-  setAttribute(n, TypeAttr(), type);
-  setAttribute(n, TypeCheckedAttr(), true);
-  setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(n, flags);
-  }
-  return n;
-}
-
-inline Node* NodeManager::mkVarPtr(const TypeNode& type, uint32_t flags) {
-  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
-  setAttribute(*n, TypeAttr(), type);
-  setAttribute(*n, TypeCheckedAttr(), true);
-  setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL);
-  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewVar(*n, flags);
-  }
-  return n;
-}
-
-inline Node NodeManager::mkBoundVar(const TypeNode& type) {
-  Node n = NodeBuilder<0>(this, kind::BOUND_VARIABLE);
-  setAttribute(n, TypeAttr(), type);
-  setAttribute(n, TypeCheckedAttr(), true);
-  return n;
-}
-
-inline Node* NodeManager::mkBoundVarPtr(const TypeNode& type) {
-  Node* n = NodeBuilder<0>(this, kind::BOUND_VARIABLE).constructNodePtr();
-  setAttribute(*n, TypeAttr(), type);
-  setAttribute(*n, TypeCheckedAttr(), true);
-  return n;
-}
-
-inline Node NodeManager::mkInstConstant(const TypeNode& type) {
-  Node n = NodeBuilder<0>(this, kind::INST_CONSTANT);
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(TypeCheckedAttr(), true);
-  return n;
-}
-
-inline Node NodeManager::mkAbstractValue(const TypeNode& type) {
-  Node n = mkConst(AbstractValue(++d_abstractValueCount));
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(TypeCheckedAttr(), true);
-  return n;
-}
-
 template <class T>
 Node NodeManager::mkConst(const T& val) {
   return mkConstInternal<Node, T>(val);
diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h
new file mode 100644
index 000000000..ab55baa6e
--- /dev/null
+++ b/src/expr/node_manager_attributes.h
@@ -0,0 +1,48 @@
+/*********************                                                        */
+/*! \file node_manager_attributes.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#pragma once
+
+#include "expr/attribute.h"
+
+namespace CVC4 {
+namespace expr {
+
+// Definition of an attribute for the variable name.
+// TODO: hide this attribute behind a NodeManager interface.
+namespace attr {
+  struct VarNameTag { };
+  struct GlobalVarTag { };
+  struct SortArityTag { };
+  struct DatatypeTupleTag { };
+  struct DatatypeRecordTag { };
+  struct TypeTag { };
+  struct TypeCheckedTag { };
+}/* CVC4::expr::attr namespace */
+
+typedef Attribute<attr::VarNameTag, std::string> VarNameAttr;
+typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr;
+typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr;
+/** Attribute true for datatype types that are replacements for tuple types */
+typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr;
+/** Attribute true for datatype types that are replacements for record types */
+typedef expr::Attribute<expr::attr::DatatypeRecordTag, TypeNode> DatatypeRecordAttr;
+typedef expr::Attribute<expr::attr::TypeTag, TypeNode> TypeAttr;
+typedef expr::Attribute<expr::attr::TypeCheckedTag, bool> TypeCheckedAttr;
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index f3cf992ba..672fc6aae 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -19,6 +19,7 @@
 #include <vector>
 
 #include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
 #include "expr/type.h"
 #include "expr/type_node.h"
 #include "util/exception.h"
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index aa7039f52..b2138c9a1 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -18,10 +18,11 @@
 
 #include "expr/type_checker.h"
 #include "expr/node_manager.h"
+#include "expr/node_manager_attributes.h"
 
 ${typechecker_includes}
 
-#line 25 "${template}"
+#line 26 "${template}"
 
 namespace CVC4 {
 namespace expr {
@@ -34,7 +35,7 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
   switch(n.getKind()) {
   case kind::VARIABLE:
   case kind::SKOLEM:
-    typeNode = nodeManager->getAttribute(n, NodeManager::TypeAttr());
+    typeNode = nodeManager->getAttribute(n, TypeAttr());
     break;
   case kind::BUILTIN:
     typeNode = nodeManager->builtinOperatorType();
@@ -45,16 +46,16 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
 
 ${typerules}
 
-#line 49 "${template}"
+#line 50 "${template}"
 
   default:
     Debug("getType") << "FAILURE" << std::endl;
     Unhandled(n.getKind());
   }
 
-  nodeManager->setAttribute(n, NodeManager::TypeAttr(), typeNode);
-  nodeManager->setAttribute(n, NodeManager::TypeCheckedAttr(),
-                            check || nodeManager->getAttribute(n, NodeManager::TypeCheckedAttr()));
+  nodeManager->setAttribute(n, TypeAttr(), typeNode);
+  nodeManager->setAttribute(n, TypeCheckedAttr(),
+                            check || nodeManager->getAttribute(n, TypeCheckedAttr()));
 
   return typeNode;
 
@@ -68,7 +69,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
   switch(n.getKind()) {
 ${construles}
 
-#line 72 "${template}"
+#line 73 "${template}"
 
   default:;
   }
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 2fc380224..54fd2f3e8 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -16,6 +16,7 @@
 
 #include <vector>
 
+#include "expr/node_manager_attributes.h"
 #include "expr/type_node.h"
 #include "expr/type_properties.h"
 
@@ -482,4 +483,15 @@ TypeNode TypeNode::leastCommonPredicateSubtype(TypeNode t0, TypeNode t1){
   }
 }
 
+/** Is this a sort kind */
+bool TypeNode::isSort() const {
+  return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) ||
+    ( isPredicateSubtype() && getSubtypeParentType().isSort() );
+}
+
+/** Is this a sort constructor kind */
+bool TypeNode::isSortConstructor() const {
+  return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 145ca2aba..75d6d8063 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -916,17 +916,6 @@ inline bool TypeNode::isSExpr() const {
     ( isPredicateSubtype() && getSubtypeParentType().isSExpr() );
 }
 
-/** Is this a sort kind */
-inline bool TypeNode::isSort() const {
-  return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) ||
-    ( isPredicateSubtype() && getSubtypeParentType().isSort() );
-}
-
-/** Is this a sort constructor kind */
-inline bool TypeNode::isSortConstructor() const {
-  return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
-}
-
 /** Is this a predicate subtype */
 inline bool TypeNode::isPredicateSubtype() const {
   return getKind() == kind::SUBTYPE_TYPE;