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>
51 const cln::cl_I& get_cl_I()
const {
return d_value; }
57 Integer(
const cln::cl_I& val) : d_value(val) {}
59 void readInt(
const cln::cl_read_flags& flags,
const std::string& s,
unsigned base)
throw(std::invalid_argument) {
61 if(s.find_first_not_of(
'0') == std::string::npos) {
65 d_value = read_integer(flags,
"0", NULL, NULL);
67 d_value = read_integer(flags, s.c_str(), NULL, NULL);
71 ss <<
"Integer() failed to parse value \"" << s <<
"\" in base " << base;
72 throw std::invalid_argument(ss.str());
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;
84 flags.lsyntax = cln::lsyntax_commonlisp;
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");
91 st.replace(0, 1,
"#o");
93 readInt(flags, st, base);
96 flags.rational_base = 10;
99 readInt(flags, s, base);
113 explicit Integer(
const char* sp,
unsigned base = 10) throw (std::invalid_argument) {
114 parseInt(std::string(sp), base);
117 explicit Integer(
const std::string& s,
unsigned base = 10) throw (std::invalid_argument) {
123 Integer(
signed int z) : d_value((signed long int)z) {}
124 Integer(
unsigned int z) : d_value((unsigned long int)z) {}
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)) {}
136 if(
this == &x)
return *
this;
142 return d_value == y.d_value;
151 return d_value != y.d_value;
155 return d_value < y.d_value;
159 return d_value <= y.d_value;
163 return d_value > y.d_value;
167 return d_value >= y.d_value;
172 return Integer( d_value + y.d_value );
175 d_value += y.d_value;
180 return Integer( d_value - y.d_value );
183 d_value -= y.d_value;
188 return Integer( d_value * y.d_value );
191 d_value *= y.d_value;
197 return Integer(cln::logior(d_value, y.d_value));
201 return Integer(cln::logand(d_value, y.d_value));
205 return Integer(cln::logxor(d_value, y.d_value));
209 return Integer(cln::lognot(d_value));
218 return Integer( d_value << ipow);
222 return !extractBitRange(1, i).isZero();
228 return Integer(cln::logior(d_value, mask));
233 cln::cl_byte range(amount, size);
234 cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1;
237 return Integer(cln::deposit_field(allones, d_value, range));
241 return cln::cl_I_to_uint(d_value);
247 cln::cl_byte range(bitCount, low);
248 return Integer(cln::ldb(d_value, range));
255 return Integer( cln::floor1(d_value, y.d_value) );
262 return Integer( cln::floor2(d_value, y.d_value).remainder );
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;
277 return Integer( cln::ceiling1(d_value, y.d_value) );
284 return Integer( cln::ceiling2(d_value, y.d_value).remainder );
328 euclidianQR(q,r, *
this, y);
338 euclidianQR(q,r, *
this, y);
347 return Integer( cln::exquo(d_value, y.d_value) );
351 cln::cl_byte range(exp, 0);
352 return Integer(cln::ldb(d_value, range));
356 return d_value >> exp;
366 cln::cl_I result= cln::expt_pos(d_value,exp);
371 throw Exception(
"Negative exponent in Integer::pow()");
379 cln::cl_I result = cln::gcd(d_value, y.d_value);
387 cln::cl_I result = cln::lcm(d_value, y.d_value);
395 cln::cl_I result = cln::rem(y.d_value, d_value);
396 return cln::zerop(result);
403 return d_value >= 0 ? *
this : -*
this;
407 std::stringstream ss;
410 fprintbinary(ss,d_value);
413 fprintoctal(ss,d_value);
416 fprintdecimal(ss,d_value);
419 fprinthexadecimal(ss,d_value);
422 throw Exception(
"Unhandled base in Integer::toString()");
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]));
435 cln::cl_I sgn = cln::signum(d_value);
436 return cln::cl_I_to_int(sgn);
457 return d_value == -1;
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);
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);
483 return equal_hashcode(d_value);
493 return cln::logbitp(n, d_value);
501 if (d_value <= 0)
return 0;
503 return cln::power2p(d_value);
515 size_t len = cln::integer_length(d_value);
521 size_t ord2 = cln::ord2(d_value);
522 return (len == ord2) ? (len + 1) : len;
524 return cln::integer_length(d_value);
531 g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
536 return (a <=b ) ? a : b;
541 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.
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
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.
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.
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)
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