A bag of unrelated fixes to bring trunk more in-line with recent

policy discussion (no dead code, no unimplemented unit tests...), and
other fixes:

* src/expr/node_builder.h: uncomment AndNodeBuilder, OrNodeBuilder,
  PlusNodeBuilder, and MultNodeBuilder.  (These had been dead code for
  awhile.)

* src/expr/node_value.cpp: toString() is much more reasonable now,
  printing S-exprs and using variable names (instead of printing raw
  pointer values).  Next, we'll want to define a pretty-printing
  theory interface and perhaps hook this up to that.

* test/unit/expr/node_black.h: implement testIterator(),
  testToString(), and testToStream().

* test/unit/expr/node_builder_black.h: implement testIterator() and
  testAppend(), and add some code to avoid the warnings on clear() for
  unused NodeBuilders.

* src/expr/node_builder.h: redefine "iterator" to be over Nodes rather
  than over NodeValues.  Doesn't make sense to expose the underlying
  NodeValues.  This shouldn't affect anyone, no one was using
  NodeBuilder iterators.

* fix some comments in source code

3 files changed, 84 insertions, 57 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index c1b2a87d2..f5da56d96 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -114,24 +114,17 @@ public:
   inline NodeBuilder(NodeManager* nm, Kind k);
   inline ~NodeBuilder();
 
-  typedef NodeValue::nv_iterator iterator;
-  typedef NodeValue::const_nv_iterator const_iterator;
+  typedef NodeValue::iterator<true> iterator;
+  typedef NodeValue::iterator<true> const_iterator;
 
-  iterator begin() {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    return d_nv->nv_begin();
-  }
-  iterator end() {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    return d_nv->nv_end();
-  }
   const_iterator begin() const {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    return d_nv->nv_begin();
+    return d_nv->begin<true>();
   }
+
   const_iterator end() const {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    return d_nv->nv_end();
+    return d_nv->end<true>();
   }
 
   Kind getKind() const {
@@ -186,6 +179,7 @@ public:
   }
 
   NodeBuilder& operator<<(TNode n) {
+    // FIXME: collapse if ! UNDEFINED_KIND
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
     return append(n);
   }
@@ -223,7 +217,6 @@ public:
     d_nv->toStream(out);
   }
 
-  /*
   AndNodeBuilder   operator&&(Node);
   OrNodeBuilder    operator||(Node);
   PlusNodeBuilder  operator+ (Node);
@@ -234,7 +227,6 @@ public:
   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
@@ -242,54 +234,59 @@ public:
 
 };/* class NodeBuilder */
 
-#if 0
 class AndNodeBuilder {
-  NodeBuilder d_eb;
+  NodeBuilder<> d_eb;
 
 public:
 
-  AndNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
-    if(d_eb.d_kind != AND) {
-      d_eb.collapse();
-      d_eb.d_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);
     }
   }
 
   AndNodeBuilder&   operator&&(Node);
   OrNodeBuilder     operator||(Node);
 
-  operator NodeBuilder() { return d_eb; }
+  operator NodeBuilder<>() { return d_eb; }
 
 };/* class AndNodeBuilder */
 
 class OrNodeBuilder {
-  NodeBuilder d_eb;
+  NodeBuilder<> d_eb;
 
 public:
 
-  OrNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
-    if(d_eb.d_kind != OR) {
-      d_eb.collapse();
-      d_eb.d_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);
     }
   }
 
   AndNodeBuilder    operator&&(Node);
   OrNodeBuilder&    operator||(Node);
 
-  operator NodeBuilder() { return d_eb; }
+  operator NodeBuilder<>() { return d_eb; }
 
 };/* class OrNodeBuilder */
 
 class PlusNodeBuilder {
-  NodeBuilder d_eb;
+  NodeBuilder<> d_eb;
 
 public:
 
-  PlusNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
-    if(d_eb.d_kind != PLUS) {
-      d_eb.collapse();
-      d_eb.d_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);
     }
   }
 
@@ -297,19 +294,21 @@ public:
   PlusNodeBuilder&  operator-(Node);
   MultNodeBuilder   operator*(Node);
 
-  operator NodeBuilder() { return d_eb; }
+  operator NodeBuilder<>() { return d_eb; }
 
 };/* class PlusNodeBuilder */
 
 class MultNodeBuilder {
-  NodeBuilder d_eb;
+  NodeBuilder<> d_eb;
 
 public:
 
-  MultNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
-    if(d_eb.d_kind != MULT) {
-      d_eb.collapse();
-      d_eb.d_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);
     }
   }
 
@@ -317,27 +316,32 @@ public:
   PlusNodeBuilder   operator-(Node);
   MultNodeBuilder&  operator*(Node);
 
-  operator NodeBuilder() { return d_eb; }
+  operator NodeBuilder<>() { return d_eb; }
 
 };/* class MultNodeBuilder */
 
-inline AndNodeBuilder   NodeBuilder::operator&&(Node e) {
+template <unsigned nchild_thresh>
+inline AndNodeBuilder   NodeBuilder<nchild_thresh>::operator&&(Node e) {
   return AndNodeBuilder(*this) && e;
 }
 
-inline OrNodeBuilder    NodeBuilder::operator||(Node e) {
+template <unsigned nchild_thresh>
+inline OrNodeBuilder    NodeBuilder<nchild_thresh>::operator||(Node e) {
   return OrNodeBuilder(*this) || e;
 }
 
-inline PlusNodeBuilder  NodeBuilder::operator+ (Node e) {
+template <unsigned nchild_thresh>
+inline PlusNodeBuilder  NodeBuilder<nchild_thresh>::operator+ (Node e) {
   return PlusNodeBuilder(*this) + e;
 }
 
-inline PlusNodeBuilder  NodeBuilder::operator- (Node e) {
+template <unsigned nchild_thresh>
+inline PlusNodeBuilder  NodeBuilder<nchild_thresh>::operator- (Node e) {
   return PlusNodeBuilder(*this) - e;
 }
 
-inline MultNodeBuilder  NodeBuilder::operator* (Node e) {
+template <unsigned nchild_thresh>
+inline MultNodeBuilder  NodeBuilder<nchild_thresh>::operator* (Node e) {
   return MultNodeBuilder(*this) * e;
 }
 
@@ -347,11 +351,17 @@ inline AndNodeBuilder&  AndNodeBuilder::operator&&(Node e) {
 }
 
 inline OrNodeBuilder    AndNodeBuilder::operator||(Node e) {
-  return OrNodeBuilder(d_eb.collapse()) || e;
+  Node n = d_eb;
+  d_eb.clear();
+  d_eb.append(n);
+  return OrNodeBuilder(d_eb) || e;
 }
 
 inline AndNodeBuilder   OrNodeBuilder::operator&&(Node e) {
-  return AndNodeBuilder(d_eb.collapse()) && e;
+  Node n = d_eb;
+  d_eb.clear();
+  d_eb.append(n);
+  return AndNodeBuilder(d_eb) && e;
 }
 
 inline OrNodeBuilder&   OrNodeBuilder::operator||(Node e) {
@@ -364,21 +374,32 @@ inline PlusNodeBuilder& PlusNodeBuilder::operator+(Node e) {
   return *this;
 }
 
+/*
 inline PlusNodeBuilder& PlusNodeBuilder::operator-(Node e) {
   d_eb.append(e.uMinusExpr());
   return *this;
 }
+*/
 
 inline MultNodeBuilder  PlusNodeBuilder::operator*(Node e) {
-  return MultNodeBuilder(d_eb.collapse()) * e;
+  Node n = d_eb;
+  d_eb.clear();
+  d_eb.append(n);
+  return MultNodeBuilder(d_eb) * e;
 }
 
 inline PlusNodeBuilder  MultNodeBuilder::operator+(Node e) {
-  return MultNodeBuilder(d_eb.collapse()) + e;
+  Node n = d_eb;
+  d_eb.clear();
+  d_eb.append(n);
+  return MultNodeBuilder(d_eb) + e;
 }
 
 inline PlusNodeBuilder  MultNodeBuilder::operator-(Node e) {
-  return MultNodeBuilder(d_eb.collapse()) - e;
+  Node n = d_eb;
+  d_eb.clear();
+  d_eb.append(n);
+  return MultNodeBuilder(d_eb) - e;
 }
 
 inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) {
@@ -386,8 +407,6 @@ inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) {
   return *this;
 }
 
-#endif /* 0 */
-
 }/* CVC4 namespace */
 
 #include "expr/node.h"
@@ -567,7 +586,7 @@ inline void NodeBuilder<nchild_thresh>::dealloc() {
   Assert(!d_used,
          "Internal error: NodeBuilder: dealloc() called with d_used");
 
-  for(iterator i = d_nv->nv_begin();
+  for(NodeValue::nv_iterator i = d_nv->nv_begin();
       i != d_nv->nv_end();
       ++i) {
     (*i)->dec();
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 63fe0c84a..b95f8ff0a 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -36,24 +36,24 @@ string NodeValue::toString() const {
 }
 
 void NodeValue::toStream(std::ostream& out) const {
-  out << "(" << Kind(d_kind);
   if(d_kind == kind::VARIABLE) {
     Node n(this);
     string s;
     if(n.hasAttribute(VarNameAttr(), s)) {
-      out << ":" << s;
+      out << s;
     } else {
-      out << ":" << this;
+      out << "var_" << d_id;
     }
   } else {
+    out << "(" << Kind(d_kind);
     for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
       if(i != nv_end()) {
         out << " ";
       }
-      out << *i;
+      Node(*i).toStream(out);
     }
+    out << ")";
   }
-  out << ")";
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index e8435df26..0ad7ba559 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -33,6 +33,10 @@ namespace CVC4 {
 
 template <bool ref_count> class NodeTemplate;
 template <unsigned> class NodeBuilder;
+class AndNodeBuilder;
+class OrNodeBuilder;
+class PlusNodeBuilder;
+class MultNodeBuilder;
 class NodeManager;
 
 namespace expr {
@@ -76,6 +80,10 @@ class NodeValue {
 
   template <bool> friend class CVC4::NodeTemplate;
   template <unsigned> friend class CVC4::NodeBuilder;
+  friend class CVC4::AndNodeBuilder;
+  friend class CVC4::OrNodeBuilder;
+  friend class CVC4::PlusNodeBuilder;
+  friend class CVC4::MultNodeBuilder;
   friend class CVC4::NodeManager;
 
   void inc();