From: Tim King Date: Tue, 1 Apr 2014 20:54:36 +0000 (-0400) Subject: Fixing bug 552. There was a bug when integers are made using a string with a lot... X-Git-Tag: cvc5-1.0.0~6987^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98df8ccdd49674c02360a0662fbc1765ace2d5bf;p=cvc5.git 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. --- 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 +#include + +#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 +#include +#include + +#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); + } };