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

2 files changed, 121 insertions, 50 deletions

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 90358a622..c11d5cf86 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -17,6 +17,7 @@
 
 //Used in some of the tests
 #include <vector>
+#include <sstream>
 
 #include "expr/expr_manager.h"
 #include "expr/node_value.h"
@@ -449,24 +450,52 @@ public:
   }
 
   void testIterator(){
-    /*typedef NodeValue::node_iterator iterator; */
-    /*typedef NodeValue::node_iterator const_iterator; */
-
-    /*inline iterator begin(); */
-    /*inline iterator end(); */
-    /*inline const_iterator begin() const; */
-    /*inline const_iterator end() const; */
+    NodeBuilder<> b;
+    Node x = d_nodeManager->mkVar();
+    Node y = d_nodeManager->mkVar();
+    Node z = d_nodeManager->mkVar();
+    Node n = b << x << y << z << kind::AND;
+
+    { // iterator
+      Node::iterator i = n.begin();
+      TS_ASSERT(*i++ == x);
+      TS_ASSERT(*i++ == y);
+      TS_ASSERT(*i++ == z);
+      TS_ASSERT(i == n.end());
+    }
 
-    TS_WARN( "TODO: This test still needs to be written!" );
+    { // same for const iterator
+      const Node& c = n;
+      Node::const_iterator i = c.begin();
+      TS_ASSERT(*i++ == x);
+      TS_ASSERT(*i++ == y);
+      TS_ASSERT(*i++ == z);
+      TS_ASSERT(i == n.end());
+    }
   }
 
   void testToString(){
-    /*inline std::string toString() const; */
-    TS_WARN( "TODO: This test still needs to be written!" );
+    Node w = d_nodeManager->mkVar(NULL, "w");
+    Node x = d_nodeManager->mkVar(NULL, "x");
+    Node y = d_nodeManager->mkVar(NULL, "y");
+    Node z = d_nodeManager->mkVar(NULL, "z");
+    Node m = NodeBuilder<>() << w << x << kind::OR;
+    Node n = NodeBuilder<>() << m << y << z << kind::AND;
+
+    TS_ASSERT(n.toString() == "(AND (OR w x) y z)");
   }
 
   void testToStream(){
-    /*inline void toStream(std::ostream&) const;*/
-    TS_WARN( "TODO: This test still needs to be written!" );
+    NodeBuilder<> b;
+    Node w = d_nodeManager->mkVar(NULL, "w");
+    Node x = d_nodeManager->mkVar(NULL, "x");
+    Node y = d_nodeManager->mkVar(NULL, "y");
+    Node z = d_nodeManager->mkVar(NULL, "z");
+    Node m = NodeBuilder<>() << x << y << kind::OR;
+    Node n = NodeBuilder<>() << w << m << z << kind::AND;
+
+    stringstream sstr;
+    n.toStream(sstr);
+    TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
   }
 };
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 5dc327a67..e956806b8 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -24,6 +24,7 @@
 #include "expr/node_manager.h"
 #include "expr/node.h"
 #include "expr/kind.h"
+#include "util/Assert.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -203,7 +204,28 @@ public:
   }
 
   void testIterator(){
-    TS_WARN( "TODO: This test still needs to be written!" );
+    NodeBuilder<> b;
+    Node x = d_nm->mkVar();
+    Node y = d_nm->mkVar();
+    Node z = d_nm->mkVar();
+    b << x << y << z << kind::AND;
+
+    {
+      NodeBuilder<>::iterator i = b.begin();
+      TS_ASSERT(*i++ == x);
+      TS_ASSERT(*i++ == y);
+      TS_ASSERT(*i++ == z);
+      TS_ASSERT(i == b.end());
+    }
+
+    {
+      const NodeBuilder<>& c = b;
+      NodeBuilder<>::const_iterator i = c.begin();
+      TS_ASSERT(*i++ == x);
+      TS_ASSERT(*i++ == y);
+      TS_ASSERT(*i++ == z);
+      TS_ASSERT(i == b.end());
+    }
   }
 
   void testGetKind(){
@@ -241,6 +263,8 @@ public:
     push_back(noKind, K);
     TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K);
 
+    noKind << AND;// avoid exception on marking it used
+    Node n = noKind;// avoid warning on clear()
     noKind.clear();
     TS_ASSERT_EQUALS(noKind.getNumChildren(), 0);
     push_back(noKind, K);
@@ -250,10 +274,9 @@ public:
     push_back(noKind, K);
     TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K);
 
-
     noKind << specKind;
-    Node n = noKind;
-    TS_ASSERT_THROWS_ANYTHING(noKind.getNumChildren(););
+    n = noKind;
+    TS_ASSERT_THROWS_ANYTHING( noKind.getNumChildren() );
   }
 
   void testOperatorSquare(){
@@ -319,6 +342,7 @@ public:
     TS_ASSERT_EQUALS(nb.getNumChildren(), K);
     TS_ASSERT_DIFFERS(nb.begin(), nb.end());
 
+    Node n = nb;// avoid warning on clear()
     nb.clear();
 
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
@@ -332,6 +356,7 @@ public:
     TS_ASSERT_EQUALS(nb.getNumChildren(), K);
     TS_ASSERT_DIFFERS(nb.begin(), nb.end());
 
+    n = nb;// avoid warning on clear()
     nb.clear(specKind);
 
     TS_ASSERT_EQUALS(nb.getKind(), specKind);
@@ -339,10 +364,9 @@ public:
     TS_ASSERT_EQUALS(nb.begin(), nb.end());
 
     push_back(nb, K);
-    Node n = nb;
+    n = nb;// avoid warning on clear()
     nb.clear();
 
-
     TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
     TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
     TS_ASSERT_EQUALS(nb.begin(), nb.end());
@@ -366,9 +390,9 @@ public:
     TS_ASSERT_EQUALS(modified.getKind(), specKind);
 
     NodeBuilder<> nb(specKind);
-    Node n = nb;
+    Node n = nb;// avoid warning on clear()
     nb.clear(PLUS);
-    TS_ASSERT_THROWS_ANYTHING(nb << PLUS;);
+    TS_ASSERT_THROWS_ANYTHING( nb << PLUS; );
 
     NodeBuilder<> testRef;
     TS_ASSERT_EQUALS((testRef << specKind).getKind(), specKind);
@@ -414,30 +438,53 @@ public:
   }
 
   void testAppend(){
-    /*
-      NodeBuilder& append(const Node& n) {
-    Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    Debug("prop") << "append: " << this << " " << n << "[" << n.d_ev << "]" << std::endl;
-    allocateEvIfNecessaryForAppend();
-    NodeValue* ev = n.d_ev;
-    ev->inc();
-    d_ev->d_children[d_ev->d_nchildren++] = ev;
-    return *this;
-  }
-     */
-    /*
-      
-  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");
-    for(Iterator i = begin; i != end; ++i) {
-      append(*i);
-    }
-    return *this;
-  }
-
-    */
-    TS_WARN( "TODO: This test still needs to be written!" );
+    Node x = d_nm->mkVar();
+    Node y = d_nm->mkVar();
+    Node z = d_nm->mkVar();
+    Node m = d_nm->mkNode(AND, y, z, x);
+    Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
+    Node o = d_nm->mkNode(XOR, y, x, z);
+    Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z);
+    Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y));
+
+    NodeBuilder<> b;
+
+    // test append(TNode)
+    b.append(n).append(o).append(q);
+
+    TS_ASSERT(b.getNumChildren() == 3);
+    TS_ASSERT(b[0] == n);
+    TS_ASSERT(b[1] == o);
+    TS_ASSERT(b[2] == q);
+
+    vector<Node> v;
+    v.push_back(m);
+    v.push_back(p);
+    v.push_back(q);
+    // test append(vector<Node>)
+    b.append(v);
+
+    TS_ASSERT(b.getNumChildren() == 6);
+    TS_ASSERT(b[0] == n);
+    TS_ASSERT(b[1] == o);
+    TS_ASSERT(b[2] == q);
+    TS_ASSERT(b[3] == m);
+    TS_ASSERT(b[4] == p);
+    TS_ASSERT(b[5] == q);
+
+    // test append(iterator, iterator)
+    b.append(v.rbegin(), v.rend());
+
+    TS_ASSERT(b.getNumChildren() == 9);
+    TS_ASSERT(b[0] == n);
+    TS_ASSERT(b[1] == o);
+    TS_ASSERT(b[2] == q);
+    TS_ASSERT(b[3] == m);
+    TS_ASSERT(b[4] == p);
+    TS_ASSERT(b[5] == q);
+    TS_ASSERT(b[6] == q);
+    TS_ASSERT(b[7] == p);
+    TS_ASSERT(b[8] == m);
   }
 
   void testOperatorNodeCast(){
@@ -476,12 +523,10 @@ public:
     push_back(b,K/2);
     push_back(c,K/2);
 
-
     a.toStream(astream);
     b.toStream(bstream);
     c.toStream(cstream);
 
-
     astr = astream.str();
     bstr = bstream.str();
     cstr = cstream.str();
@@ -489,7 +534,7 @@ public:
     TS_ASSERT_EQUALS(astr, bstr);
     TS_ASSERT_DIFFERS(astr, cstr);
 
-
+    Node n = a; n = b; n = c;// avoid warning on clear()
     a.clear(specKind);
     b.clear(specKind);
     c.clear(specKind);
@@ -497,17 +542,14 @@ public:
     bstream.flush();
     cstream.flush();
 
-
     push_back(a,2*K);
     push_back(b,2*K);
     push_back(c,2*K+1);
 
-
     a.toStream(astream);
     b.toStream(bstream);
     c.toStream(cstream);
 
-
     astr = astream.str();
     bstr = bstream.str();
     cstr = cstream.str();