diff options
author | Tim King <taking@cs.nyu.edu> | 2014-04-01 16:54:36 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-04-01 16:54:36 -0400 |
commit | 98df8ccdd49674c02360a0662fbc1765ace2d5bf (patch) | |
tree | b80e3c78a79b45401a21a9bfb03bf63174e55199 /src/util/integer_cln_imp.h | |
parent | e347f43940c53a8dfdaa022bc19900fcee631c08 (diff) |
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
Diffstat (limited to 'src/util/integer_cln_imp.h')
-rw-r--r-- | src/util/integer_cln_imp.h | 62 |
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); |