diff options
author | nafur <nafur@users.noreply.github.com> | 2020-06-22 21:11:38 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-22 12:11:38 -0700 |
commit | 1a08524c269a583b5d12f0d4c6f88045b44bdbf7 (patch) | |
tree | 284aa134a9778c4c3d3487a631e6481e425105c1 /src/util/integer_cln_imp.h | |
parent | d85e90bfcc0bebe52b2da0bad638bc2fe9ef50b0 (diff) |
Allow for better interaction of Integer/Rational with mpz_class/mpq_class. (#4612)
Diffstat (limited to 'src/util/integer_cln_imp.h')
-rw-r--r-- | src/util/integer_cln_imp.h | 413 |
1 files changed, 211 insertions, 202 deletions
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index dc4a13137..a6ed6f14a 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -24,6 +24,7 @@ #include <cln/integer.h> #include <cln/integer_io.h> #include <cln/modinteger.h> + #include <iostream> #include <limits> #include <sstream> @@ -35,53 +36,22 @@ namespace CVC4 { class Rational; -class CVC4_PUBLIC Integer { -private: - /** - * Stores the value of the rational is stored in a C++ CLN integer class. - */ - cln::cl_I d_value; - - /** - * Gets a reference to the cln data that backs up the integer. - * Only accessible to friend classes. - */ - const cln::cl_I& get_cl_I() const { return d_value; } +class CVC4_PUBLIC Integer +{ + friend class CVC4::Rational; + public: /** * Constructs an Integer by copying a CLN C++ primitive. */ Integer(const cln::cl_I& val) : d_value(val) {} - // Throws a std::invalid_argument on invalid input `s` for the given base. - void readInt(const cln::cl_read_flags& flags, - const std::string& s, - unsigned base); - - // Throws a std::invalid_argument on invalid inputs. - void parseInt(const std::string& s, unsigned base); - - // These constants are to help with CLN conversion in 32 bit. - // See http://www.ginac.de/CLN/cln.html#Conversions - static signed int s_fastSignedIntMax; /* 2^29 - 1 */ - static signed int s_fastSignedIntMin; /* -2^29 */ - static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */ - - static signed long s_slowSignedIntMax; /* std::numeric_limits<signed int>::max() */ - static signed long s_slowSignedIntMin; /* std::numeric_limits<signed int>::min() */ - static unsigned long s_slowUnsignedIntMax; /* std::numeric_limits<unsigned int>::max() */ - static unsigned long s_signedLongMin; - static unsigned long s_signedLongMax; - static unsigned long s_unsignedLongMax; -public: /** Constructs a rational with the value 0. */ - Integer() : d_value(0){} + Integer() : d_value(0) {} /** * Constructs a Integer from a C string. - * Throws std::invalid_argument if the string is not a valid rational. - * For more information about what is a valid rational string, - * see GMP's documentation for mpq_set_str(). + * Throws std::invalid_argument if the string is not a valid integer. */ explicit Integer(const char* sp, unsigned base = 10) { @@ -95,13 +65,13 @@ public: Integer(const Integer& q) : d_value(q.d_value) {} - Integer( signed int z) : d_value((signed long int)z) {} + Integer(signed int z) : d_value((signed long int)z) {} Integer(unsigned int z) : d_value((unsigned long int)z) {} - Integer( signed long int z) : d_value(z) {} + Integer(signed long int z) : d_value(z) {} Integer(unsigned long int z) : d_value(z) {} #ifdef CVC4_NEED_INT64_T_OVERLOADS - Integer( int64_t z) : d_value(static_cast<long>(z)) {} + Integer(int64_t z) : d_value(static_cast<long>(z)) {} Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {} #endif /* CVC4_NEED_INT64_T_OVERLOADS */ @@ -110,103 +80,90 @@ public: /** * Returns a copy of d_value to enable public access of CLN data. */ - cln::cl_I getValue() const - { - return d_value; - } + const cln::cl_I& getValue() const { return d_value; } - Integer& operator=(const Integer& x){ - if(this == &x) return *this; + Integer& operator=(const Integer& x) + { + if (this == &x) return *this; d_value = x.d_value; return *this; } - bool operator==(const Integer& y) const { - return d_value == y.d_value; - } - - Integer operator-() const{ - return Integer(-(d_value)); - } + bool operator==(const Integer& y) const { return d_value == y.d_value; } + Integer operator-() const { return Integer(-(d_value)); } - bool operator!=(const Integer& y) const { - return d_value != y.d_value; - } + bool operator!=(const Integer& y) const { return d_value != y.d_value; } - bool operator< (const Integer& y) const { - return d_value < y.d_value; - } + bool operator<(const Integer& y) const { return d_value < y.d_value; } - bool operator<=(const Integer& y) const { - return d_value <= y.d_value; - } + bool operator<=(const Integer& y) const { return d_value <= y.d_value; } - bool operator> (const Integer& y) const { - return d_value > y.d_value; - } + bool operator>(const Integer& y) const { return d_value > y.d_value; } - bool operator>=(const Integer& y) const { - return d_value >= y.d_value; - } + bool operator>=(const Integer& y) const { return d_value >= y.d_value; } - - Integer operator+(const Integer& y) const { - return Integer( d_value + y.d_value ); + Integer operator+(const Integer& y) const + { + return Integer(d_value + y.d_value); } - Integer& operator+=(const Integer& y) { + Integer& operator+=(const Integer& y) + { d_value += y.d_value; return *this; } - Integer operator-(const Integer& y) const { - return Integer( d_value - y.d_value ); + Integer operator-(const Integer& y) const + { + return Integer(d_value - y.d_value); } - Integer& operator-=(const Integer& y) { + Integer& operator-=(const Integer& y) + { d_value -= y.d_value; return *this; } - Integer operator*(const Integer& y) const { - return Integer( d_value * y.d_value ); + Integer operator*(const Integer& y) const + { + return Integer(d_value * y.d_value); } - Integer& operator*=(const Integer& y) { + Integer& operator*=(const Integer& y) + { d_value *= y.d_value; return *this; } - - Integer bitwiseOr(const Integer& y) const { + Integer bitwiseOr(const Integer& y) const + { return Integer(cln::logior(d_value, y.d_value)); } - Integer bitwiseAnd(const Integer& y) const { + Integer bitwiseAnd(const Integer& y) const + { return Integer(cln::logand(d_value, y.d_value)); } - Integer bitwiseXor(const Integer& y) const { + Integer bitwiseXor(const Integer& y) const + { return Integer(cln::logxor(d_value, y.d_value)); } - Integer bitwiseNot() const { - return Integer(cln::lognot(d_value)); - } - + Integer bitwiseNot() const { return Integer(cln::lognot(d_value)); } /** * Return this*(2^pow). */ - Integer multiplyByPow2(uint32_t pow) const { + Integer multiplyByPow2(uint32_t pow) const + { cln::cl_I ipow(pow); - return Integer( d_value << ipow); + return Integer(d_value << ipow); } - bool isBitSet(uint32_t i) const { - return !extractBitRange(1, i).isZero(); - } + bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); } - Integer setBit(uint32_t i) const { + Integer setBit(uint32_t i) const + { cln::cl_I mask(1); mask = mask << i; return Integer(cln::logior(d_value, mask)); @@ -214,13 +171,11 @@ public: Integer oneExtend(uint32_t size, uint32_t amount) const; - uint32_t toUnsignedInt() const { - return cln::cl_I_to_uint(d_value); - } - + uint32_t toUnsignedInt() const { return cln::cl_I_to_uint(d_value); } /** See CLN Documentation. */ - Integer extractBitRange(uint32_t bitCount, uint32_t low) const { + Integer extractBitRange(uint32_t bitCount, uint32_t low) const + { cln::cl_byte range(bitCount, low); return Integer(cln::ldb(d_value, range)); } @@ -228,20 +183,26 @@ public: /** * Returns the floor(this / y) */ - Integer floorDivideQuotient(const Integer& y) const { - return Integer( cln::floor1(d_value, y.d_value) ); + Integer floorDivideQuotient(const Integer& y) const + { + return Integer(cln::floor1(d_value, y.d_value)); } /** * Returns r == this - floor(this/y)*y */ - Integer floorDivideRemainder(const Integer& y) const { - return Integer( cln::floor2(d_value, y.d_value).remainder ); + Integer floorDivideRemainder(const Integer& y) const + { + return Integer(cln::floor2(d_value, y.d_value).remainder); } - /** + /** * Computes a floor quoient and remainder for x divided by y. */ - static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { + static void floorQR(Integer& q, + Integer& r, + const Integer& x, + const Integer& y) + { cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value); q.d_value = res.quotient; r.d_value = res.remainder; @@ -250,43 +211,53 @@ public: /** * Returns the ceil(this / y) */ - Integer ceilingDivideQuotient(const Integer& y) const { - return Integer( cln::ceiling1(d_value, y.d_value) ); + Integer ceilingDivideQuotient(const Integer& y) const + { + return Integer(cln::ceiling1(d_value, y.d_value)); } /** * Returns the ceil(this / y) */ - Integer ceilingDivideRemainder(const Integer& y) const { - return Integer( cln::ceiling2(d_value, y.d_value).remainder ); + Integer ceilingDivideRemainder(const Integer& y) const + { + return Integer(cln::ceiling2(d_value, y.d_value).remainder); } /** - * Computes a quoitent and remainder according to Boute's Euclidean definition. - * euclidianDivideQuotient, euclidianDivideRemainder. + * Computes a quoitent and remainder according to Boute's Euclidean + * definition. euclidianDivideQuotient, euclidianDivideRemainder. * * Boute, Raymond T. (April 1992). * The Euclidean definition of the functions div and mod. * ACM Transactions on Programming Languages and Systems (TOPLAS) * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862. */ - static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { + static void euclidianQR(Integer& q, + Integer& r, + const Integer& x, + const Integer& y) + { // compute the floor and then fix the value up if needed. - floorQR(q,r,x,y); + floorQR(q, r, x, y); - if(r.strictlyNegative()){ + if (r.strictlyNegative()) + { // if r < 0 // abs(r) < abs(y) // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y) // n = y * q + r // n = y * q - abs(y) + r + abs(y) - if(r.sgn() >= 0){ + if (r.sgn() >= 0) + { // y = abs(y) // n = y * q - y + r + y // n = y * (q-1) + (r+y) q -= 1; r += y; - }else{ + } + else + { // y = -abs(y) // n = y * q + y + r - y // n = y * (q+1) + (r-y) @@ -300,9 +271,10 @@ public: * Returns the quoitent according to Boute's Euclidean definition. * See the documentation for euclidianQR. */ - Integer euclidianDivideQuotient(const Integer& y) const { - Integer q,r; - euclidianQR(q,r, *this, y); + Integer euclidianDivideQuotient(const Integer& y) const + { + Integer q, r; + euclidianQR(q, r, *this, y); return q; } @@ -310,9 +282,10 @@ public: * Returns the remainfing according to Boute's Euclidean definition. * See the documentation for euclidianQR. */ - Integer euclidianDivideRemainder(const Integer& y) const { - Integer q,r; - euclidianQR(q,r, *this, y); + Integer euclidianDivideRemainder(const Integer& y) const + { + Integer q, r; + euclidianQR(q, r, *this, y); return r; } @@ -321,14 +294,13 @@ public: */ Integer exactQuotient(const Integer& y) const; - Integer modByPow2(uint32_t exp) const { + Integer modByPow2(uint32_t exp) const + { cln::cl_byte range(exp, 0); return Integer(cln::ldb(d_value, range)); } - Integer divByPow2(uint32_t exp) const { - return d_value >> exp; - } + Integer divByPow2(uint32_t exp) const { return d_value >> exp; } /** * Raise this Integer to the power <code>exp</code>. @@ -340,7 +312,8 @@ public: /** * Return the greatest common divisor of this integer with another. */ - Integer gcd(const Integer& y) const { + Integer gcd(const Integer& y) const + { cln::cl_I result = cln::gcd(d_value, y.d_value); return Integer(result); } @@ -348,7 +321,8 @@ public: /** * Return the least common multiple of this integer with another. */ - Integer lcm(const Integer& y) const { + Integer lcm(const Integer& y) const + { cln::cl_I result = cln::lcm(d_value, y.d_value); return Integer(result); } @@ -380,7 +354,8 @@ public: /** * Return true if *this exactly divides y. */ - bool divides(const Integer& y) const { + bool divides(const Integer& y) const + { cln::cl_I result = cln::rem(y.d_value, d_value); return cln::zerop(result); } @@ -388,31 +363,24 @@ public: /** * Return the absolute value of this integer. */ - Integer abs() const { - return d_value >= 0 ? *this : -*this; - } + Integer abs() const { return d_value >= 0 ? *this : -*this; } - std::string toString(int base = 10) const{ + std::string toString(int base = 10) const + { std::stringstream ss; - switch(base){ - case 2: - fprintbinary(ss,d_value); - break; - case 8: - fprintoctal(ss,d_value); - break; - case 10: - fprintdecimal(ss,d_value); - break; - case 16: - fprinthexadecimal(ss,d_value); - break; - default: - throw Exception("Unhandled base in Integer::toString()"); + switch (base) + { + case 2: fprintbinary(ss, d_value); break; + case 8: fprintoctal(ss, d_value); break; + case 10: fprintdecimal(ss, d_value); break; + case 16: fprinthexadecimal(ss, d_value); break; + default: throw Exception("Unhandled base in Integer::toString()"); } std::string output = ss.str(); - for( unsigned i = 0; i <= output.length(); ++i){ - if(isalpha(output[i])){ + for (unsigned i = 0; i <= output.length(); ++i) + { + if (isalpha(output[i])) + { output.replace(i, 1, 1, tolower(output[i])); } } @@ -420,31 +388,21 @@ public: return output; } - int sgn() const { + int sgn() const + { cln::cl_I sgn = cln::signum(d_value); return cln::cl_I_to_int(sgn); } + inline bool strictlyPositive() const { return sgn() > 0; } - inline bool strictlyPositive() const { - return sgn() > 0; - } - - inline bool strictlyNegative() const { - return sgn() < 0; - } + inline bool strictlyNegative() const { return sgn() < 0; } - inline bool isZero() const { - return sgn() == 0; - } + inline bool isZero() const { return sgn() == 0; } - inline bool isOne() const { - return d_value == 1; - } + inline bool isOne() const { return d_value == 1; } - inline bool isNegativeOne() const { - return d_value == -1; - } + inline bool isNegativeOne() const { return d_value == -1; } /** fits the C "signed int" primitive */ bool fitsSignedInt() const; @@ -460,20 +418,26 @@ public: bool fitsUnsignedLong() const; - long getLong() const { + long getLong() const + { // ensure there isn't overflow - CheckArgument(d_value <= std::numeric_limits<long>::max(), this, + CheckArgument(d_value <= std::numeric_limits<long>::max(), + this, "Overflow detected in Integer::getLong()"); - CheckArgument(d_value >= std::numeric_limits<long>::min(), this, + CheckArgument(d_value >= std::numeric_limits<long>::min(), + this, "Overflow detected in Integer::getLong()"); return cln::cl_I_to_long(d_value); } - unsigned long getUnsignedLong() const { + unsigned long getUnsignedLong() const + { // ensure there isn't overflow - CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), this, + CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), + this, "Overflow detected in Integer::getUnsignedLong()"); - CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), this, + CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), + this, "Overflow detected in Integer::getUnsignedLong()"); return cln::cl_I_to_ulong(d_value); } @@ -482,9 +446,7 @@ public: * Computes the hash of the node from the first word of the * numerator, the denominator. */ - size_t hash() const { - return equal_hashcode(d_value); - } + size_t hash() const { return equal_hashcode(d_value); } /** * Returns true iff bit n is set. @@ -492,15 +454,14 @@ public: * @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); - } + bool testBit(unsigned n) const { return cln::logbitp(n, d_value); } /** * Returns k if the integer is equal to 2^(k-1) * @return k if the integer is equal to 2^(k-1) and 0 otherwise */ - unsigned isPow2() const { + unsigned isPow2() const + { if (d_value <= 0) return 0; // power2p returns n such that d_value = 2^(n-1) return cln::power2p(d_value); @@ -510,53 +471,101 @@ public: * If x != 0, returns the unique n s.t. 2^{n-1} <= abs(x) < 2^{n}. * If x == 0, returns 1. */ - size_t length() const { + size_t length() const + { int s = sgn(); - if(s == 0){ + if (s == 0) + { return 1; - }else if(s < 0){ + } + else if (s < 0) + { size_t len = cln::integer_length(d_value); - /*If this is -2^n, return len+1 not len to stay consistent with the definition above! - * From CLN's documentation of integer_length: - * This is the smallest n >= 0 such that -2^n <= x < 2^n. - * If x > 0, this is the unique n > 0 such that 2^(n-1) <= x < 2^n. + /*If this is -2^n, return len+1 not len to stay consistent with the + * definition above! From CLN's documentation of integer_length: This is + * the smallest n >= 0 such that -2^n <= x < 2^n. If x > 0, this is the + * unique n > 0 such that 2^(n-1) <= x < 2^n. */ size_t ord2 = cln::ord2(d_value); return (len == ord2) ? (len + 1) : len; - }else{ + } + else + { return cln::integer_length(d_value); } } -/* cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */ -/* This function ("extended gcd") returns the greatest common divisor g of a and b and at the same time the representation of g as an integral linear combination of a and b: u and v with u*a+v*b = g, g >= 0. u and v will be normalized to be of smallest possible absolute value, in the following sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy the inequalities abs(u) <= abs(b)/(2*g), abs(v) <= abs(a)/(2*g). */ - static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){ + /* cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */ + /* This function ("extended gcd") returns the greatest common divisor g of a + * and b and at the same time the representation of g as an integral linear + * combination of a and b: u and v with u*a+v*b = g, g >= 0. u and v will be + * normalized to be of smallest possible absolute value, in the following + * sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy + * the inequalities abs(u) <= abs(b)/(2*g), abs(v) <= abs(a)/(2*g). */ + static void extendedGcd( + Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b) + { g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value); } /** Returns a reference to the minimum of two integers. */ - static const Integer& min(const Integer& a, const Integer& b){ - return (a <=b ) ? a : b; + static const Integer& min(const Integer& a, const Integer& b) + { + return (a <= b) ? a : b; } /** Returns a reference to the maximum of two integers. */ - static const Integer& max(const Integer& a, const Integer& b){ - return (a >= b ) ? a : b; + static const Integer& max(const Integer& a, const Integer& b) + { + return (a >= b) ? a : b; } - friend class CVC4::Rational; -};/* class Integer */ + private: + /** + * Gets a reference to the cln data that backs up the integer. + * Only accessible to friend classes. + */ + const cln::cl_I& get_cl_I() const { return d_value; } + // Throws a std::invalid_argument on invalid input `s` for the given base. + void readInt(const cln::cl_read_flags& flags, + const std::string& s, + unsigned base); -struct IntegerHashFunction { - inline size_t operator()(const CVC4::Integer& i) const { - return i.hash(); - } -};/* struct IntegerHashFunction */ + // Throws a std::invalid_argument on invalid inputs. + void parseInt(const std::string& s, unsigned base); + + // These constants are to help with CLN conversion in 32 bit. + // See http://www.ginac.de/CLN/cln.html#Conversions + static signed int s_fastSignedIntMax; /* 2^29 - 1 */ + static signed int s_fastSignedIntMin; /* -2^29 */ + static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */ + + static signed long + s_slowSignedIntMax; /* std::numeric_limits<signed int>::max() */ + static signed long + s_slowSignedIntMin; /* std::numeric_limits<signed int>::min() */ + static unsigned long + s_slowUnsignedIntMax; /* std::numeric_limits<unsigned int>::max() */ + static unsigned long s_signedLongMin; + static unsigned long s_signedLongMax; + static unsigned long s_unsignedLongMax; + + /** + * Stores the value of the rational is stored in a C++ CLN integer class. + */ + cln::cl_I d_value; +}; /* class Integer */ + +struct IntegerHashFunction +{ + inline size_t operator()(const CVC4::Integer& i) const { return i.hash(); } +}; /* struct IntegerHashFunction */ -inline std::ostream& operator<<(std::ostream& os, const Integer& n) { +inline std::ostream& operator<<(std::ostream& os, const Integer& n) +{ return os << n.toString(); } -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* CVC4__INTEGER_H */ |