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, 8 insertions, 0 deletions

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();