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 pow(unsigned long int exp) const
Raise this Integer to the power exp.
bool operator>=(const Integer &y) const
Integer setBit(uint32_t i) const
Returns the Integer obtained by setting the ith bit of the current Integer to 1.
std::string toString(int base=10) const
Integer & operator+=(const Integer &y)
Integer lcm(const Integer &y) const
Return the least common multiple of this integer with another.
bool isNegativeOne() const
uint32_t toUnsignedInt() const
Integer floorDivideQuotient(const Integer &y) const
Returns the floor(this / y)
bool operator!=(const Integer &y) const
Integer divByPow2(uint32_t exp) const
Returns y / 2^exp.
void DebugCheckArgument(bool cond, const T &arg, const char *fmt,...)
bool operator<=(const Integer &y) const
bool isBitSet(uint32_t i) const
Integer abs() const
Return the absolute value of this integer.
Integer multiplyByPow2(uint32_t pow) const
Return this*(2^pow).
unsigned long getUnsignedLong() const
size_t operator()(const CVC4::Integer &i) const
Integer(unsigned long int z)
size_t hash() const
Computes the hash of the node from the first word of the numerator, the denominator.
Integer(const Integer &q)
static void extendedGcd(Integer &g, Integer &s, Integer &t, const Integer &a, const Integer &b)
Integer exactQuotient(const Integer &y) const
If y divides *this, then exactQuotient returns (this/y)
Integer ceilingDivideQuotient(const Integer &y) const
Returns the ceil(this / y)
A multi-precision rational constant.
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Integer & operator-=(const Integer &y)
CVC4's exception base class and some associated utilities.
Integer operator-(const Integer &y) const
bool strictlyNegative() const
Integer gcd(const Integer &y) const
Return the greatest common divisor of this integer with another.
bool divides(const Integer &y) const
All non-zero integers z, z.divide(0) ! zero.divides(zero)
Integer & operator=(const Integer &x)
size_t length() const
If x != 0, returns the smallest n s.t.
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 floorDivideRemainder(const Integer &y) const
Returns r == this - floor(this/y)*y.
size_t gmpz_hash(const mpz_t toHash)
Hashes the gmp integer primitive in a word by word fashion.
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
[[ Add one-line brief description here ]]
Integer()
Constructs a rational with the value 0.
Integer bitwiseNot() const
Integer euclidianDivideQuotient(const Integer &y) const
Returns the quoitent according to Boute's Euclidean definition.
Integer euclidianDivideRemainder(const Integer &y) const
Returns the remainfing according to Boute's Euclidean definition.
Integer operator-() const
Integer ceilingDivideRemainder(const Integer &y) const
Returns the ceil(this / y)
bool testBit(unsigned n) const
Returns true iff bit n is set.
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool strictlyPositive() const
Integer bitwiseXor(const Integer &y) const
Integer modByPow2(uint32_t exp) const
Returns y mod 2^exp.
static const Integer & min(const Integer &a, const Integer &b)
Returns a reference to the minimum of two integers.
Integer bitwiseOr(const Integer &y) const
static const Integer & max(const Integer &a, const Integer &b)
Returns a reference to the maximum of two integers.
static void floorQR(Integer &q, Integer &r, const Integer &x, const Integer &y)
Computes a floor quotient and remainder for x divided by y.
Integer extractBitRange(uint32_t bitCount, uint32_t low) const
See GMP Documentation.
Integer(signed long int z)
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 operator+(const Integer &y) const
Integer bitwiseAnd(const Integer &y) const
unsigned isPow2() const
Returns k if the integer is equal to 2^(k-1)
bool operator==(const Integer &y) const
Integer operator*(const Integer &y) const