Fixing bug 552. There was a bug when integers are made using a string with a lot of leading 0s on old versions of CLN.1.3.x

1 files changed, 10 insertions, 52 deletions

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 197c615e1..05d820dbc 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -38,66 +38,24 @@ class Rational;
 class CVC4_PUBLIC Integer {
 private:
   /**
-   * Stores the value of the rational is stored in a C++ GMP integer class.
-   * Using this instead of mpz_t allows for easier destruction.
+   * Stores the value of the rational is stored in a C++ CLN integer class.
    */
   cln::cl_I d_value;
 
   /**
-   * Gets a reference to the gmp data that backs up the integer.
+   * Gets a reference to the cln data that backs up the integer.
    * Only accessible to friend classes.
    */
-  //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.
+   * Constructs an Integer by copying a CLN C++ primitive.
    */
-  //Integer(const mpz_class& val) : d_value(val) {}
   Integer(const cln::cl_I& val) : d_value(val) {}
 
-  void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
-    try {
-      if(s.find_first_not_of('0') == std::string::npos) {
-        // String of all zeroes, CLN has a bug for these inputs up to and
-        // including CLN v1.3.2.
-        // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
-        d_value = read_integer(flags, "0", NULL, NULL);
-      } else {
-        d_value = read_integer(flags, s.c_str(), NULL, NULL);
-      }
-    } catch(...) {
-      std::stringstream ss;
-      ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
-      throw std::invalid_argument(ss.str());
-    }
-  }
+  void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument);
 
-  void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
-    cln::cl_read_flags flags;
-    flags.syntax = cln::syntax_integer;
-    flags.lsyntax = cln::lsyntax_standard;
-    flags.rational_base = base;
-    if(base == 0) {
-      // infer base in a manner consistent with GMP
-      if(s[0] == '0') {
-        flags.lsyntax = cln::lsyntax_commonlisp;
-        std::string st = s;
-        if(s[1] == 'X' || s[1] == 'x') {
-          st.replace(0, 2, "#x");
-        } else if(s[1] == 'B' || s[1] == 'b') {
-          st.replace(0, 2, "#b");
-        } else {
-          st.replace(0, 1, "#o");
-        }
-        readInt(flags, st, base);
-        return;
-      } else {
-        flags.rational_base = 10;
-      }
-    }
-    readInt(flags, s, base);
-  }
+  void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument);
 
 public:
 
@@ -219,15 +177,15 @@ public:
   }
 
   bool isBitSet(uint32_t i) const {
-    return !extractBitRange(1, i).isZero(); 
+    return !extractBitRange(1, i).isZero();
   }
-  
+
   Integer setBit(uint32_t i) const {
     cln::cl_I mask(1);
-    mask = mask << i; 
-    return Integer(cln::logior(d_value, mask)); 
+    mask = mask << i;
+    return Integer(cln::logior(d_value, mask));
   }
-  
+
   Integer oneExtend(uint32_t size, uint32_t amount) const {
     DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
     cln::cl_byte range(amount, size);