src/util/integer_gmp_imp.h

   1 /*********************                                                        */
   2 /*! \file integer_gmp_imp.h
   3  ** \verbatim
   4  ** Original author: Tim King
   5  ** Major contributors: Morgan Deters, Liana Hadarean
   6  ** Minor contributors (to current version): Dejan Jovanovic
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief A multiprecision integer constant; wraps a GMP multiprecision
  13  ** integer.
  14  **
  15  ** A multiprecision integer constant; wraps a GMP multiprecision integer.
  16  **/
  17
  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
  34 class CVC4_PUBLIC Integer {
  35 private:
  36   /**
  37    * Stores the value of the rational is stored in a C++ GMP integer class.
  38    * Using this instead of mpz_t allows for easier destruction.
  39    */
  40   mpz_class d_value;
  41
  42   /**
  43    * Gets a reference to the gmp data that backs up the integer.
  44    * Only accessible to friend classes.
  45    */
  46   const mpz_class& get_mpz() const { return d_value; }
  47
  48   /**
  49    * Constructs an Integer by copying a GMP C++ primitive.
  50    */
  51   Integer(const mpz_class& val) : d_value(val) {}
  52
  53 public:
  54
  55   /** Constructs a rational with the value 0. */
  56   Integer() : d_value(0){}
  57
  58   /**
  59    * Constructs a Integer from a C string.
  60    * Throws std::invalid_argument if the string is not a valid rational.
  61    * For more information about what is a valid rational string,
  62    * see GMP's documentation for mpq_set_str().
  63    */
  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
  81   Integer& operator=(const Integer& x){
  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   }
 120   Integer& operator+=(const Integer& y) {
 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   }
 128   Integer& operator-=(const Integer& y) {
 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   }
 136   Integer& operator*=(const Integer& y) {
 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
 166   /**
 167    * Return this*(2^pow).
 168    */
 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
 175   /**
 176    * Returns the Integer obtained by setting the ith bit of the
 177    * current Integer to 1.
 178    */
 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
 189   /**
 190    * Returns the integer with the binary representation of size bits
 191    * extended with amount 1's
 192    */
 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
 209   /** See GMP Documentation. */
 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
 221   /**
 222    * Returns the floor(this / y)
 223    */
 224   Integer floorDivideQuotient(const Integer& y) const {
 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
 230   /**
 231    * Returns r == this - floor(this/y)*y
 232    */
 233   Integer floorDivideRemainder(const Integer& y) const {
 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
 239   /**
 240    * Computes a floor quotient and remainder for x divided by y.
 241    */
 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
 246   /**
 247    * Returns the ceil(this / y)
 248    */
 249   Integer ceilingDivideQuotient(const Integer& y) const {
 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
 255   /**
 256    * Returns the ceil(this / y)
 257    */
 258   Integer ceilingDivideRemainder(const Integer& y) const {
 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
 264   /**
 265    * Computes a quoitent and remainder according to Boute's Euclidean definition.
 266    * euclidianDivideQuotient, euclidianDivideRemainder.
 267    *
 268    * Boute, Raymond T. (April 1992).
 269    * The Euclidean definition of the functions div and mod.
 270    * ACM Transactions on Programming Languages and Systems (TOPLAS)
 271    * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
 272    */
 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   }
 298   /**
 299    * Returns the quoitent according to Boute's Euclidean definition.
 300    * See the documentation for euclidianQR.
 301    */
 302   Integer euclidianDivideQuotient(const Integer& y) const {
 303     Integer q,r;
 304     euclidianQR(q,r, *this, y);
 305     return q;
 306   }
 307
 308   /**
 309    * Returns the remainfing according to Boute's Euclidean definition.
 310    * See the documentation for euclidianQR.
 311    */
 312   Integer euclidianDivideRemainder(const Integer& y) const {
 313     Integer q,r;
 314     euclidianQR(q,r, *this, y);
 315     return r;
 316   }
 317
 318
 319   /**
 320    * If y divides *this, then exactQuotient returns (this/y)
 321    */
 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
 329   /**
 330    * Returns y mod 2^exp
 331    */
 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
 338   /**
 339    * Returns y / 2^exp
 340    */
 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
 372   /**
 373    * Raise this Integer to the power <code>exp</code>.
 374    *
 375    * @param exp the exponent
 376    */
 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
 383   /**
 384    * Return the greatest common divisor of this integer with another.
 385    */
 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
 392   /**
 393    * Return the least common multiple of this integer with another.
 394    */
 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
 401   /**
 402    * All non-zero integers z, z.divide(0)
 403    * ! zero.divides(zero)
 404    */
 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
 410   /**
 411    * Return the absolute value of this integer.
 412    */
 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
 444   /**
 445    * Computes the hash of the node from the first word of the
 446    * numerator, the denominator.
 447    */
 448   size_t hash() const {
 449     return gmpz_hash(d_value.get_mpz_t());
 450   }
 451
 452   /**
 453    * Returns true iff bit n is set.
 454    *
 455    * @param n the bit to test (0 == least significant bit)
 456    * @return true if bit n is set in this integer; false otherwise
 457    */
 458   bool testBit(unsigned n) const {
 459     return mpz_tstbit(d_value.get_mpz_t(), n);
 460   }
 461
 462   /**
 463    * Returns k if the integer is equal to 2^(k-1)
 464    * @return k if the integer is equal to 2^(k-1) and 0 otherwise
 465    */
 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
 477   /**
 478    * If x != 0, returns the smallest n s.t. 2^{n-1} <= abs(x) < 2^{n}.
 479    * If x == 0, returns 1.
 480    */
 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
 495   /** Returns a reference to the minimum of two integers. */
 496   static const Integer& min(const Integer& a, const Integer& b){
 497     return (a <=b ) ? a : b;
 498   }
 499
 500   /** Returns a reference to the maximum of two integers. */
 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
 508 struct IntegerHashFunction {
 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 */