* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"

  (etc.) now work for Nodes a, b, c, d, e.  Also refcounting fixes for
  NodeBuilder in certain cases

* (various places) don't overload __gnu_cxx::hash<>, instead provide
  an explicit hash function to hash_maps and hash_sets.

* add a new kind of assert, DtorAssert(), which doesn't throw
  exceptions (right now it operates like a usual C assert()).  For use
  in destructors.

* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).

* fix some Make rule dependencies

* reformat node.h as per code formatting policy

* added Theory and NodeBuilder unit tests

9 files changed, 967 insertions, 748 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 1aa2e61fa..bd02cf452 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -31,7 +31,7 @@ EXTRA_DIST = \
 	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
+@srcdir@/kind.h: mkkind kind_prologue.h kind_middle.h kind_epilogue.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
 	chmod +x @srcdir@/mkkind
 	(@srcdir@/mkkind \
 		@srcdir@/kind_prologue.h \
diff --git a/src/expr/node.h b/src/expr/node.h
index 5655d7e3a..e4e57fc62 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -36,8 +36,9 @@ namespace CVC4 {
 
 class Type;
 class NodeManager;
-template<bool ref_count>
-  class NodeTemplate;
+
+template<bool ref_count> class NodeTemplate;
+
 /**
  * The Node class encapsulates the NodeValue with reference counting.
  */
@@ -49,14 +50,14 @@ typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
 
 namespace expr {
-  class NodeValue;
+
+class NodeValue;
 
   namespace attr {
     class AttributeManager;
   }/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
 
-using CVC4::expr::NodeValue;
+}/* CVC4::expr namespace */
 
 /**
  * Encapsulation of an NodeValue pointer.  The reference count is
@@ -64,390 +65,335 @@ using CVC4::expr::NodeValue;
  * @param ref_count if true reference are counted in the NodeValue
  */
 template<bool ref_count>
-  class NodeTemplate {
-
-    /**
-     * The NodeValue has access to the private constructors, so that the
-     * iterators can can create new nodes.
-     */
-    friend class NodeValue;
-
-    /** A convenient null-valued encapsulated pointer */
-    static NodeTemplate s_null;
-
-    /** The referenced NodeValue */
-    NodeValue* d_nv;
-
-    /**
-     * This constructor is reserved for use by the NodeTemplate package; one
-     * must construct an NodeTemplate using one of the build mechanisms of the
-     * NodeTemplate package.
-     *
-     * FIXME: there's a type-system escape here to cast away the const,
-     * since the refcount needs to be updated.  But conceptually Nodes
-     * don't change their arguments, and it's nice to have
-     * const_iterators over them.
-     *
-     * This really does needs to be explicit to avoid hard to track errors with
-     * Nodes implicitly wrapping NodeValues
-     */
-    explicit NodeTemplate(const NodeValue*);
-
-    friend class NodeTemplate<true> ;
-    friend class NodeTemplate<false> ;
-    friend class NodeManager;
-    template<unsigned>
-      friend class NodeBuilder;
-    friend class ::CVC4::expr::attr::AttributeManager;
-
-    /**
-     * Assigns the expression value and does reference counting. No assumptions
-     * are made on the expression, and should only be used if we know what we 
-     * are doing.
-     *
-     * @param ev the expression value to assign
-     */
-    void assignNodeValue(NodeValue* ev);
-
-  public:
-
-    /** Default constructor, makes a null expression. */
-    NodeTemplate() : d_nv(&NodeValue::s_null) { }
-
-    /**
-     * Conversion between nodes that are reference-counted and those that are
-     * not.
-     * @param node the node to make copy of
-     */
-    NodeTemplate(const NodeTemplate<!ref_count>& 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& node);
-
-    /**
-     * Assignment operator for nodes, copies the relevant information from node
-     * to this node.
-     * @param node the node to copy
-     * @return reference to this node
-     */
-    NodeTemplate& operator=(const NodeTemplate& node);
-
-    /**
-     * Assignment operator for nodes, copies the relevant information from node
-     * to this node.
-     * @param node the node to copy
-     * @return reference to this node
-     */
-    NodeTemplate& operator=(const NodeTemplate<!ref_count>& node);
-
-    /**
-     * Destructor. If ref_count is true it will decrement the reference count
-     * and, if zero, collect the NodeValue.
-     */
-    ~NodeTemplate();
-
-    /**
-     * Return the null node.
-     * @return the null node
-     */
-    static NodeTemplate null() {
-      return s_null;
-    }
-
-    /**
-     * Returns true if this expression is a null expression.
-     * @return true if null
-     */
-    bool isNull() const {
-      return d_nv == &NodeValue::s_null;
-    }
-
-    /**
-     * Structural comparison operator for expressions.
-     * @param node the node to compare to
-     * @return true if expressions are equal, false otherwise
-     */
-    template <bool ref_count_1>
-    bool operator==(const NodeTemplate<ref_count_1>& node) const {
-      return d_nv == node.d_nv;
-    }
-
-    /**
-     * Structural comparison operator for expressions.
-     * @param node the node to compare to
-     * @return false if expressions are equal, true otherwise
-     */
-    template <bool ref_count_1>
-    bool operator!=(const NodeTemplate<ref_count_1>& node) const {
-      return d_nv != node.d_nv;
-    }
+class NodeTemplate {
+
+  /**
+   * The NodeValue has access to the private constructors, so that the
+   * iterators can can create new nodes.
+   */
+  friend class expr::NodeValue;
+
+  /** A convenient null-valued encapsulated pointer */
+  static NodeTemplate s_null;
+
+  /** The referenced NodeValue */
+  expr::NodeValue* d_nv;
+
+  /**
+   * This constructor is reserved for use by the NodeTemplate package; one
+   * must construct an NodeTemplate using one of the build mechanisms of the
+   * NodeTemplate package.
+   *
+   * FIXME: there's a type-system escape here to cast away the const,
+   * since the refcount needs to be updated.  But conceptually Nodes
+   * don't change their arguments, and it's nice to have
+   * const_iterators over them.
+   *
+   * This really does needs to be explicit to avoid hard to track errors with
+   * Nodes implicitly wrapping NodeValues
+   */
+  explicit NodeTemplate(const expr::NodeValue*);
+
+  friend class NodeTemplate<true> ;
+  friend class NodeTemplate<false> ;
+  friend class NodeManager;
+
+  template<unsigned>
+  friend class NodeBuilder;
+
+  friend class ::CVC4::expr::attr::AttributeManager;
+
+  /**
+   * Assigns the expression value and does reference counting. No assumptions
+   * are made on the expression, and should only be used if we know what we 
+   * are doing.
+   *
+   * @param ev the expression value to assign
+   */
+  void assignNodeValue(expr::NodeValue* ev);
+
+public:
+
+  /** Default constructor, makes a null expression. */
+  NodeTemplate() : d_nv(&expr::NodeValue::s_null) { }
+
+  /**
+   * Conversion between nodes that are reference-counted and those that are
+   * not.
+   * @param node the node to make copy of
+   */
+  NodeTemplate(const NodeTemplate<!ref_count>& 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& node);
+
+  /**
+   * Assignment operator for nodes, copies the relevant information from node
+   * to this node.
+   * @param node the node to copy
+   * @return reference to this node
+   */
+  NodeTemplate& operator=(const NodeTemplate& node);
+
+  /**
+   * Assignment operator for nodes, copies the relevant information from node
+   * to this node.
+   * @param node the node to copy
+   * @return reference to this node
+   */
+  NodeTemplate& operator=(const NodeTemplate<!ref_count>& node);
+
+  /**
+   * Destructor. If ref_count is true it will decrement the reference count
+   * and, if zero, collect the NodeValue.
+   */
+  ~NodeTemplate() throw();
+
+  /**
+   * Return the null node.
+   * @return the null node
+   */
+  static NodeTemplate null() {
+    return s_null;
+  }
 
-    /**
-     * We compare by expression ids so, keeping things deterministic and having
-     * that subexpressions have to be smaller than the enclosing expressions.
-     * @param node the node to compare to
-     * @return true if this expression is smaller
-     */
-    template <bool ref_count_1>
-    inline bool operator<(const NodeTemplate<ref_count_1>& node) const {
-      return d_nv->d_id < node.d_nv->d_id;
-    }
+  /**
+   * Returns true if this expression is a null expression.
+   * @return true if null
+   */
+  bool isNull() const {
+    return d_nv == &expr::NodeValue::s_null;
+  }
 
-    /**
-     * Returns the i-th child of this node.
-     * @param i the index of the child
-     * @return the node representing the i-th child
-     */
-    NodeTemplate operator[](int i) const {
-      Assert(i >= 0 && unsigned(i) < d_nv->d_nchildren);
-      return NodeTemplate(d_nv->d_children[i]);
-    }
+  /**
+   * Structural comparison operator for expressions.
+   * @param node the node to compare to
+   * @return true if expressions are equal, false otherwise
+   */
+  template <bool ref_count_1>
+  bool operator==(const NodeTemplate<ref_count_1>& node) const {
+    return d_nv == node.d_nv;
+  }
 
-    /**
-     * Returns true if this node is atomic (has no more Boolean structure)
-     * @return true if atomic
-     */
-    bool isAtomic() const;
-
-    /**
-     * Returns the hash value of this node.
-     * @return the hash value
-     */
-    size_t hash() const {
-      return d_nv->getId();
-    }
+  /**
+   * Structural comparison operator for expressions.
+   * @param node the node to compare to
+   * @return false if expressions are equal, true otherwise
+   */
+  template <bool ref_count_1>
+  bool operator!=(const NodeTemplate<ref_count_1>& node) const {
+    return d_nv != node.d_nv;
+  }
 
-    /**
-     * Returns the unique id of this node
-     * @return the ud
-     */
-    uint64_t getId() const {
-      return d_nv->getId();
-    }
+  /**
+   * We compare by expression ids so, keeping things deterministic and having
+   * that subexpressions have to be smaller than the enclosing expressions.
+   * @param node the node to compare to
+   * @return true if this expression is smaller
+   */
+  template <bool ref_count_1>
+  inline bool operator<(const NodeTemplate<ref_count_1>& node) const {
+    return d_nv->d_id < node.d_nv->d_id;
+  }
 
-    /**
-     * Returns a node representing the operator of this expression.
-     * If this is an APPLY, then the operator will be a functional term.
-     * Otherwise, it will be a node with kind BUILTIN
-     */
-    inline NodeTemplate<true> getOperator() const {
-      switch(getKind()) {
-      case kind::APPLY:
-        /* The operator is the first child. */
-        return NodeTemplate<true> (d_nv->d_children[0]);
-
-      case kind::EQUAL:
-      case kind::ITE:
-      case kind::TUPLE:
-      case kind::NOT:
-      case kind::AND:
-      case kind::IFF:
-      case kind::IMPLIES:
-      case kind::OR:
-      case kind::XOR:
-      case kind::PLUS:
-        /* Should return a BUILTIN node. */
-        Unimplemented("getOperator() on non-APPLY kind: " + getKind());
-        break;
-
-      case kind::FALSE:
-      case kind::TRUE:
-      case kind::SKOLEM:
-      case kind::VARIABLE:
-        IllegalArgument(*this,"getOperator() called on kind with no operator");
-        break;
-
-      default:
-        Unhandled(getKind());
-      }
-
-      NodeTemplate<true> n; // NULL Node for default return
-      return n;
-    }
+  /**
+   * Returns the i-th child of this node.
+   * @param i the index of the child
+   * @return the node representing the i-th child
+   */
+  NodeTemplate operator[](int i) const {
+    Assert(i >= 0 && unsigned(i) < d_nv->d_nchildren);
+    return NodeTemplate(d_nv->d_children[i]);
+  }
 
-    /** Returns true if the node has an operator (i.e., it's not a variable or a constant). */
-    inline bool hasOperator() const {
-      switch(getKind()) {
-      case kind::APPLY:
-      case kind::EQUAL:
-      case kind::ITE:
-      case kind::TUPLE:
-      case kind::FALSE:
-      case kind::TRUE:
-      case kind::NOT:
-      case kind::AND:
-      case kind::IFF:
-      case kind::IMPLIES:
-      case kind::OR:
-      case kind::XOR:
-      case kind::PLUS:
-        return true;
-
-      case kind::SKOLEM:
-      case kind::VARIABLE:
-        return false;
-
-      default:
-        Unhandled(getKind());
-      }
+  /**
+   * Returns true if this node is atomic (has no more Boolean structure)
+   * @return true if atomic
+   */
+  bool isAtomic() const;
+
+  /**
+   * Returns the hash value of this node.
+   * @return the hash value
+   */
+  size_t hash() const {
+    return d_nv->getId();
+  }
 
-    }
+  /**
+   * Returns the unique id of this node
+   * @return the ud
+   */
+  uint64_t getId() const {
+    return d_nv->getId();
+  }
 
-    /**
-     * Returns the type of this node.
-     * @return the type
-     */
-    const Type* getType() const;
-
-    /**
-     * Returns the kind of this node.
-     * @return the kind
-     */
-    inline Kind getKind() const {
-      return Kind(d_nv->d_kind);
-    }
+  /**
+   * Returns a node representing the operator of this expression.
+   * If this is an APPLY, then the operator will be a functional term.
+   * Otherwise, it will be a node with kind BUILTIN
+   */
+  NodeTemplate<true> getOperator() const;
+
+  /** Returns true if the node has an operator (i.e., it's not a variable or a constant). */
+  bool hasOperator() const;
+
+  /**
+   * Returns the type of this node.
+   * @return the type
+   */
+  const Type* getType() const;
+
+  /**
+   * Returns the kind of this node.
+   * @return the kind
+   */
+  inline Kind getKind() const {
+    return Kind(d_nv->d_kind);
+  }
 
-    /**
-     * Returns the number of children this node has.
-     * @return the number of children
-     */
-    inline size_t getNumChildren() const;
-
-    /**
-     * Returns the value of the given attribute that this has been attached.
-     * @param attKind the kind of the attribute
-     * @return the value of the attribute
-     */
-    template <class AttrKind>
-      inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
-
-    // Note that there are two, distinct hasAttribute() declarations for
-    // a reason (rather than using a pointer-valued argument with a
-    // default value): they permit more optimized code in the underlying
-    // hasAttribute() implementations.
-
-    /**
-     * Returns true if this node has been associated an attribute of given kind.
-     * Additionaly, if a pointer to the value_kind is give, and the attribute
-     * value has been set for this node, it will be returned.
-     * @param attKind the kind of the attribute
-     * @return true if this node has the requested attribute
-     */
-    template <class AttrKind>
-      inline bool hasAttribute(const AttrKind& attKind) const;
-
-    /**
-     * Returns true if this node has been associated an attribute of given kind.
-     * Additionaly, if a pointer to the value_kind is give, and the attribute
-     * value has been set for this node, it will be returned.
-     * @param attKind the kind of the attribute
-     * @param value where to store the value if it exists
-     * @return true if this node has the requested attribute
-     */
-    template <class AttrKind>
-      inline bool 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;
-    /** Constant iterator allowing for scanning through the children. */
-    typedef typename NodeValue::iterator<ref_count> const_iterator;
-
-    /**
-     * Returns the iterator pointing to the first child.
-     * @return the iterator
-     */
-    inline iterator begin() {
-      return d_nv->begin<ref_count>();
-    }
+  /**
+   * Returns the number of children this node has.
+   * @return the number of children
+   */
+  inline size_t getNumChildren() const;
+
+  /**
+   * Returns the value of the given attribute that this has been attached.
+   * @param attKind the kind of the attribute
+   * @return the value of the attribute
+   */
+  template <class AttrKind>
+  inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
+
+  // Note that there are two, distinct hasAttribute() declarations for
+  // a reason (rather than using a pointer-valued argument with a
+  // default value): they permit more optimized code in the underlying
+  // hasAttribute() implementations.
+
+  /**
+   * Returns true if this node has been associated an attribute of given kind.
+   * Additionaly, if a pointer to the value_kind is give, and the attribute
+   * value has been set for this node, it will be returned.
+   * @param attKind the kind of the attribute
+   * @return true if this node has the requested attribute
+   */
+  template <class AttrKind>
+  inline bool hasAttribute(const AttrKind& attKind) const;
+
+  /**
+   * Returns true if this node has been associated an attribute of given kind.
+   * Additionaly, if a pointer to the value_kind is give, and the attribute
+   * value has been set for this node, it will be returned.
+   * @param attKind the kind of the attribute
+   * @param value where to store the value if it exists
+   * @return true if this node has the requested attribute
+   */
+  template <class AttrKind>
+  inline bool 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 expr::NodeValue::iterator<ref_count> iterator;
+  /** Constant iterator allowing for scanning through the children. */
+  typedef typename expr::NodeValue::iterator<ref_count> const_iterator;
+
+  /**
+   * Returns the iterator pointing to the first child.
+   * @return the iterator
+   */
+  inline iterator begin() {
+    return d_nv->begin<ref_count>();
+  }
 
-    /**
-     * Returns the iterator pointing to the end of the children (one beyond the
-     * last one.
-     * @return the end of the children iterator.
-     */
-    inline iterator end() {
-      return d_nv->end<ref_count>();
-    }
+  /**
+   * Returns the iterator pointing to the end of the children (one beyond the
+   * last one.
+   * @return the end of the children iterator.
+   */
+  inline iterator end() {
+    return d_nv->end<ref_count>();
+  }
 
-    /**
-     * Returns the const_iterator pointing to the first child.
-     * @return the const_iterator
-     */
-    inline const_iterator begin() const {
-      return d_nv->begin<ref_count>();
-    }
+  /**
+   * Returns the const_iterator pointing to the first child.
+   * @return the const_iterator
+   */
+  inline const_iterator begin() const {
+    return d_nv->begin<ref_count>();
+  }
 
-    /**
-     * Returns the const_iterator pointing to the end of the children (one
-     * beyond the last one.
-     * @return the end of the children const_iterator.
-     */
-    inline const_iterator end() const {
-      return d_nv->end<ref_count>();
-    }
+  /**
+   * Returns the const_iterator pointing to the end of the children (one
+   * beyond the last one.
+   * @return the end of the children const_iterator.
+   */
+  inline const_iterator end() const {
+    return d_nv->end<ref_count>();
+  }
 
-    /**
-     * Converts this node into a string representation.
-     * @return the string representation of this node.
-     */
-    inline std::string toString() const {
-      return d_nv->toString();
-    }
+  /**
+   * Converts this node into a string representation.
+   * @return the string representation of this node.
+   */
+  inline std::string toString() const {
+    return d_nv->toString();
+  }
 
-    /**
-     * Converst this node into a string representation and sends it to the
-     * given stream
-     * @param out the sream to serialise this node to
-     */
-    inline void toStream(std::ostream& out) const {
-      d_nv->toStream(out);
-    }
+  /**
+   * Converst this node into a string representation and sends it to the
+   * given stream
+   * @param out the sream to serialise this node to
+   */
+  inline void toStream(std::ostream& out) const {
+    d_nv->toStream(out);
+  }
 
-    /**
-     * Very basic pretty printer for Node.
-     * @param o output stream to print to.
-     * @param indent number of spaces to indent the formula by.
-     */
-    void printAst(std::ostream & o, int indent = 0) const;
-
-    NodeTemplate<true> eqNode(const NodeTemplate& right) const;
-
-    NodeTemplate<true> notNode() const;
-    NodeTemplate<true> andNode(const NodeTemplate& right) const;
-    NodeTemplate<true> orNode(const NodeTemplate& right) const;
-    NodeTemplate<true> iteNode(const NodeTemplate& thenpart,
-                         const NodeTemplate& elsepart) const;
-    NodeTemplate<true> iffNode(const NodeTemplate& right) const;
-    NodeTemplate<true> impNode(const NodeTemplate& right) const;
-    NodeTemplate<true> xorNode(const NodeTemplate& right) const;
-
-  private:
-
-    /**
-     * Indents the given stream a given amount of spaces.
-     * @param out the stream to indent
-     * @param indent the numer of spaces
-     */
-    static void indent(std::ostream& out, int indent) {
-      for(int i = 0; i < indent; i++)
-        out << ' ';
-    }
+  /**
+   * Very basic pretty printer for Node.
+   * @param o output stream to print to.
+   * @param indent number of spaces to indent the formula by.
+   */
+  void printAst(std::ostream & o, int indent = 0) const;
+
+  NodeTemplate<true> eqNode(const NodeTemplate& right) const;
+
+  NodeTemplate<true> notNode() const;
+  NodeTemplate<true> andNode(const NodeTemplate& right) const;
+  NodeTemplate<true> orNode(const NodeTemplate& right) const;
+  NodeTemplate<true> iteNode(const NodeTemplate& thenpart,
+                             const NodeTemplate& elsepart) const;
+  NodeTemplate<true> iffNode(const NodeTemplate& right) const;
+  NodeTemplate<true> impNode(const NodeTemplate& right) const;
+  NodeTemplate<true> xorNode(const NodeTemplate& right) const;
+
+private:
+
+  /**
+   * Indents the given stream a given amount of spaces.
+   * @param out the stream to indent
+   * @param indent the numer of spaces
+   */
+  static void indent(std::ostream& out, int indent) {
+    for(int i = 0; i < indent; i++)
+      out << ' ';
+  }
 
-  };/* class NodeTemplate */
+};/* class NodeTemplate */
 
 /**
  * Serializes a given node to the given stream.
@@ -464,239 +410,313 @@ inline std::ostream& operator<<(std::ostream& out, const Node& node) {
 
 #include <ext/hash_map>
 
-// for hashtables
-namespace __gnu_cxx {
-template<>
-  struct hash<CVC4::Node> {
-    size_t operator()(const CVC4::Node& node) const {
-      return (size_t) node.hash();
-    }
-  };
-}/* __gnu_cxx namespace */
-
 #include "expr/attribute.h"
 #include "expr/node_manager.h"
 
 namespace CVC4 {
 
-template<bool ref_count>
-  inline size_t NodeTemplate<ref_count>::getNumChildren() const {
-    return d_nv->d_nchildren;
+// for hash_maps, hash_sets..
+struct NodeHashFcn {
+  size_t operator()(const CVC4::Node& node) const {
+    return (size_t) node.hash();
   }
+};
 
 template<bool ref_count>
-  template<class AttrKind>
-    inline typename AttrKind::value_type NodeTemplate<ref_count>::
-    getAttribute(const AttrKind&) const {
-      Assert( NodeManager::currentNM() != NULL,
+inline size_t NodeTemplate<ref_count>::getNumChildren() const {
+  return d_nv->d_nchildren;
+}
+
+template<bool ref_count>
+template<class AttrKind>
+inline typename AttrKind::value_type NodeTemplate<ref_count>::
+getAttribute(const AttrKind&) const {
+  Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-      return NodeManager::currentNM()->getAttribute(*this, AttrKind());
-    }
+  return NodeManager::currentNM()->getAttribute(*this, AttrKind());
+}
 
 template<bool ref_count>
-  template<class AttrKind>
-    inline bool NodeTemplate<ref_count>::
-    hasAttribute(const AttrKind&) const {
-      Assert( NodeManager::currentNM() != NULL,
+template<class AttrKind>
+inline bool NodeTemplate<ref_count>::
+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());
-    }
+  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,
+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 ?" );
-      return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
-    }
+  return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
+}
 
 template<bool ref_count>
-  template<class AttrKind>
-    inline void NodeTemplate<ref_count>::
-    setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
-      Assert( NodeManager::currentNM() != NULL,
+template<class AttrKind>
+inline void NodeTemplate<ref_count>::
+setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
+  Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-      NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
-    }
+  NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
+}
 
 template<bool ref_count>
-  NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&NodeValue::s_null);
+NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
 
 ////FIXME: This function is a major hack! Should be changed ASAP
 ////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:
-    case ITE:
-    case IFF:
-    case IMPLIES:
-    case OR:
-    case AND:
-      return false;
-    default:
-      return true;
-    }
+bool NodeTemplate<ref_count>::isAtomic() const {
+  using namespace kind;
+  switch(getKind()) {
+  case NOT:
+  case XOR:
+  case ITE:
+  case IFF:
+  case IMPLIES:
+  case OR:
+  case AND:
+    return false;
+  default:
+    return true;
   }
+}
 
 // FIXME: escape from type system convenient but is there a better
 // way?  Nodes conceptually don't change their expr values but of
 // course they do modify the refcount.  But it's nice to be able to
 // support node_iterators over const NodeValue*.  So.... hm.
 template<bool ref_count>
-  NodeTemplate<ref_count>::NodeTemplate(const NodeValue* ev) :
-    d_nv(const_cast<NodeValue*> (ev)) {
-    Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
-    if(ref_count)
-      d_nv->inc();
+NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
+  d_nv(const_cast<expr::NodeValue*> (ev)) {
+  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  if(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>
-  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();
+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(const NodeTemplate& e) {
-    Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
-    d_nv = e.d_nv;
-    if(ref_count)
-      d_nv->inc();
+NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& 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)
-      d_nv->dec();
-    Assert(ref_count || d_nv->d_rc > 0,
-           "Temporary node pointing to an expired node");
+NodeTemplate<ref_count>::~NodeTemplate() throw() {
+  DtorAssert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  if(ref_count) {
+    d_nv->dec();
   }
+  DtorAssert(ref_count || d_nv->d_rc > 0,
+             "Temporary node pointing to an expired node");
+}
 
 template<bool ref_count>
-  void NodeTemplate<ref_count>::assignNodeValue(NodeValue* ev) {
-    d_nv = ev;
-    if(ref_count)
-      d_nv->inc();
+void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
+  d_nv = ev;
+  if(ref_count) {
+    d_nv->inc();
   }
+}
 
 template<bool ref_count>
-  NodeTemplate<ref_count>& NodeTemplate<ref_count>::
-    operator=(const NodeTemplate& e) {
-    Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
-    Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
-    if(EXPECT_TRUE( d_nv != e.d_nv )) {
-      if(ref_count)
-        d_nv->dec();
-      d_nv = e.d_nv;
-      if(ref_count)
-        d_nv->inc();
+NodeTemplate<ref_count>& NodeTemplate<ref_count>::
+operator=(const NodeTemplate& e) {
+  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+  if(EXPECT_TRUE( d_nv != e.d_nv )) {
+    if(ref_count) {
+      d_nv->dec();
+    }
+    d_nv = e.d_nv;
+    if(ref_count) {
+      d_nv->inc();
     }
-    return *this;
   }
+  return *this;
+}
 
 template<bool ref_count>
-  NodeTemplate<ref_count>& NodeTemplate<ref_count>::
-    operator=(const NodeTemplate<!ref_count>& e) {
-    Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
-    Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
-    if(EXPECT_TRUE( d_nv != e.d_nv )) {
-      if(ref_count)
-        d_nv->dec();
-      d_nv = e.d_nv;
-      if(ref_count)
-        d_nv->inc();
+NodeTemplate<ref_count>& NodeTemplate<ref_count>::
+operator=(const NodeTemplate<!ref_count>& e) {
+  Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+  Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+  if(EXPECT_TRUE( d_nv != e.d_nv )) {
+    if(ref_count) {
+      d_nv->dec();
+    }
+    d_nv = e.d_nv;
+    if(ref_count) {
+      d_nv->inc();
     }
-    return *this;
   }
+  return *this;
+}
 
 template<bool ref_count>
-  NodeTemplate<true> NodeTemplate<ref_count>::eqNode(const NodeTemplate<
-      ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
-  }
+NodeTemplate<true> NodeTemplate<ref_count>::eqNode(const NodeTemplate<
+                                                   ref_count>& right) const {
+  return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
+}
 
 template<bool ref_count>
-  NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
-    return NodeManager::currentNM()->mkNode(kind::NOT, *this);
-  }
+NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
+  return NodeManager::currentNM()->mkNode(kind::NOT, *this);
+}
 
 template<bool ref_count>
-  NodeTemplate<true> NodeTemplate<ref_count>::andNode(const NodeTemplate<
-      ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
-  }
+NodeTemplate<true> NodeTemplate<ref_count>::andNode(const NodeTemplate<
+                                                    ref_count>& right) const {
+  return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
+}
 
 template<bool ref_count>
-  NodeTemplate<true> NodeTemplate<ref_count>::orNode(const NodeTemplate<
-      ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
-  }
+NodeTemplate<true> NodeTemplate<ref_count>::orNode(const NodeTemplate<
+                                                   ref_count>& right) const {
+  return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
+}
 
 template<bool ref_count>
-  NodeTemplate<true> NodeTemplate<ref_count>::iteNode(const NodeTemplate<
-      ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const {
-    return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
-  }
+NodeTemplate<true> NodeTemplate<ref_count>::iteNode(const NodeTemplate<
+                                                    ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const {
+  return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
+}
 
 template<bool ref_count>
-  NodeTemplate<true> NodeTemplate<ref_count>::iffNode(const NodeTemplate<
-      ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
-  }
+NodeTemplate<true> NodeTemplate<ref_count>::iffNode(const NodeTemplate<
+                                                    ref_count>& right) const {
+  return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
+}
 
 template<bool ref_count>
-  NodeTemplate<true> NodeTemplate<ref_count>::impNode(const NodeTemplate<
-      ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
-  }
+NodeTemplate<true> NodeTemplate<ref_count>::impNode(const NodeTemplate<
+                                                    ref_count>& right) const {
+  return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
+}
 
 template<bool ref_count>
-  NodeTemplate<true> NodeTemplate<ref_count>::xorNode(const NodeTemplate<
-      ref_count>& right) const {
-    return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
-  }
+NodeTemplate<true> NodeTemplate<ref_count>::xorNode(const NodeTemplate<
+                                                    ref_count>& right) const {
+  return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
+}
 
 template<bool ref_count>
-  void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
-    indent(out, ind);
-    out << '(';
-    out << getKind();
-    if(getKind() == kind::VARIABLE) {
-      out << ' ' << getId();
-
-    } else if(getNumChildren() >= 1) {
-      for(const_iterator child = begin(); child != end(); ++child) {
-        out << std::endl;
-        NodeTemplate((*child)).printAst(out, ind + 1);
-      }
+void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
+  indent(out, ind);
+  out << '(';
+  out << getKind();
+  if(getKind() == kind::VARIABLE) {
+    out << ' ' << getId();
+
+  } else if(getNumChildren() >= 1) {
+    for(const_iterator child = begin(); child != end(); ++child) {
       out << std::endl;
-      indent(out, ind);
+      NodeTemplate((*child)).printAst(out, ind + 1);
     }
-    out << ')';
+    out << std::endl;
+    indent(out, ind);
   }
+  out << ')';
+}
 
-template<bool ref_count>
-  const Type* NodeTemplate<ref_count>::getType() const {
-    Assert( NodeManager::currentNM() != NULL,
-        "There is no current CVC4::NodeManager associated to this thread.\n"
-        "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-    return NodeManager::currentNM()->getType(*this);
+/**
+ * Returns a node representing the operator of this expression.
+ * If this is an APPLY, then the operator will be a functional term.
+ * Otherwise, it will be a node with kind BUILTIN
+ */
+template <bool ref_count>
+NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
+  switch(Kind k = getKind()) {
+  case kind::APPLY:
+    /* The operator is the first child. */
+    return NodeTemplate<true>(d_nv->d_children[0]);
+
+  case kind::EQUAL:
+  case kind::ITE:
+  case kind::TUPLE:
+  case kind::NOT:
+  case kind::AND:
+  case kind::IFF:
+  case kind::IMPLIES:
+  case kind::OR:
+  case kind::XOR:
+  case kind::PLUS: {
+    /* Returns a BUILTIN node. */
+    /* TODO: construct a singleton at load-time? */
+    /* TODO: maybe keep a table like the TheoryOfTable ? */
+    NodeTemplate<true> n = NodeManager::currentNM()->mkNode(k);
+    return NodeManager::currentNM()->mkNode(kind::BUILTIN, n);
   }
 
+  case kind::FALSE:
+  case kind::TRUE:
+  case kind::SKOLEM:
+  case kind::VARIABLE:
+    IllegalArgument(*this, "getOperator() called on kind with no operator");
+
+  default:
+    Unhandled(getKind());
+  }
+}
+
+/**
+ * Returns true if the node has an operator (i.e., it's not a variable or a constant).
+ */
+template <bool ref_count>
+bool NodeTemplate<ref_count>::hasOperator() const {
+  switch(getKind()) {
+  case kind::APPLY:
+  case kind::EQUAL:
+  case kind::ITE:
+  case kind::TUPLE:
+  case kind::FALSE:
+  case kind::TRUE:
+  case kind::NOT:
+  case kind::AND:
+  case kind::IFF:
+  case kind::IMPLIES:
+  case kind::OR:
+  case kind::XOR:
+  case kind::PLUS:
+    return true;
+
+  case kind::SKOLEM:
+  case kind::VARIABLE:
+    return false;
+
+  default:
+    Unhandled(getKind());
+  }
+}
 
+template<bool ref_count>
+const Type* NodeTemplate<ref_count>::getType() const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  return NodeManager::currentNM()->getType(*this);
+}
 
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
@@ -721,7 +741,6 @@ static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n)
   Warning().flush();
 }
 
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_H */
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index f5da56d96..4dc3c06d0 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -63,20 +63,20 @@ class NodeBuilder {
   // extract another
   bool d_used;
 
-  NodeValue *d_nv;
-  NodeValue d_inlineNv;
-  NodeValue *d_childrenStorage[nchild_thresh];
+  expr::NodeValue *d_nv;
+  expr::NodeValue d_inlineNv;
+  expr::NodeValue *d_childrenStorage[nchild_thresh];
 
-  bool nvIsAllocated() {
+  bool nvIsAllocated() const {
     return d_nv->d_nchildren > nchild_thresh;
   }
 
   template <unsigned N>
-  bool nvIsAllocated(const NodeBuilder<N>& nb) {
+  bool nvIsAllocated(const NodeBuilder<N>& nb) const {
     return nb.d_nv->d_nchildren > N;
   }
 
-  bool evNeedsToBeAllocated() {
+  bool evNeedsToBeAllocated() const {
     return d_nv->d_nchildren == d_size;
   }
 
@@ -93,17 +93,31 @@ class NodeBuilder {
   }
 
   // dealloc: only call this with d_used == false and nvIsAllocated()
-  inline void dealloc();
+  inline void dealloc() throw();
 
   void crop() {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     if(EXPECT_FALSE( nvIsAllocated() ) && EXPECT_TRUE( d_size > d_nv->d_nchildren )) {
-      d_nv = (NodeValue*)
-        std::realloc(d_nv, sizeof(NodeValue) +
-                     ( sizeof(NodeValue*) * (d_size = d_nv->d_nchildren) ));
+      d_nv = (expr::NodeValue*)
+        std::realloc(d_nv, sizeof(expr::NodeValue) +
+                     ( sizeof(expr::NodeValue*) * (d_size = d_nv->d_nchildren) ));
     }
   }
 
+  NodeBuilder& collapseTo(Kind k) {
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+    AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR,
+                   k, "illegal collapsing kind");
+
+    if(getKind() != k) {
+      Node n = *this;
+      clear();
+      d_nv->d_kind = k;
+      append(n);
+    }
+    return *this;
+  }
+
 public:
 
   inline NodeBuilder();
@@ -112,67 +126,48 @@ public:
   template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb);
   inline NodeBuilder(NodeManager* nm);
   inline NodeBuilder(NodeManager* nm, Kind k);
-  inline ~NodeBuilder();
+  inline ~NodeBuilder() throw();
 
-  typedef NodeValue::iterator<true> iterator;
-  typedef NodeValue::iterator<true> const_iterator;
+  typedef expr::NodeValue::iterator<true> iterator;
+  typedef expr::NodeValue::iterator<true> const_iterator;
 
   const_iterator begin() const {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     return d_nv->begin<true>();
   }
 
   const_iterator end() const {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     return d_nv->end<true>();
   }
 
   Kind getKind() const {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     return d_nv->getKind();
   }
 
   unsigned getNumChildren() const {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     return d_nv->getNumChildren();
   }
 
   Node operator[](int i) const {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     Assert(i >= 0 && i < d_nv->getNumChildren());
     return Node(d_nv->d_children[i]);
   }
 
+  /**
+   * "Reset" this node builder (optionally setting a new kind for it),
+   * using the same memory as before.  This should leave the
+   * NodeBuilder<> in the state it was after initial construction.
+   */
   void clear(Kind k = kind::UNDEFINED_KIND);
 
-  // Compound expression constructors
-  /*
-  NodeBuilder& eqExpr(TNode right);
-  NodeBuilder& notExpr();
-  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&&(TNode right) { return andExpr(right); }
-  NodeBuilder& operator||(TNode 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_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     Assert(d_nv->getKind() == kind::UNDEFINED_KIND);
     d_nv->d_kind = k;
     return *this;
@@ -180,21 +175,21 @@ public:
 
   NodeBuilder& operator<<(TNode n) {
     // FIXME: collapse if ! UNDEFINED_KIND
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     return append(n);
   }
 
   // For pushing sequences of children
   NodeBuilder& append(const std::vector<Node>& children) {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     return append(children.begin(), children.end());
   }
 
   NodeBuilder& append(TNode n) {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     Debug("prop") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl;
     allocateEvIfNecessaryForAppend();
-    NodeValue* ev = n.d_nv;
+    expr::NodeValue* ev = n.d_nv;
     ev->inc();
     d_nv->d_children[d_nv->d_nchildren++] = ev;
     return *this;
@@ -202,209 +197,309 @@ public:
 
   template <class Iterator>
   NodeBuilder& append(const Iterator& begin, const Iterator& end) {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     for(Iterator i = begin; i != end; ++i) {
       append(*i);
     }
     return *this;
   }
 
-  // not const
   operator Node();
+  operator Node() const;
 
   inline void toStream(std::ostream& out) const {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
+    Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
     d_nv->toStream(out);
   }
 
-  AndNodeBuilder   operator&&(Node);
-  OrNodeBuilder    operator||(Node);
-  PlusNodeBuilder  operator+ (Node);
-  PlusNodeBuilder  operator- (Node);
-  MultNodeBuilder  operator* (Node);
+  NodeBuilder& operator&=(TNode);
+  NodeBuilder& operator|=(TNode);
+  NodeBuilder& operator+=(TNode);
+  NodeBuilder& operator-=(TNode);
+  NodeBuilder& operator*=(TNode);
 
   friend class AndNodeBuilder;
   friend class OrNodeBuilder;
   friend class PlusNodeBuilder;
   friend class MultNodeBuilder;
-  
+
   //Yet 1 more example of how terrifying C++ is as a language
   //This is needed for copy constructors of different sizes to access private fields
   template <unsigned N> friend class NodeBuilder;
 
 };/* class NodeBuilder */
 
+// TODO: add templatized NodeTemplate<ref_count> to all above and
+// below inlines for 'const [T]Node&' arguments?  Technically a lot of
+// time is spent in the TNode conversion and copy constructor, but
+// this should be optimized into a simple pointer copy (?)
+// TODO: double-check this.
+
 class AndNodeBuilder {
+public:
   NodeBuilder<> d_eb;
 
-public:
+  inline AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
+    d_eb.collapseTo(kind::AND);
+  }
 
-  AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
-    if(d_eb.d_nv->d_kind != kind::AND) {
-      Node n = d_eb;
-      d_eb.clear();
-      d_eb.d_nv->d_kind = kind::AND;
-      d_eb.append(n);
-    }
+  inline AndNodeBuilder(TNode a, TNode b) : d_eb(kind::AND) {
+    d_eb << a << b;
   }
 
-  AndNodeBuilder&   operator&&(Node);
-  OrNodeBuilder     operator||(Node);
+  template <bool rc>
+  inline AndNodeBuilder& operator&&(const NodeTemplate<rc>&);
 
-  operator NodeBuilder<>() { return d_eb; }
+  template <bool rc>
+  inline OrNodeBuilder operator||(const NodeTemplate<rc>&);
+
+  inline operator NodeBuilder<>() { return d_eb; }
+  inline operator Node() { return d_eb; }
 
 };/* class AndNodeBuilder */
 
 class OrNodeBuilder {
+public:
   NodeBuilder<> d_eb;
 
-public:
+  inline OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
+    d_eb.collapseTo(kind::OR);
+  }
 
-  OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
-    if(d_eb.d_nv->d_kind != kind::OR) {
-      Node n = d_eb;
-      d_eb.clear();
-      d_eb.d_nv->d_kind = kind::OR;
-      d_eb.append(n);
-    }
+  inline OrNodeBuilder(TNode a, TNode b) : d_eb(kind::OR) {
+    d_eb << a << b;
   }
 
-  AndNodeBuilder    operator&&(Node);
-  OrNodeBuilder&    operator||(Node);
+  template <bool rc>
+  inline AndNodeBuilder operator&&(const NodeTemplate<rc>&);
+
+  template <bool rc>
+  inline OrNodeBuilder& operator||(const NodeTemplate<rc>&);
 
-  operator NodeBuilder<>() { return d_eb; }
+  inline operator NodeBuilder<>() { return d_eb; }
+  inline operator Node() { return d_eb; }
 
 };/* class OrNodeBuilder */
 
 class PlusNodeBuilder {
+public:
   NodeBuilder<> d_eb;
 
-public:
+  inline PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
+    d_eb.collapseTo(kind::PLUS);
+  }
 
-  PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
-    if(d_eb.d_nv->d_kind != kind::PLUS) {
-      Node n = d_eb;
-      d_eb.clear();
-      d_eb.d_nv->d_kind = kind::PLUS;
-      d_eb.append(n);
-    }
+  inline PlusNodeBuilder(TNode a, TNode b) : d_eb(kind::PLUS) {
+    d_eb << a << b;
   }
 
-  PlusNodeBuilder&  operator+(Node);
-  PlusNodeBuilder&  operator-(Node);
-  MultNodeBuilder   operator*(Node);
+  template <bool rc>
+  inline PlusNodeBuilder& operator+(const NodeTemplate<rc>&);
+
+  template <bool rc>
+  inline PlusNodeBuilder& operator-(const NodeTemplate<rc>&);
+
+  template <bool rc>
+  inline MultNodeBuilder operator*(const NodeTemplate<rc>&);
 
-  operator NodeBuilder<>() { return d_eb; }
+  inline operator NodeBuilder<>() { return d_eb; }
+  inline operator Node() { return d_eb; }
 
 };/* class PlusNodeBuilder */
 
 class MultNodeBuilder {
+public:
   NodeBuilder<> d_eb;
 
-public:
+  inline MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
+    d_eb.collapseTo(kind::MULT);
+  }
 
-  MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
-    if(d_eb.d_nv->d_kind != kind::MULT) {
-      Node n = d_eb;
-      d_eb.clear();
-      d_eb.d_nv->d_kind = kind::MULT;
-      d_eb.append(n);
-    }
+  inline MultNodeBuilder(TNode a, TNode b) : d_eb(kind::MULT) {
+    d_eb << a << b;
   }
 
-  PlusNodeBuilder   operator+(Node);
-  PlusNodeBuilder   operator-(Node);
-  MultNodeBuilder&  operator*(Node);
+  template <bool rc>
+  inline PlusNodeBuilder operator+(const NodeTemplate<rc>&);
 
-  operator NodeBuilder<>() { return d_eb; }
+  template <bool rc>
+  inline PlusNodeBuilder operator-(const NodeTemplate<rc>&);
+
+  template <bool rc>
+  inline MultNodeBuilder& operator*(const NodeTemplate<rc>&);
+
+  inline operator NodeBuilder<>() { return d_eb; }
+  inline operator Node() { return d_eb; }
 
 };/* class MultNodeBuilder */
 
 template <unsigned nchild_thresh>
-inline AndNodeBuilder   NodeBuilder<nchild_thresh>::operator&&(Node e) {
-  return AndNodeBuilder(*this) && e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator&=(TNode e) {
+  return collapseTo(kind::AND).append(e);
 }
 
 template <unsigned nchild_thresh>
-inline OrNodeBuilder    NodeBuilder<nchild_thresh>::operator||(Node e) {
-  return OrNodeBuilder(*this) || e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator|=(TNode e) {
+  return collapseTo(kind::OR).append(e);
 }
 
 template <unsigned nchild_thresh>
-inline PlusNodeBuilder  NodeBuilder<nchild_thresh>::operator+ (Node e) {
-  return PlusNodeBuilder(*this) + e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator+=(TNode e) {
+  return collapseTo(kind::PLUS).append(e);
 }
 
 template <unsigned nchild_thresh>
-inline PlusNodeBuilder  NodeBuilder<nchild_thresh>::operator- (Node e) {
-  return PlusNodeBuilder(*this) - e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator-=(TNode e) {
+  return collapseTo(kind::PLUS).append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
 }
 
 template <unsigned nchild_thresh>
-inline MultNodeBuilder  NodeBuilder<nchild_thresh>::operator* (Node e) {
-  return MultNodeBuilder(*this) * e;
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator*=(TNode e) {
+  return collapseTo(kind::MULT).append(e);
 }
 
-inline AndNodeBuilder&  AndNodeBuilder::operator&&(Node e) {
-  d_eb.append(e);
+template <bool rc>
+inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate<rc>& n) {
+  d_eb.append(n);
   return *this;
 }
 
-inline OrNodeBuilder    AndNodeBuilder::operator||(Node e) {
-  Node n = d_eb;
-  d_eb.clear();
-  d_eb.append(n);
-  return OrNodeBuilder(d_eb) || e;
+template <bool rc>
+inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& n) {
+  return OrNodeBuilder(Node(d_eb), n);
 }
 
-inline AndNodeBuilder   OrNodeBuilder::operator&&(Node e) {
-  Node n = d_eb;
-  d_eb.clear();
+inline AndNodeBuilder& operator&&(AndNodeBuilder& a, const AndNodeBuilder& b) {
+  return a && Node(b.d_eb);
+}
+inline AndNodeBuilder& operator&&(AndNodeBuilder& a, const OrNodeBuilder& b) {
+  return a && Node(b.d_eb);
+}
+inline OrNodeBuilder operator||(AndNodeBuilder& a, const AndNodeBuilder& b) {
+  return a || Node(b.d_eb);
+}
+inline OrNodeBuilder operator||(AndNodeBuilder& a, const OrNodeBuilder& b) {
+  return a || Node(b.d_eb);
+}
+
+template <bool rc>
+inline AndNodeBuilder OrNodeBuilder::operator&&(const NodeTemplate<rc>& n) {
+  return AndNodeBuilder(Node(d_eb), n);
+}
+
+template <bool rc>
+inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate<rc>& n) {
   d_eb.append(n);
-  return AndNodeBuilder(d_eb) && e;
+  return *this;
 }
 
-inline OrNodeBuilder&   OrNodeBuilder::operator||(Node e) {
-  d_eb.append(e);
+inline AndNodeBuilder operator&&(OrNodeBuilder& a, const AndNodeBuilder& b) {
+  return a && Node(b.d_eb);
+}
+inline AndNodeBuilder operator&&(OrNodeBuilder& a, const OrNodeBuilder& b) {
+  return a && Node(b.d_eb);
+}
+inline OrNodeBuilder& operator||(OrNodeBuilder& a, const AndNodeBuilder& b) {
+  return a || Node(b.d_eb);
+}
+inline OrNodeBuilder& operator||(OrNodeBuilder& a, const OrNodeBuilder& b) {
+  return a || Node(b.d_eb);
+}
+
+template <bool rc>
+inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate<rc>& n) {
+  d_eb.append(n);
   return *this;
 }
 
-inline PlusNodeBuilder& PlusNodeBuilder::operator+(Node e) {
-  d_eb.append(e);
+template <bool rc>
+inline PlusNodeBuilder& PlusNodeBuilder::operator-(const NodeTemplate<rc>& n) {
+  d_eb.append(NodeManager::currentNM()->mkNode(kind::UMINUS, n));
   return *this;
 }
 
+template <bool rc>
+inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) {
+  return MultNodeBuilder(Node(d_eb), n);
+}
+
 /*
-inline PlusNodeBuilder& PlusNodeBuilder::operator-(Node e) {
-  d_eb.append(e.uMinusExpr());
+inline PlusNodeBuilder& PlusNodeBuilder::operator+(PlusNodeBuilder& b) { return *this + Node(d_eb); }
+inline PlusNodeBuilder& PlusNodeBuilder::operator+(MultNodeBuilder& b) { return *this + Node(d_eb); }
+inline PlusNodeBuilder& PlusNodeBuilder::operator-(PlusNodeBuilder& b) { return *this - Node(d_eb); }
+inline PlusNodeBuilder& PlusNodeBuilder::operator-(MultNodeBuilder& b) { return *this - Node(d_eb); }
+inline MultNodeBuilder PlusNodeBuilder::operator*(PlusNodeBuilder& b) { return *this * Node(d_eb); }
+inline MultNodeBuilder PlusNodeBuilder::operator*(MultNodeBuilder& b) { return *this * Node(d_eb); }
+*/
+
+template <bool rc>
+inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) {
+  return PlusNodeBuilder(Node(d_eb), n);
+}
+
+template <bool rc>
+inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) {
+  return PlusNodeBuilder(Node(d_eb), n);
+}
+
+template <bool rc>
+inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) {
+  d_eb.append(n);
   return *this;
 }
+
+/*
+inline PlusNodeBuilder MultNodeBuilder::operator+(const PlusNodeBuilder& b) { return *this + Node(d_eb); }
+inline PlusNodeBuilder MultNodeBuilder::operator+(const MultNodeBuilder& b) { return *this + Node(d_eb); }
+inline PlusNodeBuilder MultNodeBuilder::operator-(const PlusNodeBuilder& b) { return *this - Node(d_eb); }
+inline PlusNodeBuilder MultNodeBuilder::operator-(const MultNodeBuilder& b) { return *this - Node(d_eb); }
+inline MultNodeBuilder& MultNodeBuilder::operator*(const PlusNodeBuilder& b) { return *this * Node(d_eb); }
+inline MultNodeBuilder& MultNodeBuilder::operator*(const MultNodeBuilder& b) { return *this * Node(d_eb); }
 */
 
-inline MultNodeBuilder  PlusNodeBuilder::operator*(Node e) {
-  Node n = d_eb;
-  d_eb.clear();
-  d_eb.append(n);
-  return MultNodeBuilder(d_eb) * e;
+template <bool rc1, bool rc2>
+inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+  return AndNodeBuilder(a, b);
 }
 
-inline PlusNodeBuilder  MultNodeBuilder::operator+(Node e) {
-  Node n = d_eb;
-  d_eb.clear();
-  d_eb.append(n);
-  return MultNodeBuilder(d_eb) + e;
+template <bool rc1, bool rc2>
+inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+  return OrNodeBuilder(a, b);
 }
 
-inline PlusNodeBuilder  MultNodeBuilder::operator-(Node e) {
-  Node n = d_eb;
-  d_eb.clear();
-  d_eb.append(n);
-  return MultNodeBuilder(d_eb) - e;
+template <bool rc1, bool rc2>
+inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+  return PlusNodeBuilder(a, b);
 }
 
-inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) {
-  d_eb.append(e);
-  return *this;
+template <bool rc1, bool rc2>
+inline PlusNodeBuilder operator-(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+  return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b));
+}
+
+template <bool rc1, bool rc2>
+inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+  return MultNodeBuilder(a, b);
+}
+
+template <bool rc>
+inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, const AndNodeBuilder& b) {
+  return a && Node(b.d_eb);
+}
+
+template <bool rc>
+inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, const OrNodeBuilder& b) {
+  return a && Node(b.d_eb);
+}
+
+template <bool rc>
+inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, const AndNodeBuilder& b) {
+  return a || Node(b.d_eb);
+}
+
+template <bool rc>
+inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, const OrNodeBuilder& b) {
+  return a || Node(b.d_eb);
 }
 
 }/* CVC4 namespace */
@@ -436,7 +531,6 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
   d_inlineNv(0),
   d_childrenStorage() {
 
-  //Message() << "kind " << k << std::endl;
   d_inlineNv.d_kind = k;
 }
 
@@ -458,6 +552,11 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>&
   }
   d_nv->d_kind = nb.d_nv->d_kind;
   d_nv->d_nchildren = nb.d_nv->d_nchildren;
+  for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
+      i != d_nv->nv_end();
+      ++i) {
+    (*i)->inc();
+  }
 }
 
 template <unsigned nchild_thresh>
@@ -479,6 +578,11 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
   }
   d_nv->d_kind = nb.d_nv->d_kind;
   d_nv->d_nchildren = nb.d_nv->d_nchildren;
+  for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
+      i != d_nv->nv_end();
+      ++i) {
+    (*i)->inc();
+  }
 }
 
 template <unsigned nchild_thresh>
@@ -490,7 +594,7 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
   d_nv(&d_inlineNv),
   d_inlineNv(0),
   d_childrenStorage() {
-  d_inlineNv.d_kind = NodeValue::kindToDKind(kind::UNDEFINED_KIND);
+  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
 }
 
 template <unsigned nchild_thresh>
@@ -503,12 +607,11 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
   d_inlineNv(0),
   d_childrenStorage() {
 
-  //Message() << "kind " << k << std::endl;
   d_inlineNv.d_kind = k;
 }
 
 template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
+inline NodeBuilder<nchild_thresh>::~NodeBuilder() throw() {
   if(!d_used) {
     // Warning("NodeBuilder unused at destruction\n");
     // Commented above, as it happens a lot, for example with exceptions
@@ -536,12 +639,12 @@ void NodeBuilder<nchild_thresh>::clear(Kind k) {
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::realloc() {
   if(EXPECT_FALSE( nvIsAllocated() )) {
-    d_nv = (NodeValue*)
+    d_nv = (expr::NodeValue*)
       std::realloc(d_nv,
-                   sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) ));
+                   sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) ));
   } else {
-    d_nv = (NodeValue*)
-      std::malloc(sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) ));
+    d_nv = (expr::NodeValue*)
+      std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) ));
     d_nv->d_id = 0;
     d_nv->d_rc = 0;
     d_nv->d_kind = d_inlineNv.d_kind;
@@ -557,13 +660,13 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
   Assert( d_size < toSize );
 
   if(EXPECT_FALSE( nvIsAllocated() )) {
-    d_nv = (NodeValue*)
-      std::realloc(d_nv, sizeof(NodeValue) +
-                   ( sizeof(NodeValue*) * (d_size = toSize) ));
+    d_nv = (expr::NodeValue*)
+      std::realloc(d_nv, sizeof(expr::NodeValue) +
+                   ( sizeof(expr::NodeValue*) * (d_size = toSize) ));
   } else {
-    d_nv = (NodeValue*)
-      std::malloc(sizeof(NodeValue) +
-                  ( sizeof(NodeValue*) * (d_size = toSize) ));
+    d_nv = (expr::NodeValue*)
+      std::malloc(sizeof(expr::NodeValue) +
+                  ( sizeof(expr::NodeValue*) * (d_size = toSize) ));
     d_nv->d_id = 0;
     d_nv->d_rc = 0;
     d_nv->d_kind = d_inlineNv.d_kind;
@@ -579,14 +682,14 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
 }
 
 template <unsigned nchild_thresh>
-inline void NodeBuilder<nchild_thresh>::dealloc() {
+inline void NodeBuilder<nchild_thresh>::dealloc() throw() {
   /* Prefer asserts to if() because usually these conditions have been
    * checked already, so we don't want to do a double-check in
    * production; these are just sanity checks for debug builds */
-  Assert(!d_used,
-         "Internal error: NodeBuilder: dealloc() called with d_used");
+  DtorAssert(!d_used,
+             "Internal error: NodeBuilder: dealloc() called with d_used");
 
-  for(NodeValue::nv_iterator i = d_nv->nv_begin();
+  for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
       i != d_nv->nv_end();
       ++i) {
     (*i)->dec();
@@ -597,19 +700,109 @@ inline void NodeBuilder<nchild_thresh>::dealloc() {
 }
 
 template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator Node() const {// const version
+  Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
+  Assert(d_nv->getKind() != kind::UNDEFINED_KIND,
+         "Can't make an expression of an undefined kind!");
+
+  if(d_nv->d_kind == kind::VARIABLE) {
+    Assert(d_nv->d_nchildren == 0);
+    expr::NodeValue *nv = (expr::NodeValue*)
+      std::malloc(sizeof(expr::NodeValue) +
+                  (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF??
+    nv->d_nchildren = 0;
+    nv->d_kind = kind::VARIABLE;
+    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+    nv->d_rc = 0;
+    //d_used = true; // const version
+    //d_nv = NULL; // const version
+    return Node(nv);
+  }
+
+  // implementation differs depending on whether the expression value
+  // was malloc'ed or not
+
+  if(EXPECT_FALSE( nvIsAllocated() )) {
+    // Lookup the expression value in the pool we already have (with insert)
+    expr::NodeValue* nv = d_nm->poolLookup(d_nv);
+    // If something else is there, we reuse it
+    if(nv != NULL) {
+      // expression already exists in node manager
+      //dealloc(); // const version
+      //d_used = true; // const version
+      return Node(nv);
+    }
+    // Otherwise copy children out
+    nv = (expr::NodeValue*)
+      std::malloc(sizeof(expr::NodeValue) +
+                  ( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
+    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+    nv->d_rc = 0;
+    nv->d_kind = d_nv->d_kind;
+    nv->d_nchildren = d_nv->d_nchildren;
+    std::copy(d_nv->d_children,
+              d_nv->d_children + d_nv->d_nchildren,
+              nv->d_children);
+    // inc child refcounts
+    for(expr::NodeValue::nv_iterator i = nv->nv_begin();
+        i != nv->nv_end();
+        ++i) {
+      (*i)->inc();
+    }
+    d_nm->poolInsert(nv);
+    return Node(nv);
+  }
+
+  // Lookup the expression value in the pool we already have
+  expr::NodeValue* ev = d_nm->poolLookup(d_nv);
+  //DANGER d_nv should be ptr-to-const in the above line b/c it points to d_inlineNv
+  if(ev != NULL) {
+    // expression already exists in node manager
+    //d_used = true; // const version
+    Debug("prop") << "result: " << Node(ev) << std::endl;
+    return Node(ev);
+  }
+
+  // otherwise create the canonical expression value for this node
+  ev = (expr::NodeValue*)
+    std::malloc(sizeof(expr::NodeValue) +
+                ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
+  ev->d_nchildren = d_inlineNv.d_nchildren;
+  ev->d_kind = d_inlineNv.d_kind;
+  ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+  ev->d_rc = 0;
+  std::copy(d_inlineNv.d_children,
+            d_inlineNv.d_children + d_inlineNv.d_nchildren,
+            ev->d_children);
+  //d_used = true;
+  //d_nv = NULL;
+  //d_inlineNv.d_nchildren = 0;// inhibit decr'ing refcounts of children in dtor
+  // inc child refcounts
+  for(expr::NodeValue::nv_iterator i = ev->nv_begin();
+      i != ev->nv_end();
+      ++i) {
+    (*i)->inc();
+  }
+
+  // Make the new expression
+  d_nm->poolInsert(ev);
+  return Node(ev);
+}
+
+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_used, "NodeBuilder is one-shot only; attempt to access it after conversion");
   Assert(d_nv->getKind() != kind::UNDEFINED_KIND,
          "Can't make an expression of an undefined kind!");
 
   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 ));// FIXME :: WTF??
+    expr::NodeValue *nv = (expr::NodeValue*)
+      std::malloc(sizeof(expr::NodeValue) +
+                  (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF??
     nv->d_nchildren = 0;
     nv->d_kind = kind::VARIABLE;
-    nv->d_id = NodeValue::next_id++;// FIXME multithreading
+    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
     nv->d_rc = 0;
     d_used = true;
     d_nv = NULL;
@@ -622,7 +815,7 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
 
   if(EXPECT_FALSE( nvIsAllocated() )) {
     // Lookup the expression value in the pool we already have (with insert)
-    NodeValue* nv = d_nm->poolLookup(d_nv);
+    expr::NodeValue* nv = d_nm->poolLookup(d_nv);
     // If something else is there, we reuse it
     if(nv != NULL) {
       // expression already exists in node manager
@@ -631,19 +824,18 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
       Debug("prop") << "result: " << Node(nv) << std::endl;
       return Node(nv);
     }
-    // Otherwise crop and set the expression value to the allocate one
+    // Otherwise crop and set the expression value to the allocated one
     crop();
     nv = d_nv;
+    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
     d_nv = NULL;
     d_used = true;
     d_nm->poolInsert(nv);
-    Node n(nv);
-    Debug("prop") << "result: " << n << std::endl;
-    return n;
+    return Node(nv);
   }
 
   // Lookup the expression value in the pool we already have
-  NodeValue* ev = d_nm->poolLookup(&d_inlineNv);
+  expr::NodeValue* ev = d_nm->poolLookup(&d_inlineNv);
   if(ev != NULL) {
     // expression already exists in node manager
     d_used = true;
@@ -652,12 +844,12 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
   }
 
   // otherwise create the canonical expression value for this node
-  ev = (NodeValue*)
-    std::malloc(sizeof(NodeValue) +
-                ( sizeof(NodeValue*) * d_inlineNv.d_nchildren ));
+  ev = (expr::NodeValue*)
+    std::malloc(sizeof(expr::NodeValue) +
+                ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
   ev->d_nchildren = d_inlineNv.d_nchildren;
   ev->d_kind = d_inlineNv.d_kind;
-  ev->d_id = NodeValue::next_id++;// FIXME multithreading
+  ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading
   ev->d_rc = 0;
   std::copy(d_inlineNv.d_children,
             d_inlineNv.d_children + d_inlineNv.d_nchildren,
@@ -668,9 +860,7 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
 
   // Make the new expression
   d_nm->poolInsert(ev);
-  Node n(ev);
-  Debug("prop") << "result: " << n << std::endl;
-  return n;
+  return Node(ev);
 }
 
 template <unsigned nchild_thresh>
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 00fcf52c4..62bcc7516 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -29,16 +29,6 @@
 #include "expr/kind.h"
 #include "expr/expr.h"
 
-namespace __gnu_cxx {
-  template<>
-  struct hash<CVC4::NodeValue*> {
-    size_t operator()(const CVC4::NodeValue* nv) const {
-      return (size_t)nv->hash();
-    }
-  };
-}/* __gnu_cxx namespace */
-
-
 namespace CVC4 {
 
 class Type;
@@ -61,20 +51,21 @@ class NodeManager {
 
   template <unsigned> friend class CVC4::NodeBuilder;
 
-  typedef __gnu_cxx::hash_set<NodeValue*, __gnu_cxx::hash<NodeValue*>, NodeValue::NodeValueEq> NodeValueSet;
+  typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueHashFcn,
+                              expr::NodeValue::NodeValueEq> NodeValueSet;
   NodeValueSet d_nodeValueSet;
 
   expr::attr::AttributeManager d_attrManager;
 
-  NodeValue* poolLookup(NodeValue* nv) const;
-  void poolInsert(NodeValue* nv);
+  expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
+  void poolInsert(expr::NodeValue* nv);
 
   friend class NodeManagerScope;
 
 public:
 
   NodeManager() {
-    poolInsert( &NodeValue::s_null );
+    poolInsert( &expr::NodeValue::s_null );
   }
 
   static NodeManager* currentNM() { return s_current; }
@@ -152,7 +143,7 @@ public:
     Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
   }
 
-  ~NodeManagerScope() {
+  ~NodeManagerScope() throw() {
     NodeManager::s_current = d_oldNodeManager;
     Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n";
   }
@@ -224,9 +215,9 @@ 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!");
+inline void NodeManager::poolInsert(expr::NodeValue* nv) {
+  Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(),
+         "NodeValue already in the pool!");
   d_nodeValueSet.insert(nv);
 }
 
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index b95f8ff0a..5c5765011 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -24,6 +24,7 @@
 using namespace std;
 
 namespace CVC4 {
+namespace expr {
 
 size_t NodeValue::next_id = 1;
 
@@ -56,4 +57,5 @@ void NodeValue::toStream(std::ostream& out) const {
   }
 }
 
+}/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 0ad7ba559..523c5387b 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -98,7 +98,7 @@ class NodeValue {
   NodeValue(int);
 
   /** Destructor decrements the ref counts of its children */
-  ~NodeValue();
+  ~NodeValue() throw();
 
   typedef NodeValue** nv_iterator;
   typedef NodeValue const* const* const_nv_iterator;
@@ -165,17 +165,26 @@ public:
   }
 
   inline bool compareTo(const NodeValue* nv) const {
-    if(d_kind != nv->d_kind)
+    if(d_kind != nv->d_kind) {
       return false;
-    if(d_nchildren != nv->d_nchildren)
+    }
+
+    if(d_nchildren != nv->d_nchildren) {
       return false;
+    }
+
     const_nv_iterator i = nv_begin();
     const_nv_iterator j = nv->nv_begin();
     const_nv_iterator i_end = nv_end();
+
     while(i != i_end) {
-      if ((*i) != (*j)) return false;
-      ++i; ++j;
+      if((*i) != (*j)) {
+        return false;
+      }
+      ++i;
+      ++j;
     }
+
     return true;
   }
 
@@ -196,6 +205,7 @@ public:
   static inline unsigned kindToDKind(Kind k) {
     return ((unsigned) k) & kindMask;
   }
+
   static inline Kind dKindToKind(unsigned d) {
     return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
   }
@@ -215,7 +225,7 @@ inline NodeValue::NodeValue(int) :
   d_nchildren(0) {
 }
 
-inline NodeValue::~NodeValue() {
+inline NodeValue::~NodeValue() throw() {
   for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
     (*i)->dec();
   }
@@ -254,6 +264,13 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
   return d_children + d_nchildren;
 }
 
+// for hash_maps, hash_sets, ...
+struct NodeValueHashFcn {
+  size_t operator()(const CVC4::expr::NodeValue* nv) const {
+    return (size_t)nv->hash();
+  }
+};/* struct NodeValueHashFcn */
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index bfa38ec28..5838790a8 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -23,18 +23,15 @@
 
 #include <ext/hash_map>
 
-namespace __gnu_cxx {
-template<>
-  struct hash<std::string> {
-    size_t operator()(const std::string& str) const {
-      return hash<const char*>()(str.c_str());
-    }
-  };
-}/* __gnu_cxx namespace */
-
 namespace CVC4 {
 namespace parser {
 
+struct StringHashFcn {
+  size_t operator()(const std::string& str) const {
+    return __gnu_cxx::hash<const char*>()(str.c_str());
+  }
+};
+
 /**
  * Generic symbol table for looking up variables by name.
  */
@@ -44,12 +41,9 @@ class SymbolTable {
 private:
 
   /** The name to expression bindings */
-  typedef __gnu_cxx::hash_map<std::string, ObjectType>
+  typedef __gnu_cxx::hash_map<std::string, ObjectType, StringHashFcn>
   LookupTable;
-/*
-  typedef __gnu_cxx::hash_map<std::string, std::stack<ObjectType> >
-  LookupTable;
-*/
+
   /** The table iterator */
   typedef typename LookupTable::iterator table_iterator;
   /** The table iterator */
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index da3f7b1ed..9af15ba31 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -46,7 +46,7 @@ private:
   SatSolver *d_satSolver;
 
   /** Cache of what literal have been registered to a node. */
-  __gnu_cxx::hash_map<Node, SatLiteral> d_translationCache;
+  __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFcn> d_translationCache;
 
 protected:
 
diff --git a/src/util/Assert.h b/src/util/Assert.h
index 8f03ecd45..3b42f2887 100644
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -24,6 +24,8 @@
 #include "cvc4_config.h"
 #include "config.h"
 
+#include <cassert>
+
 namespace CVC4 {
 
 class CVC4_PUBLIC AssertionException : public Exception {
@@ -196,6 +198,8 @@ public:
       throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
     } \
   } while(0)
+#define DtorAlwaysAssert(cond, msg...) \
+  assert(EXPECT_TRUE( cond ))
 #define Unreachable(msg...) \
   throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define Unhandled(msg...) \
@@ -215,9 +219,11 @@ public:
 
 #ifdef CVC4_ASSERTIONS
 #  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
+#  define DtorAssert(cond, msg...) assert(EXPECT_TRUE( cond ))
 #  define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
 #else /* ! CVC4_ASSERTIONS */
 #  define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
+#  define DtorAssert(cond, msg...) /*EXPECT_TRUE( cond )*/
 #  define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
 #endif /* CVC4_ASSERTIONS */