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 
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 
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 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
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
void DebugCheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:155
bool operator<=(const Integer &y) const
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)
STL namespace.
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.
Integer & operator=(const Integer &x)
size_t length() const
If x != 0, returns the unique 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
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
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 quoient and remainder for x divided by y.
Integer extractBitRange(uint32_t bitCount, uint32_t low) const
See CLN Documentation.
Integer(signed long int z)
bool isZero() const
Integer & operator*=(const Integer &y)
Integer(unsigned int z)
Integer(const char *sp, unsigned base=10)
Constructs a Integer from a C string.
Integer oneExtend(uint32_t size, uint32_t amount) const
Integer operator+(const Integer &y) const
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