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 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&#39;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 isOne() const
bool strictlyNegative() const
void DebugCheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:155
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&#39;s Euclidean definition.
Integer floorDivideQuotient(const Integer &y) const
Returns the floor(this / y)
bool isBitSet(uint32_t i) const
Integer(signed int z)
Integer(unsigned long int z)
Integer(const Integer &q)
bool isZero() const
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.
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
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&#39;s exception base class and some associated utilities.
long getLong() const
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&#39;s Euclidean definition.
Integer operator+(const Integer &y) const
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
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.
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 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
int sgn() 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)
Integer(unsigned int z)
bool strictlyPositive() const
Integer bitwiseAnd(const Integer &y) const
Integer operator-() const
Integer euclidianDivideQuotient(const Integer &y) const
Returns the quoitent according to Boute&#39;s Euclidean definition.
Integer bitwiseOr(const Integer &y) const