* src/expr/node.h: add a copy constructor. Apparently GCC doesn't

  recognize an instantiation of the join conversion/copy ctor with
  ref_count = ref_count_1 as a copy constructor.  Problems with
  reference counts ensue.

* src/theory/theory.h, src/theory/theory.cpp: Theory base
  implementation work.  Changed from continuation-style theory calls
  to having an data member for the output channel.  registerTerm() and
  preRegisterTerm() work.

* src/theory/output_channel.h, src/theory/theory.h,
  src/theory/theory.cpp, src/theory/uf/theory_uf.h,
  src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into
  OutputChannel.

* test/unit/expr/node_black.h: remove testPlusNode(),
  testUMinusNode(), testMultNode().

* src/expr/attribute.h: new facilities ManagedAttribute<> and
  CDAttribute<>, and add new template parameters to Attribute<>.  Make
  CDAttribute<>s work with context manager.

* src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and
  TypeAttr are now "owned" (defined) by the NodeManager.  The
  AttributeManager knows nothing of specific attributes, it just as
  all the code for dealing generically with attributes.

* test/unit/expr/node_white.h: test new attribute facilities.

* src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes
  away.

* src/theory/Makefile.am: fixed improper linking of theories

* src/theory/theory_engine.h: some implementation work (mainly stubs
  for now, just to make sure TheoryUF can be instantiated properly,
  etc.)

* src/expr/node_value.cpp, src/expr/node_value.h: move a number of
  function implementations to the header and make them inline

* src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of
  function implementations to the header and make them inline

* src/theory/theoryof_table_prologue.h,
  src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof,
  src/theory/Makefile.am: make the theoryOf() table from kinds and
  implement TheoryEngine::theoryOf().

* src/theory/arith/Makefile, src/theory/bool/Makefile: generated these
  stub Makefiles (with contrib/addsourcedir) as per policy

* src/theory/arith, src/theory/bool [directory properties]: add .deps
  to svn:ignore.

* contrib/configure-in-place: permit configuring "in-place" in the
  source directory.

* contrib/get-authors, contrib/dimacs_to_smt.pl,
  contrib/update-copyright.pl, contrib/get-authors,
  contrib/addsourcedir, src/expr/mkkind: copyright notice

* src/expr/node_manager.h, src/expr/node_builder.h,
  src/prop/prop_engine.h, src/prop/prop_engine.cpp,
  src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp,
  src/theory/output_channel.h: turn "const Node&"-typed formal
  parameters into "TNode"

* src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans"
  to avoid keyword clash on containing namespace

* src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h,
  src/theory/arith/theory_def.h: "define" a theory simply (for automatic
  theoryOf() generator).

* src/Makefile.am: build theory subdirectory before prop, smt, etc. so that
  src/theory/theoryof_table.h header gets generated before it's needed

* src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a
  separate CVC4::kind namespace to avoid its contents from cluttering
  the CVC4 root namespace.  Import the symbol "Kind" into the CVC4 namespace
  but not the enum values.

* src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h,
  src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp,
  src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g,
  src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp,
  test/unit/expr/node_white.h, test/unit/expr/node_black.h,
  test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h:
  update for having moved Kind into CVC4::kind.

* src/parser/parser.cpp: added file-does-not-exist check (was failing
  silently).

13 files changed, 663 insertions, 366 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index a75b97b74..27c64e9ef 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -24,7 +24,11 @@ libexpr_la_SOURCES = \
 	command.h \
 	command.cpp
 
-EXTRA_DIST = @srcdir@/kind.h kind_prologue.h kind_middle.h kind_epilogue.h
+EXTRA_DIST = \
+	@srcdir@/kind.h \
+	kind_prologue.h \
+	kind_middle.h \
+	kind_epilogue.h
 
 @srcdir@/kind.h: @srcdir@/mkkind kind_prologue.h kind_middle.h kind_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
 	chmod +x @srcdir@/mkkind
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 5620d7795..4bc569620 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -11,23 +11,6 @@
  ** information.
  **
  ** Node attributes.
- **
- ** Attribute structures:
- **
- ** An attribute structure looks like the following:
- **
- ** struct VarNameAttr {
- **
- **   // the value type for this attribute
- **   typedef std::string value_type;
- **
- **   // an extra hash value (to avoid same-value-type collisions)
- **   enum { hash_value = 1 };
- **
- **   // cleanup routine when the Node goes away
- **   static inline void cleanup(const std::string&) {
- **   }
- ** }
  **/
 
 /* There are strong constraints on ordering of declarations of
@@ -44,7 +27,7 @@
 
 #include "config.h"
 #include "context/context.h"
-#include "expr/soft_node.h"
+#include "expr/node.h"
 #include "expr/type.h"
 
 #include "util/output.h"
@@ -54,81 +37,149 @@ namespace expr {
 
 // ATTRIBUTE HASH FUNCTIONS ====================================================
 
+namespace attr {
+
+/**
+ * A hash function for attribute table keys.  Attribute table keys are
+ * pairs, (unique-attribute-id, Node).
+ */
 struct AttrHashFcn {
-  enum { LARGE_PRIME = 1 };
-  std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const {
+  enum { LARGE_PRIME = 32452843ul };
+  std::size_t operator()(const std::pair<uint64_t, TNode>& p) const {
     return p.first * LARGE_PRIME + p.second.hash();
   }
 };
 
+/**
+ * A hash function for boolean-valued attribute table keys; here we
+ * don't have to store a pair as the key, because we use a known bit
+ * in [0..63] for each attribute
+ */
 struct AttrHashBoolFcn {
-  std::size_t operator()(const SoftNode& n) const {
+  std::size_t operator()(TNode n) const {
     return n.hash();
   }
 };
 
+}/* CVC4::expr::attr namespace */
+
 // ATTRIBUTE TYPE MAPPINGS =====================================================
 
+namespace attr {
+
+/**
+ * KindValueToTableValueMapping is a compile-time-only mechanism to
+ * convert "attribute value types" into "table value types" and back
+ * again.
+ *
+ * Each instantiation <T> is expected to have three members:
+ *
+ *   typename table_value_type
+ *
+ *      A type representing the underlying table's value_type for
+ *      attribute value type (T).  It may be different from T, e.g. T
+ *      could be a pointer-to-Foo, but the underlying table value_type
+ *      might be pointer-to-void.
+ *
+ *   static [convertible-to-table_value_type] convert([convertible-from-T])
+ *
+ *      Converts a T into a table_value_type.  Used to convert an
+ *      attribute value on setting it (and assigning it into the
+ *      underlying table).  See notes on specializations of
+ *      KindValueToTableValueMapping, below.
+ *
+ *   static [convertible-to-T] convertBack([convertible-from-table_value_type])
+ *
+ *      Converts a table_value_type back into a T.  Used to convert an
+ *      underlying table value back into the attribute's expected type
+ *      when retrieving it from the table.  See notes on
+ *      specializations of KindValueToTableValueMapping, below.
+ *
+ * This general (non-specialized) implementation of the template does
+ * nothing.
+ */
 template <class T>
 struct KindValueToTableValueMapping {
+  /** Simple case: T == table_value_type */
   typedef T table_value_type;
+  /** No conversion necessary */
   inline static T convert(const T& t) { return t; }
+  /** No conversion necessary */
   inline static T convertBack(const T& t) { return t; }
 };
 
-template <>
-struct KindValueToTableValueMapping<bool> {
-  typedef uint64_t table_value_type;
-  inline static uint64_t convert(const bool& t) { return t; }
-  inline static bool convertBack(const uint64_t& t) { return t; }
-};
-
+/**
+ * Specialization of KindValueToTableValueMapping<> for pointer-valued
+ * attributes.
+ */
 template <class T>
 struct KindValueToTableValueMapping<T*> {
+  /** Table's value type is void* */
   typedef void* table_value_type;
+  /** A simple reinterpret_cast<>() conversion from T* to void* */
   inline static void* convert(const T* const& t) {
     return reinterpret_cast<void*>(const_cast<T*>(t));
   }
+  /** A simple reinterpret_cast<>() conversion from void* to T* */
   inline static T* convertBack(void* const& t) {
     return reinterpret_cast<T*>(t);
   }
 };
 
+/**
+ * Specialization of KindValueToTableValueMapping<> for const
+ * pointer-valued attributes.
+ */
 template <class T>
 struct KindValueToTableValueMapping<const T*> {
+  /** Table's value type is void* */
   typedef void* table_value_type;
+  /** A simple reinterpret_cast<>() conversion from const T* const to void* */
   inline static void* convert(const T* const& t) {
     return reinterpret_cast<void*>(const_cast<T*>(t));
   }
+  /** A simple reinterpret_cast<>() conversion from const void* const to T* */
   inline static const T* convertBack(const void* const& t) {
     return reinterpret_cast<const T*>(t);
   }
 };
 
-template <class AttrKind, class T>
-struct OwnTable;
-
-template <class AttrKind, class T>
-struct KindValueToTableValueMapping<OwnTable<AttrKind, T> > {
-  typedef typename KindValueToTableValueMapping<T>::table_value_type table_value_type;
-};
-
-template <class AttrKind>
-struct KindTableMapping {
-  typedef typename AttrKind::value_type table_identifier;
-};
+}/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE HASH TABLES =======================================================
 
-// use a TAG to indicate which table it should be in
+namespace attr {
+
+/**
+ * An "AttrHash<value_type>"---the hash table underlying
+ * attributes---is simply a mapping of pair<unique-attribute-id, Node>
+ * to value_type using our specialized hash function for these pairs.
+ */
 template <class value_type>
-struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {};
+struct AttrHash :
+    public __gnu_cxx::hash_map<std::pair<uint64_t, TNode>,
+                               value_type,
+                               AttrHashFcn> {
+};
 
+/**
+ * In the case of Boolean-valued attributes we have a special
+ * "AttrHash<bool>" to pack bits together in words.
+ */
 template <>
-class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> {
-
-  typedef __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> super;
-
+class AttrHash<bool> :
+    protected __gnu_cxx::hash_map<TNode,
+                                  uint64_t,
+                                  AttrHashBoolFcn> {
+
+  /** A "super" type, like in Java, for easy reference below. */
+  typedef __gnu_cxx::hash_map<TNode, uint64_t, AttrHashBoolFcn> super;
+
+  /**
+   * BitAccessor allows us to return a bit "by reference."  Of course,
+   * we don't require bit-addressibility supported by the system, we
+   * do it with a complex type.
+   */
   class BitAccessor {
 
     uint64_t& d_word;
@@ -159,9 +210,15 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas
     }
   };
 
+  /**
+   * A (somewhat degenerate) iterator over boolean-valued attributes.
+   * This iterator doesn't support anything except comparison and
+   * dereference.  It's intended just for the result of find() on the
+   * table.
+   */
   class BitIterator {
 
-    std::pair<const SoftNode, uint64_t>* d_entry;
+    std::pair<const TNode, uint64_t>* d_entry;
 
     unsigned d_bit;
 
@@ -172,12 +229,12 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas
       d_bit(0) {
     }
 
-    BitIterator(std::pair<const SoftNode, uint64_t>& entry, unsigned bit) :
+    BitIterator(std::pair<const TNode, uint64_t>& entry, unsigned bit) :
       d_entry(&entry),
       d_bit(bit) {
     }
 
-    std::pair<const SoftNode, BitAccessor> operator*() {
+    std::pair<const TNode, BitAccessor> operator*() {
       return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit));
     }
 
@@ -186,9 +243,15 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas
     }
   };
 
+  /**
+   * A (somewhat degenerate) const_iterator over boolean-valued
+   * attributes.  This const_iterator doesn't support anything except
+   * comparison and dereference.  It's intended just for the result of
+   * find() on the table.
+   */
   class ConstBitIterator {
 
-    const std::pair<const SoftNode, uint64_t>* d_entry;
+    const std::pair<const TNode, uint64_t>* d_entry;
 
     unsigned d_bit;
 
@@ -199,12 +262,12 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas
       d_bit(0) {
     }
 
-    ConstBitIterator(const std::pair<const SoftNode, uint64_t>& entry, unsigned bit) :
+    ConstBitIterator(const std::pair<const TNode, uint64_t>& entry, unsigned bit) :
       d_entry(&entry),
       d_bit(bit) {
     }
 
-    std::pair<const SoftNode, bool> operator*() {
+    std::pair<const TNode, bool> operator*() {
       return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false);
     }
 
@@ -215,14 +278,20 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas
 
 public:
 
-  typedef std::pair<uint64_t, SoftNode> key_type;
+  typedef std::pair<uint64_t, TNode> key_type;
   typedef bool data_type;
   typedef std::pair<const key_type, data_type> value_type;
 
+  /** an iterator type; see above for limitations */
   typedef BitIterator iterator;
+  /** a const_iterator type; see above for limitations */
   typedef ConstBitIterator const_iterator;
 
-  BitIterator find(const std::pair<uint64_t, SoftNode>& k) {
+  /**
+   * Find the boolean value in the hash table.  Returns something ==
+   * end() if not found.
+   */
+  BitIterator find(const std::pair<uint64_t, TNode>& k) {
     super::iterator i = super::find(k.second);
     if(i == super::end()) {
       return BitIterator();
@@ -235,11 +304,16 @@ public:
     return BitIterator(*i, k.first);
   }
 
+  /** The "off the end" iterator */
   BitIterator end() {
     return BitIterator();
   }
 
-  ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const {
+  /**
+   * Find the boolean value in the hash table.  Returns something ==
+   * end() if not found.
+   */
+  ConstBitIterator find(const std::pair<uint64_t, TNode>& k) const {
     super::const_iterator i = super::find(k.second);
     if(i == super::end()) {
       return ConstBitIterator();
@@ -252,154 +326,301 @@ public:
     return ConstBitIterator(*i, k.first);
   }
 
+  /** The "off the end" const_iterator */
   ConstBitIterator end() const {
     return ConstBitIterator();
   }
 
-  BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) {
+  /**
+   * Access the hash table using the underlying operator[].  Inserts
+   * the key into the table (associated to default value) if it's not
+   * already there.
+   */
+  BitAccessor operator[](const std::pair<uint64_t, TNode>& k) {
     uint64_t& word = super::operator[](k.second);
     return BitAccessor(word, k.first);
   }
 };/* class AttrHash<bool> */
 
-// ATTRIBUTE PATTERN ===========================================================
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE CLEANUP FUNCTIONS =================================================
+
+namespace attr {
+
+/** Default cleanup for unmanaged Attribute<> */
+template <class T>
+struct AttributeCleanupFcn {
+  inline void cleanup(const T&) {}
+};
+
+/** Default cleanup for ManagedAttribute<> */
+template <class T>
+struct ManagedAttributeCleanupFcn {
+};
+
+/** Specialization for T* */
+template <class T>
+struct ManagedAttributeCleanupFcn<T*> {
+  inline void cleanup(T* p) { delete p; }
+};
+
+/** Specialization for const T* */
+template <class T>
+struct ManagedAttributeCleanupFcn<const T*> {
+  inline void cleanup(const T* p) { delete p; }
+};
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE DEFINITION ========================================================
 
 /**
  * An "attribute type" structure.
+ *
+ * @param T the tag for the attribute kind.
+ *
+ * @param value_t the underlying value_type for the attribute kind
+ *
+ * @param CleanupFcn Clean-up routine for associated values when the
+ * Node goes away.  Useful, e.g., for pointer-valued attributes when
+ * the values are "owned" by the table.
+ *
+ * @param context_dependent whether this attribute kind is
+ * context-dependent
  */
-template <class T, class value_t>
+template <class T,
+          class value_t,
+          class CleanupFcn = attr::AttributeCleanupFcn<value_t>,
+          bool context_dependent = false>
 struct Attribute {
 
-  /** the value type for this attribute */
+  /** The value type for this attribute. */
   typedef value_t value_type;
 
-  /** cleanup routine when the Node goes away */
-  static inline void cleanup(const value_t&) {}
-
+  /** Get the unique ID associated to this attribute. */
   static inline uint64_t getId() { return s_id; }
-  static inline uint64_t getHashValue() { return s_hashValue; }
 
+  /**
+   * This attribute does not have a default value: calling
+   * hasAttribute() for a Node that hasn't had this attribute set will
+   * return false, and getAttribute() for the Node will return a
+   * default-constructed value_type.
+   */
   static const bool has_default_value = false;
 
 private:
 
-  /** an id */
+  /**
+   * The unique ID associated to this attribute.  Assigned statically,
+   * at load time.
+   */
   static const uint64_t s_id;
-
-  /** an extra hash value (to avoid same-value-type collisions) */
-  static const uint64_t s_hashValue;
 };
 
 /**
  * An "attribute type" structure for boolean flags (special).
  */
-template <class T>
-struct Attribute<T, bool> {
+template <class T, class CleanupFcn, bool context_dependent>
+struct Attribute<T, bool, CleanupFcn, context_dependent> {
 
-  /** the value type for this attribute */
+  /** The value type for this attribute; here, bool. */
   typedef bool value_type;
 
-  /** cleanup routine when the Node goes away */
-  static inline void cleanup(const bool&) {}
-
+  /** Get the unique ID associated to this attribute. */
   static inline uint64_t getId() { return s_id; }
-  static inline uint64_t getHashValue() { return s_hashValue; }
 
+  /**
+   * Such bool-valued attributes ("flags") have a default value: they
+   * are false for all nodes on entry.  Calling hasAttribute() for a
+   * Node that hasn't had this attribute set will return true, and
+   * getAttribute() for the Node will return the default_value below.
+   */
   static const bool has_default_value = true;
+
+  /**
+   * Default value of the attribute for Nodes without one explicitly
+   * set.
+   */
   static const bool default_value = false;
 
+  /**
+   * Check that the ID is a valid ID for bool-valued attributes.  Fail
+   * an assert if not.  Otherwise return the id.
+   */
   static inline uint64_t checkID(uint64_t id) {
-    AlwaysAssert(id <= 63,
-                 "Too many boolean node attributes registered during initialization !");
+    AlwaysAssert( id <= 63,
+                  "Too many boolean node attributes registered "
+                  "during initialization !" );
     return id;
   }
 
 private:
 
-  /** a bit assignment */
+  /** IDs for bool-valued attributes are actually bit assignments. */
   static const uint64_t s_id;
-
-  /** an extra hash value (to avoid same-value-type collisions) */
-  static const uint64_t s_hashValue;
 };
 
-// SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ======================================
-
-namespace attr {
-  struct VarName {};
-  struct Type {};
-
-  template <class T>
-  struct LastAttributeId {
-    static uint64_t s_id;
-  };
-
-  template <class T>
-  uint64_t LastAttributeId<T>::s_id = 0;
-}/* CVC4::expr::attr namespace */
+// FIXME make context-dependent
+template <class T,
+          class value_type>
+struct CDAttribute :
+    public Attribute<T, value_type, attr::AttributeCleanupFcn<value_type>, true> {};
 
-typedef Attribute<attr::VarName, std::string> VarNameAttr;
-typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
+// FIXME make context-dependent
+template <class T,
+          class value_type,
+          class CleanupFcn = attr::ManagedAttributeCleanupFcn<value_type> >
+struct ManagedAttribute :
+    public Attribute<T, value_type, CleanupFcn, false> {};
 
 // ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
 
-template <class T, class value_t>
-const uint64_t Attribute<T, value_t>::s_id =
-  attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
-template <class T, class value_t>
-const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
+namespace attr {
 
+/**
+ * This is the last-attribute-assigner.  IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
 template <class T>
-const uint64_t Attribute<T, bool>::s_id =
-  Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++);
+struct LastAttributeId {
+  static uint64_t s_id;
+};
+
+/** Initially zero. */
 template <class T>
-const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
+uint64_t LastAttributeId<T>::s_id = 0;
 
-class AttributeManager;
+}/* CVC4::expr::attr namespace */
 
-template <class T>
-struct getTable {
-  //inline AttrHash<KindTableValueMapping<T> >& get(AttributeManager& am);
-};
+/** Assign unique IDs to attributes at load time. */
+template <class T, class value_t, class CleanupFcn, bool context_dependent>
+const uint64_t Attribute<T, value_t, CleanupFcn, context_dependent>::s_id =
+  attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
+
+/**
+ * Assign unique IDs to bool-valued attributes at load time, checking
+ * that they are in range.
+ */
+template <class T, class CleanupFcn, bool context_dependent>
+const uint64_t Attribute<T, bool, CleanupFcn, context_dependent>::s_id =
+  Attribute<T, bool, CleanupFcn, context_dependent>::checkID(attr::LastAttributeId<bool>::s_id++);
 
 // ATTRIBUTE MANAGER ===========================================================
 
+namespace attr {
+
+/**
+ * A container for the main attribute tables of the system.  There's a
+ * one-to-one NodeManager : AttributeManager correspondence.
+ */
 class AttributeManager {
-  NodeManager* d_nm;
 
-  AttrHash<bool>    d_bools;
+  /** Underlying hash table for boolean-valued attributes */
+  AttrHash<bool>        d_bools;
+  /** Underlying hash table for integral-valued attributes */
   AttrHash<uint64_t>    d_ints;
-  AttrHash<SoftNode>    d_exprs;
+  /** Underlying hash table for node-valued attributes */
+  AttrHash<TNode>       d_exprs;
+  /** Underlying hash table for string-valued attributes */
   AttrHash<std::string> d_strings;
+  /** Underlying hash table for pointer-valued attributes */
   AttrHash<void*>       d_ptrs;
 
+  /**
+   * getTable<> is a helper template that gets the right table from an
+   * AttributeManager given its type.
+   */
   template <class T>
   friend struct getTable;
 
 public:
-  AttributeManager(NodeManager* nm) : d_nm(nm) {}
 
+  /** Construct an attribute manager. */
+  AttributeManager() {}
+
+  /**
+   * Get a particular attribute on a particular node.
+   *
+   * @param n the node about which to inquire
+   *
+   * @param const AttrKind& the attribute kind to get
+   *
+   * @return the attribute value, if set, or a default-constructed
+   * AttrKind::value_type if not.
+   */
   template <class AttrKind>
-  typename AttrKind::value_type getAttribute(const Node& n,
+  typename AttrKind::value_type getAttribute(TNode n,
                                              const AttrKind&) const;
 
+  // Note that there are two, distinct hasAttribute() declarations for
+  // a reason (rather than using a default argument): they permit more
+  // optimized code.  The first (without parameter "ret") need never
+  // check whether its parameter is NULL.
+
+  /**
+   * Determine if a particular attribute exists for a particular node.
+   *
+   * @param n the node about which to inquire
+   *
+   * @param const AttrKind& the attribute kind to inquire about
+   *
+   * @return true if the given node has the given attribute
+   */
   template <class AttrKind>
-  bool hasAttribute(const Node& n,
+  bool hasAttribute(TNode n,
                     const AttrKind&) const;
 
+  /**
+   * Determine if a particular attribute exists for a particular node,
+   * and get it if it does.
+   *
+   * @param n the node about which to inquire
+   *
+   * @param const AttrKind& the attribute kind to inquire about
+   *
+   * @param ret a pointer to a return value, set in case the node has
+   * the attribute
+   *
+   * @return true if the given node has the given attribute
+   */
   template <class AttrKind>
-  bool hasAttribute(const Node& n,
+  bool hasAttribute(TNode n,
                     const AttrKind&,
-                    typename AttrKind::value_type*) const;
-
+                    typename AttrKind::value_type& ret) const;
+
+  /**
+   * Set a particular attribute on a particular node.
+   *
+   * @param n the node for which to set the attribute
+   *
+   * @param const AttrKind& the attribute kind to set
+   *
+   * @param ret a pointer to a return value, set in case the node has
+   * the attribute
+   *
+   * @return true if the given node has the given attribute
+   */
   template <class AttrKind>
-  void setAttribute(const Node& n,
+  void setAttribute(TNode n,
                     const AttrKind&,
                     const typename AttrKind::value_type& value);
 };
 
+}/* CVC4::expr::attr namespace */
+
 // MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
 
+namespace attr {
+
+/**
+ * The getTable<> template provides (static) access to the
+ * AttributeManager field holding the table.
+ */
+template <class T>
+struct getTable;
+
+/** Access the "d_bools" member of AttributeManager. */
 template <>
 struct getTable<bool> {
   typedef AttrHash<bool> table_type;
@@ -411,6 +632,7 @@ struct getTable<bool> {
   }
 };
 
+/** Access the "d_ints" member of AttributeManager. */
 template <>
 struct getTable<uint64_t> {
   typedef AttrHash<uint64_t> table_type;
@@ -422,9 +644,10 @@ struct getTable<uint64_t> {
   }
 };
 
+/** Access the "d_exprs" member of AttributeManager. */
 template <>
 struct getTable<Node> {
-  typedef AttrHash<SoftNode> table_type;
+  typedef AttrHash<TNode> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_exprs;
   }
@@ -433,6 +656,7 @@ struct getTable<Node> {
   }
 };
 
+/** Access the "d_strings" member of AttributeManager. */
 template <>
 struct getTable<std::string> {
   typedef AttrHash<std::string> table_type;
@@ -444,8 +668,9 @@ struct getTable<std::string> {
   }
 };
 
+/** Access the "d_ptrs" member of AttributeManager. */
 template <class T>
-struct getTable<const T*> {
+struct getTable<T*> {
   typedef AttrHash<void*> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_ptrs;
@@ -455,8 +680,9 @@ struct getTable<const T*> {
   }
 };
 
+/** Access the "d_ptrs" member of AttributeManager. */
 template <class T>
-struct getTable<T*> {
+struct getTable<const T*> {
   typedef AttrHash<void*> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_ptrs;
@@ -466,10 +692,15 @@ struct getTable<T*> {
   }
 };
 
+}/* CVC4::expr::attr namespace */
+
 // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
 
+namespace attr {
+
+// implementation for AttributeManager::getAttribute()
 template <class AttrKind>
-typename AttrKind::value_type AttributeManager::getAttribute(const Node& n,
+typename AttrKind::value_type AttributeManager::getAttribute(TNode n,
                                                              const AttrKind&) const {
 
   typedef typename AttrKind::value_type value_type;
@@ -486,45 +717,56 @@ typename AttrKind::value_type AttributeManager::getAttribute(const Node& n,
   return mapping::convertBack((*i).second);
 }
 
-/* helper template class for hasAttribute(), specialized based on
+/* Helper template class for hasAttribute(), specialized based on
  * whether AttrKind has a "default value" that all Nodes implicitly
  * have or not. */
 template <bool has_default, class AttrKind>
 struct HasAttribute;
 
+/**
+ * Specialization of HasAttribute<> helper template for AttrKinds
+ * with a default value.
+ */
 template <class AttrKind>
 struct HasAttribute<true, AttrKind> {
+  /** This implementation is simple; it's always true. */
   static inline bool hasAttribute(const AttributeManager* am,
-                                  const Node& n) {
+                                  TNode n) {
     return true;
   }
 
+  /**
+   * This implementation returns the AttrKind's default value if the
+   * Node doesn't have the given attribute.
+   */
   static inline bool hasAttribute(const AttributeManager* am,
-                                  const Node& n,
-                                  typename AttrKind::value_type* ret) {
-    if(ret != NULL) {
-      typedef typename AttrKind::value_type value_type;
-      typedef KindValueToTableValueMapping<value_type> mapping;
-      typedef typename getTable<value_type>::table_type table_type;
-
-      const table_type& ah = getTable<value_type>::get(*am);
-      typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
-
-      if(i == ah.end()) {
-        *ret = AttrKind::default_value;
-      } else {
-        *ret = mapping::convertBack((*i).second);
-      }
+                                  TNode n,
+                                  typename AttrKind::value_type& ret) {
+    typedef typename AttrKind::value_type value_type;
+    typedef KindValueToTableValueMapping<value_type> mapping;
+    typedef typename getTable<value_type>::table_type table_type;
+
+    const table_type& ah = getTable<value_type>::get(*am);
+    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
+
+    if(i == ah.end()) {
+      ret = AttrKind::default_value;
+    } else {
+      ret = mapping::convertBack((*i).second);
     }
 
     return true;
   }
 };
 
+/**
+ * Specialization of HasAttribute<> helper template for AttrKinds
+ * without a default value.
+ */
 template <class AttrKind>
 struct HasAttribute<false, AttrKind> {
   static inline bool hasAttribute(const AttributeManager* am,
-                                  const Node& n) {
+                                  TNode n) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
     typedef typename getTable<value_type>::table_type table_type;
@@ -540,8 +782,8 @@ struct HasAttribute<false, AttrKind> {
   }
 
   static inline bool hasAttribute(const AttributeManager* am,
-                                  const Node& n,
-                                  typename AttrKind::value_type* ret) {
+                                  TNode n,
+                                  typename AttrKind::value_type& ret) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
     typedef typename getTable<value_type>::table_type table_type;
@@ -553,29 +795,27 @@ struct HasAttribute<false, AttrKind> {
       return false;
     }
 
-    if(ret != NULL) {
-      *ret = mapping::convertBack((*i).second);
-    }
+    ret = mapping::convertBack((*i).second);
 
     return true;
   }
 };
 
 template <class AttrKind>
-bool AttributeManager::hasAttribute(const Node& n,
+bool AttributeManager::hasAttribute(TNode n,
                                     const AttrKind&) const {
   return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n);
 }
 
 template <class AttrKind>
-bool AttributeManager::hasAttribute(const Node& n,
+bool AttributeManager::hasAttribute(TNode n,
                                     const AttrKind&,
-                                    typename AttrKind::value_type* ret) const {
+                                    typename AttrKind::value_type& ret) const {
   return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n, ret);
 }
 
 template <class AttrKind>
-inline void AttributeManager::setAttribute(const Node& n,
+inline void AttributeManager::setAttribute(TNode n,
                                            const AttrKind&,
                                            const typename AttrKind::value_type& value) {
 
@@ -587,6 +827,7 @@ inline void AttributeManager::setAttribute(const Node& n,
   ah[std::make_pair(AttrKind::getId(), n)] = mapping::convert(value);
 }
 
+}/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
 
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 7dc8c8f96..35bdc947a 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -19,6 +19,8 @@
 
 #include "util/output.h"
 
+using namespace CVC4::kind;
+
 namespace CVC4 {
 
 std::ostream& operator<<(std::ostream& out, const Expr& e) {
diff --git a/src/expr/kind_middle.h b/src/expr/kind_middle.h
index 49e43ba68..a4ba5a92b 100644
--- a/src/expr/kind_middle.h
+++ b/src/expr/kind_middle.h
@@ -16,11 +16,17 @@
 
   LAST_KIND
 
-};/* enum Kind */
+};/* enum Kind_t */
+
+}/* CVC4::kind namespace */
+
+// import Kind into the "CVC4" namespace but keep the individual kind
+// constants under kind::
+typedef ::CVC4::kind::Kind_t Kind;
 
 inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
-  using namespace CVC4;
+  using namespace CVC4::kind;
 
   switch(k) {
 
diff --git a/src/expr/kind_prologue.h b/src/expr/kind_prologue.h
index 7f4a0a3a2..08468385b 100644
--- a/src/expr/kind_prologue.h
+++ b/src/expr/kind_prologue.h
@@ -20,8 +20,9 @@
 #include <iostream>
 
 namespace CVC4 {
+namespace kind {
 
-enum Kind {
+enum Kind_t {
   /* undefined */
   UNDEFINED_KIND = -1,
   /** Null Kind */
diff --git a/src/expr/mkkind b/src/expr/mkkind
index b0a8f4565..bc10f1e2c 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -2,6 +2,7 @@
 #
 # mkkind
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010  The CVC4 Project
 #
 # The purpose of this script is to create kind.h from a prologue,
 # middle, epilogue, and a list of theory kinds.
@@ -17,7 +18,7 @@ cat <<EOF
 /*********************                                           -*- C++ -*-  */
 /** kind.h
  **
- ** Copyright 2009, 2010  The AcSys Group, New York University, and as below.
+ ** Copyright 2010  The AcSys Group, New York University, and as below.
  **
  ** This header file automatically generated by:
  **
diff --git a/src/expr/node.h b/src/expr/node.h
index 03f3e9da3..19e50c5c2 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -28,6 +28,8 @@
 #include "expr/type.h"
 #include "util/Assert.h"
 
+#include "util/output.h"
+
 namespace CVC4 {
 
 class Type;
@@ -107,14 +109,22 @@ template<bool ref_count>
     NodeTemplate() : d_nv(&NodeValue::s_null) { }
 
     /**
-     * Copy constructor for nodes that can accept the nodes that are reference
-     * counted or not.
+     * Conversion between nodes that are reference-counted and those that are
+     * not.
      * @param node the node to make copy of
      */
     template<bool ref_count_1>
       NodeTemplate(const NodeTemplate<ref_count_1>& node);
 
     /**
+     * Copy constructor.  Note that GCC does NOT recognize an instantiation of
+     * the above template as a copy constructor and problems ensue.  So we
+     * provide an explicit one here.
+     * @param node the node to make copy of
+     */
+    NodeTemplate(const NodeTemplate<ref_count>& node);
+
+    /**
      * Assignment operator for nodes, copies the relevant information from node
      * to this node.
      * @param node the node to copy
@@ -233,9 +243,24 @@ template<bool ref_count>
      * @param attKind the kind of the attribute
      * @return the value of the attribute
      */
-    template<class AttrKind>
+    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
@@ -244,8 +269,17 @@ template<bool ref_count>
      * @param value where to store the value if it exists
      * @return true if this node has the requested attribute
      */
-    template<class AttrKind>
-      inline bool hasAttribute(const AttrKind& attKind, typename AttrKind::value_type* value = NULL) const;
+    template <class AttrKind>
+      inline bool hasAttribute(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 typename NodeValue::iterator<ref_count> iterator;
@@ -325,15 +359,6 @@ template<bool ref_count>
     NodeTemplate uMinusNode() const;
     NodeTemplate multNode(const NodeTemplate& right) 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);
-
   private:
 
     /**
@@ -343,7 +368,6 @@ template<bool ref_count>
      */
     void debugPrint();
 
-
     /**
      * Indents the given stream a given amount of spaces.
      * @param out the stream to indent
@@ -404,7 +428,17 @@ template<bool ref_count>
 template<bool ref_count>
   template<class AttrKind>
     inline bool NodeTemplate<ref_count>::
-    hasAttribute(const AttrKind&, typename AttrKind::value_type* ret) const {
+    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(*this, AttrKind());
+    }
+
+template<bool ref_count>
+  template<class AttrKind>
+    inline bool NodeTemplate<ref_count>::
+    hasAttribute(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 ?" );
@@ -428,6 +462,7 @@ template<bool ref_count>
 ////TODO: Should use positive definition, i.e. what kinds are atomic.
 template<bool ref_count>
   bool NodeTemplate<ref_count>::isAtomic() const {
+    using namespace kind;
     switch(getKind()) {
     case NOT:
     case XOR:
@@ -454,6 +489,8 @@ template<bool ref_count>
       d_nv->inc();
   }
 
+// the code for these two "conversion/copy constructors" is identical, but
+// apparently we need both.  see comment in the class.
 template<bool ref_count>
   template<bool ref_count_1>
     NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count_1>& e) {
@@ -464,6 +501,14 @@ template<bool ref_count>
     }
 
 template<bool ref_count>
+  NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count>& e) {
+    Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
+    d_nv = e.d_nv;
+    if(ref_count)
+      d_nv->inc();
+  }
+
+template<bool ref_count>
   NodeTemplate<ref_count>::~NodeTemplate() {
     Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
     if(ref_count)
@@ -498,48 +543,48 @@ template<bool ref_count>
 template<bool ref_count>
   NodeTemplate<ref_count> NodeTemplate<ref_count>::eqNode(const NodeTemplate<
       ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
+    return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
   }
 
 template<bool ref_count>
   NodeTemplate<ref_count> NodeTemplate<ref_count>::notNode() const {
-    return NodeManager::currentNM()->mkNode(NOT, *this);
+    return NodeManager::currentNM()->mkNode(kind::NOT, *this);
   }
 
 template<bool ref_count>
   NodeTemplate<ref_count> NodeTemplate<ref_count>::andNode(const NodeTemplate<
       ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(AND, *this, right);
+    return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
   }
 
 template<bool ref_count>
   NodeTemplate<ref_count> NodeTemplate<ref_count>::orNode(const NodeTemplate<
       ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(OR, *this, right);
+    return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
   }
 
 template<bool ref_count>
   NodeTemplate<ref_count> NodeTemplate<ref_count>::iteNode(const NodeTemplate<
       ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const {
-    return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
+    return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
   }
 
 template<bool ref_count>
   NodeTemplate<ref_count> NodeTemplate<ref_count>::iffNode(const NodeTemplate<
       ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(IFF, *this, right);
+    return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
   }
 
 template<bool ref_count>
   NodeTemplate<ref_count> NodeTemplate<ref_count>::impNode(const NodeTemplate<
       ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
+    return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
   }
 
 template<bool ref_count>
   NodeTemplate<ref_count> NodeTemplate<ref_count>::xorNode(const NodeTemplate<
       ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(XOR, *this, right);
+    return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
   }
 
 template<bool ref_count>
@@ -547,7 +592,7 @@ template<bool ref_count>
     indent(out, ind);
     out << '(';
     out << getKind();
-    if(getKind() == VARIABLE) {
+    if(getKind() == kind::VARIABLE) {
       out << ' ' << getId();
 
     } else if(getNumChildren() >= 1) {
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index cd34c415b..0b89fcb5e 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -13,6 +13,9 @@
  ** A builder interface for nodes.
  **/
 
+/* strong dependency; make sure node is included first */
+#include "node.h"
+
 #ifndef __CVC4__NODE_BUILDER_H
 #define __CVC4__NODE_BUILDER_H
 
@@ -145,42 +148,42 @@ public:
     return Node(d_nv->d_children[i]);
   }
 
-  void clear(Kind k = UNDEFINED_KIND);
+  void clear(Kind k = kind::UNDEFINED_KIND);
 
   // Compound expression constructors
   /*
-  NodeBuilder& eqExpr(const Node& right);
+  NodeBuilder& eqExpr(TNode right);
   NodeBuilder& notExpr();
-  NodeBuilder& andExpr(const Node& right);
-  NodeBuilder& orExpr(const Node& right);
-  NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart);
-  NodeBuilder& iffExpr(const Node& right);
-  NodeBuilder& impExpr(const Node& right);
-  NodeBuilder& xorExpr(const Node& right);
+  NodeBuilder& andExpr(TNode right);
+  NodeBuilder& orExpr(TNode right);
+  NodeBuilder& iteExpr(TNode thenpart, TNode elsepart);
+  NodeBuilder& iffExpr(TNode right);
+  NodeBuilder& impExpr(TNode right);
+  NodeBuilder& xorExpr(TNode right);
   */
 
   /* TODO design: these modify NodeBuilder ?? */
   /*
   NodeBuilder& operator!() { return notExpr(); }
-  NodeBuilder& operator&&(const Node& right) { return andExpr(right); }
-  NodeBuilder& operator||(const Node& right) { return orExpr(right);  }
+  NodeBuilder& operator&&(TNode right) { return andExpr(right); }
+  NodeBuilder& operator||(TNode right) { return orExpr(right);  }
   */
 
   /*
-  NodeBuilder& operator&&=(const Node& right) { return andExpr(right); }
-  NodeBuilder& operator||=(const Node& right) { return orExpr(right);  }
+  NodeBuilder& operator&&=(TNode right) { return andExpr(right); }
+  NodeBuilder& operator||=(TNode right) { return orExpr(right);  }
   */
 
   // "Stream" expression constructor syntax
 
   NodeBuilder& operator<<(const Kind& k) {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    Assert(d_nv->getKind() == UNDEFINED_KIND);
+    Assert(d_nv->getKind() == kind::UNDEFINED_KIND);
     d_nv->d_kind = k;
     return *this;
   }
 
-  NodeBuilder& operator<<(const Node& n) {
+  NodeBuilder& operator<<(TNode n) {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
     return append(n);
   }
@@ -191,7 +194,7 @@ public:
     return append(children.begin(), children.end());
   }
 
-  NodeBuilder& append(const Node& n) {
+  NodeBuilder& append(TNode n) {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
     Debug("prop") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl;
     allocateEvIfNecessaryForAppend();
@@ -466,7 +469,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
   d_nv(&d_inlineNv),
   d_inlineNv(0),
   d_childrenStorage() {
-  d_inlineNv.d_kind = UNDEFINED_KIND;
+  d_inlineNv.d_kind = NodeValue::kindToDKind(kind::UNDEFINED_KIND);
 }
 
 template <unsigned nchild_thresh>
@@ -573,16 +576,16 @@ inline void NodeBuilder<nchild_thresh>::dealloc() {
 template <unsigned nchild_thresh>
 NodeBuilder<nchild_thresh>::operator Node() {// not const
   Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-  Assert(d_nv->getKind() != UNDEFINED_KIND,
+  Assert(d_nv->getKind() != kind::UNDEFINED_KIND,
          "Can't make an expression of an undefined kind!");
 
-  if(d_nv->d_kind == VARIABLE) {
+  if(d_nv->d_kind == kind::VARIABLE) {
     Assert(d_nv->d_nchildren == 0);
     NodeValue *nv = (NodeValue*)
       std::malloc(sizeof(NodeValue) +
                   ( sizeof(NodeValue*) * d_inlineNv.d_nchildren ));
     nv->d_nchildren = 0;
-    nv->d_kind = VARIABLE;
+    nv->d_kind = kind::VARIABLE;
     nv->d_id = NodeValue::next_id++;// FIXME multithreading
     nv->d_rc = 0;
     d_used = true;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 556b577e5..b11361827 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -13,11 +13,7 @@
  ** Expression manager implementation.
  **/
 
-#include "node_builder.h"
 #include "node_manager.h"
-#include "expr/node.h"
-#include "expr/attribute.h"
-#include "util/output.h"
 
 using namespace std;
 using namespace CVC4::expr;
@@ -28,64 +24,11 @@ __thread NodeManager* NodeManager::s_current = 0;
 
 NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
   NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
-  if (find == d_nodeValueSet.end()) {
+  if(find == d_nodeValueSet.end()) {
     return NULL;
   } else {
     return *find;
   }
 }
 
-void NodeManager::poolInsert(NodeValue* nv) {
-  Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in"
-         "the pool!");
-  d_nodeValueSet.insert(nv);
-}
-
-// general expression-builders
-
-Node NodeManager::mkNode(Kind kind) {
-  return NodeBuilder<>(this, kind);
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1) {
-  return NodeBuilder<>(this, kind) << child1;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2) {
-  return NodeBuilder<>(this, kind) << child1 << child2;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
-  return NodeBuilder<>(this, kind) << child1 << child2 << child3;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
-  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
-  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
-}
-
-// N-ary version
-Node NodeManager::mkNode(Kind kind, const vector<Node>& children) {
-  return NodeBuilder<>(this, kind).append(children);
-}
-
-Node NodeManager::mkVar(const Type* type, const std::string& name) {
-  Node n = mkVar(type);
-  n.setAttribute(VarNameAttr(), name);
-  return n;
-}
-
-Node NodeManager::mkVar(const Type* type) {
-  Node n = NodeBuilder<>(this, VARIABLE);
-  n.setAttribute(TypeAttr(), type);
-  return n;
-}
-
-Node NodeManager::mkVar() {
-  return NodeBuilder<>(this, VARIABLE);
-}
-
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1c46743e9..bcb5f6d47 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -40,6 +40,19 @@ namespace CVC4 {
 
 class Type;
 
+namespace expr {
+namespace attr {
+
+struct VarName {};
+struct Type {};
+
+}/* CVC4::expr::attr namespace */
+
+typedef Attribute<attr::VarName, std::string> VarNameAttr;
+typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
+
+}/* CVC4::expr namespace */
+
 class NodeManager {
   static __thread NodeManager* s_current;
 
@@ -48,7 +61,7 @@ class NodeManager {
   typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet;
   NodeValueSet d_nodeValueSet;
 
-  expr::AttributeManager d_attrManager;
+  expr::attr::AttributeManager d_attrManager;
 
   NodeValue* poolLookup(NodeValue* nv) const;
   void poolInsert(NodeValue* nv);
@@ -57,7 +70,7 @@ class NodeManager {
 
 public:
 
-  NodeManager() : d_attrManager(this) {
+  NodeManager() {
     poolInsert( &NodeValue::s_null );
   }
 
@@ -65,11 +78,11 @@ public:
 
   // general expression-builders
   Node mkNode(Kind kind);
-  Node mkNode(Kind kind, const Node& child1);
-  Node mkNode(Kind kind, const Node& child1, const Node& child2);
-  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3);
-  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
-  Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
+  Node mkNode(Kind kind, TNode child1);
+  Node mkNode(Kind kind, TNode child1, TNode child2);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5);
   // N-ary version
   Node mkNode(Kind kind, const std::vector<Node>& children);
 
@@ -79,20 +92,29 @@ public:
   Node mkVar();
 
   template <class AttrKind>
-  inline typename AttrKind::value_type getAttribute(const Node& n,
+  inline typename AttrKind::value_type getAttribute(TNode n,
                                                     const AttrKind&) 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.
+
+  template <class AttrKind>
+  inline bool hasAttribute(TNode n,
+                           const AttrKind&) const;
+
   template <class AttrKind>
-  inline bool hasAttribute(const Node& n,
+  inline bool hasAttribute(TNode n,
                            const AttrKind&,
-                           typename AttrKind::value_type* = NULL) const;
+                           typename AttrKind::value_type&) const;
 
   template <class AttrKind>
-  inline void setAttribute(const Node& n,
+  inline void setAttribute(TNode n,
                            const AttrKind&,
                            const typename AttrKind::value_type& value);
 
-  inline const Type* getType(const Node& n);
+  inline const Type* getType(TNode n);
 };
 
 class NodeManagerScope {
@@ -112,29 +134,94 @@ public:
 };
 
 template <class AttrKind>
-inline typename AttrKind::value_type NodeManager::getAttribute(const Node& n,
+inline typename AttrKind::value_type NodeManager::getAttribute(TNode n,
                                                                const AttrKind&) const {
   return d_attrManager.getAttribute(n, AttrKind());
 }
 
 template <class AttrKind>
-inline bool NodeManager::hasAttribute(const Node& n,
+inline bool NodeManager::hasAttribute(TNode n,
+                                      const AttrKind&) const {
+  return d_attrManager.hasAttribute(n, AttrKind());
+}
+
+template <class AttrKind>
+inline bool NodeManager::hasAttribute(TNode n,
                                       const AttrKind&,
-                                      typename AttrKind::value_type* ret) const {
+                                      typename AttrKind::value_type& ret) const {
   return d_attrManager.hasAttribute(n, AttrKind(), ret);
 }
 
 template <class AttrKind>
-inline void NodeManager::setAttribute(const Node& n,
+inline void NodeManager::setAttribute(TNode n,
                                       const AttrKind&,
                                       const typename AttrKind::value_type& value) {
   d_attrManager.setAttribute(n, AttrKind(), value);
 }
 
-inline const Type* NodeManager::getType(const Node& n) {
+inline const Type* NodeManager::getType(TNode n) {
   return getAttribute(n,CVC4::expr::TypeAttr());
 }
 
+inline void NodeManager::poolInsert(NodeValue* nv) {
+  Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in"
+         "the pool!");
+  d_nodeValueSet.insert(nv);
+}
+
+}/* CVC4 namespace */
+
+#include "expr/node_builder.h"
+
+namespace CVC4 {
+
+// general expression-builders
+
+inline Node NodeManager::mkNode(Kind kind) {
+  return NodeBuilder<>(this, kind);
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1) {
+  return NodeBuilder<>(this, kind) << child1;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
+  return NodeBuilder<>(this, kind) << child1 << child2;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) {
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) {
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
+}
+
+inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) {
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
+}
+
+// N-ary version
+inline Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
+  return NodeBuilder<>(this, kind).append(children);
+}
+
+inline Node NodeManager::mkVar(const Type* type, const std::string& name) {
+  Node n = mkVar(type);
+  n.setAttribute(expr::VarNameAttr(), name);
+  return n;
+}
+
+inline Node NodeManager::mkVar(const Type* type) {
+  Node n = NodeBuilder<>(this, kind::VARIABLE);
+  n.setAttribute(expr::TypeAttr(), type);
+  return n;
+}
+
+inline Node NodeManager::mkVar() {
+  return NodeBuilder<>(this, kind::VARIABLE);
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_MANAGER_H */
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 863ddf649..63fe0c84a 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -29,59 +29,6 @@ size_t NodeValue::next_id = 1;
 
 NodeValue NodeValue::s_null;
 
-NodeValue::NodeValue() :
-  d_id(0),
-  d_rc(MAX_RC),
-  d_kind(NULL_EXPR),
-  d_nchildren(0) {
-}
-
-NodeValue::NodeValue(int) :
-  d_id(0),
-  d_rc(0),
-  d_kind(kindToDKind(UNDEFINED_KIND)),
-  d_nchildren(0) {
-}
-
-NodeValue::~NodeValue() {
-  for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
-    (*i)->dec();
-  }
-}
-
-void NodeValue::inc() {
-  // FIXME multithreading
-  if(EXPECT_TRUE( d_rc < MAX_RC )) {
-    ++d_rc;
-  }
-}
-
-void NodeValue::dec() {
-  // FIXME multithreading
-  if(EXPECT_TRUE( d_rc < MAX_RC )) {
-    --d_rc;
-    if(EXPECT_FALSE( d_rc == 0 )) {
-      // FIXME gc
-    }
-  }
-}
-
-NodeValue::nv_iterator NodeValue::nv_begin() {
-  return d_children;
-}
-
-NodeValue::nv_iterator NodeValue::nv_end() {
-  return d_children + d_nchildren;
-}
-
-NodeValue::const_nv_iterator NodeValue::nv_begin() const {
-  return d_children;
-}
-
-NodeValue::const_nv_iterator NodeValue::nv_end() const {
-  return d_children + d_nchildren;
-}
-
 string NodeValue::toString() const {
   stringstream ss;
   toStream(ss);
@@ -90,10 +37,10 @@ string NodeValue::toString() const {
 
 void NodeValue::toStream(std::ostream& out) const {
   out << "(" << Kind(d_kind);
-  if(d_kind == VARIABLE) {
+  if(d_kind == kind::VARIABLE) {
     Node n(this);
     string s;
-    if(n.hasAttribute(VarNameAttr(), &s)) {
+    if(n.hasAttribute(VarNameAttr(), s)) {
       out << ":" << s;
     } else {
       out << ":" << this;
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index f0220d37a..85b8a6d60 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -191,10 +191,63 @@ public:
     return ((unsigned) k) & kindMask;
   }
   static inline Kind dKindToKind(unsigned d) {
-    return (d == kindMask) ? UNDEFINED_KIND : Kind(d);
+    return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
   }
 };
 
+inline NodeValue::NodeValue() :
+  d_id(0),
+  d_rc(MAX_RC),
+  d_kind(kind::NULL_EXPR),
+  d_nchildren(0) {
+}
+
+inline NodeValue::NodeValue(int) :
+  d_id(0),
+  d_rc(0),
+  d_kind(kindToDKind(kind::UNDEFINED_KIND)),
+  d_nchildren(0) {
+}
+
+inline NodeValue::~NodeValue() {
+  for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
+    (*i)->dec();
+  }
+}
+
+inline void NodeValue::inc() {
+  // FIXME multithreading
+  if(EXPECT_TRUE( d_rc < MAX_RC )) {
+    ++d_rc;
+  }
+}
+
+inline void NodeValue::dec() {
+  // FIXME multithreading
+  if(EXPECT_TRUE( d_rc < MAX_RC )) {
+    --d_rc;
+    if(EXPECT_FALSE( d_rc == 0 )) {
+      // FIXME gc
+    }
+  }
+}
+
+inline NodeValue::nv_iterator NodeValue::nv_begin() {
+  return d_children;
+}
+
+inline NodeValue::nv_iterator NodeValue::nv_end() {
+  return d_children + d_nchildren;
+}
+
+inline NodeValue::const_nv_iterator NodeValue::nv_begin() const {
+  return d_children;
+}
+
+inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
+  return d_children + d_nchildren;
+}
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
 
diff --git a/src/expr/soft_node.h b/src/expr/soft_node.h
deleted file mode 100644
index 0bf9b47cf..000000000
--- a/src/expr/soft_node.h
+++ /dev/null
@@ -1,36 +0,0 @@
-/*********************                                                        */
-/** soft_node.h
- ** Original author: mdeters
- ** 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.
- **
- ** Encapsulation of a pointer to node information that is explicitly
- ** NOT reference-counted.  These "smart pointers" do NOT keep live
- ** the NodeValue object to which they refer.
- **/
-
-#ifndef __CVC4__SOFT_NODE_H
-#define __CVC4__SOFT_NODE_H
-
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace expr {
-
-/**
- * For now, treat SoftNodes as regular Nodes.  We'll address this
- * later.
- */
-typedef CVC4::Node SoftNode;
-typedef CVC4::Node TNode;
-
-}/* CVC4::expr namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SOFT_NODE_H */