cvc4-1.3
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:
44  cln::cl_I d_value;
45 
50  //const mpz_class& get_mpz() const { return d_value; }
51  const cln::cl_I& get_cl_I() const { return d_value; }
52 
56  //Integer(const mpz_class& val) : d_value(val) {}
57  Integer(const cln::cl_I& val) : d_value(val) {}
58 
59  void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
60  try {
61  if(s.find_first_not_of('0') == std::string::npos) {
62  // String of all zeroes, CLN has a bug for these inputs up to and
63  // including CLN v1.3.2.
64  // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
65  d_value = read_integer(flags, "0", NULL, NULL);
66  } else {
67  d_value = read_integer(flags, s.c_str(), NULL, NULL);
68  }
69  } catch(...) {
70  std::stringstream ss;
71  ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
72  throw std::invalid_argument(ss.str());
73  }
74  }
75 
76  void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
77  cln::cl_read_flags flags;
78  flags.syntax = cln::syntax_integer;
79  flags.lsyntax = cln::lsyntax_standard;
80  flags.rational_base = base;
81  if(base == 0) {
82  // infer base in a manner consistent with GMP
83  if(s[0] == '0') {
84  flags.lsyntax = cln::lsyntax_commonlisp;
85  std::string st = s;
86  if(s[1] == 'X' || s[1] == 'x') {
87  st.replace(0, 2, "#x");
88  } else if(s[1] == 'B' || s[1] == 'b') {
89  st.replace(0, 2, "#b");
90  } else {
91  st.replace(0, 1, "#o");
92  }
93  readInt(flags, st, base);
94  return;
95  } else {
96  flags.rational_base = 10;
97  }
98  }
99  readInt(flags, s, base);
100  }
101 
102 public:
103 
105  Integer() : d_value(0){}
106 
113  explicit Integer(const char* sp, unsigned base = 10) throw (std::invalid_argument) {
114  parseInt(std::string(sp), base);
115  }
116 
117  explicit Integer(const std::string& s, unsigned base = 10) throw (std::invalid_argument) {
118  parseInt(s, base);
119  }
120 
121  Integer(const Integer& q) : d_value(q.d_value) {}
122 
123  Integer( signed int z) : d_value((signed long int)z) {}
124  Integer(unsigned int z) : d_value((unsigned long int)z) {}
125  Integer( signed long int z) : d_value(z) {}
126  Integer(unsigned long int z) : d_value(z) {}
127 
128 #ifdef CVC4_NEED_INT64_T_OVERLOADS
129  Integer( int64_t z) : d_value(static_cast<long>(z)) {}
130  Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
131 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
132 
133  ~Integer() {}
134 
136  if(this == &x) return *this;
137  d_value = x.d_value;
138  return *this;
139  }
140 
141  bool operator==(const Integer& y) const {
142  return d_value == y.d_value;
143  }
144 
146  return Integer(-(d_value));
147  }
148 
149 
150  bool operator!=(const Integer& y) const {
151  return d_value != y.d_value;
152  }
153 
154  bool operator< (const Integer& y) const {
155  return d_value < y.d_value;
156  }
157 
158  bool operator<=(const Integer& y) const {
159  return d_value <= y.d_value;
160  }
161 
162  bool operator> (const Integer& y) const {
163  return d_value > y.d_value;
164  }
165 
166  bool operator>=(const Integer& y) const {
167  return d_value >= y.d_value;
168  }
169 
170 
171  Integer operator+(const Integer& y) const {
172  return Integer( d_value + y.d_value );
173  }
175  d_value += y.d_value;
176  return *this;
177  }
178 
179  Integer operator-(const Integer& y) const {
180  return Integer( d_value - y.d_value );
181  }
183  d_value -= y.d_value;
184  return *this;
185  }
186 
187  Integer operator*(const Integer& y) const {
188  return Integer( d_value * y.d_value );
189  }
191  d_value *= y.d_value;
192  return *this;
193  }
194 
195 
196  Integer bitwiseOr(const Integer& y) const {
197  return Integer(cln::logior(d_value, y.d_value));
198  }
199 
200  Integer bitwiseAnd(const Integer& y) const {
201  return Integer(cln::logand(d_value, y.d_value));
202  }
203 
204  Integer bitwiseXor(const Integer& y) const {
205  return Integer(cln::logxor(d_value, y.d_value));
206  }
207 
208  Integer bitwiseNot() const {
209  return Integer(cln::lognot(d_value));
210  }
211 
212 
216  Integer multiplyByPow2(uint32_t pow) const {
217  cln::cl_I ipow(pow);
218  return Integer( d_value << ipow);
219  }
220 
221  bool isBitSet(uint32_t i) const {
222  return !extractBitRange(1, i).isZero();
223  }
224 
225  Integer setBit(uint32_t i) const {
226  cln::cl_I mask(1);
227  mask = mask << i;
228  return Integer(cln::logior(d_value, mask));
229  }
230 
231  Integer oneExtend(uint32_t size, uint32_t amount) const {
232  DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
233  cln::cl_byte range(amount, size);
234  cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
235  Integer temp(allones);
236 
237  return Integer(cln::deposit_field(allones, d_value, range));
238  }
239 
240  uint32_t toUnsignedInt() const {
241  return cln::cl_I_to_uint(d_value);
242  }
243 
244 
246  Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
247  cln::cl_byte range(bitCount, low);
248  return Integer(cln::ldb(d_value, range));
249  }
250 
255  return Integer( cln::floor1(d_value, y.d_value) );
256  }
257 
262  return Integer( cln::floor2(d_value, y.d_value).remainder );
263  }
267  static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
268  cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value);
269  q.d_value = res.quotient;
270  r.d_value = res.remainder;
271  }
272 
277  return Integer( cln::ceiling1(d_value, y.d_value) );
278  }
279 
284  return Integer( cln::ceiling2(d_value, y.d_value).remainder );
285  }
286 
296  static void euclidianQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
297  // compute the floor and then fix the value up if needed.
298  floorQR(q,r,x,y);
299 
300  if(r.strictlyNegative()){
301  // if r < 0
302  // abs(r) < abs(y)
303  // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
304  // n = y * q + r
305  // n = y * q - abs(y) + r + abs(y)
306  if(r.sgn() >= 0){
307  // y = abs(y)
308  // n = y * q - y + r + y
309  // n = y * (q-1) + (r+y)
310  q -= 1;
311  r += y;
312  }else{
313  // y = -abs(y)
314  // n = y * q + y + r - y
315  // n = y * (q+1) + (r-y)
316  q += 1;
317  r -= y;
318  }
319  }
320  }
321 
327  Integer q,r;
328  euclidianQR(q,r, *this, y);
329  return q;
330  }
331 
337  Integer q,r;
338  euclidianQR(q,r, *this, y);
339  return r;
340  }
341 
345  Integer exactQuotient(const Integer& y) const {
346  DebugCheckArgument(y.divides(*this), y);
347  return Integer( cln::exquo(d_value, y.d_value) );
348  }
349 
350  Integer modByPow2(uint32_t exp) const {
351  cln::cl_byte range(exp, 0);
352  return Integer(cln::ldb(d_value, range));
353  }
354 
355  Integer divByPow2(uint32_t exp) const {
356  return d_value >> exp;
357  }
358 
364  Integer pow(unsigned long int exp) const {
365  if(exp > 0){
366  cln::cl_I result= cln::expt_pos(d_value,exp);
367  return Integer( result );
368  }else if(exp == 0){
369  return Integer( 1 );
370  }else{
371  throw Exception("Negative exponent in Integer::pow()");
372  }
373  }
374 
378  Integer gcd(const Integer& y) const {
379  cln::cl_I result = cln::gcd(d_value, y.d_value);
380  return Integer(result);
381  }
382 
386  Integer lcm(const Integer& y) const {
387  cln::cl_I result = cln::lcm(d_value, y.d_value);
388  return Integer(result);
389  }
390 
394  bool divides(const Integer& y) const {
395  cln::cl_I result = cln::rem(y.d_value, d_value);
396  return cln::zerop(result);
397  }
398 
402  Integer abs() const {
403  return d_value >= 0 ? *this : -*this;
404  }
405 
406  std::string toString(int base = 10) const{
407  std::stringstream ss;
408  switch(base){
409  case 2:
410  fprintbinary(ss,d_value);
411  break;
412  case 8:
413  fprintoctal(ss,d_value);
414  break;
415  case 10:
416  fprintdecimal(ss,d_value);
417  break;
418  case 16:
419  fprinthexadecimal(ss,d_value);
420  break;
421  default:
422  throw Exception("Unhandled base in Integer::toString()");
423  }
424  std::string output = ss.str();
425  for( unsigned i = 0; i <= output.length(); ++i){
426  if(isalpha(output[i])){
427  output.replace(i, 1, 1, tolower(output[i]));
428  }
429  }
430 
431  return output;
432  }
433 
434  int sgn() const {
435  cln::cl_I sgn = cln::signum(d_value);
436  return cln::cl_I_to_int(sgn);
437  }
438 
439 
440  inline bool strictlyPositive() const {
441  return sgn() > 0;
442  }
443 
444  inline bool strictlyNegative() const {
445  return sgn() < 0;
446  }
447 
448  inline bool isZero() const {
449  return sgn() == 0;
450  }
451 
452  inline bool isOne() const {
453  return d_value == 1;
454  }
455 
456  inline bool isNegativeOne() const {
457  return d_value == -1;
458  }
459 
460  long getLong() const {
461  // ensure there isn't overflow
462  CheckArgument(d_value <= std::numeric_limits<long>::max(), this,
463  "Overflow detected in Integer::getLong()");
464  CheckArgument(d_value >= std::numeric_limits<long>::min(), this,
465  "Overflow detected in Integer::getLong()");
466  return cln::cl_I_to_long(d_value);
467  }
468 
469  unsigned long getUnsignedLong() const {
470  // ensure there isn't overflow
471  CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), this,
472  "Overflow detected in Integer::getUnsignedLong()");
473  CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), this,
474  "Overflow detected in Integer::getUnsignedLong()");
475  return cln::cl_I_to_ulong(d_value);
476  }
477 
482  size_t hash() const {
483  return equal_hashcode(d_value);
484  }
485 
492  bool testBit(unsigned n) const {
493  return cln::logbitp(n, d_value);
494  }
495 
500  unsigned isPow2() const {
501  if (d_value <= 0) return 0;
502  // power2p returns n such that d_value = 2^(n-1)
503  return cln::power2p(d_value);
504  }
505 
510  size_t length() const {
511  int s = sgn();
512  if(s == 0){
513  return 1;
514  }else if(s < 0){
515  size_t len = cln::integer_length(d_value);
516  /*If this is -2^n, return len+1 not len to stay consistent with the definition above!
517  * From CLN's documentation of integer_length:
518  * This is the smallest n >= 0 such that -2^n <= x < 2^n.
519  * If x > 0, this is the unique n > 0 such that 2^(n-1) <= x < 2^n.
520  */
521  size_t ord2 = cln::ord2(d_value);
522  return (len == ord2) ? (len + 1) : len;
523  }else{
524  return cln::integer_length(d_value);
525  }
526  }
527 
528 /* cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */
529 /* 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). */
530  static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){
531  g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
532  }
533 
535  static const Integer& min(const Integer& a, const Integer& b){
536  return (a <=b ) ? a : b;
537  }
538 
540  static const Integer& max(const Integer& a, const Integer& b){
541  return (a >= b ) ? a : b;
542  }
543 
544  friend class CVC4::Rational;
545 };/* class Integer */
546 
548  inline size_t operator()(const CVC4::Integer& i) const {
549  return i.hash();
550  }
551 };/* struct IntegerHashFunction */
552 
553 inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
554  return os << n.toString();
555 }
556 
557 }/* CVC4 namespace */
558 
559 #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)
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 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)
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.
std::ostream & operator<<(std::ostream &out, SimplificationMode mode)
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