20 #ifndef __CVC4__INTEGER_H 21 #define __CVC4__INTEGER_H 27 #include <cln/integer.h> 28 #include <cln/input.h> 29 #include <cln/integer_io.h> 49 const cln::cl_I& get_cl_I()
const {
return d_value; }
54 Integer(
const cln::cl_I& val) : d_value(val) {}
56 void readInt(
const cln::cl_read_flags& flags,
const std::string& s,
unsigned base)
throw(std::invalid_argument);
58 void parseInt(
const std::string& s,
unsigned base)
throw(std::invalid_argument);
71 explicit Integer(
const char* sp,
unsigned base = 10) throw (
std::invalid_argument) {
72 parseInt(std::string(sp), base);
75 explicit Integer(
const std::string& s,
unsigned base = 10) throw (
std::invalid_argument) {
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) {}
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)) {}
94 if(
this == &x)
return *
this;
100 return d_value == y.d_value;
109 return d_value != y.d_value;
113 return d_value < y.d_value;
117 return d_value <= y.d_value;
121 return d_value > y.d_value;
125 return d_value >= y.d_value;
130 return Integer( d_value + y.d_value );
133 d_value += y.d_value;
138 return Integer( d_value - y.d_value );
141 d_value -= y.d_value;
146 return Integer( d_value * y.d_value );
149 d_value *= y.d_value;
155 return Integer(cln::logior(d_value, y.d_value));
159 return Integer(cln::logand(d_value, y.d_value));
163 return Integer(cln::logxor(d_value, y.d_value));
167 return Integer(cln::lognot(d_value));
176 return Integer( d_value << ipow);
180 return !extractBitRange(1, i).isZero();
186 return Integer(cln::logior(d_value, mask));
191 cln::cl_byte range(amount, size);
192 cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1;
195 return Integer(cln::deposit_field(allones, d_value, range));
199 return cln::cl_I_to_uint(d_value);
205 cln::cl_byte range(bitCount, low);
206 return Integer(cln::ldb(d_value, range));
213 return Integer( cln::floor1(d_value, y.d_value) );
220 return Integer( cln::floor2(d_value, y.d_value).remainder );
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;
235 return Integer( cln::ceiling1(d_value, y.d_value) );
242 return Integer( cln::ceiling2(d_value, y.d_value).remainder );
286 euclidianQR(q,r, *
this, y);
296 euclidianQR(q,r, *
this, y);
305 return Integer( cln::exquo(d_value, y.d_value) );
309 cln::cl_byte range(exp, 0);
310 return Integer(cln::ldb(d_value, range));
314 return d_value >> exp;
324 cln::cl_I result= cln::expt_pos(d_value,exp);
329 throw Exception(
"Negative exponent in Integer::pow()");
337 cln::cl_I result = cln::gcd(d_value, y.d_value);
345 cln::cl_I result = cln::lcm(d_value, y.d_value);
353 cln::cl_I result = cln::rem(y.d_value, d_value);
354 return cln::zerop(result);
361 return d_value >= 0 ? *this : -*
this;
365 std::stringstream ss;
368 fprintbinary(ss,d_value);
371 fprintoctal(ss,d_value);
374 fprintdecimal(ss,d_value);
377 fprinthexadecimal(ss,d_value);
380 throw Exception(
"Unhandled base in Integer::toString()");
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]));
393 cln::cl_I sgn = cln::signum(d_value);
394 return cln::cl_I_to_int(sgn);
415 return d_value == -1;
419 bool fitsSignedInt()
const;
422 bool fitsUnsignedInt()
const;
424 int getSignedInt()
const;
426 unsigned int getUnsignedInt()
const;
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);
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);
451 return equal_hashcode(d_value);
461 return cln::logbitp(n, d_value);
469 if (d_value <= 0)
return 0;
471 return cln::power2p(d_value);
483 size_t len = cln::integer_length(d_value);
489 size_t ord2 = cln::ord2(d_value);
490 return (len == ord2) ? (len + 1) : len;
492 return cln::integer_length(d_value);
499 g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
504 return (a <=b ) ? a : b;
509 return (a >= b ) ? a : b;
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 strictlyNegative() const
void DebugCheckArgument(bool cond, const T &arg, const char *fmt,...)
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's Euclidean definition.
Integer floorDivideQuotient(const Integer &y) const
Returns the floor(this / y)
bool isBitSet(uint32_t i) const
Integer(unsigned long int z)
Integer(const Integer &q)
static void extendedGcd(Integer &g, Integer &s, Integer &t, const Integer &a, const Integer &b)
Integer operator-(const Integer &y) const
uint32_t toUnsignedInt() const
A multi-precision rational constant.
std::ostream & operator<<(std::ostream &, const Command &)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
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's exception base class and some associated utilities.
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's Euclidean definition.
Integer operator+(const Integer &y) const
Integer modByPow2(uint32_t exp) const
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
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(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's Euclidean definition.
Integer bitwiseOr(const Integer &y) const