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

1 files changed, 5 insertions, 5 deletions

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 */