1 /********************* */
2 /*! \file integer_gmp_imp.h
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
12 ** \brief A multiprecision integer constant; wraps a GMP multiprecision
15 ** A multiprecision integer constant; wraps a GMP multiprecision integer.
18 #include "cvc4_public.h"
20 #ifndef __CVC4__INTEGER_H
21 #define __CVC4__INTEGER_H
27 #include "util/gmp_util.h"
28 #include "util/exception.h"
34 class CVC4_PUBLIC Integer
{
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.
43 * Gets a reference to the gmp data that backs up the integer.
44 * Only accessible to friend classes.
46 const mpz_class
& get_mpz() const { return d_value
; }
49 * Constructs an Integer by copying a GMP C++ primitive.
51 Integer(const mpz_class
& val
) : d_value(val
) {}
55 /** Constructs a rational with the value 0. */
56 Integer() : d_value(0){}
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().
64 explicit Integer(const char* s
, unsigned base
= 10);
65 explicit Integer(const std::string
& s
, unsigned base
= 10);
67 Integer(const Integer
& q
) : d_value(q
.d_value
) {}
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
) {}
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 */
81 Integer
& operator=(const Integer
& x
){
82 if(this == &x
) return *this;
87 bool operator==(const Integer
& y
) const {
88 return d_value
== y
.d_value
;
91 Integer
operator-() const {
92 return Integer(-(d_value
));
96 bool operator!=(const Integer
& y
) const {
97 return d_value
!= y
.d_value
;
100 bool operator< (const Integer
& y
) const {
101 return d_value
< y
.d_value
;
104 bool operator<=(const Integer
& y
) const {
105 return d_value
<= y
.d_value
;
108 bool operator> (const Integer
& y
) const {
109 return d_value
> y
.d_value
;
112 bool operator>=(const Integer
& y
) const {
113 return d_value
>= y
.d_value
;
117 Integer
operator+(const Integer
& y
) const {
118 return Integer( d_value
+ y
.d_value
);
120 Integer
& operator+=(const Integer
& y
) {
121 d_value
+= y
.d_value
;
125 Integer
operator-(const Integer
& y
) const {
126 return Integer( d_value
- y
.d_value
);
128 Integer
& operator-=(const Integer
& y
) {
129 d_value
-= y
.d_value
;
133 Integer
operator*(const Integer
& y
) const {
134 return Integer( d_value
* y
.d_value
);
136 Integer
& operator*=(const Integer
& y
) {
137 d_value
*= y
.d_value
;
142 Integer
bitwiseOr(const Integer
& y
) const {
144 mpz_ior(result
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
145 return Integer(result
);
148 Integer
bitwiseAnd(const Integer
& y
) const {
150 mpz_and(result
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
151 return Integer(result
);
154 Integer
bitwiseXor(const Integer
& y
) const {
156 mpz_xor(result
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
157 return Integer(result
);
160 Integer
bitwiseNot() const {
162 mpz_com(result
.get_mpz_t(), d_value
.get_mpz_t());
163 return Integer(result
);
167 * Return this*(2^pow).
169 Integer
multiplyByPow2(uint32_t pow
) const{
171 mpz_mul_2exp(result
.get_mpz_t(), d_value
.get_mpz_t(), pow
);
172 return Integer( result
);
176 * Returns the Integer obtained by setting the ith bit of the
177 * current Integer to 1.
179 Integer
setBit(uint32_t i
) const {
180 mpz_class res
= d_value
;
181 mpz_setbit(res
.get_mpz_t(), i
);
185 bool isBitSet(uint32_t i
) const {
186 return !extractBitRange(1, i
).isZero();
190 * Returns the integer with the binary representation of size bits
191 * extended with amount 1's
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
;
198 for (unsigned i
= size
; i
< size
+ amount
; ++i
) {
199 mpz_setbit(res
.get_mpz_t(), i
);
205 uint32_t toUnsignedInt() const {
206 return mpz_get_ui(d_value
.get_mpz_t());
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)
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
);
222 * Returns the floor(this / y)
224 Integer
floorDivideQuotient(const Integer
& y
) const {
226 mpz_fdiv_q(q
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
231 * Returns r == this - floor(this/y)*y
233 Integer
floorDivideRemainder(const Integer
& y
) const {
235 mpz_fdiv_r(r
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
240 * Computes a floor quotient and remainder for x divided by y.
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());
247 * Returns the ceil(this / y)
249 Integer
ceilingDivideQuotient(const Integer
& y
) const {
251 mpz_cdiv_q(q
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
256 * Returns the ceil(this / y)
258 Integer
ceilingDivideRemainder(const Integer
& y
) const {
260 mpz_cdiv_r(r
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
265 * Computes a quoitent and remainder according to Boute's Euclidean definition.
266 * euclidianDivideQuotient, euclidianDivideRemainder.
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.
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.
277 if(r
.strictlyNegative()){
280 // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
282 // n = y * q - abs(y) + r + abs(y)
285 // n = y * q - y + r + y
286 // n = y * (q-1) + (r+y)
291 // n = y * q + y + r - y
292 // n = y * (q+1) + (r-y)
299 * Returns the quoitent according to Boute's Euclidean definition.
300 * See the documentation for euclidianQR.
302 Integer
euclidianDivideQuotient(const Integer
& y
) const {
304 euclidianQR(q
,r
, *this, y
);
309 * Returns the remainfing according to Boute's Euclidean definition.
310 * See the documentation for euclidianQR.
312 Integer
euclidianDivideRemainder(const Integer
& y
) const {
314 euclidianQR(q
,r
, *this, y
);
320 * If y divides *this, then exactQuotient returns (this/y)
322 Integer
exactQuotient(const Integer
& y
) const {
323 DebugCheckArgument(y
.divides(*this), y
);
325 mpz_divexact(q
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
330 * Returns y mod 2^exp
332 Integer
modByPow2(uint32_t exp
) const {
334 mpz_fdiv_r_2exp(res
.get_mpz_t(), d_value
.get_mpz_t(), exp
);
341 Integer
divByPow2(uint32_t exp
) const {
343 mpz_fdiv_q_2exp(res
.get_mpz_t(), d_value
.get_mpz_t(), exp
);
349 return mpz_sgn(d_value
.get_mpz_t());
352 inline bool strictlyPositive() const {
356 inline bool strictlyNegative() const {
360 inline bool isZero() const {
365 return mpz_cmp_si(d_value
.get_mpz_t(), 1) == 0;
368 bool isNegativeOne() const {
369 return mpz_cmp_si(d_value
.get_mpz_t(), -1) == 0;
373 * Raise this Integer to the power <code>exp</code>.
375 * @param exp the exponent
377 Integer
pow(unsigned long int exp
) const {
379 mpz_pow_ui(result
.get_mpz_t(),d_value
.get_mpz_t(),exp
);
380 return Integer( result
);
384 * Return the greatest common divisor of this integer with another.
386 Integer
gcd(const Integer
& y
) const {
388 mpz_gcd(result
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
389 return Integer(result
);
393 * Return the least common multiple of this integer with another.
395 Integer
lcm(const Integer
& y
) const {
397 mpz_lcm(result
.get_mpz_t(), d_value
.get_mpz_t(), y
.d_value
.get_mpz_t());
398 return Integer(result
);
402 * All non-zero integers z, z.divide(0)
403 * ! zero.divides(zero)
405 bool divides(const Integer
& y
) const {
406 int res
= mpz_divisible_p(y
.d_value
.get_mpz_t(), d_value
.get_mpz_t());
411 * Return the absolute value of this integer.
413 Integer
abs() const {
414 return d_value
>= 0 ? *this : -*this;
417 std::string
toString(int base
= 10) const{
418 return d_value
.get_str(base
);
421 bool fitsSignedInt() const;
423 bool fitsUnsignedInt() const;
425 signed int getSignedInt() const;
427 unsigned int getUnsignedInt() const;
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()");
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()");
445 * Computes the hash of the node from the first word of the
446 * numerator, the denominator.
448 size_t hash() const {
449 return gmpz_hash(d_value
.get_mpz_t());
453 * Returns true iff bit n is set.
455 * @param n the bit to test (0 == least significant bit)
456 * @return true if bit n is set in this integer; false otherwise
458 bool testBit(unsigned n
) const {
459 return mpz_tstbit(d_value
.get_mpz_t(), n
);
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
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;
478 * If x != 0, returns the smallest n s.t. 2^{n-1} <= abs(x) < 2^{n}.
479 * If x == 0, returns 1.
481 size_t length() const {
485 return mpz_sizeinbase(d_value
.get_mpz_t(),2);
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());
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
;
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
;
505 friend class CVC4::Rational
;
506 };/* class Integer */
508 struct IntegerHashFunction
{
509 inline size_t operator()(const CVC4::Integer
& i
) const {
512 };/* struct IntegerHashFunction */
514 inline std::ostream
& operator<<(std::ostream
& os
, const Integer
& n
) {
515 return os
<< n
.toString();
518 }/* CVC4 namespace */
520 #endif /* __CVC4__INTEGER_H */