* theory "tree" rewriting implemented and works

* added TheoryArith::preRewrite() to test and demonstrate
  the use of pre-rewriting.

* array types and type checking now supported

* array type checking now supported

* theoryOf() dispatching properly to arrays now

* theories now required to implement a (simple) identify()
  function that returns a string identifying them for
  debugging/user output purposes

* added "builtin" theory to hold all built-in kinds and their
  type rules and rewriting (currently only exploding distinct)

* fixed production build failure (regarding NodeSetDepth)

* removed an errant "using namespace std" in util/bitvector.h
  (and made associated trivial fixes elsewhere)

* fixes to make unexpected exceptions more verbose in debug builds

* fixes to make multiple, cascading assertion fails simpler

* minor other fixes to comments etc.

1 files changed, 18 insertions, 0 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index d81190d7a..0cb9ed026 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -566,6 +566,24 @@ public:
     return append(n);
   }
 
+  /**
+   * If this Node-under-construction has a Kind set, collapse it and
+   * append the given Node as a child.  Otherwise, simply append.
+   * FIXME: do we really want that collapse behavior?  We had agreed
+   * on it but then never wrote code like that.
+   */
+  NodeBuilder<nchild_thresh>& operator<<(TypeNode n) {
+    Assert(!isUsed(), "NodeBuilder is one-shot only; "
+           "attempt to access it after conversion");
+    /* FIXME: disable this "collapsing" for now..
+    if(EXPECT_FALSE( getKind() != kind::UNDEFINED_KIND )) {
+      Node n2 = operator Node();
+      clear();
+      append(n2);
+    }*/
+    return append(n);
+  }
+
   /** Append a sequence of children to this TypeNode-under-construction. */
   inline NodeBuilder<nchild_thresh>&
   append(const std::vector<TypeNode>& children) {