cvc4-1.3
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 
26 #include "util/gmp_util.h"
27 #include "util/exception.h"
28 
29 namespace CVC4 {
30 
31 class Rational;
32 
33 class CVC4_PUBLIC Integer {
34 private:
39  mpz_class d_value;
40 
45  const mpz_class& get_mpz() const { return d_value; }
46 
50  Integer(const mpz_class& val) : d_value(val) {}
51 
52 public:
53 
55  Integer() : d_value(0){}
56 
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) {}
65 
66  Integer(const Integer& q) : d_value(q.d_value) {}
67 
68  Integer( signed int z) : d_value(z) {}
69  Integer(unsigned int z) : d_value(z) {}
70  Integer( signed long int z) : d_value(z) {}
71  Integer(unsigned long int z) : d_value(z) {}
72 
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)) {}
76 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
77 
78  ~Integer() {}
79 
81  if(this == &x) return *this;
82  d_value = x.d_value;
83  return *this;
84  }
85 
86  bool operator==(const Integer& y) const {
87  return d_value == y.d_value;
88  }
89 
90  Integer operator-() const {
91  return Integer(-(d_value));
92  }
93 
94 
95  bool operator!=(const Integer& y) const {
96  return d_value != y.d_value;
97  }
98 
99  bool operator< (const Integer& y) const {
100  return d_value < y.d_value;
101  }
102 
103  bool operator<=(const Integer& y) const {
104  return d_value <= y.d_value;
105  }
106 
107  bool operator> (const Integer& y) const {
108  return d_value > y.d_value;
109  }
110 
111  bool operator>=(const Integer& y) const {
112  return d_value >= y.d_value;
113  }
114 
115 
116  Integer operator+(const Integer& y) const {
117  return Integer( d_value + y.d_value );
118  }
120  d_value += y.d_value;
121  return *this;
122  }
123 
124  Integer operator-(const Integer& y) const {
125  return Integer( d_value - y.d_value );
126  }
128  d_value -= y.d_value;
129  return *this;
130  }
131 
132  Integer operator*(const Integer& y) const {
133  return Integer( d_value * y.d_value );
134  }
136  d_value *= y.d_value;
137  return *this;
138  }
139 
140 
141  Integer bitwiseOr(const Integer& y) const {
142  mpz_class result;
143  mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
144  return Integer(result);
145  }
146 
147  Integer bitwiseAnd(const Integer& y) const {
148  mpz_class result;
149  mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
150  return Integer(result);
151  }
152 
153  Integer bitwiseXor(const Integer& y) const {
154  mpz_class result;
155  mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
156  return Integer(result);
157  }
158 
159  Integer bitwiseNot() const {
160  mpz_class result;
161  mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
162  return Integer(result);
163  }
164 
168  Integer multiplyByPow2(uint32_t pow) const{
169  mpz_class result;
170  mpz_mul_2exp(result.get_mpz_t(), d_value.get_mpz_t(), pow);
171  return Integer( result );
172  }
173 
178  Integer setBit(uint32_t i) const {
179  mpz_class res = d_value;
180  mpz_setbit(res.get_mpz_t(), i);
181  return Integer(res);
182  }
183 
184  bool isBitSet(uint32_t i) const {
185  return !extractBitRange(1, i).isZero();
186  }
187 
192  Integer oneExtend(uint32_t size, uint32_t amount) const {
193  // check that the size is accurate
194  DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
195  mpz_class res = d_value;
196 
197  for (unsigned i = size; i < size + amount; ++i) {
198  mpz_setbit(res.get_mpz_t(), i);
199  }
200 
201  return Integer(res);
202  }
203 
204  uint32_t toUnsignedInt() const {
205  return mpz_get_ui(d_value.get_mpz_t());
206  }
207 
209  Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
210  // bitCount = high-low+1
211  uint32_t high = low + bitCount-1;
212  //— Function: void mpz_fdiv_r_2exp (mpz_t r, mpz_t n, mp_bitcnt_t b)
213  mpz_class rem, div;
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);
216 
217  return Integer(div);
218  }
219 
224  mpz_class q;
225  mpz_fdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
226  return Integer( q );
227  }
228 
233  mpz_class r;
234  mpz_fdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
235  return Integer( r );
236  }
237 
241  static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
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());
243  }
244 
249  mpz_class q;
250  mpz_cdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
251  return Integer( q );
252  }
253 
258  mpz_class r;
259  mpz_cdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
260  return Integer( r );
261  }
262 
272  static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
273  // compute the floor and then fix the value up if needed.
274  floorQR(q,r,x,y);
275 
276  if(r.strictlyNegative()){
277  // if r < 0
278  // abs(r) < abs(y)
279  // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
280  // n = y * q + r
281  // n = y * q - abs(y) + r + abs(y)
282  if(r.sgn() >= 0){
283  // y = abs(y)
284  // n = y * q - y + r + y
285  // n = y * (q-1) + (r+y)
286  q -= 1;
287  r += y;
288  }else{
289  // y = -abs(y)
290  // n = y * q + y + r - y
291  // n = y * (q+1) + (r-y)
292  q += 1;
293  r -= y;
294  }
295  }
296  }
302  Integer q,r;
303  euclidianQR(q,r, *this, y);
304  return q;
305  }
306 
312  Integer q,r;
313  euclidianQR(q,r, *this, y);
314  return r;
315  }
316 
317 
321  Integer exactQuotient(const Integer& y) const {
322  DebugCheckArgument(y.divides(*this), y);
323  mpz_class q;
324  mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
325  return Integer( q );
326  }
327 
331  Integer modByPow2(uint32_t exp) const {
332  mpz_class res;
333  mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
334  return Integer(res);
335  }
336 
340  Integer divByPow2(uint32_t exp) const {
341  mpz_class res;
342  mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
343  return Integer(res);
344  }
345 
346 
347  int sgn() const {
348  return mpz_sgn(d_value.get_mpz_t());
349  }
350 
351  inline bool strictlyPositive() const {
352  return sgn() > 0;
353  }
354 
355  inline bool strictlyNegative() const {
356  return sgn() < 0;
357  }
358 
359  inline bool isZero() const {
360  return sgn() == 0;
361  }
362 
363  bool isOne() const {
364  return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0;
365  }
366 
367  bool isNegativeOne() const {
368  return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0;
369  }
370 
376  Integer pow(unsigned long int exp) const {
377  mpz_class result;
378  mpz_pow_ui(result.get_mpz_t(),d_value.get_mpz_t(),exp);
379  return Integer( result );
380  }
381 
385  Integer gcd(const Integer& y) const {
386  mpz_class result;
387  mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
388  return Integer(result);
389  }
390 
394  Integer lcm(const Integer& y) const {
395  mpz_class result;
396  mpz_lcm(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
397  return Integer(result);
398  }
399 
404  bool divides(const Integer& y) const {
405  int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t());
406  return res != 0;
407  }
408 
412  Integer abs() const {
413  return d_value >= 0 ? *this : -*this;
414  }
415 
416  std::string toString(int base = 10) const{
417  return d_value.get_str(base);
418  }
419 
420  //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
421 
422  long getLong() const {
423  long si = d_value.get_si();
424  // ensure there wasn't overflow
425  CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this,
426  "Overflow detected in Integer::getLong()");
427  return si;
428  }
429  unsigned long getUnsignedLong() const {
430  unsigned long ui = d_value.get_ui();
431  // ensure there wasn't overflow
432  CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this,
433  "Overflow detected in Integer::getUnsignedLong()");
434  return ui;
435  }
436 
441  size_t hash() const {
442  return gmpz_hash(d_value.get_mpz_t());
443  }
444 
451  bool testBit(unsigned n) const {
452  return mpz_tstbit(d_value.get_mpz_t(), n);
453  }
454 
459  unsigned isPow2() const {
460  if (d_value <= 0) return 0;
461  // check that the number of ones in the binary representation is 1
462  if (mpz_popcount(d_value.get_mpz_t()) == 1) {
463  // return the index of the first one plus 1
464  return mpz_scan1(d_value.get_mpz_t(), 0) + 1;
465  }
466  return 0;
467  }
468 
469 
474  size_t length() const {
475  if(sgn() == 0){
476  return 1;
477  }else{
478  return mpz_sizeinbase(d_value.get_mpz_t(),2);
479  }
480  }
481 
482  static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){
483  //see the documentation for:
484  //mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b);
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());
486  }
487 
489  static const Integer& min(const Integer& a, const Integer& b){
490  return (a <=b ) ? a : b;
491  }
492 
494  static const Integer& max(const Integer& a, const Integer& b){
495  return (a >= b ) ? a : b;
496  }
497 
498  friend class CVC4::Rational;
499 };/* class Integer */
500 
501 struct IntegerHashFunction {
502  inline size_t operator()(const CVC4::Integer& i) const {
503  return i.hash();
504  }
505 };/* struct IntegerHashFunction */
506 
507 inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
508  return os << n.toString();
509 }
510 
511 }/* CVC4 namespace */
512 
513 #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
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(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
Return true if *this exactly divides y.
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
Definition: README:39
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
[[ 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.
Integer(const std::string &s, unsigned base=10)
std::ostream & operator<<(std::ostream &out, ModelFormatMode mode)
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
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
Definition: NEWS:4
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