20 #ifndef __CVC4__INTEGER_H 21 #define __CVC4__INTEGER_H 46 const mpz_class& get_mpz()
const {
return d_value; }
51 Integer(
const mpz_class& val) : d_value(val) {}
64 explicit Integer(
const char* s,
unsigned base = 10);
65 explicit Integer(
const std::string& s,
unsigned base = 10);
71 Integer(
signed long int z) : d_value(z) {}
72 Integer(
unsigned long int z) : d_value(z) {}
74 #ifdef CVC4_NEED_INT64_T_OVERLOADS 75 Integer( int64_t z) : d_value(static_cast<long>(z)) {}
76 Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
82 if(
this == &x)
return *
this;
88 return d_value == y.d_value;
97 return d_value != y.d_value;
101 return d_value < y.d_value;
105 return d_value <= y.d_value;
109 return d_value > y.d_value;
113 return d_value >= y.d_value;
118 return Integer( d_value + y.d_value );
121 d_value += y.d_value;
126 return Integer( d_value - y.d_value );
129 d_value -= y.d_value;
134 return Integer( d_value * y.d_value );
137 d_value *= y.d_value;
144 mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
150 mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
156 mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
162 mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
171 mpz_mul_2exp(result.get_mpz_t(), d_value.get_mpz_t(), pow);
180 mpz_class res = d_value;
181 mpz_setbit(res.get_mpz_t(), i);
186 return !extractBitRange(1, i).isZero();
196 mpz_class res = d_value;
198 for (
unsigned i = size; i < size + amount; ++i) {
199 mpz_setbit(res.get_mpz_t(), i);
206 return mpz_get_ui(d_value.get_mpz_t());
212 uint32_t high = low + bitCount-1;
215 mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high+1);
216 mpz_fdiv_q_2exp(div.get_mpz_t(), rem.get_mpz_t(), low);
226 mpz_fdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
235 mpz_fdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
243 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());
251 mpz_cdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
260 mpz_cdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
304 euclidianQR(q,r, *
this, y);
314 euclidianQR(q,r, *
this, y);
325 mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
334 mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
343 mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
349 return mpz_sgn(d_value.get_mpz_t());
365 return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0;
369 return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0;
379 mpz_pow_ui(result.get_mpz_t(),d_value.get_mpz_t(),exp);
388 mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
397 mpz_lcm(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
406 int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t());
414 return d_value >= 0 ? *this : -*
this;
418 return d_value.get_str(base);
421 bool fitsSignedInt()
const;
423 bool fitsUnsignedInt()
const;
425 signed int getSignedInt()
const;
427 unsigned int getUnsignedInt()
const;
430 long si = d_value.get_si();
432 CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
this,
433 "Overflow detected in Integer::getLong()");
437 unsigned long ui = d_value.get_ui();
439 CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0,
this,
440 "Overflow detected in Integer::getUnsignedLong()");
459 return mpz_tstbit(d_value.get_mpz_t(), n);
467 if (d_value <= 0)
return 0;
469 if (mpz_popcount(d_value.get_mpz_t()) == 1) {
471 return mpz_scan1(d_value.get_mpz_t(), 0) + 1;
485 return mpz_sizeinbase(d_value.get_mpz_t(),2);
492 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());
497 return (a <=b ) ? a : b;
502 return (a >= b ) ? a : b;
Integer bitwiseXor(const Integer &y) const
Integer & operator+=(const Integer &y)
Integer oneExtend(uint32_t size, uint32_t amount) const
Returns the integer with the binary representation of size bits extended with amount 1's...
Integer setBit(uint32_t i) const
Returns the Integer obtained by setting the ith bit of the current Integer to 1.
Integer pow(unsigned long int exp) const
Raise this Integer to the power exp.
bool testBit(unsigned n) const
Returns true iff bit n is set.
bool strictlyNegative() const
void DebugCheckArgument(bool cond, const T &arg, const char *fmt,...)
Integer gcd(const Integer &y) const
Return the greatest common divisor of this integer with another.
size_t hash() const
Computes the hash of the node from the first word of the numerator, the denominator.
bool isNegativeOne() const
Integer abs() const
Return the absolute value of this integer.
Integer euclidianDivideRemainder(const Integer &y) const
Returns the remainfing according to Boute's Euclidean definition.
Integer floorDivideQuotient(const Integer &y) const
Returns the floor(this / y)
bool isBitSet(uint32_t i) const
Integer(unsigned long int z)
Integer(const Integer &q)
static void extendedGcd(Integer &g, Integer &s, Integer &t, const Integer &a, const Integer &b)
Integer operator-(const Integer &y) const
uint32_t toUnsignedInt() const
A multi-precision rational constant.
std::ostream & operator<<(std::ostream &, const Command &)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
std::string toString(int base=10) const
size_t operator()(const CVC4::Integer &i) const
Integer extractBitRange(uint32_t bitCount, uint32_t low) const
See GMP Documentation.
Integer & operator-=(const Integer &y)
CVC4's exception base class and some associated utilities.
bool operator==(const Integer &y) const
bool operator!=(const Integer &y) const
Integer & operator=(const Integer &x)
static void euclidianQR(Integer &q, Integer &r, const Integer &x, const Integer &y)
Computes a quoitent and remainder according to Boute's Euclidean definition.
Integer operator+(const Integer &y) const
Integer modByPow2(uint32_t exp) const
Returns y mod 2^exp.
size_t gmpz_hash(const mpz_t toHash)
Hashes the gmp integer primitive in a word by word fashion.
[[ Add one-line brief description here ]]
Integer()
Constructs a rational with the value 0.
Integer ceilingDivideQuotient(const Integer &y) const
Returns the ceil(this / y)
Integer exactQuotient(const Integer &y) const
If y divides *this, then exactQuotient returns (this/y)
bool operator<=(const Integer &y) const
size_t length() const
If x != 0, returns the smallest n s.t.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Integer bitwiseNot() const
Integer lcm(const Integer &y) const
Return the least common multiple of this integer with another.
bool operator>=(const Integer &y) const
unsigned long getUnsignedLong() const
Integer divByPow2(uint32_t exp) const
Returns y / 2^exp.
Integer multiplyByPow2(uint32_t pow) const
Return this*(2^pow).
static const Integer & min(const Integer &a, const Integer &b)
Returns a reference to the minimum of two integers.
Integer floorDivideRemainder(const Integer &y) const
Returns r == this - floor(this/y)*y.
static const Integer & max(const Integer &a, const Integer &b)
Returns a reference to the maximum of two integers.
Integer ceilingDivideRemainder(const Integer &y) const
Returns the ceil(this / y)
Integer operator*(const Integer &y) const
static void floorQR(Integer &q, Integer &r, const Integer &x, const Integer &y)
Computes a floor quotient and remainder for x divided by y.
unsigned isPow2() const
Returns k if the integer is equal to 2^(k-1)
bool divides(const Integer &y) const
All non-zero integers z, z.divide(0) ! zero.divides(zero)
Integer(signed long int z)
Integer & operator*=(const Integer &y)
bool strictlyPositive() const
Integer bitwiseAnd(const Integer &y) const
Integer operator-() const
Integer euclidianDivideQuotient(const Integer &y) const
Returns the quoitent according to Boute's Euclidean definition.
Integer bitwiseOr(const Integer &y) const