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 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,...)
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(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,...)
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.
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
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
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)
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)
Integer & operator*=(const Integer &y)
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
Integer operator*(const Integer &y) const