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

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index c1b2a87d289bb073084cfcd02e34c514869945a5..f5da56d967a264b52e5a724d519d0479536c85f7 100644 (file)
--- 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 63fe0c84ab312cc3109c89cc847c0949e671b5c3..b95f8ff0a593dcc29d7e0378462fe4c7af41a010 100644 (file)
--- 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 e8435df266eb2a0177fed44a5c1402d740b3dd30..0ad7ba55997e7cc63ed4471a54c65c668bdca06d 100644 (file)
--- 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();

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5946764166bb71124110ee42366fea354a034f0d..7495e410054a7d649530d5397e9c8d77fba83cef 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -24,6 +24,7 @@
 #include "util/result.h"
 #include "util/model.h"
 
+// FIXME private header in public code
 #include "expr/node.h"
 
 // In terms of abstraction, this is below (and provides services to)

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 994416838aee0c008841fced222fda5fb47263cd..fd784ccce2cf473e989ef9f5a991dc8fee80c7ef 100644 (file)
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -1 +1,3 @@
 PLUS
+MULT
+UMINUS

diff --git a/src/theory/theoryof_table_epilogue.h b/src/theory/theoryof_table_epilogue.h
index 7483248ec3fe143e935690b28e6b05d236130b19..11f75183a682e58fefa647b2accea2d14504c561 100644 (file)
--- a/src/theory/theoryof_table_epilogue.h
+++ b/src/theory/theoryof_table_epilogue.h
@@ -10,7 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** The theoryOf table.
+ ** The epilogue section for the automatically-generated theoryOf table.
+ ** See the mktheoryof script.
  **/
 
 };/* class TheoryOfTable */

diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h
index 17a945d0100cf2bd5f84cfdc898fe9ea938a450d..f3ad433a3af96101d5c9ec6bdb7b5aece3aa0dc9 100644 (file)
--- a/src/theory/theoryof_table_middle.h
+++ b/src/theory/theoryof_table_middle.h
@@ -10,7 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** The theoryOf table.
+ ** The middle section for the automatically-generated theoryOf table.
+ ** See the mktheoryof script.
  **/
 
 namespace CVC4 {

diff --git a/src/theory/theoryof_table_prologue.h b/src/theory/theoryof_table_prologue.h
index 47fd2d9b29261d0fdb984cc60d32d84d38bd6314..6e83d6d2c3cb0ff6e69bf13480fa74cbfb0d5da2 100644 (file)
--- a/src/theory/theoryof_table_prologue.h
+++ b/src/theory/theoryof_table_prologue.h
@@ -10,7 +10,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** The theoryOf table.
+ ** The prologue section for the automatically-generated theoryOf table.
+ ** See the mktheoryof script.
  **/
 
 #include "cvc4_private.h"

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 90358a622b3d3fe719800dedc3cbc0db746645c1..c11d5cf86287d882c0693eae1b0b2ef5b53a7f28 100644 (file)
--- 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 5dc327a676a75d574f7ca2327da6936f88d5b3a1..e956806b8151012761a5403233180fd5832bcb66 100644 (file)
--- 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();