** Don't fear the files-changed list, almost all changes are in the **

** file-level documentation at the top of the sources.              **

This is the "make bugzilla stop bugging me" bugfix commit.

* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
  Updated documentation in the file.  Resolves bug #99.

* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
  moved into a separate file.  Partially resolves bug #100.

* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
  namespace) instead of metakind.h (where it was in CVC4::metakind).
  This clears up a warning (private #inclusion) from the SMT and SMT2
  parsers, and maybe makes more sense anyways, since this is based on
  the kind (and not the metakind) of an operator.

* Documentation improvement; doxygen top-level \file gestures, \brief
  gestures for files, etc.  Changed contrib/update-copyright.pl for
  this change, and post-processed to add \brief.  Resolves bug #98.

* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
  They no longer made sense.  Resolves bug #91.

29 files changed, 782 insertions, 831 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index c3c3fccf6..cacae45ce 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -12,6 +12,7 @@ libexpr_la_SOURCES = \
 	type_node.cpp \
 	builtin_type_rules.h \
 	node_builder.h \
+	convenience_node_builders.h \
 	@srcdir@/expr.h \
 	type.h \
 	type.cpp \
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index bc724cdd1..5aaa7393a 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** attribute.cpp
+/*! \file attribute.cpp
+ ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: dejan
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief AttributeManager implementation.
  **
  ** AttributeManager implementation.
  **/
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 619f60a6c..2ef34a771 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** attribute.h
+/*! \file attribute.h
+ ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: dejan
  ** Minor contributors (to current version): cconway, taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Node attributes.
  **
  ** Node attributes.
  **/
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 4ac89afec..b5ccb6f79 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** attribute_internals.h
+/*! \file attribute_internals.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan, taking, cconway
+ ** Minor contributors (to current version): taking, dejan, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Node attributes' internals.
  **
  ** Node attributes' internals.
  **/
diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h
index e0ad0b038..afd206260 100644
--- a/src/expr/builtin_type_rules.h
+++ b/src/expr/builtin_type_rules.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** builtin_type_rules.cpp
+/*! \file builtin_type_rules.cpp
+ ** \verbatim
  ** Original author: dejan
  ** Major contributors: none
  ** This file is part of the CVC4 prototype.
@@ -7,7 +8,11 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add brief comments here ]]
+ **
+ ** [[ Add file-specific comments here ]]
  **/
 
 #include "cvc4_private.h"
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 5fc9dee20..6c466a74c 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** command.cpp
+/*! \file command.cpp
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of command objects.
  **
  ** Implementation of command objects.
  **/
diff --git a/src/expr/command.h b/src/expr/command.h
index 5061722f6..388ad62e6 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** command.h
+/*! \file command.h
+ ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): cconway
+ ** Major contributors: cconway, dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of the command pattern on SmtEngines.
  **
  ** Implementation of the command pattern on SmtEngines.  Command
  ** objects are generated by the parser (typically) to implement the
diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h
new file mode 100644
index 000000000..655accde3
--- /dev/null
+++ b/src/expr/convenience_node_builders.h
@@ -0,0 +1,401 @@
+/*********************                                                        */
+/*! \file convenience_node_builders.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Convenience node builders.
+ **
+ ** These are convenience node builders for building AND, OR, PLUS,
+ ** and MULT expressions.
+ **
+ ** \todo These should be moved into theory code (say,
+ ** src/theory/booleans/node_builders.h and
+ ** src/theory/arith/node_builders.h), but for now they're here
+ ** because their design requires CVC4::NodeBuilder to friend them.
+ **/
+
+// TODO: add templatized NodeTemplate<ref_count> to all these 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.
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONVENIENCE_NODE_BUILDERS_H
+#define __CVC4__CONVENIENCE_NODE_BUILDERS_H
+
+#include "expr/node_builder.h"
+
+namespace CVC4 {
+
+class AndNodeBuilder {
+public:
+  NodeBuilder<> d_eb;
+
+  inline AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
+    d_eb.collapseTo(kind::AND);
+  }
+
+  inline AndNodeBuilder(TNode a, TNode b) : d_eb(kind::AND) {
+    d_eb << a << b;
+  }
+
+  template <bool rc>
+  inline AndNodeBuilder& operator&&(const NodeTemplate<rc>&);
+
+  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;
+
+  inline OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
+    d_eb.collapseTo(kind::OR);
+  }
+
+  inline OrNodeBuilder(TNode a, TNode b) : d_eb(kind::OR) {
+    d_eb << a << b;
+  }
+
+  template <bool rc>
+  inline AndNodeBuilder operator&&(const NodeTemplate<rc>&);
+
+  template <bool rc>
+  inline OrNodeBuilder& operator||(const NodeTemplate<rc>&);
+
+  inline operator NodeBuilder<>() { return d_eb; }
+  inline operator Node() { return d_eb; }
+
+};/* class OrNodeBuilder */
+
+class PlusNodeBuilder {
+public:
+  NodeBuilder<> d_eb;
+
+  inline PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
+    d_eb.collapseTo(kind::PLUS);
+  }
+
+  inline PlusNodeBuilder(TNode a, TNode b) : d_eb(kind::PLUS) {
+    d_eb << a << b;
+  }
+
+  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>&);
+
+  inline operator NodeBuilder<>() { return d_eb; }
+  inline operator Node() { return d_eb; }
+
+};/* class PlusNodeBuilder */
+
+class MultNodeBuilder {
+public:
+  NodeBuilder<> d_eb;
+
+  inline MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
+    d_eb.collapseTo(kind::MULT);
+  }
+
+  inline MultNodeBuilder(TNode a, TNode b) : d_eb(kind::MULT) {
+    d_eb << a << b;
+  }
+
+  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>&);
+
+  inline operator NodeBuilder<>() { return d_eb; }
+  inline operator Node() { return d_eb; }
+
+};/* class MultNodeBuilder */
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator&=(TNode e) {
+  return collapseTo(kind::AND).append(e);
+}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator|=(TNode e) {
+  return collapseTo(kind::OR).append(e);
+}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator+=(TNode e) {
+  return collapseTo(kind::PLUS).append(e);
+}
+
+template <unsigned nchild_thresh>
+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 NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator*=(TNode e) {
+  return collapseTo(kind::MULT).append(e);
+}
+
+template <bool rc>
+inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate<rc>& n) {
+  d_eb.append(n);
+  return *this;
+}
+
+template <bool rc>
+inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& n) {
+  return OrNodeBuilder(Node(d_eb), n);
+}
+
+inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
+                                  const AndNodeBuilder& b) {
+  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
+                                  const OrNodeBuilder& b) {
+  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline OrNodeBuilder operator||(AndNodeBuilder& a,
+                                const AndNodeBuilder& b) {
+  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline OrNodeBuilder operator||(AndNodeBuilder& a,
+                                const OrNodeBuilder& b) {
+  return a || Node(const_cast<NodeBuilder<>&>(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 *this;
+}
+
+inline AndNodeBuilder operator&&(OrNodeBuilder& a,
+                                 const AndNodeBuilder& b) {
+  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline AndNodeBuilder operator&&(OrNodeBuilder& a,
+                                 const OrNodeBuilder& b) {
+  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline OrNodeBuilder& operator||(OrNodeBuilder& a,
+                                 const AndNodeBuilder& b) {
+  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline OrNodeBuilder& operator||(OrNodeBuilder& a,
+                                 const OrNodeBuilder& b) {
+  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate<rc>& n) {
+  d_eb.append(n);
+  return *this;
+}
+
+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& operator+(PlusNodeBuilder& a,
+                                  const PlusNodeBuilder& b) {
+  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline PlusNodeBuilder& operator+(PlusNodeBuilder& a,
+                                  const MultNodeBuilder& b) {
+  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline PlusNodeBuilder& operator-(PlusNodeBuilder&a,
+                                  const PlusNodeBuilder& b) {
+  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline PlusNodeBuilder& operator-(PlusNodeBuilder& a,
+                                  const MultNodeBuilder& b) {
+  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline MultNodeBuilder operator*(PlusNodeBuilder& a,
+                                 const PlusNodeBuilder& b) {
+  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline MultNodeBuilder operator*(PlusNodeBuilder& a,
+                                 const MultNodeBuilder& b) {
+  return a * Node(const_cast<NodeBuilder<>&>(b.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),
+                         NodeManager::currentNM()->mkNode(kind::UMINUS, n));
+}
+
+template <bool rc>
+inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) {
+  d_eb.append(n);
+  return *this;
+}
+
+inline PlusNodeBuilder operator+(MultNodeBuilder& a,
+                                 const PlusNodeBuilder& b) {
+  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline PlusNodeBuilder operator+(MultNodeBuilder& a,
+                                 const MultNodeBuilder& b) {
+  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline PlusNodeBuilder operator-(MultNodeBuilder& a,
+                                 const PlusNodeBuilder& b) {
+  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline PlusNodeBuilder operator-(MultNodeBuilder& a,
+                                 const MultNodeBuilder& b) {
+  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline MultNodeBuilder& operator*(MultNodeBuilder& a,
+                                  const PlusNodeBuilder& b) {
+  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+inline MultNodeBuilder& operator*(MultNodeBuilder& a,
+                                  const MultNodeBuilder& b) {
+  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc1, bool rc2>
+inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a,
+                                 const NodeTemplate<rc2>& b) {
+  return AndNodeBuilder(a, b);
+}
+
+template <bool rc1, bool rc2>
+inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a,
+                                const NodeTemplate<rc2>& b) {
+  return OrNodeBuilder(a, b);
+}
+
+template <bool rc1, bool rc2>
+inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a,
+                                 const NodeTemplate<rc2>& b) {
+  return PlusNodeBuilder(a, b);
+}
+
+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(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a,
+                                 const OrNodeBuilder& b) {
+  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
+                                const AndNodeBuilder& b) {
+  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
+                                const OrNodeBuilder& b) {
+  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
+                                 const PlusNodeBuilder& b) {
+  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
+                                 const MultNodeBuilder& b) {
+  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
+                                 const PlusNodeBuilder& b) {
+  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
+                                 const MultNodeBuilder& b) {
+  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
+                                 const PlusNodeBuilder& b) {
+  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
+                                 const MultNodeBuilder& b) {
+  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
+}
+
+template <bool rc>
+inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) {
+  return NodeManager::currentNM()->mkNode(kind::UMINUS, a);
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONVENIENCE_NODE_BUILDERS_H */
diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index 6dc9453d2..761dd6d24 100644
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -1,12 +1,17 @@
 /*********************                                                        */
-/** declaration_scope.cpp
+/*! \file declaration_scope.cpp
+ ** \verbatim
  ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Convenience class for scoping variable and type declarations (implementation).
  **
  ** Convenience class for scoping variable and type declarations (implementation)
  **/
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index e33aa25fa..a6947c536 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -1,12 +1,17 @@
 /*********************                                                        */
-/** context.h
+/*! \file declaration_scope.h
+ ** \verbatim
  ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Convenience class for scoping variable and type declarations.
  **
  ** Convenience class for scoping variable and type declarations.
  **/
diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index 38f8fc787..cb983b006 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -1,9 +1,21 @@
-/*
- * expr_manager_scope.h
- *
- *  Created on: Apr 7, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file expr_manager_scope.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 #ifndef __CVC4__EXPR_MANAGER_SCOPE_H
 #define __CVC4__EXPR_MANAGER_SCOPE_H
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index bf0e2f96e..3eb2a8109 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** expr_manager_template.cpp
+/*! \file expr_manager_template.cpp
+ ** \verbatim
  ** Original author: dejan
  ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Public-facing expression manager interface, implementation.
  **
  ** Public-facing expression manager interface, implementation.
  **/
@@ -71,17 +74,6 @@ BitVectorType ExprManager::bitVectorType(unsigned size) const {
   return Type(d_nodeManager, new TypeNode(d_nodeManager->bitVectorType(size)));
 }
 
-Expr ExprManager::mkExpr(Kind kind) {
-  const unsigned n = 0;
-  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
-                "Exprs with kind %s must have at least %u children and "
-                "at most %u children (the one under construction has %u)",
-                kind::kindToString(kind).c_str(),
-                minArity(kind), maxArity(kind), n);
-  NodeManagerScope nms(d_nodeManager);
-  return Expr(this, d_nodeManager->mkNodePtr(kind));
-}
-
 Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
   const unsigned n = 1;
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
@@ -252,7 +244,7 @@ Expr ExprManager::mkVar(const Type& type) {
 
 Expr ExprManager::mkAssociative(Kind kind,
                                 const std::vector<Expr>& children) {
-  CheckArgument( metakind::isAssociative(kind), kind,
+  CheckArgument( kind::isAssociative(kind), kind,
                  "Illegal kind in mkAssociative: %s",
                  kind::kindToString(kind).c_str());
 
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 4cde091ac..707d9a26e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** expr_manager_template.h
+/*! \file expr_manager_template.h
+ ** \verbatim
  ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): taking, cconway
+ ** Major contributors: cconway, mdeters
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Public-facing expression manager interface.
  **
  ** Public-facing expression manager interface.
  **/
@@ -101,13 +104,6 @@ public:
   BitVectorType bitVectorType(unsigned size) const;
 
   /**
-   * Make a unary expression of a given kind (TRUE, FALSE,...).
-   * @param kind the kind of expression
-   * @return the expression
-   */
-  Expr mkExpr(Kind kind);
-
-  /**
    * Make a unary expression of a given kind (NOT, BVNOT, ...).
    * @param child1 kind the kind of expression
    * @return the expression
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index edd49f032..b4359cf2a 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** expr_template.cpp
+/*! \file expr_template.cpp
+ ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
- ** Minor contributors (to current version): cconway, taking
+ ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Public-facing expression interface, implementation.
  **
  ** Public-facing expression interface, implementation.
  **/
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 6597d5f14..73aa666e6 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** expr_template.h
+/*! \file expr_template.h
+ ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
  ** Minor contributors (to current version): cconway, taking
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Public-facing expression interface.
  **
  ** Public-facing expression interface.
  **/
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 96c34a02a..718fd58f4 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** kind_template.h
+/*! \file kind_template.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
  ** Minor contributors (to current version): none
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Template for the Node kind header.
  **
  ** Template for the Node kind header.
  **/
@@ -57,6 +60,23 @@ ${kind_printers}
   return out;
 }
 
+/** Returns true if the given kind is associative. This is used by ExprManager to
+ * decide whether it's safe to modify big expressions by changing the grouping of
+ * the arguments. */
+/* TODO: This could be generated. */
+inline bool isAssociative(::CVC4::Kind k) {
+  switch(k) {
+  case kind::AND:
+  case kind::OR:
+  case kind::MULT:
+  case kind::PLUS:
+    return true;
+
+  default:
+    return false;
+  }
+}
+
 inline std::string kindToString(::CVC4::Kind k) {
   std::stringstream ss;
   ss << k;
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index fc0910893..079199359 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** metakind_template.h
+/*! \file metakind_template.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Template for the metakind header.
  **
  ** Template for the metakind header.
  **/
@@ -294,23 +297,6 @@ ${metakind_ubchildren}
   return ubs[k];
 }
 
-/** Returns true if the given kind is associative. This is used by ExprManager to
- * decide whether it's safe to modify big expressions by changing the grouping of
- * the arguments. */
-/* TODO: This could be generated. */
-inline bool isAssociative(::CVC4::Kind k) {
-  switch(k) {
-  case kind::AND:
-  case kind::OR:
-  case kind::MULT:
-  case kind::PLUS:
-    return true;
-
-  default:
-    return false;
-  }
-}
-
 }/* CVC4::kind::metakind namespace */
 }/* CVC4::kind namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 7ebea8a70..2b6417e8a 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** node.cpp
+/*! \file node.cpp
+ ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: dejan
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Reference-counted encapsulation of a pointer to node information.
  **
  ** Reference-counted encapsulation of a pointer to node information.
  **/
diff --git a/src/expr/node.h b/src/expr/node.h
index 0daa3f58c..cfaab142d 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** node.h
+/*! \file node.h
+ ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): cconway, taking
+ ** Major contributors: cconway, dejan
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Reference-counted encapsulation of a pointer to node information.
  **
  ** Reference-counted encapsulation of a pointer to node information.
  **/
@@ -138,8 +141,8 @@ class NodeTemplate {
   friend class NodeTemplate<false>;
   friend class NodeManager;
 
-  template <class Builder>
-  friend class NodeBuilderBase;
+  template <unsigned nchild_thresh>
+  friend class NodeBuilder;
 
   friend class ::CVC4::expr::attr::AttributeManager;
 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 877c50d82..d81190d7a 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** node_builder.h
+/*! \file node_builder.h
+ ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): taking, dejan
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A builder interface for Nodes.
  **
  ** A builder interface for Nodes.
  **
@@ -101,12 +104,12 @@
  **         returned in a Node wrapper.
  **
  ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper
- ** temporary for the NodeValue in the NodeBuilderBase<>::operator
- ** Node() member function.  If we create a temporary (for example by
- ** writing Debug("builder") << Node(nv) << endl), the NodeValue will
- ** have its reference count incremented from zero to one, then
- ** decremented, which makes it eligible for collection before the
- ** builder has even returned it!  So this is a no-no.
+ ** temporary for the NodeValue in the NodeBuilder<>::operator Node()
+ ** member function.  If we create a temporary (for example by writing
+ ** Debug("builder") << Node(nv) << endl), the NodeValue will have its
+ ** reference count incremented from zero to one, then decremented,
+ ** which makes it eligible for collection before the builder has even
+ ** returned it!  So this is a no-no.
  **
  ** There are also two cases when the NodeBuilder is clear()'ed:
  **
@@ -131,32 +134,10 @@
  **      d_nv is deallocated.
  **
  ** Regarding the backing store (typically on the stack): the file
- ** below provides three classes (two of them are templates):
- **
- **   template <class Builder> class NodeBuilderBase;
- **
- **     This is the base class for node builders.  It can not be used
- **     directly.  It contains a shared implementation but is intended
- **     to be subclassed.  Derived classes supply its "in-line" buffer.
- **
- **   class BackedNodeBuilder;
- **
- **     This is the usable form for a user-supplied-backing-store node
- **     builder.  A user can allocate a buffer large enough for a
- **     NodeValue with N children (say, on the stack), then pass a
- **     pointer to this buffer, and the parameter N, to a
- **     BackedNodeBuilder.  It will use this buffer to build its
- **     NodeValue until the number of children exceeds N; then it will
- **     allocate d_nv on the heap.
- **
- **     To ensure that the buffer is properly-sized, it is recommended
- **     to use the makeStackNodeBuilder(b, N) macro to make a
- **     BackedNodeBuilder "b" with a stack-allocated buffer large
- **     enough to hold N children.
+ ** below provides the template:
  **
  **   template <unsigned nchild_thresh> class NodeBuilder;
  **
- **     This is the conceptually easiest form of NodeBuilder to use.
  **     The default:
  **
  **       NodeBuilder<> b;
@@ -164,9 +145,7 @@
  **     gives you a backing buffer with capacity for 10 children in
  **     the same place as the NodeBuilder<> itself is allocated.  You
  **     can specify another size as a template parameter, but it must
- **     be a compile-time constant (which is why the BackedNodeBuilder
- **     creator-macro "makeStackNodeBuilder(b, N)" is sometimes
- **     preferred).
+ **     be a compile-time constant.
  **/
 
 #include "cvc4_private.h"
@@ -185,8 +164,8 @@
 namespace CVC4 {
   static const unsigned default_nchild_thresh = 10;
 
-  template <class Builder>
-  class NodeBuilderBase;
+  template <unsigned nchild_thresh>
+  class NodeBuilder;
 
   class NodeManager;
 }/* CVC4 namespace */
@@ -199,38 +178,31 @@ namespace CVC4 {
 
 namespace CVC4 {
 
-template <class Builder>
-inline std::ostream& operator<<(std::ostream&, const NodeBuilderBase<Builder>&);
+template <unsigned nchild_thresh>
+inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&);
 
+/* see expr/convenience_node_builders.h */
 class AndNodeBuilder;
 class OrNodeBuilder;
 class PlusNodeBuilder;
 class MultNodeBuilder;
 
 /**
- * A base class for NodeBuilders.  When extending this class, use:
- *
- *   class MyExtendedNodeBuilder :
- *       public NodeBuilderBase<MyExtendedNodeBuilder> { ... };
- *
- * This ensures that certain member functions return the right
- * (derived) class type.
- *
- * There are no virtual functions here, and that should remain the
- * case!  This class is just used for sharing of implementation.  Two
- * types derive from it: BackedNodeBuilder (which allows for an
- * external buffer), and the NodeBuilder<> template, which requires
- * that you give it a compile-time constant backing-store size.
+ * The main template NodeBuilder.
  */
-template <class Builder>
-class NodeBuilderBase {
-protected:
-
+template <unsigned nchild_thresh = default_nchild_thresh>
+class NodeBuilder {
   /**
-   * A reference to an "in-line" stack-allocated buffer for use by the
+   * An "in-line" stack-allocated buffer for use by the
    * NodeBuilder.
    */
-  expr::NodeValue& d_inlineNv;
+  expr::NodeValue d_inlineNv;
+  /**
+   * Space for the children of the node being constructed.  This is
+   * never accessed directly, but rather through
+   * d_inlineNv.d_children[i].
+   */
+  expr::NodeValue* d_inlineNvChildSpace[nchild_thresh];
 
   /**
    * A pointer to the "current" NodeValue buffer; either &d_inlineNv
@@ -242,16 +214,13 @@ protected:
   NodeManager* d_nm;
 
   /**
-   * The maximum number of children that can be held in this "in-line"
-   * buffer.
-   */
-  const uint16_t d_inlineNvMaxChildren;
-
-  /**
    * The number of children allocated in d_nv.
    */
   uint16_t d_nvMaxChildren;
 
+  template <unsigned N>
+  void internalCopy(const NodeBuilder<N>& nb);
+
   /**
    * Returns whether or not this NodeBuilder has been "used"---i.e.,
    * whether a Node has been extracted with operator Node().
@@ -267,7 +236,7 @@ protected:
   inline void setUsed() {
     Assert(!isUsed(), "Internal error: bad `used' state in NodeBuilder!");
     Assert(d_inlineNv.d_nchildren == 0 &&
-           d_nvMaxChildren == d_inlineNvMaxChildren,
+           d_nvMaxChildren == nchild_thresh,
            "Internal error: bad `inline' state in NodeBuilder!");
     d_nv = NULL;
   }
@@ -279,7 +248,7 @@ protected:
   inline void setUnused() {
     Assert(isUsed(), "Internal error: bad `used' state in NodeBuilder!");
     Assert(d_inlineNv.d_nchildren == 0 &&
-           d_nvMaxChildren == d_inlineNvMaxChildren,
+           d_nvMaxChildren == nchild_thresh,
            "Internal error: bad `inline' state in NodeBuilder!");
     d_nv = &d_inlineNv;
   }
@@ -377,7 +346,7 @@ protected:
     }
   }
 
-  Builder& collapseTo(Kind k) {
+  NodeBuilder<nchild_thresh>& collapseTo(Kind k) {
     AssertArgument(k != kind::UNDEFINED_KIND &&
                    k != kind::NULL_EXPR &&
                    k < kind::LAST_KIND,
@@ -389,27 +358,98 @@ protected:
       d_nv->d_kind = expr::NodeValue::kindToDKind(k);
       return append(n);
     }
-    return static_cast<Builder&>(*this);
+    return *this;
+  }
+
+public:
+
+  inline NodeBuilder() :
+    d_nv(&d_inlineNv),
+    d_nm(NodeManager::currentNM()),
+    d_nvMaxChildren(nchild_thresh) {
+
+    d_inlineNv.d_id = 0;
+    d_inlineNv.d_rc = 0;
+    d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
+    d_inlineNv.d_nchildren = 0;
   }
 
-protected:
+  inline NodeBuilder(Kind k) :
+    d_nv(&d_inlineNv),
+    d_nm(NodeManager::currentNM()),
+    d_nvMaxChildren(nchild_thresh) {
 
-  inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren,
-                         Kind k = kind::UNDEFINED_KIND);
-  inline NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren,
-                         NodeManager* nm, Kind k = kind::UNDEFINED_KIND);
+    Assert(k != kind::NULL_EXPR, "illegal Node-building kind");
 
-private:
-  // disallow copy or assignment of these base classes directly (there
-  // would be no backing store!)
-  NodeBuilderBase(const NodeBuilderBase& nb);
-  NodeBuilderBase& operator=(const NodeBuilderBase& nb);
+    d_inlineNv.d_id = 0;
+    d_inlineNv.d_rc = 0;
+    d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+    d_inlineNv.d_nchildren = 0;
+  }
 
-public:
+  inline NodeBuilder(NodeManager* nm) :
+    d_nv(&d_inlineNv),
+    d_nm(nm),
+    d_nvMaxChildren(nchild_thresh) {
+
+    d_inlineNv.d_id = 0;
+    d_inlineNv.d_rc = 0;
+    d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND);
+    d_inlineNv.d_nchildren = 0;
+  }
+
+  inline NodeBuilder(NodeManager* nm, Kind k) :
+    d_nv(&d_inlineNv),
+    d_nm(nm),
+    d_nvMaxChildren(nchild_thresh) {
+
+    Assert(k != kind::NULL_EXPR, "illegal Node-building kind");
 
-  // Intentionally not virtual; we don't want a vtable.  Don't
-  // override this in a derived class.
-  inline ~NodeBuilderBase();
+    d_inlineNv.d_id = 0;
+    d_inlineNv.d_rc = 0;
+    d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
+    d_inlineNv.d_nchildren = 0;
+  }
+
+  inline ~NodeBuilder() {
+    if(EXPECT_FALSE( nvIsAllocated() )) {
+      dealloc();
+    } else if(EXPECT_FALSE( !isUsed() )) {
+      decrRefCounts();
+    }
+  }
+
+  // These implementations are identical, but we need to have both of
+  // these because the templatized version isn't recognized as a
+  // generalization of a copy constructor (and a default copy
+  // constructor will be generated [?])
+  inline NodeBuilder(const NodeBuilder& nb) :
+    d_nv(&d_inlineNv),
+    d_nm(nb.d_nm),
+    d_nvMaxChildren(nchild_thresh) {
+
+    d_inlineNv.d_id = 0;
+    d_inlineNv.d_rc = 0;
+    d_inlineNv.d_kind = nb.d_nv->d_kind;
+    d_inlineNv.d_nchildren = 0;
+
+    internalCopy(nb);
+  }
+
+  // technically this is a conversion, not a copy
+  template <unsigned N>
+  inline NodeBuilder(const NodeBuilder<N>& nb) :
+    d_nv(&d_inlineNv),
+    d_nm(nb.d_nm),
+    d_nvMaxChildren(nchild_thresh) {
+
+    d_inlineNv.d_id = 0;
+    d_inlineNv.d_rc = 0;
+    d_inlineNv.d_kind = nb.d_nv->d_kind;
+    d_inlineNv.d_nchildren = 0;
+
+    internalCopy(nb);
+  }
 
   typedef expr::NodeValue::iterator< NodeTemplate<true>  > iterator;
   typedef expr::NodeValue::iterator< NodeTemplate<true> > const_iterator;
@@ -485,9 +525,9 @@ public:
    * allocated, and decrements the reference counts of any currently
    * children in the NodeBuilder.
    *
-   * This should leave the BackedNodeBuilder in the state it was after
+   * This should leave the NodeBuilder in the state it was after
    * initial construction, except for Kind, which is set to the
-   * argument (if provided), or UNDEFINED_KIND.  In particular, the
+   * argument, if provided, or UNDEFINED_KIND.  In particular, the
    * associated NodeManager is not affected by clear().
    */
   void clear(Kind k = kind::UNDEFINED_KIND);
@@ -495,7 +535,7 @@ public:
   // "Stream" expression constructor syntax
 
   /** Set the Kind of this Node-under-construction. */
-  inline Builder& operator<<(const Kind& k) {
+  inline NodeBuilder<nchild_thresh>& operator<<(const Kind& k) {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
     Assert(getKind() == kind::UNDEFINED_KIND,
@@ -505,7 +545,7 @@ public:
                    k < kind::LAST_KIND,
                    k, "illegal node-building kind");
     d_nv->d_kind = expr::NodeValue::kindToDKind(k);
-    return static_cast<Builder&>(*this);
+    return *this;
   }
 
   /**
@@ -514,7 +554,7 @@ public:
    * FIXME: do we really want that collapse behavior?  We had agreed
    * on it but then never wrote code like that.
    */
-  Builder& operator<<(TNode n) {
+  NodeBuilder<nchild_thresh>& operator<<(TNode n) {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
     /* FIXME: disable this "collapsing" for now..
@@ -527,7 +567,7 @@ public:
   }
 
   /** Append a sequence of children to this TypeNode-under-construction. */
-  inline Builder&
+  inline NodeBuilder<nchild_thresh>&
   append(const std::vector<TypeNode>& children) {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
@@ -536,7 +576,7 @@ public:
 
   /** Append a sequence of children to this Node-under-construction. */
   template <bool ref_count>
-  inline Builder&
+  inline NodeBuilder<nchild_thresh>&
   append(const std::vector<NodeTemplate<ref_count> >& children) {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
@@ -545,17 +585,17 @@ public:
 
   /** Append a sequence of children to this Node-under-construction. */
   template <class Iterator>
-  Builder& append(const Iterator& begin, const Iterator& end) {
+  NodeBuilder<nchild_thresh>& append(const Iterator& begin, const Iterator& end) {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
     for(Iterator i = begin; i != end; ++i) {
       append(*i);
     }
-    return static_cast<Builder&>(*this);
+    return *this;
   }
 
   /** Append a child to this Node-under-construction. */
-  Builder& append(TNode n) {
+  NodeBuilder<nchild_thresh>& append(TNode n) {
     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");
@@ -563,11 +603,11 @@ public:
     expr::NodeValue* nv = n.d_nv;
     nv->inc();
     d_nv->d_children[d_nv->d_nchildren++] = nv;
-    return static_cast<Builder&>(*this);
+    return *this;
   }
 
   /** Append a child to this Node-under-construction. */
-  Builder& append(const TypeNode& typeNode) {
+  NodeBuilder<nchild_thresh>& append(const TypeNode& typeNode) {
     Assert(!isUsed(), "NodeBuilder is one-shot only; "
            "attempt to access it after conversion");
     Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node");
@@ -575,7 +615,7 @@ public:
     expr::NodeValue* nv = typeNode.d_nv;
     nv->inc();
     d_nv->d_children[d_nv->d_nchildren++] = nv;
-    return static_cast<Builder&>(*this);
+    return *this;
   }
 
 private:
@@ -609,592 +649,38 @@ public:
     d_nv->toStream(out, depth);
   }
 
-  Builder& operator&=(TNode);
-  Builder& operator|=(TNode);
-  Builder& operator+=(TNode);
-  Builder& operator-=(TNode);
-  Builder& operator*=(TNode);
+  NodeBuilder<nchild_thresh>& operator&=(TNode);
+  NodeBuilder<nchild_thresh>& operator|=(TNode);
+  NodeBuilder<nchild_thresh>& operator+=(TNode);
+  NodeBuilder<nchild_thresh>& operator-=(TNode);
+  NodeBuilder<nchild_thresh>& operator*=(TNode);
 
   friend class AndNodeBuilder;
   friend class OrNodeBuilder;
   friend class PlusNodeBuilder;
   friend class MultNodeBuilder;
 
-};/* class NodeBuilderBase */
-
-/**
- * Backing-store interface version for NodeBuilders.  To construct one
- * of these, you need to create a backing store (preferably on the
- * stack) for it to hold its "inline" NodeValue.  There's a
- * convenience macro defined below, makeStackNodeBuilder(b, N),
- * defined below to define a stack-allocated BackedNodeBuilder "b"
- * with room for N children on the stack.
- */
-class BackedNodeBuilder : public NodeBuilderBase<BackedNodeBuilder> {
-public:
-  inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren) :
-    NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
-  }
-
-  inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, Kind k) :
-    NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
-  }
-
-  inline BackedNodeBuilder(expr::NodeValue* buf,
-                           unsigned maxChildren,
-                           NodeManager* nm) :
-    NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
-  }
-
-  inline BackedNodeBuilder(expr::NodeValue* buf,
-                           unsigned maxChildren,
-                           NodeManager* nm,
-                           Kind k) :
-    NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
-  }
-
-  // we don't want a vtable, so do not declare a dtor!
-  //inline ~BackedNodeBuilder();
-
-private:
-  // disallow copy or assignment (there would be no backing store!)
-  BackedNodeBuilder(const BackedNodeBuilder& nb);
-  BackedNodeBuilder& operator=(const BackedNodeBuilder& nb);
-
-};/* class BackedNodeBuilder */
-
-/**
- * Stack-allocate a BackedNodeBuilder with a stack-allocated backing
- * store of size __n.  The BackedNodeBuilder will be named __v.
- *
- * __v must be a simple name.  __n must be convertible to size_t, and
- * will be evaluated only once.  This macro may only be used where
- * declarations are permitted.
- */
-#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_backednodebuilder_nchildren__ ## __v)
-// IF THE ABOVE ASSERTION FAILS, write another compiler-specific
-// version of makeStackNodeBuilder() that works for your compiler
-// (even if it's suboptimal, ignoring its __n argument, and just
-// creates a NodeBuilder<10>).
-
-
-/**
- * Simple NodeBuilder interface.  This is a template that requires
- * that the number of children of the "inline"-allocated NodeValue be
- * specified as a template parameter (which means it must be a
- * compile-time constant).
- */
-template <unsigned nchild_thresh = default_nchild_thresh>
-class NodeBuilder : public NodeBuilderBase<NodeBuilder<nchild_thresh> > {
-  // This is messy:
-  // 1. This (anonymous) struct here must be a POD to avoid the
-  //    compiler laying out things in a different way.
-  // 2. The layout is engineered carefully.  We can't just
-  //    stack-allocate enough bytes as a char[] because we break
-  //    strict-aliasing rules.  The first thing in the struct is a
-  //    "NodeValue" so a pointer to this struct should be safely
-  //    castable to a pointer to a NodeValue (same alignment).
-  struct BackingStore {
-    expr::NodeValue n;
-    expr::NodeValue* c[nchild_thresh];
-  } d_backingStore;
-
-  typedef NodeBuilderBase<NodeBuilder<nchild_thresh> > super;
-
-  template <unsigned N>
-  void internalCopy(const NodeBuilder<N>& nb);
-
-public:
-  inline NodeBuilder() :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >
-      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
-       nchild_thresh) {
-  }
-
-  inline NodeBuilder(Kind k) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >
-      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
-       nchild_thresh,
-       k) {
-  }
-
-  inline NodeBuilder(NodeManager* nm) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >
-      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
-       nchild_thresh,
-       nm) {
-  }
-
-  inline NodeBuilder(NodeManager* nm, Kind k) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >
-      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
-       nchild_thresh,
-       nm,
-       k) {
-  }
-
-  // These implementations are identical, but we need to have both of
-  // these because the templatized version isn't recognized as a
-  // generalization of a copy constructor (and a default copy
-  // constructor will be generated [?])
-  inline NodeBuilder(const NodeBuilder& nb) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >
-      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
-       nchild_thresh,
-       nb.d_nm,
-       nb.getKind()) {
-    internalCopy(nb);
-  }
-
-  // technically this is a conversion, not a copy
-  template <unsigned N>
-  inline NodeBuilder(const NodeBuilder<N>& nb) :
-    NodeBuilderBase<NodeBuilder<nchild_thresh> >
-      (reinterpret_cast<expr::NodeValue*>(&d_backingStore),
-       nchild_thresh,
-       nb.d_nm,
-       nb.getKind()) {
-    internalCopy(nb);
-  }
-
-  // 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
   template <unsigned N>
   friend class NodeBuilder;
-
 };/* class NodeBuilder<> */
 
+}/* CVC4 namespace */
+
 // 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;
-
-  inline AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
-    d_eb.collapseTo(kind::AND);
-  }
-
-  inline AndNodeBuilder(TNode a, TNode b) : d_eb(kind::AND) {
-    d_eb << a << b;
-  }
-
-  template <bool rc>
-  inline AndNodeBuilder& operator&&(const NodeTemplate<rc>&);
-
-  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;
-
-  inline OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
-    d_eb.collapseTo(kind::OR);
-  }
-
-  inline OrNodeBuilder(TNode a, TNode b) : d_eb(kind::OR) {
-    d_eb << a << b;
-  }
-
-  template <bool rc>
-  inline AndNodeBuilder operator&&(const NodeTemplate<rc>&);
-
-  template <bool rc>
-  inline OrNodeBuilder& operator||(const NodeTemplate<rc>&);
-
-  inline operator NodeBuilder<>() { return d_eb; }
-  inline operator Node() { return d_eb; }
-
-};/* class OrNodeBuilder */
-
-class PlusNodeBuilder {
-public:
-  NodeBuilder<> d_eb;
-
-  inline PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
-    d_eb.collapseTo(kind::PLUS);
-  }
-
-  inline PlusNodeBuilder(TNode a, TNode b) : d_eb(kind::PLUS) {
-    d_eb << a << b;
-  }
-
-  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>&);
-
-  inline operator NodeBuilder<>() { return d_eb; }
-  inline operator Node() { return d_eb; }
-
-};/* class PlusNodeBuilder */
-
-class MultNodeBuilder {
-public:
-  NodeBuilder<> d_eb;
-
-  inline MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) {
-    d_eb.collapseTo(kind::MULT);
-  }
-
-  inline MultNodeBuilder(TNode a, TNode b) : d_eb(kind::MULT) {
-    d_eb << a << b;
-  }
-
-  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>&);
-
-  inline operator NodeBuilder<>() { return d_eb; }
-  inline operator Node() { return d_eb; }
-
-};/* class MultNodeBuilder */
-
-template <class Builder>
-inline Builder& NodeBuilderBase<Builder>::operator&=(TNode e) {
-  return collapseTo(kind::AND).append(e);
-}
-
-template <class Builder>
-inline Builder& NodeBuilderBase<Builder>::operator|=(TNode e) {
-  return collapseTo(kind::OR).append(e);
-}
-
-template <class Builder>
-inline Builder& NodeBuilderBase<Builder>::operator+=(TNode e) {
-  return collapseTo(kind::PLUS).append(e);
-}
-
-template <class Builder>
-inline Builder& NodeBuilderBase<Builder>::operator-=(TNode e) {
-  return collapseTo(kind::PLUS).
-    append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
-}
-
-template <class Builder>
-inline Builder& NodeBuilderBase<Builder>::operator*=(TNode e) {
-  return collapseTo(kind::MULT).append(e);
-}
-
-template <bool rc>
-inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate<rc>& n) {
-  d_eb.append(n);
-  return *this;
-}
-
-template <bool rc>
-inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& n) {
-  return OrNodeBuilder(Node(d_eb), n);
-}
-
-inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
-                                  const AndNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
-                                  const OrNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline OrNodeBuilder operator||(AndNodeBuilder& a,
-                                const AndNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline OrNodeBuilder operator||(AndNodeBuilder& a,
-                                const OrNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(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 *this;
-}
-
-inline AndNodeBuilder operator&&(OrNodeBuilder& a,
-                                 const AndNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline AndNodeBuilder operator&&(OrNodeBuilder& a,
-                                 const OrNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline OrNodeBuilder& operator||(OrNodeBuilder& a,
-                                 const AndNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline OrNodeBuilder& operator||(OrNodeBuilder& a,
-                                 const OrNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate<rc>& n) {
-  d_eb.append(n);
-  return *this;
-}
-
-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& operator+(PlusNodeBuilder& a,
-                                  const PlusNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder& operator+(PlusNodeBuilder& a,
-                                  const MultNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder& operator-(PlusNodeBuilder&a,
-                                  const PlusNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder& operator-(PlusNodeBuilder& a,
-                                  const MultNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline MultNodeBuilder operator*(PlusNodeBuilder& a,
-                                 const PlusNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline MultNodeBuilder operator*(PlusNodeBuilder& a,
-                                 const MultNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.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),
-                         NodeManager::currentNM()->mkNode(kind::UMINUS, n));
-}
-
-template <bool rc>
-inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) {
-  d_eb.append(n);
-  return *this;
-}
-
-inline PlusNodeBuilder operator+(MultNodeBuilder& a,
-                                 const PlusNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder operator+(MultNodeBuilder& a,
-                                 const MultNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder operator-(MultNodeBuilder& a,
-                                 const PlusNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder operator-(MultNodeBuilder& a,
-                                 const MultNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline MultNodeBuilder& operator*(MultNodeBuilder& a,
-                                  const PlusNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline MultNodeBuilder& operator*(MultNodeBuilder& a,
-                                  const MultNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc1, bool rc2>
-inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a,
-                                 const NodeTemplate<rc2>& b) {
-  return AndNodeBuilder(a, b);
-}
-
-template <bool rc1, bool rc2>
-inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a,
-                                const NodeTemplate<rc2>& b) {
-  return OrNodeBuilder(a, b);
-}
-
-template <bool rc1, bool rc2>
-inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a,
-                                 const NodeTemplate<rc2>& b) {
-  return PlusNodeBuilder(a, b);
-}
-
-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(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a,
-                                 const OrNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
-                                const AndNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
-                                const OrNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
-                                 const PlusNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
-                                 const MultNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
-                                 const PlusNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
-                                 const MultNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
-                                 const PlusNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
-                                 const MultNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) {
-  return NodeManager::currentNM()->mkNode(kind::UMINUS, a);
-}
-
-}/* CVC4 namespace */
-
 #include "expr/node.h"
 #include "expr/node_manager.h"
 
 namespace CVC4 {
 
-template <class Builder>
-inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf,
-                                                 unsigned maxChildren,
-                                                 Kind k) :
-  d_inlineNv(*buf),
-  d_nv(&d_inlineNv),
-  d_nm(NodeManager::currentNM()),
-  d_inlineNvMaxChildren(maxChildren),
-  d_nvMaxChildren(maxChildren) {
-
-  Assert(k != kind::NULL_EXPR, "illegal Node-building kind");
-
-  d_inlineNv.d_id = 0;
-  d_inlineNv.d_rc = 0;
-  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
-  d_inlineNv.d_nchildren = 0;
-}
-
-template <class Builder>
-inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf,
-                                                 unsigned maxChildren,
-                                                 NodeManager* nm,
-                                                 Kind k) :
-  d_inlineNv(*buf),
-  d_nv(&d_inlineNv),
-  d_nm(nm),
-  d_inlineNvMaxChildren(maxChildren),
-  d_nvMaxChildren(maxChildren) {
-
-  Assert(k != kind::NULL_EXPR, "illegal Node-building kind");
-
-  d_inlineNv.d_id = 0;
-  d_inlineNv.d_rc = 0;
-  d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
-  d_inlineNv.d_nchildren = 0;
-}
-
-template <class Builder>
-inline NodeBuilderBase<Builder>::~NodeBuilderBase() {
-  if(EXPECT_FALSE( nvIsAllocated() )) {
-    dealloc();
-  } else if(EXPECT_FALSE( !isUsed() )) {
-    decrRefCounts();
-  }
-}
-
-template <class Builder>
-void NodeBuilderBase<Builder>::clear(Kind k) {
+template <unsigned nchild_thresh>
+void NodeBuilder<nchild_thresh>::clear(Kind k) {
   Assert(k != kind::NULL_EXPR, "illegal Node-building clear kind");
 
   if(EXPECT_FALSE( nvIsAllocated() )) {
@@ -1214,8 +700,8 @@ void NodeBuilderBase<Builder>::clear(Kind k) {
   d_inlineNv.d_nchildren = 0;
 }
 
-template <class Builder>
-void NodeBuilderBase<Builder>::realloc(size_t toSize) {
+template <unsigned nchild_thresh>
+void NodeBuilder<nchild_thresh>::realloc(size_t toSize) {
   Assert( toSize > d_nvMaxChildren,
           "attempt to realloc() a NodeBuilder to a smaller/equal size!" );
 
@@ -1258,8 +744,8 @@ void NodeBuilderBase<Builder>::realloc(size_t toSize) {
   }
 }
 
-template <class Builder>
-void NodeBuilderBase<Builder>::dealloc() {
+template <unsigned nchild_thresh>
+void NodeBuilder<nchild_thresh>::dealloc() {
   Assert( nvIsAllocated(),
           "Internal error: NodeBuilder: dealloc() called without a "
           "private NodeBuilder-allocated buffer" );
@@ -1272,11 +758,11 @@ void NodeBuilderBase<Builder>::dealloc() {
 
   free(d_nv);
   d_nv = &d_inlineNv;
-  d_nvMaxChildren = d_inlineNvMaxChildren;
+  d_nvMaxChildren = nchild_thresh;
 }
 
-template <class Builder>
-void NodeBuilderBase<Builder>::decrRefCounts() {
+template <unsigned nchild_thresh>
+void NodeBuilder<nchild_thresh>::decrRefCounts() {
   Assert( !nvIsAllocated(),
           "Internal error: NodeBuilder: decrRefCounts() called with a "
           "private NodeBuilder-allocated buffer" );
@@ -1291,48 +777,48 @@ void NodeBuilderBase<Builder>::decrRefCounts() {
 }
 
 
-template <class Builder>
-TypeNode NodeBuilderBase<Builder>::constructTypeNode() {
+template <unsigned nchild_thresh>
+TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() {
   return TypeNode(constructNV());
 }
 
-template <class Builder>
-TypeNode NodeBuilderBase<Builder>::constructTypeNode() const {
+template <unsigned nchild_thresh>
+TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() const {
   return TypeNode(constructNV());
 }
 
-template <class Builder>
-Node NodeBuilderBase<Builder>::constructNode() {
+template <unsigned nchild_thresh>
+Node NodeBuilder<nchild_thresh>::constructNode() {
   return Node(constructNV());
 }
 
-template <class Builder>
-Node NodeBuilderBase<Builder>::constructNode() const {
+template <unsigned nchild_thresh>
+Node NodeBuilder<nchild_thresh>::constructNode() const {
   return Node(constructNV());
 }
 
-template <class Builder>
-Node* NodeBuilderBase<Builder>::constructNodePtr() {
+template <unsigned nchild_thresh>
+Node* NodeBuilder<nchild_thresh>::constructNodePtr() {
   return new Node(constructNV());
 }
 
-template <class Builder>
-Node* NodeBuilderBase<Builder>::constructNodePtr() const {
+template <unsigned nchild_thresh>
+Node* NodeBuilder<nchild_thresh>::constructNodePtr() const {
   return new Node(constructNV());
 }
 
-template <class Builder>
-NodeBuilderBase<Builder>::operator Node() {
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator Node() {
   return constructNode();
 }
 
-template <class Builder>
-NodeBuilderBase<Builder>::operator Node() const {
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator Node() const {
   return constructNode();
 }
 
-template <class Builder>
-expr::NodeValue* NodeBuilderBase<Builder>::constructNV() {
+template <unsigned nchild_thresh>
+expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
   Assert(!isUsed(), "NodeBuilder is one-shot only; "
          "attempt to access it after conversion");
   Assert(getKind() != kind::UNDEFINED_KIND,
@@ -1396,7 +882,7 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() {
 
   if(EXPECT_TRUE( ! nvIsAllocated() )) {
     /** Case 1.  d_nv points to d_inlineNv: it is the backing store
-     ** supplied by the user (or derived class) **/
+     ** allocated "inline" in this NodeBuilder. **/
 
     // Lookup the expression value in the pool we already have
     expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
@@ -1490,7 +976,7 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() {
       expr::NodeValue* nv = d_nv;
       nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
       d_nv = &d_inlineNv;
-      d_nvMaxChildren = d_inlineNvMaxChildren;
+      d_nvMaxChildren = nchild_thresh;
       setUsed();
 
       //poolNv = nv;
@@ -1503,8 +989,8 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() {
 }
 
 // CONST VERSION OF NODE EXTRACTOR
-template <class Builder>
-expr::NodeValue* NodeBuilderBase<Builder>::constructNV() const {
+template <unsigned nchild_thresh>
+expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
   Assert(!isUsed(), "NodeBuilder is one-shot only; "
          "attempt to access it after conversion");
   Assert(getKind() != kind::UNDEFINED_KIND,
@@ -1567,7 +1053,7 @@ expr::NodeValue* NodeBuilderBase<Builder>::constructNV() const {
 
   if(EXPECT_TRUE( ! nvIsAllocated() )) {
     /** Case 1.  d_nv points to d_inlineNv: it is the backing store
-     ** supplied by the user (or derived class) **/
+     ** allocated "inline" in this NodeBuilder. **/
 
     // Lookup the expression value in the pool we already have
     expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
@@ -1683,30 +1169,30 @@ template <unsigned nchild_thresh>
 template <unsigned N>
 void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
   if(nb.isUsed()) {
-    super::setUsed();
+    setUsed();
     return;
   }
 
-  if(nb.d_nvMaxChildren > super::d_nvMaxChildren) {
-    super::realloc(nb.d_nvMaxChildren);
+  if(nb.d_nvMaxChildren > d_nvMaxChildren) {
+    realloc(nb.d_nvMaxChildren);
   }
 
   std::copy(nb.d_nv->nv_begin(),
             nb.d_nv->nv_end(),
-            super::d_nv->nv_begin());
+            d_nv->nv_begin());
 
-  super::d_nv->d_nchildren = nb.d_nv->d_nchildren;
+  d_nv->d_nchildren = nb.d_nv->d_nchildren;
 
-  for(expr::NodeValue::nv_iterator i = super::d_nv->nv_begin();
-      i != super::d_nv->nv_end();
+  for(expr::NodeValue::nv_iterator i = d_nv->nv_begin();
+      i != d_nv->nv_end();
       ++i) {
     (*i)->inc();
   }
 }
 
-template <class Builder>
+template <unsigned nchild_thresh>
 inline std::ostream& operator<<(std::ostream& out,
-                                const NodeBuilderBase<Builder>& b) {
+                                const NodeBuilder<nchild_thresh>& b) {
   b.toStream(out, Node::setdepth::getDepth(out));
   return out;
 }
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index a1b5b771f..247348497 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** node_manager.cpp
+/*! \file node_manager.cpp
+ ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, taking
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): taking, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Expression manager implementation.
  **
  ** Expression manager implementation.
  **
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5642a8372..2d96ac57a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** node_manager.h
+/*! \file node_manager.h
+ ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway
- ** Minor contributors (to current version): taking, dejan
+ ** Major contributors: cconway, dejan
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief A manager for Nodes.
  **
  ** A manager for Nodes.
  **
@@ -50,7 +53,7 @@ typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr;
 }/* CVC4::expr namespace */
 
 class NodeManager {
-  template <class Builder> friend class CVC4::NodeBuilderBase;
+  template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
   friend class NodeManagerScope;
   friend class expr::NodeValue;
 
@@ -262,10 +265,6 @@ public:
 
   // general expression-builders
 
-  /** Create a node with no children. */
-  Node mkNode(Kind kind);
-  Node* mkNodePtr(Kind kind);
-
   /** Create a node with one child. */
   Node mkNode(Kind kind, TNode child1);
   Node* mkNodePtr(Kind kind, TNode child1);
@@ -740,15 +739,6 @@ inline TypeNode NodeManager::mkSort(const std::string& name) {
   return type;
 }
 
-inline Node NodeManager::mkNode(Kind kind) {
-  return NodeBuilder<0>(this, kind);
-}
-
-inline Node* NodeManager::mkNodePtr(Kind kind) {
-  NodeBuilder<0> nb(this, kind);
-  return nb.constructNodePtr();
-}
-
 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
   return NodeBuilder<1>(this, kind) << child1;
 }
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 101be5187..c64a608fb 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** node_value.cpp
+/*! \file node_value.cpp
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
  ** Minor contributors (to current version): cconway
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief An expression node.
  **
  ** An expression node.
  **
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 260a9daae..8b2056560 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -1,5 +1,6 @@
 /*********************                                                        */
-/** node_value.h
+/*! \file node_value.h
+ ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
  ** Minor contributors (to current version): cconway, taking
@@ -8,7 +9,9 @@
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief An expression node.
  **
  ** An expression node.
  **
@@ -35,7 +38,6 @@ namespace CVC4 {
 
 template <bool ref_count> class NodeTemplate;
 class TypeNode;
-template <class Builder> class NodeBuilderBase;
 template <unsigned N> class NodeBuilder;
 class AndNodeBuilder;
 class OrNodeBuilder;
@@ -103,7 +105,6 @@ class NodeValue {
 
   template <bool> friend class ::CVC4::NodeTemplate;
   friend class ::CVC4::TypeNode;
-  template <class Builder> friend class ::CVC4::NodeBuilderBase;
   template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder;
   friend class ::CVC4::NodeManager;
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index af333f9d3..3bacb4792 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** type.cpp
+/*! \file type.cpp
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of expression types .
  **
  ** Implementation of expression types 
  **/
diff --git a/src/expr/type.h b/src/expr/type.h
index 137dbfff3..2d18c2fc8 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** type.h
+/*! \file type.h
+ ** \verbatim
  ** Original author: cconway
- ** Major contributors: mdeters, dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Interface for expression types.
  **
  ** Interface for expression types
  **/
diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h
index a847bc827..0f5b522b6 100644
--- a/src/expr/type_constant.h
+++ b/src/expr/type_constant.h
@@ -1,13 +1,17 @@
 /*********************                                                        */
-/** type_constant.h
+/*! \file type_constant.h
+ ** \verbatim
  ** Original author: dejan
+ ** Major contributors: none
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Interface for expression types.
  **
  ** Interface for expression types
  **/
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 821349b45..1afaf2b89 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -1,14 +1,17 @@
 /*********************                                                        */
-/** node.cpp
+/*! \file type_node.cpp
+ ** \verbatim
  ** Original author: dejan
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Reference-counted encapsulation of a pointer to node information.
  **
  ** Reference-counted encapsulation of a pointer to node information.
  **/
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index f7b1a6b9e..9b67c674c 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -1,12 +1,17 @@
 /*********************                                                        */
-/** type_node.h
+/*! \file type_node.h
+ ** \verbatim
  ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
- ** information.
+ ** information.\endverbatim
+ **
+ ** \brief Reference-counted encapsulation of a pointer to node information.
  **
  ** Reference-counted encapsulation of a pointer to node information.
  **/
@@ -62,8 +67,8 @@ class TypeNode {
 
   friend class NodeManager;
 
-  template <class Builder>
-  friend class NodeBuilderBase;
+  template <unsigned nchild_thresh>
+  friend class NodeBuilder;
 
   /**
    * Assigns the expression value and does reference counting. No assumptions