cvc4-1.4
integer_gmp_imp.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__INTEGER_H
21 #define __CVC4__INTEGER_H
22 
23 #include <string>
24 #include <iostream>
25 #include <limits>
26 
27 #include "util/gmp_util.h"
28 #include "util/exception.h"
29 
30 namespace CVC4 {
31 
32 class Rational;
33 
35 private:
40  mpz_class d_value;
41 
46  const mpz_class& get_mpz() const { return d_value; }
47 
51  Integer(const mpz_class& val) : d_value(val) {}
52 
53 public:
54 
56  Integer() : d_value(0){}
57 
64  explicit Integer(const char* s, unsigned base = 10);
65  explicit Integer(const std::string& s, unsigned base = 10);
66 
67  Integer(const Integer& q) : d_value(q.d_value) {}
68 
69  Integer( signed int z) : d_value(z) {}
70  Integer(unsigned int z) : d_value(z) {}
71  Integer( signed long int z) : d_value(z) {}
72  Integer(unsigned long int z) : d_value(z) {}
73 
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)) {}
77 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
78 
79  ~Integer() {}
80 
82  if(this == &x) return *this;
83  d_value = x.d_value;
84  return *this;
85  }
86 
87  bool operator==(const Integer& y) const {
88  return d_value == y.d_value;
89  }
90 
91  Integer operator-() const {
92  return Integer(-(d_value));
93  }
94 
95 
96  bool operator!=(const Integer& y) const {
97  return d_value != y.d_value;
98  }
99 
100  bool operator< (const Integer& y) const {
101  return d_value < y.d_value;
102  }
103 
104  bool operator<=(const Integer& y) const {
105  return d_value <= y.d_value;
106  }
107 
108  bool operator> (const Integer& y) const {
109  return d_value > y.d_value;
110  }
111 
112  bool operator>=(const Integer& y) const {
113  return d_value >= y.d_value;
114  }
115 
116 
117  Integer operator+(const Integer& y) const {
118  return Integer( d_value + y.d_value );
119  }
121  d_value += y.d_value;
122  return *this;
123  }
124 
125  Integer operator-(const Integer& y) const {
126  return Integer( d_value - y.d_value );
127  }
129  d_value -= y.d_value;
130  return *this;
131  }
132 
133  Integer operator*(const Integer& y) const {
134  return Integer( d_value * y.d_value );
135  }
137  d_value *= y.d_value;
138  return *this;
139  }
140 
141 
142  Integer bitwiseOr(const Integer& y) const {
143  mpz_class result;
144  mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
145  return Integer(result);
146  }
147 
148  Integer bitwiseAnd(const Integer& y) const {
149  mpz_class result;
150  mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
151  return Integer(result);
152  }
153 
154  Integer bitwiseXor(const Integer& y) const {
155  mpz_class result;
156  mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
157  return Integer(result);
158  }
159 
160  Integer bitwiseNot() const {
161  mpz_class result;
162  mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
163  return Integer(result);
164  }
165 
169  Integer multiplyByPow2(uint32_t pow) const{
170  mpz_class result;
171  mpz_mul_2exp(result.get_mpz_t(), d_value.get_mpz_t(), pow);
172  return Integer( result );
173  }
174 
179  Integer setBit(uint32_t i) const {
180  mpz_class res = d_value;
181  mpz_setbit(res.get_mpz_t(), i);
182  return Integer(res);
183  }
184 
185  bool isBitSet(uint32_t i) const {
186  return !extractBitRange(1, i).isZero();
187  }
188 
193  Integer oneExtend(uint32_t size, uint32_t amount) const {
194  // check that the size is accurate
195  DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
196  mpz_class res = d_value;
197 
198  for (unsigned i = size; i < size + amount; ++i) {
199  mpz_setbit(res.get_mpz_t(), i);
200  }
201 
202  return Integer(res);
203  }
204 
205  uint32_t toUnsignedInt() const {
206  return mpz_get_ui(d_value.get_mpz_t());
207  }
208 
210  Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
211  // bitCount = high-low+1
212  uint32_t high = low + bitCount-1;
213  //— Function: void mpz_fdiv_r_2exp (mpz_t r, mpz_t n, mp_bitcnt_t b)
214  mpz_class rem, div;
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);
217 
218  return Integer(div);
219  }
220 
225  mpz_class q;
226  mpz_fdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
227  return Integer( q );
228  }
229 
234  mpz_class r;
235  mpz_fdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
236  return Integer( r );
237  }
238 
242  static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
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());
244  }
245 
250  mpz_class q;
251  mpz_cdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
252  return Integer( q );
253  }
254 
259  mpz_class r;
260  mpz_cdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
261  return Integer( r );
262  }
263 
273  static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
274  // compute the floor and then fix the value up if needed.
275  floorQR(q,r,x,y);
276 
277  if(r.strictlyNegative()){
278  // if r < 0
279  // abs(r) < abs(y)
280  // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
281  // n = y * q + r
282  // n = y * q - abs(y) + r + abs(y)
283  if(r.sgn() >= 0){
284  // y = abs(y)
285  // n = y * q - y + r + y
286  // n = y * (q-1) + (r+y)
287  q -= 1;
288  r += y;
289  }else{
290  // y = -abs(y)
291  // n = y * q + y + r - y
292  // n = y * (q+1) + (r-y)
293  q += 1;
294  r -= y;
295  }
296  }
297  }
303  Integer q,r;
304  euclidianQR(q,r, *this, y);
305  return q;
306  }
307 
313  Integer q,r;
314  euclidianQR(q,r, *this, y);
315  return r;
316  }
317 
318 
322  Integer exactQuotient(const Integer& y) const {
323  DebugCheckArgument(y.divides(*this), y);
324  mpz_class q;
325  mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
326  return Integer( q );
327  }
328 
332  Integer modByPow2(uint32_t exp) const {
333  mpz_class res;
334  mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
335  return Integer(res);
336  }
337 
341  Integer divByPow2(uint32_t exp) const {
342  mpz_class res;
343  mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
344  return Integer(res);
345  }
346 
347 
348  int sgn() const {
349  return mpz_sgn(d_value.get_mpz_t());
350  }
351 
352  inline bool strictlyPositive() const {
353  return sgn() > 0;
354  }
355 
356  inline bool strictlyNegative() const {
357  return sgn() < 0;
358  }
359 
360  inline bool isZero() const {
361  return sgn() == 0;
362  }
363 
364  bool isOne() const {
365  return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0;
366  }
367 
368  bool isNegativeOne() const {
369  return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0;
370  }
371 
377  Integer pow(unsigned long int exp) const {
378  mpz_class result;
379  mpz_pow_ui(result.get_mpz_t(),d_value.get_mpz_t(),exp);
380  return Integer( result );
381  }
382 
386  Integer gcd(const Integer& y) const {
387  mpz_class result;
388  mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
389  return Integer(result);
390  }
391 
395  Integer lcm(const Integer& y) const {
396  mpz_class result;
397  mpz_lcm(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
398  return Integer(result);
399  }
400 
405  bool divides(const Integer& y) const {
406  int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t());
407  return res != 0;
408  }
409 
413  Integer abs() const {
414  return d_value >= 0 ? *this : -*this;
415  }
416 
417  std::string toString(int base = 10) const{
418  return d_value.get_str(base);
419  }
420 
421  bool fitsSignedInt() const;
422 
423  bool fitsUnsignedInt() const;
424 
425  signed int getSignedInt() const;
426 
427  unsigned int getUnsignedInt() const;
428 
429  long getLong() const {
430  long si = d_value.get_si();
431  // ensure there wasn't overflow
432  CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this,
433  "Overflow detected in Integer::getLong()");
434  return si;
435  }
436  unsigned long getUnsignedLong() const {
437  unsigned long ui = d_value.get_ui();
438  // ensure there wasn't overflow
439  CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this,
440  "Overflow detected in Integer::getUnsignedLong()");
441  return ui;
442  }
443 
448  size_t hash() const {
449  return gmpz_hash(d_value.get_mpz_t());
450  }
451 
458  bool testBit(unsigned n) const {
459  return mpz_tstbit(d_value.get_mpz_t(), n);
460  }
461 
466  unsigned isPow2() const {
467  if (d_value <= 0) return 0;
468  // check that the number of ones in the binary representation is 1
469  if (mpz_popcount(d_value.get_mpz_t()) == 1) {
470  // return the index of the first one plus 1
471  return mpz_scan1(d_value.get_mpz_t(), 0) + 1;
472  }
473  return 0;
474  }
475 
476 
481  size_t length() const {
482  if(sgn() == 0){
483  return 1;
484  }else{
485  return mpz_sizeinbase(d_value.get_mpz_t(),2);
486  }
487  }
488 
489  static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){
490  //see the documentation for:
491  //mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b);
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());
493  }
494 
496  static const Integer& min(const Integer& a, const Integer& b){
497  return (a <=b ) ? a : b;
498  }
499 
501  static const Integer& max(const Integer& a, const Integer& b){
502  return (a >= b ) ? a : b;
503  }
504 
505  friend class CVC4::Rational;
506 };/* class Integer */
507 
509  inline size_t operator()(const CVC4::Integer& i) const {
510  return i.hash();
511  }
512 };/* struct IntegerHashFunction */
513 
514 inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
515  return os << n.toString();
516 }
517 
518 }/* CVC4 namespace */
519 
520 #endif /* __CVC4__INTEGER_H */
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,...)
Definition: exception.h:155
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(signed int z)
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,...)
Definition: exception.h:140
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.
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
size_t gmpz_hash(const mpz_t toHash)
Hashes the gmp integer primitive in a word by word fashion.
Definition: gmp_util.h:28
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:568
[[ 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.
bool isOne() const
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.
long getLong() 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.
Integer extractBitRange(uint32_t bitCount, uint32_t low) const
See GMP Documentation.
Integer(signed long int z)
bool isZero() const
Integer & operator*=(const Integer &y)
Integer(unsigned int z)
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
int sgn() const
Integer operator*(const Integer &y) const