* Addressed issues brought up in Chris's review of Morgan's

  NodeManager (bug #65).  Better documentation, etc.

* As part of this, removed NodeManager::mkVar() (which created a
  variable of unknown type).  This requires changes to lots of unit
  tests, which were using this function.

* Performed some review of parser code (my code review #73).

  + I changed the way exceptions were caught and rethrown in
    src/parser/input.cpp.

  + ParserExceptions weren't being properly constructed (d_line and
    d_column weren't intiialized and could contain junk, leading to
    weird error messages).  Fixed.

* Fix to the current working directory used by run_regression script.
  Makes exceptional output easier to match against (in expected error
  output).

* (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we
  compile any C code and don't use the C++ compiler.

3 files changed, 281 insertions, 120 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 213a4cb35..5c0cfb987 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -241,7 +241,8 @@ class MultNodeBuilder;
 /**
  * A base class for NodeBuilders.  When extending this class, use:
  *
- *   class MyExtendedNodeBuilder : public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
+ *   class MyExtendedNodeBuilder :
+ *       public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
  *
  * This ensures that certain member functions return the right
  * (derived) class type.
@@ -396,13 +397,14 @@ protected:
       expr::NodeValue* newBlock = (expr::NodeValue*)
         std::realloc(d_nv,
                      sizeof(expr::NodeValue) +
-                     ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = d_nv->d_nchildren) ));
+                     ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
       if(newBlock == NULL) {
         // In this case, d_nv was NOT freed.  If we throw, the
         // deallocation should occur on destruction of the
         // NodeBuilder.
         throw std::bad_alloc();
       }
+      d_nvMaxChildren = d_nv->d_nchildren;
       d_nv = newBlock;
     }
   }
@@ -446,37 +448,43 @@ public:
 
   /** Get the begin-const-iterator of this Node-under-construction. */
   inline const_iterator begin() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return d_nv->begin<true>();
   }
 
   /** Get the end-const-iterator of this Node-under-construction. */
   inline const_iterator end() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return d_nv->end<true>();
   }
 
   /** Get the kind of this Node-under-construction. */
   inline Kind getKind() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return d_nv->getKind();
   }
 
   /** Get the kind of this Node-under-construction. */
   inline kind::MetaKind getMetaKind() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return d_nv->getMetaKind();
   }
 
   /** Get the current number of children of this Node-under-construction. */
   inline unsigned getNumChildren() const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return d_nv->getNumChildren();
   }
 
   /** Access to children of this Node-under-construction. */
   inline Node operator[](int i) const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren(),
            "index out of range for NodeBuilder[]");
     return Node(d_nv->getChild(i));
@@ -500,7 +508,8 @@ public:
 
   /** Set the Kind of this Node-under-construction. */
   inline Builder& operator<<(const Kind& k) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     Assert(getKind() == kind::UNDEFINED_KIND,
            "can't redefine the Kind of a NodeBuilder");
     AssertArgument(k != kind::UNDEFINED_KIND &&
@@ -518,7 +527,8 @@ public:
    * on it but then never wrote code like that.
    */
   Builder& operator<<(TNode n) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     /* FIXME: disable this "collapsing" for now..
     if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) {
       Node n2 = operator Node();
@@ -529,15 +539,19 @@ public:
   }
 
   /** Append a sequence of children to this Node-under-construction. */
-  inline Builder& append(const std::vector<Node>& children) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+  template <bool ref_count>
+  inline Builder&
+  append(const std::vector<NodeTemplate<ref_count> >& children) {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     return append(children.begin(), children.end());
   }
 
   /** Append a sequence of children to this Node-under-construction. */
   template <class Iterator>
   Builder& append(const Iterator& begin, const Iterator& end) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     for(Iterator i = begin; i != end; ++i) {
       append(*i);
     }
@@ -546,7 +560,8 @@ public:
 
   /** Append a child to this Node-under-construction. */
   Builder& append(TNode n) {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node");
     allocateNvIfNecessaryForAppend();
     expr::NodeValue* nv = n.d_nv;
@@ -561,7 +576,8 @@ public:
   operator Node() const;
 
   inline void toStream(std::ostream& out, int depth = -1) const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
     d_nv->toStream(out, depth);
   }
 
@@ -596,7 +612,9 @@ public:
     NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
   }
 
-  inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm) :
+  inline BackedNodeBuilder(expr::NodeValue* buf,
+                           unsigned maxChildren,
+                           NodeManager* nm) :
     NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
   }
 
@@ -627,8 +645,12 @@ private:
  */
 #define makeStackNodeBuilder(__v, __n)                                  \
   const size_t __cvc4_backednodebuilder_nchildren__ ## __v = (__n);     \
-  ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v[1 + (((sizeof(::CVC4::expr::NodeValue) + sizeof(::CVC4::expr::NodeValue*) + 1) / sizeof(::CVC4::expr::NodeValue*)) * __cvc4_backednodebuilder_nchildren__ ## __v)]; \
-  ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v, \
+  ::CVC4::expr::NodeValue __cvc4_backednodebuilder_buf__ ## __v         \
+      [1 + ( ( ( sizeof(::CVC4::expr::NodeValue) +                      \
+                sizeof(::CVC4::expr::NodeValue*) + 1 ) /                \
+               sizeof(::CVC4::expr::NodeValue*) ) *                     \
+             __cvc4_backednodebuilder_nchildren__ ## __v)];             \
+  ::CVC4::BackedNodeBuilder __v(__cvc4_backednodebuilder_buf__ ## __v,  \
                                 __cvc4_backednodebuilder_nchildren__ ## __v)
 // IF THE ABOVE ASSERTION FAILS, write another compiler-specific
 // version of makeStackNodeBuilder() that works for your compiler
@@ -718,7 +740,8 @@ public:
   // we don't want a vtable, so do not declare a dtor!
   //inline ~NodeBuilder();
 
-  // This is needed for copy constructors of different sizes to access private fields
+  // This is needed for copy constructors of different sizes to access
+  // private fields
   template <unsigned N>
   friend class NodeBuilder;
 
@@ -845,7 +868,8 @@ inline Builder& NodeBuilderBase<Builder>::operator+=(TNode e) {
 
 template <class Builder>
 inline Builder& NodeBuilderBase<Builder>::operator-=(TNode e) {
-  return collapseTo(kind::PLUS).append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
+  return collapseTo(kind::PLUS).
+    append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
 }
 
 template <class Builder>
@@ -1171,12 +1195,13 @@ void NodeBuilderBase<Builder>::realloc(size_t toSize) {
     // Ensure d_nv is not modified on allocation failure
     expr::NodeValue* newBlock = (expr::NodeValue*)
       std::realloc(d_nv, sizeof(expr::NodeValue) +
-                   ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) ));
+                   ( sizeof(expr::NodeValue*) * toSize ));
     if(newBlock == NULL) {
       // In this case, d_nv was NOT freed.  If we throw, the
       // deallocation should occur on destruction of the NodeBuilder.
       throw std::bad_alloc();
     }
+    d_nvMaxChildren = toSize;
     // Here, the copy (between two heap-allocated buffers) has already
     // been done for us by the std::realloc().
     d_nv = newBlock;
@@ -1184,10 +1209,11 @@ void NodeBuilderBase<Builder>::realloc(size_t toSize) {
     // Ensure d_nv is not modified on allocation failure
     expr::NodeValue* newBlock = (expr::NodeValue*)
       std::malloc(sizeof(expr::NodeValue) +
-                  ( sizeof(expr::NodeValue*) * (d_nvMaxChildren = toSize) ));
+                  ( sizeof(expr::NodeValue*) * toSize ));
     if(newBlock == NULL) {
       throw std::bad_alloc();
     }
+    d_nvMaxChildren = toSize;
 
     d_nv = newBlock;
     d_nv->d_id = 0;
@@ -1239,7 +1265,8 @@ void NodeBuilderBase<Builder>::decrRefCounts() {
 // NON-CONST VERSION OF NODE EXTRACTOR
 template <class Builder>
 NodeBuilderBase<Builder>::operator Node() {
-  Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+  Assert(!isUsed(), "NodeBuilder is one-shot only; "
+         "attempt to access it after conversion");
   Assert(getKind() != kind::UNDEFINED_KIND,
          "Can't make an expression of an undefined kind!");
 
@@ -1410,7 +1437,8 @@ NodeBuilderBase<Builder>::operator Node() {
 // CONST VERSION OF NODE EXTRACTOR
 template <class Builder>
 NodeBuilderBase<Builder>::operator Node() const {
-  Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+  Assert(!isUsed(), "NodeBuilder is one-shot only; "
+         "attempt to access it after conversion");
   Assert(getKind() != kind::UNDEFINED_KIND,
          "Can't make an expression of an undefined kind!");
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 8f254ed9f..e735b7f09 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -58,33 +58,41 @@ NodeManager::~NodeManager() {
 }
 
 /**
- * This class ensure that NodeManager::d_reclaiming gets set to false
+ * This class ensures that NodeManager::d_reclaiming gets set to false
  * even on exceptional exit from NodeManager::reclaimZombies().
  */
 struct Reclaim {
   bool& d_reclaimField;
+
   Reclaim(bool& reclaim) :
     d_reclaimField(reclaim) {
 
     Debug("gc") << ">> setting RECLAIM field\n";
     d_reclaimField = true;
   }
+
   ~Reclaim() {
     Debug("gc") << "<< clearing RECLAIM field\n";
     d_reclaimField = false;
   }
 };
 
+/**
+ * Similarly, ensure d_nodeUnderDeletion gets set to NULL even on
+ * exceptional exit from NodeManager::reclaimZombies().
+ */
 struct NVReclaim {
-  NodeValue*& d_reclaimField;
-  NVReclaim(NodeValue*& reclaim) :
-    d_reclaimField(reclaim) {
+  NodeValue*& d_deletionField;
+
+  NVReclaim(NodeValue*& deletionField) :
+    d_deletionField(deletionField) {
 
     Debug("gc") << ">> setting NVRECLAIM field\n";
   }
+
   ~NVReclaim() {
     Debug("gc") << "<< clearing NVRECLAIM field\n";
-    d_reclaimField = NULL;
+    d_deletionField = NULL;
   }
 };
 
@@ -107,11 +115,11 @@ void NodeManager::reclaimZombies() {
   // Let's say we're reclaiming zombie NodeValue "A" and its child "B"
   // then becomes a zombie (NodeManager::gc(B) is called).
   //
-  // One way to handle B's zombification is simply to put it into
-  // d_zombies.  This is what we do.  However, if we're currently
-  // processing d_zombies in the loop below, such addition may be
-  // invisible to us (B is leaked) or even invalidate our iterator,
-  // causing a crash.
+  // One way to handle B's zombification would be simply to put it
+  // into d_zombies.  This is what we do.  However, if we were to
+  // concurrently process d_zombies in the loop below, such addition
+  // may be invisible to us (B is leaked) or even invalidate our
+  // iterator, causing a crash.  So we need to copy the set away.
 
   vector<NodeValue*> zombies;
   zombies.reserve(d_zombies.size());
@@ -149,6 +157,6 @@ void NodeManager::reclaimZombies() {
       free(nv);
     }
   }
-}
+}/* NodeManager::reclaimZombies() */
 
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 71242f2e1..04d2ddac7 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -65,25 +65,100 @@ class NodeManager {
 
   expr::attr::AttributeManager d_attrManager;
 
+  /**
+   * The node value we're currently freeing.  This unique node value
+   * is permitted to have outstanding TNodes to it (in "soft"
+   * contexts, like as a key in attribute tables), even though
+   * normally it's an error to have a TNode to a node value with a
+   * reference count of 0.  Being "under deletion" also enables
+   * assertions that inc() is not called on it.  (A poorly-behaving
+   * attribute cleanup function could otherwise create a "Node" that
+   * points to the node value that is in the process of being deleted,
+   * springing it back to life.)
+   */
   expr::NodeValue* d_nodeUnderDeletion;
+
+  /**
+   * True iff we are in reclaimZombies().  This avoids unnecessary
+   * recursion; a NodeValue being deleted might zombify other
+   * NodeValues, but these shouldn't trigger a (recursive) call to
+   * reclaimZombies().
+   */
   bool d_reclaiming;
+
+  /**
+   * The set of zombie nodes.  We may want to revisit this design, as
+   * we might like to delete nodes in least-recently-used order.  But
+   * we also need to avoid processing a zombie twice.
+   */
   ZombieSet d_zombies;
 
+  /**
+   * A set of operator singletons (w.r.t.  to this NodeManager
+   * instance) for operators.  Conceptually, Nodes with kind, say,
+   * PLUS, are APPLYs of a PLUS operator to arguments.  This array
+   * holds the set of operators for these things.  A PLUS operator is
+   * a Node with kind "BUILTIN", and if you call
+   * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
+   */
+  Node d_operators[kind::LAST_KIND];
+
+  /**
+   * Look up a NodeValue in the pool associated to this NodeManager.
+   * The NodeValue argument need not be a "completely-constructed"
+   * NodeValue.  In particular, "non-inlined" constants are permited
+   * (see below).
+   *
+   * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
+   * correctly set, and d_children[0..n-1] should be valid (extant)
+   * NodeValues for lookup.
+   *
+   * For CONSTANT metakinds, nv's d_kind should be set correctly.
+   * Normally a CONSTANT would have d_nchildren == 0 and the constant
+   * value inlined in the d_children space.  However, here we permit
+   * "non-inlined" NodeValues to avoid unnecessary copying.  For
+   * these, d_nchildren == 1, and d_nchildren is a pointer to the
+   * constant value.
+   *
+   * The point of this complex design is to permit efficient lookups
+   * (without fully constructing a NodeValue).  In the case that the
+   * argument is not fully constructed, and this function returns
+   * NULL, the caller should fully construct an equivalent one before
+   * calling poolInsert().  NON-FULLY-CONSTRUCTED NODEVALUES are not
+   * permitted in the pool!
+   */
   inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
-  void poolInsert(expr::NodeValue* nv);
+
+  /**
+   * Insert a NodeValue into the NodeManager's pool.
+   *
+   * It is an error to insert a NodeValue already in the pool.
+   * Enquire first with poolLookup().
+   */
+  inline void poolInsert(expr::NodeValue* nv);
+
+  /**
+   * Remove a NodeValue from the NodeManager's pool.
+   *
+   * It is an error to request the removal of a NodeValue from the
+   * pool that is not in the pool.
+   */
   inline void poolRemove(expr::NodeValue* nv);
 
-  bool isCurrentlyDeleting(const expr::NodeValue* nv) const{
+  /**
+   * Determine if nv is currently being deleted by the NodeManager.
+   */
+  inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
     return d_nodeUnderDeletion == nv;
   }
 
-  Node d_operators[kind::LAST_KIND];
-
   /**
    * Register a NodeValue as a zombie.
    */
   inline void gc(expr::NodeValue* nv) {
     Assert(nv->d_rc == 0);
+    // if d_reclaiming is set, make sure we don't call
+    // reclaimZombies(), because it's already running.
     if(d_reclaiming) {// FIXME multithreading
       // currently reclaiming zombies; just push onto the list
       Debug("gc") << "zombifying node value " << nv
@@ -169,6 +244,7 @@ public:
   static NodeManager* currentNM() { return s_current; }
 
   // general expression-builders
+
   /** Create a node with no children. */
   Node mkNode(Kind kind);
 
@@ -182,33 +258,45 @@ public:
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
 
   /** Create a node with four children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
+              TNode child4);
 
   /** Create a node with five children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5);
+  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
+              TNode child4, TNode child5);
 
   /** Create a node with an arbitrary number of children. */
-  Node mkNode(Kind kind, const std::vector<Node>& children);
-
-  // NOTE: variables are special, because duplicates are permitted
+  template <bool ref_count>
+  Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
-  /** Create a variable with the given type and name. */
+  /**
+   * Create a variable with the given type and name.  NOTE that no
+   * lookup is done on the name.  If you mkVar(type, "a") and then
+   * mkVar(type, "a") again, you have two variables.
+   */
   Node mkVar(Type* type, const std::string& name);
 
   /** Create a variable with the given type. */
   Node mkVar(Type* type);
 
-  /** Create a variable of unknown type (?). */
-  Node mkVar();
-
-  /** Create a constant of type T */
+  /**
+   * Create a constant of type T.  It will have the appropriate
+   * CONST_* kind defined for T.
+   */
   template <class T>
   Node mkConst(const T&);
 
-  /** Determine whether Nodes of a particular Kind have operators. */
-  static inline bool hasOperator(Kind mk);
+  /**
+   * Determine whether Nodes of a particular Kind have operators.
+   * @returns true if Nodes of Kind k have operators.
+   */
+  static inline bool hasOperator(Kind k);
 
-  /** Get the (singleton) operator of an OPERATOR-kinded kind. */
+  /**
+   * Get the (singleton) operator of an OPERATOR-kinded kind.  The
+   * returned node n will have kind BUILTIN, and calling
+   * n.getConst<CVC4::Kind>() will yield k.
+   */
   inline TNode operatorOf(Kind k) {
     AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
                     "Kind is not an OPERATOR-kinded kind "
@@ -216,7 +304,8 @@ public:
     return d_operators[k];
   }
 
-  /** Retrieve an attribute for a node.
+  /**
+   * Retrieve an attribute for a node.
    *
    * @param nv the node value
    * @param attr an instance of the attribute kind to retrieve.
@@ -227,43 +316,52 @@ public:
   inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
                                                     const AttrKind& attr) const;
 
-  /** Check whether an attribute is set for a node.
+  /**
+   * Check whether an attribute is set for a node.
    *
    * @param nv the node value
    * @param attr an instance of the attribute kind to check
-   * @returns <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+   * @returns <code>true</code> iff <code>attr</code> is set for
+   * <code>nv</code>.
    */
   template <class AttrKind>
   inline bool hasAttribute(expr::NodeValue* nv,
                            const AttrKind& attr) const;
 
-  /** Check whether an attribute is set for a node.
+  /**
+   * Check whether an attribute is set for a node, and, if so,
+   * retrieve it.
    *
    * @param nv the node value
    * @param attr an instance of the attribute kind to check
    * @param value a reference to an object of the attribute's value type.
    * <code>value</code> will be set to the value of the attribute, if it is
-   * set for <code>nv</code>; otherwise, it will be set to the default value of
-   * the attribute.
-   * @returns <code>true</code> iff <code>attr</code> is set for <code>nv</code>.
+   * set for <code>nv</code>; otherwise, it will be set to the default
+   * value of the attribute.
+   * @returns <code>true</code> iff <code>attr</code> is set for
+   * <code>nv</code>.
    */
   template <class AttrKind>
   inline bool getAttribute(expr::NodeValue* nv,
                            const AttrKind& attr,
                            typename AttrKind::value_type& value) const;
 
-  /** Set an attribute for a node.
-    *
-    * @param nv the node value
-    * @param attr an instance of the attribute kind to set
-    * @param value the value of <code>attr</code> for <code>nv</code>
-    */
+  /**
+   * Set an attribute for a node.  If the node doesn't have the
+   * attribute, this function assigns one.  If the node has one, this
+   * overwrites it.
+   *
+   * @param nv the node value
+   * @param attr an instance of the attribute kind to set
+   * @param value the value of <code>attr</code> for <code>nv</code>
+   */
   template <class AttrKind>
   inline void setAttribute(expr::NodeValue* nv,
                            const AttrKind&,
                            const typename AttrKind::value_type& value);
 
-  /** Retrieve an attribute for a TNode.
+  /**
+   * Retrieve an attribute for a TNode.
    *
    * @param n the node
    * @param attr an instance of the attribute kind to retrieve.
@@ -274,12 +372,8 @@ public:
   inline typename AttrKind::value_type getAttribute(TNode n,
                                                     const AttrKind&) const;
 
-  /* NOTE: 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. */
-
-  /** Check whether an attribute is set for a TNode.
+  /**
+   * Check whether an attribute is set for a TNode.
    *
    * @param n the node
    * @param attr an instance of the attribute kind to check
@@ -289,7 +383,9 @@ public:
   inline bool hasAttribute(TNode n,
                            const AttrKind& attr) const;
 
-  /** Check whether an attribute is set for a TNode.
+  /**
+   * Check whether an attribute is set for a TNode and, if so, retieve
+   * it.
    *
    * @param n the node
    * @param attr an instance of the attribute kind to check
@@ -304,33 +400,46 @@ public:
                            const AttrKind& attr,
                            typename AttrKind::value_type& value) const;
 
-  /** Set an attribute for a TNode.
-    *
-    * @param n the node
-    * @param attr an instance of the attribute kind to set
-    * @param value the value of <code>attr</code> for <code>n</code>
-    */
+  /**
+   * Set an attribute for a node.  If the node doesn't have the
+   * attribute, this function assigns one.  If the node has one, this
+   * overwrites it.
+   *
+   * @param n the node
+   * @param attr an instance of the attribute kind to set
+   * @param value the value of <code>attr</code> for <code>n</code>
+   */
   template <class AttrKind>
   inline void setAttribute(TNode n,
                            const AttrKind&,
                            const typename AttrKind::value_type& value);
 
-  /** Get the type for booleans. */
+  /** Get the (singleton) type for booleans. */
   inline BooleanType* booleanType() const {
     return BooleanType::getInstance();
   }
 
-  /** Get the type for sorts. */
+  /** Get the (singleton) type for sorts. */
   inline KindType* kindType() const {
     return KindType::getInstance();
   }
 
-  /** Make a function type from domain to range. */
+  /**
+   * Make a function type from domain to range.
+   *
+   * @param domain the domain type
+   * @param range the range type
+   * @returns the functional type domain -> range
+   */
   inline FunctionType* mkFunctionType(Type* domain, Type* range) const;
 
   /**
    * Make a function type with input types from
    * argTypes. <code>argTypes</code> must have at least one element.
+   *
+   * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
+   * @param range the range type
+   * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
    */
   inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
                                       Type* range) const;
@@ -399,24 +508,37 @@ public:
 
   NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) {
     NodeManager::s_current = nm;
-    Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
+    Debug("current") << "node manager scope: "
+                     << NodeManager::s_current << "\n";
   }
 
   ~NodeManagerScope() {
     NodeManager::s_current = d_oldNodeManager;
-    Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n";
+    Debug("current") << "node manager scope: "
+                     << "returning to " << NodeManager::s_current << "\n";
   }
 };
 
 /**
- * Creates
- * a <code>NodeManagerScope</code> with the underlying <code>NodeManager</code>
- * of a given <code>Expr</code> or <code>ExprManager</code>.
- * The <code>NodeManagerScope</code> is destroyed when the <code>ExprManagerScope</code>
- * is destroyed. See <code>NodeManagerScope</code> for more information.
+ * Creates a <code>NodeManagerScope</code> with the underlying
+ * <code>NodeManager</code> of a given <code>Expr</code> or
+ * <code>ExprManager</code>.  The <code>NodeManagerScope</code> is
+ * destroyed when the <code>ExprManagerScope</code> is destroyed. See
+ * <code>NodeManagerScope</code> for more information.
  */
-// NOTE: Without this, we'd need Expr to be a friend of ExprManager.
-// [chris 3/25/2010] Why?
+// NOTE: Here, it seems ExprManagerScope is redundant, since we have
+// NodeManagerScope already.  However, without this class, we'd need
+// Expr to be a friend of ExprManager, because in the implementation
+// of Expr functions, it needs to set the current NodeManager
+// correctly (and to do that it needs access to
+// ExprManager::getNodeManager()).  So, we make ExprManagerScope a
+// friend of ExprManager's, since it's implementation is simple to
+// read and understand (and verify that it doesn't do any mischief).
+//
+// ExprManager::getNodeManager() can't just be made public, since
+// ExprManager is exposed to clients of the library and NodeManager is
+// not.  Similarly, ExprManagerScope shouldn't go in expr_manager.h,
+// since that's a public header.
 class ExprManagerScope {
   NodeManagerScope d_nms;
 public:
@@ -431,8 +553,8 @@ public:
 };
 
 template <class AttrKind>
-inline typename AttrKind::value_type NodeManager::getAttribute(expr::NodeValue* nv,
-                                                               const AttrKind&) const {
+inline typename AttrKind::value_type
+NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
   return d_attrManager.getAttribute(nv, AttrKind());
 }
 
@@ -443,42 +565,42 @@ inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
 }
 
 template <class AttrKind>
-inline bool NodeManager::getAttribute(expr::NodeValue* nv,
-                                      const AttrKind&,
-                                      typename AttrKind::value_type& ret) const {
+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) {
+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 {
+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 {
+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 {
+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) {
+inline void
+NodeManager::setAttribute(TNode n, const AttrKind&,
+                          const typename AttrKind::value_type& value) {
   d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
 }
 
@@ -574,6 +696,7 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) {
 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
   Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
          "NodeValue is not in the pool!");
+
   d_nodeValuePool.erase(nv);// FIXME multithreading
 }
 
@@ -620,20 +743,27 @@ 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) {
+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) {
+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;
+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) {
+template <bool ref_count>
+inline Node NodeManager::mkNode(Kind kind,
+                                const std::vector<NodeTemplate<ref_count> >&
+                                children) {
   return NodeBuilder<>(this, kind).append(children);
 }
 
@@ -644,17 +774,12 @@ inline Node NodeManager::mkVar(Type* type, const std::string& name) {
 }
 
 inline Node NodeManager::mkVar(Type* type) {
-  Node n = mkVar();
+  Node n = Node(NodeBuilder<>(this, kind::VARIABLE));
   type->inc();// reference-count the type
   n.setAttribute(TypeAttr(), type);
   return n;
 }
 
-inline Node NodeManager::mkVar() {
-  // TODO: rewrite to not use NodeBuilder
-  return NodeBuilder<>(this, kind::VARIABLE);
-}
-
 template <class T>
 Node NodeManager::mkConst(const T& val) {
   // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;