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

6 files changed, 130 insertions, 63 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 2f278625a..e8aeea494 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -104,19 +104,23 @@ BUILT_SOURCES = \
 
 if CVC4_CLN_IMP
 libutil_la_SOURCES += \
-	rational_cln_imp.cpp
+	rational_cln_imp.cpp \
+	integer_cln_imp.cpp
 endif
 if CVC4_GMP_IMP
 libutil_la_SOURCES += \
-	rational_gmp_imp.cpp
+	rational_gmp_imp.cpp \
+	integer_gmp_imp.cpp
 endif
 
 EXTRA_DIST = \
 	rational_cln_imp.h \
 	integer_cln_imp.h \
+	integer_cln_imp.cpp \
 	rational_cln_imp.cpp \
 	rational_gmp_imp.h \
 	integer_gmp_imp.h \
+	integer_gmp_imp.cpp \
 	rational_gmp_imp.cpp \
 	rational.h.in \
 	integer.h.in \
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
new file mode 100644
index 000000000..383f27688
--- /dev/null
+++ b/src/util/integer_cln_imp.cpp
@@ -0,0 +1,59 @@
+#include "cvc4autoconfig.h"
+#include "util/integer.h"
+#include <string>
+#include <sstream>
+
+#ifndef CVC4_CLN_IMP
+#  error "This source should only ever be built if CVC4_CLN_IMP is on !"
+#endif /* CVC4_CLN_IMP */
+
+using namespace std;
+using namespace CVC4;
+
+
+void Integer::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 Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
+  try {
+    // Removing leading 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.
+    size_t pos = s.find_first_not_of('0');
+    if(pos == std::string::npos) {
+      d_value = read_integer(flags, "0", NULL, NULL);
+    } else {
+      const char* cstr = s.c_str();
+      const char* start = cstr + pos;
+      const char* end = cstr + s.length();
+      d_value = read_integer(flags, start, end, NULL);
+    }
+  } catch(...) {
+    std::stringstream ss;
+    ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
+    throw std::invalid_argument(ss.str());
+  }
+}
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);
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
new file mode 100644
index 000000000..f2a888340
--- /dev/null
+++ b/src/util/integer_gmp_imp.cpp
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file integer_gmp_imp.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: Morgan Deters, Christopher L. Conway
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A multi-precision rational constant.
+ **
+ ** A multi-precision rational constant.
+ **/
+
+#include "cvc4autoconfig.h"
+#include "util/rational.h"
+#include <string>
+#include <sstream>
+#include <cmath>
+
+#ifndef CVC4_GMP_IMP
+#  error "This source should only ever be built if CVC4_GMP_IMP is on !"
+#endif /* CVC4_GMP_IMP */
+
+using namespace std;
+using namespace CVC4;
+
+
+
+Integer::Integer(const char* s, unsigned base)
+  : d_value(s, base)
+{}
+
+Integer::Integer(const std::string& s, unsigned base)
+  : d_value(s, base)
+{}
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index bd0556c22..a39de7996 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -60,8 +60,8 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  explicit Integer(const char* s, unsigned base = 10): d_value(s, base) {}
-  explicit Integer(const std::string& s, unsigned base = 10) : d_value(s, base) {}
+  explicit Integer(const char* s, unsigned base = 10);
+  explicit Integer(const std::string& s, unsigned base = 10);
 
   Integer(const Integer& q) : d_value(q.d_value) {}
 
@@ -149,7 +149,7 @@ public:
     mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
     return Integer(result);
   }
-  
+
   Integer bitwiseXor(const Integer& y) const {
     mpz_class result;
     mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
@@ -161,7 +161,7 @@ public:
     mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
     return Integer(result);
   }
-  
+
   /**
    * Return this*(2^pow).
    */
@@ -171,20 +171,20 @@ public:
     return Integer( result );
   }
 
-  /** 
+  /**
    * Returns the Integer obtained by setting the ith bit of the
-   * current Integer to 1. 
+   * current Integer to 1.
    */
   Integer setBit(uint32_t i) const {
     mpz_class res = d_value;
     mpz_setbit(res.get_mpz_t(), i);
-    return Integer(res); 
+    return Integer(res);
   }
 
   bool isBitSet(uint32_t i) const {
-    return !extractBitRange(1, i).isZero(); 
+    return !extractBitRange(1, i).isZero();
   }
-  
+
   /**
    * Returns the integer with the binary representation of size bits
    * extended with amount 1's
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index 48f32a307..de5669c11 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -24,6 +24,7 @@ using namespace CVC4;
 using namespace std;
 
 const char* largeVal = "4547897890548754897897897897890789078907890";
+const char* lotsOfLeadingZeroes = "00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001";
 
 class IntegerBlack : public CxxTest::TestSuite {
 
@@ -462,4 +463,11 @@ public:
     TS_ASSERT_EQUALS( r, Integer(-1));
 
   }
+
+  void testLeadingZeroes() {
+    string leadingZeroes(lotsOfLeadingZeroes);
+    Integer one(1u);
+    Integer one_from_string(leadingZeroes,2);
+    TS_ASSERT_EQUALS(one, one_from_string);
+  }
 };