blob: 2416b7fc34d7aa73eb4355790ba3ec8b7c288bbb [file] [log] [blame]
 /********************* */ /*! \file integer_gmp_imp.h ** \verbatim ** Original author: Tim King ** Major contributors: Morgan Deters, Liana Hadarean ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** ** \brief A multiprecision integer constant; wraps a GMP multiprecision ** integer. ** ** A multiprecision integer constant; wraps a GMP multiprecision integer. **/ #include "cvc4_public.h" #ifndef __CVC4__INTEGER_H #define __CVC4__INTEGER_H #include #include #include #include "util/gmp_util.h" #include "util/exception.h" 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; public: /** * 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; } /** * Constructs an Integer by copying a GMP C++ primitive. */ Integer(const mpz_class& val) : d_value(val) {} /** Constructs a rational with the 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(). */ 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) {} Integer( signed int z) : d_value(z) {} Integer(unsigned 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(z)) {} Integer(uint64_t z) : d_value(static_cast(z)) {} #endif /* CVC4_NEED_INT64_T_OVERLOADS */ ~Integer() {} 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; } 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) { 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) { 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) { d_value *= y.d_value; return *this; } 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 { 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 { 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 { mpz_class result; mpz_com(result.get_mpz_t(), d_value.get_mpz_t()); return Integer(result); } /** * Return this*(2^pow). */ 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 ); } /** * Returns the Integer obtained by setting the ith bit of the * 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); } bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); } /** * Returns the integer with the binary representation of size bits * extended with amount 1's */ Integer oneExtend(uint32_t size, uint32_t amount) const { // check that the size is accurate DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); mpz_class res = d_value; for (unsigned i = size; i < size + amount; ++i) { mpz_setbit(res.get_mpz_t(), i); } return Integer(res); } 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 { // bitCount = high-low+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_q_2exp(div.get_mpz_t(), rem.get_mpz_t(), low); return Integer(div); } /** * Returns the floor(this / y) */ 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 ); } /** * Returns r == this - floor(this/y)*y */ 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 ); } /** * 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()); } /** * Returns the ceil(this / y) */ 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 ); } /** * Returns the ceil(this / y) */ 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 ); } /** * 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) { // compute the floor and then fix the value up if needed. floorQR(q,r,x,y); 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){ // y = abs(y) // n = y * q - y + r + y // n = y * (q-1) + (r+y) q -= 1; r += y; }else{ // y = -abs(y) // n = y * q + y + r - y // n = y * (q+1) + (r-y) q += 1; r -= y; } } } /** * 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); return q; } /** * 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); return r; } /** * If y divides *this, then exactQuotient returns (this/y) */ Integer exactQuotient(const Integer& y) const { DebugCheckArgument(y.divides(*this), y); mpz_class q; mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); return Integer( q ); } /** * Returns y mod 2^exp */ 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); } /** * Returns y / 2^exp */ 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()); } inline bool strictlyPositive() const { return sgn() > 0; } inline bool strictlyNegative() 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 isNegativeOne() const { return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0; } /** * Raise this Integer to the power exp. * * @param exp the exponent */ 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 ); } /** * Return the greatest common divisor of this integer with another. */ 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); } /** * Return the least common multiple of this integer with another. */ 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); } /** * All non-zero integers z, z.divide(0) * ! zero.divides(zero) */ 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; } /** * Return the absolute value of this integer. */ Integer abs() const { return d_value >= 0 ? *this : -*this; } std::string toString(int base = 10) const{ return d_value.get_str(base); } bool fitsSignedInt() const; bool fitsUnsignedInt() const; signed int getSignedInt() const; unsigned int getUnsignedInt() 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()"); return si; } 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, "Overflow detected in Integer::getUnsignedLong()"); return ui; } /** * 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()); } /** * Returns true iff bit n is set. * * @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); } /** * 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 { 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) { // return the index of the first one plus 1 return mpz_scan1(d_value.get_mpz_t(), 0) + 1; } 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){ return 1; }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()); } /** Returns a reference to the minimum of two integers. */ 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; } friend class CVC4::Rational; };/* 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) { return os << n.toString(); } }/* CVC4 namespace */ #endif /* __CVC4__INTEGER_H */