Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer

implemented.  This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0.  Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder.  (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)

2 files changed, 42 insertions, 51 deletions

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 46fb82546..49c9b7952 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -570,57 +570,6 @@ public:
 #endif /* CVC4_ASSERTIONS */
   }
 
-  void testToStream() {
-    /* inline void toStream(std::ostream& out) const {
-       d_ev->toStream(out);
-       }
-     */
-
-    NodeBuilder<K> a(specKind);
-    NodeBuilder<K> b(specKind);
-    NodeBuilder<K> c(NOT);
-    string astr, bstr, cstr;
-    stringstream astream, bstream, cstream;
-
-    push_back(a, K / 2);
-    push_back(b, K / 2);
-    push_back(c, 1);
-
-    a.toStream(astream);
-    b.toStream(bstream);
-    c.toStream(cstream);
-
-    astr = astream.str();
-    bstr = bstream.str();
-    cstr = cstream.str();
-
-    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);
-    astream.flush();
-    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();
-
-    TS_ASSERT_EQUALS(astr, bstr);
-    TS_ASSERT_DIFFERS(astr, cstr);
-  }
-
   void testLeftistBuilding() {
     NodeBuilder<> nb;
 
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index 57ae247ac..f4bd1f8b8 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -294,4 +294,46 @@ public:
     TS_ASSERT_EQUALS( Integer(1000), Integer(10).pow(3) );
     TS_ASSERT_EQUALS( Integer(-1000), Integer(-10).pow(3) );
   }
+
+  void testTestBit() {
+    TS_ASSERT( ! Integer(0).testBit(6) );
+    TS_ASSERT( ! Integer(0).testBit(5) );
+    TS_ASSERT( ! Integer(0).testBit(4) );
+    TS_ASSERT( ! Integer(0).testBit(3) );
+    TS_ASSERT( ! Integer(0).testBit(2) );
+    TS_ASSERT( ! Integer(0).testBit(1) );
+    TS_ASSERT( ! Integer(0).testBit(0) );
+
+    TS_ASSERT( Integer(-1).testBit(6) );
+    TS_ASSERT( Integer(-1).testBit(5) );
+    TS_ASSERT( Integer(-1).testBit(4) );
+    TS_ASSERT( Integer(-1).testBit(3) );
+    TS_ASSERT( Integer(-1).testBit(2) );
+    TS_ASSERT( Integer(-1).testBit(1) );
+    TS_ASSERT( Integer(-1).testBit(0) );
+
+    TS_ASSERT( ! Integer(10).testBit(6) );
+    TS_ASSERT( ! Integer(10).testBit(5) );
+    TS_ASSERT( ! Integer(10).testBit(4) );
+    TS_ASSERT( Integer(10).testBit(3) );
+    TS_ASSERT( ! Integer(10).testBit(2) );
+    TS_ASSERT( Integer(10).testBit(1) );
+    TS_ASSERT( ! Integer(10).testBit(0) );
+
+    TS_ASSERT( ! Integer(14).testBit(6) );
+    TS_ASSERT( ! Integer(14).testBit(5) );
+    TS_ASSERT( ! Integer(14).testBit(4) );
+    TS_ASSERT( Integer(14).testBit(3) );
+    TS_ASSERT( Integer(14).testBit(2) );
+    TS_ASSERT( Integer(14).testBit(1) );
+    TS_ASSERT( ! Integer(14).testBit(0) );
+
+    TS_ASSERT( Integer(64).testBit(6) );
+    TS_ASSERT( ! Integer(64).testBit(5) );
+    TS_ASSERT( ! Integer(64).testBit(4) );
+    TS_ASSERT( ! Integer(64).testBit(3) );
+    TS_ASSERT( ! Integer(64).testBit(2) );
+    TS_ASSERT( ! Integer(64).testBit(1) );
+    TS_ASSERT( ! Integer(64).testBit(0) );
+  }
 };