20 #ifndef __CVC4__INTEGER_H
21 #define __CVC4__INTEGER_H
45 const mpz_class& get_mpz()
const {
return d_value; }
50 Integer(
const mpz_class& val) : d_value(val) {}
63 explicit Integer(
const char* s,
unsigned base = 10): d_value(s, base) {}
64 explicit Integer(
const std::string& s,
unsigned base = 10) : d_value(s, base) {}
70 Integer(
signed long int z) : d_value(z) {}
71 Integer(
unsigned long int z) : d_value(z) {}
73 #ifdef CVC4_NEED_INT64_T_OVERLOADS
74 Integer( int64_t z) : d_value(static_cast<long>(z)) {}
75 Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
81 if(
this == &x)
return *
this;
87 return d_value == y.d_value;
96 return d_value != y.d_value;
100 return d_value < y.d_value;
104 return d_value <= y.d_value;
108 return d_value > y.d_value;
112 return d_value >= y.d_value;
117 return Integer( d_value + y.d_value );
120 d_value += y.d_value;
125 return Integer( d_value - y.d_value );
128 d_value -= y.d_value;
133 return Integer( d_value * y.d_value );
136 d_value *= y.d_value;
143 mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
149 mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
155 mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
161 mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
170 mpz_mul_2exp(result.get_mpz_t(), d_value.get_mpz_t(), pow);
179 mpz_class res = d_value;
180 mpz_setbit(res.get_mpz_t(), i);
185 return !extractBitRange(1, i).isZero();
195 mpz_class res = d_value;
197 for (
unsigned i = size; i < size + amount; ++i) {
198 mpz_setbit(res.get_mpz_t(), i);
205 return mpz_get_ui(d_value.get_mpz_t());
211 uint32_t high = low + bitCount-1;
214 mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high+1);
215 mpz_fdiv_q_2exp(div.get_mpz_t(), rem.get_mpz_t(), low);
225 mpz_fdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
234 mpz_fdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
242 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());
250 mpz_cdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
259 mpz_cdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
303 euclidianQR(q,r, *
this, y);
313 euclidianQR(q,r, *
this, y);
324 mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
333 mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
342 mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
348 return mpz_sgn(d_value.get_mpz_t());
364 return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0;
368 return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0;
378 mpz_pow_ui(result.get_mpz_t(),d_value.get_mpz_t(),exp);
387 mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
396 mpz_lcm(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
405 int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t());
413 return d_value >= 0 ? *
this : -*
this;
417 return d_value.get_str(base);
423 long si = d_value.get_si();
425 CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
this,
426 "Overflow detected in Integer::getLong()");
430 unsigned long ui = d_value.get_ui();
432 CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0,
this,
433 "Overflow detected in Integer::getUnsignedLong()");
452 return mpz_tstbit(d_value.get_mpz_t(), n);
460 if (d_value <= 0)
return 0;
462 if (mpz_popcount(d_value.get_mpz_t()) == 1) {
464 return mpz_scan1(d_value.get_mpz_t(), 0) + 1;
478 return mpz_sizeinbase(d_value.get_mpz_t(),2);
485 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());
490 return (a <=b ) ? a : b;
495 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
Integer(const char *s, unsigned base=10)
Constructs a Integer from a C string.
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)
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
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, TypeConstant typeConstant)
[[ 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.
Integer(const std::string &s, unsigned base=10)
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
This file contains a summary of important user visible changes Changes which were previously missing *New bv2nat int2bv operators for bitvector integer inter compatibility *Support in linear logics div
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