* 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

1 files changed, 374 insertions, 184 deletions

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>