: d_value(s, base)
{}
+Integer& Integer::operator=(const Integer& x)
+{
+ if (this == &x) return *this;
+ d_value = x.d_value;
+ return *this;
+}
+
+bool Integer::operator==(const Integer& y) const
+{
+ return d_value == y.d_value;
+}
+
+Integer Integer::operator-() const { return Integer(-(d_value)); }
+
+bool Integer::operator!=(const Integer& y) const
+{
+ return d_value != y.d_value;
+}
+
+bool Integer::operator<(const Integer& y) const { return d_value < y.d_value; }
+
+bool Integer::operator<=(const Integer& y) const
+{
+ return d_value <= y.d_value;
+}
+
+bool Integer::operator>(const Integer& y) const { return d_value > y.d_value; }
+
+bool Integer::operator>=(const Integer& y) const
+{
+ return d_value >= y.d_value;
+}
+
+Integer Integer::operator+(const Integer& y) const
+{
+ return Integer(d_value + y.d_value);
+}
+
+Integer& Integer::operator+=(const Integer& y)
+{
+ d_value += y.d_value;
+ return *this;
+}
+
+Integer Integer::operator-(const Integer& y) const
+{
+ return Integer(d_value - y.d_value);
+}
+
+Integer& Integer::operator-=(const Integer& y)
+{
+ d_value -= y.d_value;
+ return *this;
+}
+
+Integer Integer::operator*(const Integer& y) const
+{
+ return Integer(d_value * y.d_value);
+}
+
+Integer& Integer::operator*=(const Integer& y)
+{
+ d_value *= y.d_value;
+ return *this;
+}
+
+Integer 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 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 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 Integer::bitwiseNot() const
+{
+ mpz_class result;
+ mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
+ return Integer(result);
+}
+
+Integer 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);
+}
+
Integer Integer::setBit(uint32_t i, bool value) const
{
mpz_class res = d_value;
return Integer(res);
}
-bool Integer::fitsSignedInt() const {
- return d_value.fits_sint_p();
+bool Integer::isBitSet(uint32_t i) const
+{
+ return !extractBitRange(1, i).isZero();
}
-bool Integer::fitsUnsignedInt() const {
- return d_value.fits_uint_p();
+Integer 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);
}
-signed int Integer::getSignedInt() const {
- // ensure there isn't overflow
- CheckArgument(d_value <= std::numeric_limits<int>::max(), this,
- "Overflow detected in Integer::getSignedInt().");
- CheckArgument(d_value >= std::numeric_limits<int>::min(), this,
- "Overflow detected in Integer::getSignedInt().");
- CheckArgument(fitsSignedInt(), this,
- "Overflow detected in Integer::getSignedInt().");
- return (signed int) d_value.get_si();
+uint32_t Integer::toUnsignedInt() const
+{
+ return mpz_get_ui(d_value.get_mpz_t());
}
-unsigned int Integer::getUnsignedInt() const {
- // ensure there isn't overflow
- CheckArgument(d_value <= std::numeric_limits<unsigned int>::max(), this,
- "Overflow detected in Integer::getUnsignedInt()");
- CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this,
- "Overflow detected in Integer::getUnsignedInt()");
- CheckArgument(fitsSignedInt(), this,
- "Overflow detected in Integer::getUnsignedInt()");
- return (unsigned int) d_value.get_ui();
+Integer 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);
}
-bool Integer::fitsSignedLong() const {
- return d_value.fits_slong_p();
+Integer 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);
}
-bool Integer::fitsUnsignedLong() const {
- return d_value.fits_ulong_p();
+Integer 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);
}
-Integer 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;
+void Integer::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());
+}
- for (unsigned i = size; i < size + amount; ++i) {
- mpz_setbit(res.get_mpz_t(), i);
+Integer 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);
+}
+
+Integer 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);
+}
+
+void Integer::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;
+ }
}
+}
- return Integer(res);
+Integer Integer::euclidianDivideQuotient(const Integer& y) const
+{
+ Integer q, r;
+ euclidianQR(q, r, *this, y);
+ return q;
+}
+
+Integer Integer::euclidianDivideRemainder(const Integer& y) const
+{
+ Integer q, r;
+ euclidianQR(q, r, *this, y);
+ return r;
}
-Integer Integer::exactQuotient(const Integer& y) const {
+Integer 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 );
+ return Integer(q);
+}
+
+Integer 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);
+}
+
+Integer 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 Integer::sgn() const { return mpz_sgn(d_value.get_mpz_t()); }
+
+bool Integer::strictlyPositive() const { return sgn() > 0; }
+
+bool Integer::strictlyNegative() const { return sgn() < 0; }
+
+bool Integer::isZero() const { return sgn() == 0; }
+
+bool Integer::isOne() const { return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0; }
+
+bool Integer::isNegativeOne() const
+{
+ return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0;
+}
+
+Integer 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);
+}
+
+Integer 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);
+}
+
+Integer 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);
}
Integer Integer::modAdd(const Integer& y, const Integer& m) const
}
return Integer(res);
}
+
+bool Integer::divides(const Integer& y) const
+{
+ int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t());
+ return res != 0;
+}
+
+Integer Integer::abs() const { return d_value >= 0 ? *this : -*this; }
+
+std::string Integer::toString(int base) const { return d_value.get_str(base); }
+
+bool Integer::fitsSignedInt() const { return d_value.fits_sint_p(); }
+
+bool Integer::fitsUnsignedInt() const { return d_value.fits_uint_p(); }
+
+signed int Integer::getSignedInt() const
+{
+ // ensure there isn't overflow
+ CheckArgument(d_value <= std::numeric_limits<int>::max(),
+ this,
+ "Overflow detected in Integer::getSignedInt().");
+ CheckArgument(d_value >= std::numeric_limits<int>::min(),
+ this,
+ "Overflow detected in Integer::getSignedInt().");
+ CheckArgument(
+ fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt().");
+ return (signed int)d_value.get_si();
+}
+
+unsigned int Integer::getUnsignedInt() const
+{
+ // ensure there isn't overflow
+ CheckArgument(d_value <= std::numeric_limits<unsigned int>::max(),
+ this,
+ "Overflow detected in Integer::getUnsignedInt()");
+ CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(),
+ this,
+ "Overflow detected in Integer::getUnsignedInt()");
+ CheckArgument(
+ fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+ return (unsigned int)d_value.get_ui();
+}
+
+bool Integer::fitsSignedLong() const { return d_value.fits_slong_p(); }
+
+bool Integer::fitsUnsignedLong() const { return d_value.fits_ulong_p(); }
+
+long Integer::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 Integer::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;
+}
+
+size_t Integer::hash() const { return gmpz_hash(d_value.get_mpz_t()); }
+
+bool Integer::testBit(unsigned n) const
+{
+ return mpz_tstbit(d_value.get_mpz_t(), n);
+}
+
+unsigned Integer::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;
+}
+
+size_t Integer::length() const
+{
+ if (sgn() == 0)
+ {
+ return 1;
+ }
+ else
+ {
+ return mpz_sizeinbase(d_value.get_mpz_t(), 2);
+ }
+}
+
+void Integer::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());
+}
+
+const Integer& Integer::min(const Integer& a, const Integer& b)
+{
+ return (a <= b) ? a : b;
+}
+
+/** Returns a reference to the maximum of two integers. */
+const Integer& Integer::max(const Integer& a, const Integer& b)
+{
+ return (a >= b) ? a : b;
+}
+
} /* namespace CVC4 */
Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
+ /** Destructor. */
~Integer() {}
- /**
- * Returns a copy of d_value to enable public access of GMP data.
- */
+ /** Returns a copy of d_value to enable public access of GMP data. */
const mpz_class& getValue() const { return d_value; }
- 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);
- }
+ /** Overload copy assignment operator. */
+ Integer& operator=(const Integer& x);
+
+ /** Overload equality comparison operator. */
+ bool operator==(const Integer& y) const;
+ /** Overload disequality comparison operator. */
+ bool operator!=(const Integer& y) const;
+ /** Overload less than comparison operator. */
+ bool operator<(const Integer& y) const;
+ /** Overload less than or equal comparison operator. */
+ bool operator<=(const Integer& y) const;
+ /** Overload greater than comparison operator. */
+ bool operator>(const Integer& y) const;
+ /** Overload greater than or equal comparison operator. */
+ bool operator>=(const Integer& y) const;
+
+ /** Overload negation operator. */
+ Integer operator-() const;
+ /** Overload addition operator. */
+ Integer operator+(const Integer& y) const;
+ /** Overload addition assignment operator. */
+ Integer& operator+=(const Integer& y);
+ /** Overload subtraction operator. */
+ Integer operator-(const Integer& y) const;
+ /** Overload subtraction assignment operator. */
+ Integer& operator-=(const Integer& y);
+ /** Overload multiplication operator. */
+ Integer operator*(const Integer& y) const;
+ /** Overload multiplication assignment operator. */
+ Integer& operator*=(const Integer& y);
+
+ /** Return the bit-wise or of this and the given Integer. */
+ Integer bitwiseOr(const Integer& y) const;
+ /** Return the bit-wise and of this and the given Integer. */
+ Integer bitwiseAnd(const Integer& y) const;
+ /** Return the bit-wise exclusive or of this and the given Integer. */
+ Integer bitwiseXor(const Integer& y) const;
+ /** Return the bit-wise not of this Integer. */
+ Integer bitwiseNot() const;
+
+ /** Return this*(2^pow). */
+ Integer multiplyByPow2(uint32_t pow) const;
/**
* Returns the Integer obtained by setting the ith bit of the
*/
Integer setBit(uint32_t i, bool value) const;
- bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); }
+ /** Return true if bit at index 'i' is 1, and false otherwise. */
+ bool isBitSet(uint32_t i) const;
/**
* Returns the integer with the binary representation of size bits
*/
Integer oneExtend(uint32_t size, uint32_t amount) const;
- 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);
- }
+ uint32_t toUnsignedInt() const;
/**
- * Returns the floor(this / y)
+ * Extract a range of bits from index 'low' to (excluding) 'low + bitCount'.
+ * Note: corresponds to the extract operator of theory BV.
*/
- 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);
- }
+ Integer extractBitRange(uint32_t bitCount, uint32_t low) const;
- /**
- * 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);
- }
+ /** Returns the floor(this / y) */
+ Integer floorDivideQuotient(const Integer& y) const;
- /**
- * Computes a floor quotient and remainder for x divided by y.
- */
+ /** Returns r == this - floor(this/y)*y */
+ Integer floorDivideRemainder(const Integer& y) const;
+
+ /** 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());
- }
+ const Integer& y);
- /**
- * 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 ceilingDivideQuotient(const Integer& y) const;
- /**
- * 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);
- }
+ /** Returns the ceil(this / y) */
+ Integer ceilingDivideRemainder(const Integer& y) const;
/**
* Computes a quotient and remainder according to Boute's Euclidean
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;
- }
- }
- }
+ const Integer& y);
/**
* 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);
- return q;
- }
+ Integer euclidianDivideQuotient(const Integer& y) const;
/**
* 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);
- return r;
- }
+ Integer euclidianDivideRemainder(const Integer& y) const;
- /**
- * If y divides *this, then exactQuotient returns (this/y)
- */
+ /** If y divides *this, then exactQuotient returns (this/y). */
Integer exactQuotient(const Integer& y) const;
- /**
- * 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 mod 2^exp. */
+ Integer modByPow2(uint32_t exp) const;
- /**
- * 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);
- }
+ /** Returns y / 2^exp. */
+ Integer divByPow2(uint32_t exp) const;
- int sgn() const { return mpz_sgn(d_value.get_mpz_t()); }
+ /** Return 1 if this is > 0, 0 if it is 0, and -1 if it is < 0. */
+ int sgn() const;
- inline bool strictlyPositive() const { return sgn() > 0; }
+ /** Return true if this is > 0. */
+ bool strictlyPositive() const;
- inline bool strictlyNegative() const { return sgn() < 0; }
+ /** Return true if this is < 0. */
+ bool strictlyNegative() const;
- inline bool isZero() const { return sgn() == 0; }
+ /** Return true if this is 0. */
+ bool isZero() const;
- bool isOne() const { return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0; }
+ /** Return true if this is 1. */
+ bool isOne() const;
- bool isNegativeOne() const
- {
- return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0;
- }
+ /** Return true if this is -1. */
+ bool isNegativeOne() const;
- /**
- * Raise this Integer to the power <code>exp</code>.
- *
- * @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);
- }
+ /** Raise this Integer to the power 'exp'. */
+ Integer pow(unsigned long int exp) const;
- /**
- * 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 greatest common divisor of this integer with another. */
+ Integer gcd(const Integer& y) const;
- /**
- * 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);
- }
+ /** Return the least common multiple of this integer with another. */
+ Integer lcm(const Integer& y) const;
- /**
- * Compute addition of this Integer x + y modulo m.
- */
+ /** Compute addition of this Integer x + y modulo m. */
Integer modAdd(const Integer& y, const Integer& m) const;
- /**
- * Compute multiplication of this Integer x * y modulo m.
- */
+ /** Compute multiplication of this Integer x * y modulo m. */
Integer modMultiply(const Integer& y, const Integer& m) const;
/**
Integer modInverse(const Integer& m) const;
/**
- * All non-zero integers z, z.divide(0)
- * ! zero.divides(zero)
+ * Return true if 'y' divides this integer.
+ * Note: All non-zero integers devide zero, and zero does not divide 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;
- }
+ bool divides(const Integer& y) const;
- /**
- * Return the absolute value of this integer.
- */
- Integer abs() const { return d_value >= 0 ? *this : -*this; }
+ /** Return the absolute value of this integer. */
+ Integer abs() const;
- std::string toString(int base = 10) const { return d_value.get_str(base); }
+ /** Return a string representation of this Integer. */
+ std::string toString(int base = 10) const;
+ /** Return true if this Integer fits into a signed int. */
bool fitsSignedInt() const;
+ /** Return true if this Integer fits into an unsigned int. */
bool fitsUnsignedInt() const;
+ /** Return the signed int representation of this Integer. */
signed int getSignedInt() const;
+ /** Return the unsigned int representation of this Integer. */
unsigned int getUnsignedInt() const;
+ /** Return true if this Integer fits into a signed long. */
bool fitsSignedLong() const;
+ /** Return true if this Integer fits into an unsigned long. */
bool fitsUnsignedLong() 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;
- }
+ /** Return the signed long representation of this Integer. */
+ long getLong() const;
+
+ /** Return the unsigned long representation of this Integer. */
+ unsigned long getUnsignedLong() const;
/**
* 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;
/**
* 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); }
+ bool testBit(unsigned n) const;
/**
* 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;
- }
+ unsigned isPow2() const;
/**
* 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);
- }
- }
+ size_t length() const;
+ /**
+ * Return the greatest common divisor of a and b, and in addition set s and t
+ * to coefficients satisfying a*s + b*t = g.
+ *
+ * Note: The returned Integer is always positive, even if one or both of a
+ * and b are negative (or zero if both inputs are zero). For more
+ * details, see https://gmplib.org/manual/Number-Theoretic-Functions.
+ */
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());
- }
+ Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b);
/** 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);
/** 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);
private:
/**
projects / cvc5.git / commitdiff