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

4 files changed, 40 insertions, 14 deletions

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 51239cbbb..d1bfafb00 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -122,7 +122,11 @@ public:
   unsigned getSize() const {
     return d_size;
   }
-};
+
+  const Integer& getValue() const {
+    return d_value;
+  }
+};/* class BitVector */
 
 inline BitVector::BitVector(const std::string& num, unsigned base) {
   AlwaysAssert( base == 2 || base == 16 );
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 */
-
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 72a653545..13bed50b3 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -155,6 +155,16 @@ public:
     return gmpz_hash(d_value.get_mpz_t());
   }
 
+  /**
+   * 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 mpz_tstbit(d_value.get_mpz_t(), n);
+  }
+
   friend class CVC4::Rational;
 };/* class Integer */
 
@@ -171,4 +181,3 @@ inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
 }/* CVC4 namespace */
 
 #endif /* __CVC4__INTEGER_H */
-
diff --git a/src/util/language.h b/src/util/language.h
index 5446357c4..fdd2a382d 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -37,7 +37,7 @@ enum Language {
   /** Auto-detect the language */
   LANG_AUTO = -1,
 
-  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,999]
+  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
   // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE
   //
   // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
@@ -49,15 +49,20 @@ enum Language {
   /** The SMTLIB v2 input language */
   LANG_SMTLIB_V2,
   /** The CVC4 input language */
-  LANG_CVC4
+  LANG_CVC4,
 
-  // START INPUT-ONLY LANGUAGES AT ENUM VALUE 1000
+  // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES
 
+  /** LANG_MAX is > any valid InputLanguage id */
+  LANG_MAX
 };/* enum Language */
 
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
   switch(lang) {
+  case LANG_AUTO:
+    out << "LANG_AUTO";
+    break;
   case LANG_SMTLIB:
     out << "LANG_SMTLIB";
     break;
@@ -67,9 +72,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_CVC4:
     out << "LANG_CVC4";
     break;
-  case LANG_AUTO:
-    out << "LANG_AUTO";
-    break;
   default:
     out << "undefined_input_language";
   }
@@ -83,7 +85,7 @@ namespace output {
 enum Language {
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
-  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,999]
+  // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9]
   // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE
   //
   // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR
@@ -97,12 +99,14 @@ enum Language {
   /** The CVC4 output language */
   LANG_CVC4 = input::LANG_CVC4,
 
-  // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 1000
+  // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
 
   /** The AST output language */
-  LANG_AST = 1000
+  LANG_AST = 10,
 
+  /** LANG_MAX is > any valid OutputLanguage id */
+  LANG_MAX
 };/* enum Language */
 
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
@@ -117,7 +121,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
     out << "LANG_CVC4";
     break;
   case LANG_AST:
-    out << "LANG_AUTO";
+    out << "LANG_AST";
     break;
   default:
     out << "undefined_output_language";