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.)

1 files changed, 11 insertions, 2 deletions

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 21f6c7581..d13c946de 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -50,7 +50,7 @@ private:
    */
   //const mpz_class& get_mpz() const { return d_value; }
   const cln::cl_I& get_cl_I() const { return d_value; }
- 
+
   /**
    * Constructs an Integer by copying a GMP C++ primitive.
    */
@@ -219,6 +219,16 @@ public:
     return equal_hashcode(d_value);
   }
 
+  /**
+   * Returns true iff bit n is set.
+   *
+   * @param n the bit to test (0 == least significant bit)
+   * @return true if bit n is set in this integer; false otherwise
+   */
+  bool testBit(unsigned n) const {
+    return cln::logbitp(n, d_value);
+  }
+
   friend class CVC4::Rational;
 };/* class Integer */
 
@@ -235,4 +245,3 @@ inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
 }/* CVC4 namespace */
 
 #endif /* __CVC4__INTEGER_H */
-