diff options
Diffstat (limited to 'src/util/integer_gmp_imp.h')
-rw-r--r-- | src/util/integer_gmp_imp.h | 343 |
1 files changed, 179 insertions, 164 deletions
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index f5da13f06..e42781c5f 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -20,9 +20,9 @@ #ifndef CVC4__INTEGER_H #define CVC4__INTEGER_H -#include <string> #include <iosfwd> #include <limits> +#include <string> #include "base/exception.h" #include "util/gmp_util.h" @@ -31,29 +31,18 @@ namespace CVC4 { 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. - */ - mpz_class d_value; - - /** - * Gets a reference to the gmp data that backs up the integer. - * Only accessible to friend classes. - */ - const mpz_class& get_mpz() const { return d_value; } +class CVC4_PUBLIC Integer +{ + friend class CVC4::Rational; + public: /** * Constructs an Integer by copying a GMP C++ primitive. */ Integer(const mpz_class& val) : d_value(val) {} -public: - /** Constructs a rational with the value 0. */ - Integer() : d_value(0){} + Integer() : d_value(0) {} /** * Constructs a Integer from a C string. @@ -66,13 +55,13 @@ public: Integer(const Integer& q) : d_value(q.d_value) {} - Integer( signed int z) : d_value(z) {} + Integer(signed int z) : d_value(z) {} Integer(unsigned int z) : d_value(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 */ @@ -81,91 +70,82 @@ public: /** * Returns a copy of d_value to enable public access of GMP data. */ - mpz_class getValue() const - { - return d_value; - } + const mpz_class& 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 + { mpz_class result; mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer(result); } - Integer bitwiseAnd(const Integer& y) const { + Integer bitwiseAnd(const Integer& y) const + { mpz_class result; 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 { + 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()); return Integer(result); } - Integer bitwiseNot() const { + Integer bitwiseNot() const + { mpz_class result; mpz_com(result.get_mpz_t(), d_value.get_mpz_t()); return Integer(result); @@ -174,25 +154,25 @@ public: /** * Return this*(2^pow). */ - Integer multiplyByPow2(uint32_t pow) const{ + Integer multiplyByPow2(uint32_t pow) const + { mpz_class result; mpz_mul_2exp(result.get_mpz_t(), d_value.get_mpz_t(), pow); - return Integer( result ); + return Integer(result); } /** * Returns the Integer obtained by setting the ith bit of the * current Integer to 1. */ - Integer setBit(uint32_t i) const { + Integer setBit(uint32_t i) const + { mpz_class res = d_value; mpz_setbit(res.get_mpz_t(), i); return Integer(res); } - bool isBitSet(uint32_t i) const { - return !extractBitRange(1, i).isZero(); - } + bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); } /** * Returns the integer with the binary representation of size bits @@ -200,17 +180,16 @@ public: */ Integer oneExtend(uint32_t size, uint32_t amount) const; - uint32_t toUnsignedInt() const { - return mpz_get_ui(d_value.get_mpz_t()); - } + uint32_t toUnsignedInt() const { return mpz_get_ui(d_value.get_mpz_t()); } /** See GMP Documentation. */ - Integer extractBitRange(uint32_t bitCount, uint32_t low) const { + Integer extractBitRange(uint32_t bitCount, uint32_t low) const + { // bitCount = high-low+1 - uint32_t high = low + bitCount-1; + uint32_t high = low + bitCount - 1; //— Function: void mpz_fdiv_r_2exp (mpz_t r, mpz_t n, mp_bitcnt_t b) mpz_class rem, div; - mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high+1); + mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high + 1); mpz_fdiv_q_2exp(div.get_mpz_t(), rem.get_mpz_t(), low); return Integer(div); @@ -219,72 +198,91 @@ public: /** * Returns the floor(this / y) */ - Integer floorDivideQuotient(const Integer& y) const { + Integer floorDivideQuotient(const Integer& y) const + { mpz_class q; mpz_fdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); - return Integer( q ); + return Integer(q); } /** * Returns r == this - floor(this/y)*y */ - Integer floorDivideRemainder(const Integer& y) const { + Integer floorDivideRemainder(const Integer& y) const + { mpz_class r; mpz_fdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); - return Integer( r ); + return Integer(r); } /** * Computes a floor quotient and remainder for x divided by y. */ - static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) { - mpz_fdiv_qr(q.d_value.get_mpz_t(), r.d_value.get_mpz_t(), x.d_value.get_mpz_t(), y.d_value.get_mpz_t()); + static void floorQR(Integer& q, + Integer& r, + const Integer& x, + const Integer& y) + { + mpz_fdiv_qr(q.d_value.get_mpz_t(), + r.d_value.get_mpz_t(), + x.d_value.get_mpz_t(), + y.d_value.get_mpz_t()); } /** * Returns the ceil(this / y) */ - Integer ceilingDivideQuotient(const Integer& y) const { + Integer ceilingDivideQuotient(const Integer& y) const + { mpz_class q; mpz_cdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); - return Integer( q ); + return Integer(q); } /** * Returns the ceil(this / y) */ - Integer ceilingDivideRemainder(const Integer& y) const { + Integer ceilingDivideRemainder(const Integer& y) const + { mpz_class r; mpz_cdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); - return Integer( r ); + return Integer(r); } /** - * Computes a quotient and remainder according to Boute's Euclidean definition. - * euclidianDivideQuotient, euclidianDivideRemainder. + * Computes a quotient 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) @@ -298,9 +296,10 @@ public: * Returns the quotient 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; } @@ -308,13 +307,13 @@ public: * Returns the remainder 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; } - /** * If y divides *this, then exactQuotient returns (this/y) */ @@ -323,7 +322,8 @@ public: /** * Returns y mod 2^exp */ - Integer modByPow2(uint32_t exp) const { + Integer modByPow2(uint32_t exp) const + { mpz_class res; mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp); return Integer(res); @@ -332,34 +332,25 @@ public: /** * Returns y / 2^exp */ - Integer divByPow2(uint32_t exp) const { + Integer divByPow2(uint32_t exp) const + { mpz_class res; mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp); return Integer(res); } + int sgn() const { return mpz_sgn(d_value.get_mpz_t()); } - int sgn() const { - return mpz_sgn(d_value.get_mpz_t()); - } + 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; } - bool isOne() const { - return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0; - } + bool isOne() const { return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0; } - bool isNegativeOne() const { + bool isNegativeOne() const + { return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0; } @@ -368,7 +359,8 @@ public: * * @param exp the exponent */ - Integer pow(unsigned long int exp) const { + Integer pow(unsigned long int exp) const + { mpz_class result; mpz_pow_ui(result.get_mpz_t(), d_value.get_mpz_t(), exp); return Integer(result); @@ -377,7 +369,8 @@ public: /** * Return the greatest common divisor of this integer with another. */ - Integer gcd(const Integer& y) const { + Integer gcd(const Integer& y) const + { mpz_class result; mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer(result); @@ -386,7 +379,8 @@ public: /** * Return the least common multiple of this integer with another. */ - Integer lcm(const Integer& y) const { + Integer lcm(const Integer& y) const + { mpz_class result; mpz_lcm(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer(result); @@ -420,7 +414,8 @@ public: * All non-zero integers z, z.divide(0) * ! zero.divides(zero) */ - bool divides(const Integer& y) const { + bool divides(const Integer& y) const + { int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t()); return res != 0; } @@ -428,13 +423,9 @@ 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{ - return d_value.get_str(base); - } + std::string toString(int base = 10) const { return d_value.get_str(base); } bool fitsSignedInt() const; @@ -448,18 +439,22 @@ public: bool fitsUnsignedLong() const; - long getLong() const { + long getLong() const + { long si = d_value.get_si(); // ensure there wasn't overflow - CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this, - "Overflow detected in Integer::getLong()."); + CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, + this, + "Overflow detected in Integer::getLong()."); return si; } - unsigned long getUnsignedLong() const { + unsigned long getUnsignedLong() const + { unsigned long ui = d_value.get_ui(); // ensure there wasn't overflow - CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this, + CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, + this, "Overflow detected in Integer::getUnsignedLong()."); return ui; } @@ -468,9 +463,7 @@ public: * Computes the hash of the node from the first word of the * numerator, the denominator. */ - size_t hash() const { - return gmpz_hash(d_value.get_mpz_t()); - } + size_t hash() const { return gmpz_hash(d_value.get_mpz_t()); } /** * Returns true iff bit n is set. @@ -478,66 +471,88 @@ 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 mpz_tstbit(d_value.get_mpz_t(), n); - } + bool testBit(unsigned n) const { return mpz_tstbit(d_value.get_mpz_t(), n); } /** * 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; // check that the number of ones in the binary representation is 1 - if (mpz_popcount(d_value.get_mpz_t()) == 1) { + if (mpz_popcount(d_value.get_mpz_t()) == 1) + { // return the index of the first one plus 1 return mpz_scan1(d_value.get_mpz_t(), 0) + 1; } - return 0; + return 0; } - /** * If x != 0, returns the smallest n s.t. 2^{n-1} <= abs(x) < 2^{n}. * If x == 0, returns 1. */ - size_t length() const { - if(sgn() == 0){ + size_t length() const + { + if (sgn() == 0) + { return 1; - }else{ - return mpz_sizeinbase(d_value.get_mpz_t(),2); + } + else + { + return mpz_sizeinbase(d_value.get_mpz_t(), 2); } } - static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){ - //see the documentation for: - //mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b); - mpz_gcdext (g.d_value.get_mpz_t(), s.d_value.get_mpz_t(), t.d_value.get_mpz_t(), a.d_value.get_mpz_t(), b.d_value.get_mpz_t()); + static void extendedGcd( + Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b) + { + // see the documentation for: + // mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b); + mpz_gcdext(g.d_value.get_mpz_t(), + s.d_value.get_mpz_t(), + t.d_value.get_mpz_t(), + a.d_value.get_mpz_t(), + b.d_value.get_mpz_t()); } /** 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 gmp data that backs up the integer. + * Only accessible to friend classes. + */ + const mpz_class& get_mpz() const { return d_value; } -struct IntegerHashFunction { - inline size_t operator()(const CVC4::Integer& i) const { - return i.hash(); - } -};/* struct IntegerHashFunction */ + /** + * Stores the value of the rational is stored in a C++ GMP integer class. + * Using this instead of mpz_t allows for easier destruction. + */ + mpz_class 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 */ |