"Leftist NodeBuilders" are now supported.

That is, "nb << a << b << c << OR << d << AND" turns into
  (AND (OR a b c) d)

The rule is:  pushing a kind onto a NodeBuilder with a nonzero
number of child Nodes in it, the action "collapses" it.  If a
kind is already associated to the NodeBuilder, it is an error.

Thus:
  NodeBuilder<> nb(AND); nb << AND;
and
  NodeBuilder<> nb; nb << AND << OR;
are both errors (if assertions are on).

In reality, though, the implementation is trickier, as the collapsing
is done lazily on the following push.  This complicates things a bit,
but by placing an Assert(false), I found that we aren't depending on
the old behavior (at least for any unit tests or regressions in the
source tree).  The Assert(false) is now removed and leftist
NodeBuilders are in business.

Fixes bug 101.

1 files changed, 31 insertions, 0 deletions

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index e3883b824..e6f8116fc 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -613,6 +613,37 @@ public:
     TS_ASSERT_DIFFERS(astr, cstr);
   }
 
+  void testLeftistBuilding() {
+    NodeBuilder<> nb;
+
+    Node a = d_nm->mkVar(*d_booleanType);
+
+    Node b = d_nm->mkVar(*d_booleanType);
+    Node c = d_nm->mkVar(*d_booleanType);
+
+    Node d = d_nm->mkVar(*d_realType);
+    Node e = d_nm->mkVar(*d_realType);
+
+    nb << a << NOT
+       << b << c << OR
+       << c << a << AND
+       << d << e << ITE;
+
+    Node n = nb;
+    TS_ASSERT_EQUALS(n.getNumChildren(), 3u);
+    TS_ASSERT_EQUALS(n.getType(), *d_realType);
+    TS_ASSERT_EQUALS(n[0].getType(), *d_booleanType);
+    TS_ASSERT_EQUALS(n[1].getType(), *d_realType);
+    TS_ASSERT_EQUALS(n[2].getType(), *d_realType);
+
+    Node nota = d_nm->mkNode(NOT, a);
+    Node nota_or_b_or_c = d_nm->mkNode(OR, nota, b, c);
+    Node n0 = d_nm->mkNode(AND, nota_or_b_or_c, c, a);
+    Node nexpected = d_nm->mkNode(ITE, n0, d, e);
+
+    TS_ASSERT_EQUALS(nexpected, n);
+  }
+
   void testConvenienceBuilders() {
     Node a = d_nm->mkVar(*d_booleanType);