cvc4-1.4
integer_cln_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 <sstream>
25 #include <iostream>
26 
27 #include <cln/integer.h>
28 #include <cln/input.h>
29 #include <cln/integer_io.h>
30 #include <limits>
31 
32 #include "util/exception.h"
33 
34 namespace CVC4 {
35 
36 class Rational;
37 
38 class CVC4_PUBLIC Integer {
39 private:
43  cln::cl_I d_value;
44 
49  const cln::cl_I& get_cl_I() const { return d_value; }
50 
54  Integer(const cln::cl_I& val) : d_value(val) {}
55 
56  void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument);
57 
58  void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument);
59 
60 public:
61 
63  Integer() : d_value(0){}
64 
71  explicit Integer(const char* sp, unsigned base = 10) throw (std::invalid_argument) {
72  parseInt(std::string(sp), base);
73  }
74 
75  explicit Integer(const std::string& s, unsigned base = 10) throw (std::invalid_argument) {
76  parseInt(s, base);
77  }
78 
79  Integer(const Integer& q) : d_value(q.d_value) {}
80 
81  Integer( signed int z) : d_value((signed long int)z) {}
82  Integer(unsigned int z) : d_value((unsigned long int)z) {}
83  Integer( signed long int z) : d_value(z) {}
84  Integer(unsigned long int z) : d_value(z) {}
85 
86 #ifdef CVC4_NEED_INT64_T_OVERLOADS
87  Integer( int64_t z) : d_value(static_cast<long>(z)) {}
88  Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
89 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
90 
91  ~Integer() {}
92 
94  if(this == &x) return *this;
95  d_value = x.d_value;
96  return *this;
97  }
98 
99  bool operator==(const Integer& y) const {
100  return d_value == y.d_value;
101  }
102 
104  return Integer(-(d_value));
105  }
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  bool operator<=(const Integer& y) const {
117  return d_value <= y.d_value;
118  }
119 
120  bool operator> (const Integer& y) const {
121  return d_value > y.d_value;
122  }
123 
124  bool operator>=(const Integer& y) const {
125  return d_value >= y.d_value;
126  }
127 
128 
129  Integer operator+(const Integer& y) const {
130  return Integer( d_value + y.d_value );
131  }
133  d_value += y.d_value;
134  return *this;
135  }
136 
137  Integer operator-(const Integer& y) const {
138  return Integer( d_value - y.d_value );
139  }
141  d_value -= y.d_value;
142  return *this;
143  }
144 
145  Integer operator*(const Integer& y) const {
146  return Integer( d_value * y.d_value );
147  }
149  d_value *= y.d_value;
150  return *this;
151  }
152 
153 
154  Integer bitwiseOr(const Integer& y) const {
155  return Integer(cln::logior(d_value, y.d_value));
156  }
157 
158  Integer bitwiseAnd(const Integer& y) const {
159  return Integer(cln::logand(d_value, y.d_value));
160  }
161 
162  Integer bitwiseXor(const Integer& y) const {
163  return Integer(cln::logxor(d_value, y.d_value));
164  }
165 
166  Integer bitwiseNot() const {
167  return Integer(cln::lognot(d_value));
168  }
169 
170 
174  Integer multiplyByPow2(uint32_t pow) const {
175  cln::cl_I ipow(pow);
176  return Integer( d_value << ipow);
177  }
178 
179  bool isBitSet(uint32_t i) const {
180  return !extractBitRange(1, i).isZero();
181  }
182 
183  Integer setBit(uint32_t i) const {
184  cln::cl_I mask(1);
185  mask = mask << i;
186  return Integer(cln::logior(d_value, mask));
187  }
188 
189  Integer oneExtend(uint32_t size, uint32_t amount) const {
190  DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
191  cln::cl_byte range(amount, size);
192  cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
193  Integer temp(allones);
194 
195  return Integer(cln::deposit_field(allones, d_value, range));
196  }
197 
198  uint32_t toUnsignedInt() const {
199  return cln::cl_I_to_uint(d_value);
200  }
201 
202 
204  Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
205  cln::cl_byte range(bitCount, low);
206  return Integer(cln::ldb(d_value, range));
207  }
208 
213  return Integer( cln::floor1(d_value, y.d_value) );
214  }
215 
220  return Integer( cln::floor2(d_value, y.d_value).remainder );
221  }
225  static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
226  cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value);
227  q.d_value = res.quotient;
228  r.d_value = res.remainder;
229  }
230 
235  return Integer( cln::ceiling1(d_value, y.d_value) );
236  }
237 
242  return Integer( cln::ceiling2(d_value, y.d_value).remainder );
243  }
244 
254  static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
255  // compute the floor and then fix the value up if needed.
256  floorQR(q,r,x,y);
257 
258  if(r.strictlyNegative()){
259  // if r < 0
260  // abs(r) < abs(y)
261  // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
262  // n = y * q + r
263  // n = y * q - abs(y) + r + abs(y)
264  if(r.sgn() >= 0){
265  // y = abs(y)
266  // n = y * q - y + r + y
267  // n = y * (q-1) + (r+y)
268  q -= 1;
269  r += y;
270  }else{
271  // y = -abs(y)
272  // n = y * q + y + r - y
273  // n = y * (q+1) + (r-y)
274  q += 1;
275  r -= y;
276  }
277  }
278  }
279 
285  Integer q,r;
286  euclidianQR(q,r, *this, y);
287  return q;
288  }
289 
295  Integer q,r;
296  euclidianQR(q,r, *this, y);
297  return r;
298  }
299 
303  Integer exactQuotient(const Integer& y) const {
304  DebugCheckArgument(y.divides(*this), y);
305  return Integer( cln::exquo(d_value, y.d_value) );
306  }
307 
308  Integer modByPow2(uint32_t exp) const {
309  cln::cl_byte range(exp, 0);
310  return Integer(cln::ldb(d_value, range));
311  }
312 
313  Integer divByPow2(uint32_t exp) const {
314  return d_value >> exp;
315  }
316 
322  Integer pow(unsigned long int exp) const {
323  if(exp > 0){
324  cln::cl_I result= cln::expt_pos(d_value,exp);
325  return Integer( result );
326  }else if(exp == 0){
327  return Integer( 1 );
328  }else{
329  throw Exception("Negative exponent in Integer::pow()");
330  }
331  }
332 
336  Integer gcd(const Integer& y) const {
337  cln::cl_I result = cln::gcd(d_value, y.d_value);
338  return Integer(result);
339  }
340 
344  Integer lcm(const Integer& y) const {
345  cln::cl_I result = cln::lcm(d_value, y.d_value);
346  return Integer(result);
347  }
348 
352  bool divides(const Integer& y) const {
353  cln::cl_I result = cln::rem(y.d_value, d_value);
354  return cln::zerop(result);
355  }
356 
360  Integer abs() const {
361  return d_value >= 0 ? *this : -*this;
362  }
363 
364  std::string toString(int base = 10) const{
365  std::stringstream ss;
366  switch(base){
367  case 2:
368  fprintbinary(ss,d_value);
369  break;
370  case 8:
371  fprintoctal(ss,d_value);
372  break;
373  case 10:
374  fprintdecimal(ss,d_value);
375  break;
376  case 16:
377  fprinthexadecimal(ss,d_value);
378  break;
379  default:
380  throw Exception("Unhandled base in Integer::toString()");
381  }
382  std::string output = ss.str();
383  for( unsigned i = 0; i <= output.length(); ++i){
384  if(isalpha(output[i])){
385  output.replace(i, 1, 1, tolower(output[i]));
386  }
387  }
388 
389  return output;
390  }
391 
392  int sgn() const {
393  cln::cl_I sgn = cln::signum(d_value);
394  return cln::cl_I_to_int(sgn);
395  }
396 
397 
398  inline bool strictlyPositive() const {
399  return sgn() > 0;
400  }
401 
402  inline bool strictlyNegative() const {
403  return sgn() < 0;
404  }
405 
406  inline bool isZero() const {
407  return sgn() == 0;
408  }
409 
410  inline bool isOne() const {
411  return d_value == 1;
412  }
413 
414  inline bool isNegativeOne() const {
415  return d_value == -1;
416  }
417 
419  bool fitsSignedInt() const;
420 
422  bool fitsUnsignedInt() const;
423 
424  int getSignedInt() const;
425 
426  unsigned int getUnsignedInt() const;
427 
428  long getLong() const {
429  // ensure there isn't overflow
430  CheckArgument(d_value <= std::numeric_limits<long>::max(), this,
431  "Overflow detected in Integer::getLong()");
432  CheckArgument(d_value >= std::numeric_limits<long>::min(), this,
433  "Overflow detected in Integer::getLong()");
434  return cln::cl_I_to_long(d_value);
435  }
436 
437  unsigned long getUnsignedLong() const {
438  // ensure there isn't overflow
439  CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), this,
440  "Overflow detected in Integer::getUnsignedLong()");
441  CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), this,
442  "Overflow detected in Integer::getUnsignedLong()");
443  return cln::cl_I_to_ulong(d_value);
444  }
445 
450  size_t hash() const {
451  return equal_hashcode(d_value);
452  }
453 
460  bool testBit(unsigned n) const {
461  return cln::logbitp(n, d_value);
462  }
463 
468  unsigned isPow2() const {
469  if (d_value <= 0) return 0;
470  // power2p returns n such that d_value = 2^(n-1)
471  return cln::power2p(d_value);
472  }
473 
478  size_t length() const {
479  int s = sgn();
480  if(s == 0){
481  return 1;
482  }else if(s < 0){
483  size_t len = cln::integer_length(d_value);
484  /*If this is -2^n, return len+1 not len to stay consistent with the definition above!
485  * From CLN's documentation of integer_length:
486  * This is the smallest n >= 0 such that -2^n <= x < 2^n.
487  * If x > 0, this is the unique n > 0 such that 2^(n-1) <= x < 2^n.
488  */
489  size_t ord2 = cln::ord2(d_value);
490  return (len == ord2) ? (len + 1) : len;
491  }else{
492  return cln::integer_length(d_value);
493  }
494  }
495 
496 /* cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */
497 /* This function ("extended gcd") returns the greatest common divisor g of a and b and at the same time the representation of g as an integral linear combination of a and b: u and v with u*a+v*b = g, g >= 0. u and v will be normalized to be of smallest possible absolute value, in the following sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy the inequalities abs(u) <= abs(b)/(2*g), abs(v) <= abs(a)/(2*g). */
498  static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){
499  g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
500  }
501 
503  static const Integer& min(const Integer& a, const Integer& b){
504  return (a <=b ) ? a : b;
505  }
506 
508  static const Integer& max(const Integer& a, const Integer& b){
509  return (a >= b ) ? a : b;
510  }
511 
512  friend class CVC4::Rational;
513 };/* class Integer */
514 
515 struct IntegerHashFunction {
516  inline size_t operator()(const CVC4::Integer& i) const {
517  return i.hash();
518  }
519 };/* struct IntegerHashFunction */
520 
521 inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
522  return os << n.toString();
523 }
524 
525 }/* CVC4 namespace */
526 
527 #endif /* __CVC4__INTEGER_H */
Integer bitwiseXor(const Integer &y) const
Integer & operator+=(const Integer &y)
Integer oneExtend(uint32_t size, uint32_t amount) const
Integer setBit(uint32_t i) const
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
Definition: expr.h:106
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)
STL namespace.
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 CLN 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
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
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 unique 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
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(const std::string &s, unsigned base=10)
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 quoient 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)
Integer(const char *sp, unsigned base=10)
Constructs a Integer from a C string.
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