cvc4-1.3
|
#include <integer_gmp_imp.h>
Public Member Functions | |
Integer () | |
Constructs a rational with the value 0. More... | |
Integer (const char *s, unsigned base=10) | |
Constructs a Integer from a C string. More... | |
Integer (const std::string &s, unsigned base=10) | |
Integer (const Integer &q) | |
Integer (signed int z) | |
Integer (unsigned int z) | |
Integer (signed long int z) | |
Integer (unsigned long int z) | |
~Integer () | |
Integer & | operator= (const Integer &x) |
bool | operator== (const Integer &y) const |
Integer | operator- () const |
bool | operator!= (const Integer &y) const |
bool | operator< (const Integer &y) const |
bool | operator<= (const Integer &y) const |
bool | operator> (const Integer &y) const |
bool | operator>= (const Integer &y) const |
Integer | operator+ (const Integer &y) const |
Integer & | operator+= (const Integer &y) |
Integer | operator- (const Integer &y) const |
Integer & | operator-= (const Integer &y) |
Integer | operator* (const Integer &y) const |
Integer & | operator*= (const Integer &y) |
Integer | bitwiseOr (const Integer &y) const |
Integer | bitwiseAnd (const Integer &y) const |
Integer | bitwiseXor (const Integer &y) const |
Integer | bitwiseNot () const |
Integer | multiplyByPow2 (uint32_t pow) const |
Return this*(2^pow). More... | |
Integer | setBit (uint32_t i) const |
Returns the Integer obtained by setting the ith bit of the current Integer to 1. More... | |
bool | isBitSet (uint32_t i) const |
Integer | oneExtend (uint32_t size, uint32_t amount) const |
Returns the integer with the binary representation of size bits extended with amount 1's. More... | |
uint32_t | toUnsignedInt () const |
Integer | extractBitRange (uint32_t bitCount, uint32_t low) const |
See GMP Documentation. More... | |
Integer | floorDivideQuotient (const Integer &y) const |
Returns the floor(this / y) More... | |
Integer | floorDivideRemainder (const Integer &y) const |
Returns r == this - floor(this/y)*y. More... | |
Integer | ceilingDivideQuotient (const Integer &y) const |
Returns the ceil(this / y) More... | |
Integer | ceilingDivideRemainder (const Integer &y) const |
Returns the ceil(this / y) More... | |
Integer | euclidianDivideQuotient (const Integer &y) const |
Returns the quoitent according to Boute's Euclidean definition. More... | |
Integer | euclidianDivideRemainder (const Integer &y) const |
Returns the remainfing according to Boute's Euclidean definition. More... | |
Integer | exactQuotient (const Integer &y) const |
If y divides *this, then exactQuotient returns (this/y) More... | |
Integer | modByPow2 (uint32_t exp) const |
Returns y mod 2^exp. More... | |
Integer | divByPow2 (uint32_t exp) const |
Returns y / 2^exp. More... | |
int | sgn () const |
bool | strictlyPositive () const |
bool | strictlyNegative () const |
bool | isZero () const |
bool | isOne () const |
bool | isNegativeOne () const |
Integer | pow (unsigned long int exp) const |
Raise this Integer to the power exp . More... | |
Integer | gcd (const Integer &y) const |
Return the greatest common divisor of this integer with another. More... | |
Integer | lcm (const Integer &y) const |
Return the least common multiple of this integer with another. More... | |
bool | divides (const Integer &y) const |
All non-zero integers z, z.divide(0) ! zero.divides(zero) More... | |
Integer | abs () const |
Return the absolute value of this integer. More... | |
std::string | toString (int base=10) const |
long | getLong () const |
unsigned long | getUnsignedLong () const |
size_t | hash () const |
Computes the hash of the node from the first word of the numerator, the denominator. More... | |
bool | testBit (unsigned n) const |
Returns true iff bit n is set. More... | |
unsigned | isPow2 () const |
Returns k if the integer is equal to 2^(k-1) More... | |
size_t | length () const |
If x != 0, returns the smallest n s.t. More... | |
Integer () | |
Constructs a rational with the value 0. More... | |
Integer (const char *sp, unsigned base=10) throw (std::invalid_argument) | |
Constructs a Integer from a C string. More... | |
Integer (const std::string &s, unsigned base=10) throw (std::invalid_argument) | |
Integer (const Integer &q) | |
Integer (signed int z) | |
Integer (unsigned int z) | |
Integer (signed long int z) | |
Integer (unsigned long int z) | |
~Integer () | |
Integer & | operator= (const Integer &x) |
bool | operator== (const Integer &y) const |
Integer | operator- () const |
bool | operator!= (const Integer &y) const |
bool | operator< (const Integer &y) const |
bool | operator<= (const Integer &y) const |
bool | operator> (const Integer &y) const |
bool | operator>= (const Integer &y) const |
Integer | operator+ (const Integer &y) const |
Integer & | operator+= (const Integer &y) |
Integer | operator- (const Integer &y) const |
Integer & | operator-= (const Integer &y) |
Integer | operator* (const Integer &y) const |
Integer & | operator*= (const Integer &y) |
Integer | bitwiseOr (const Integer &y) const |
Integer | bitwiseAnd (const Integer &y) const |
Integer | bitwiseXor (const Integer &y) const |
Integer | bitwiseNot () const |
Integer | multiplyByPow2 (uint32_t pow) const |
Return this*(2^pow). More... | |
bool | isBitSet (uint32_t i) const |
Integer | setBit (uint32_t i) const |
Integer | oneExtend (uint32_t size, uint32_t amount) const |
uint32_t | toUnsignedInt () const |
Integer | extractBitRange (uint32_t bitCount, uint32_t low) const |
See CLN Documentation. More... | |
Integer | floorDivideQuotient (const Integer &y) const |
Returns the floor(this / y) More... | |
Integer | floorDivideRemainder (const Integer &y) const |
Returns r == this - floor(this/y)*y. More... | |
Integer | ceilingDivideQuotient (const Integer &y) const |
Returns the ceil(this / y) More... | |
Integer | ceilingDivideRemainder (const Integer &y) const |
Returns the ceil(this / y) More... | |
Integer | euclidianDivideQuotient (const Integer &y) const |
Returns the quoitent according to Boute's Euclidean definition. More... | |
Integer | euclidianDivideRemainder (const Integer &y) const |
Returns the remainfing according to Boute's Euclidean definition. More... | |
Integer | exactQuotient (const Integer &y) const |
If y divides *this, then exactQuotient returns (this/y) More... | |
Integer | modByPow2 (uint32_t exp) const |
Integer | divByPow2 (uint32_t exp) const |
Integer | pow (unsigned long int exp) const |
Raise this Integer to the power exp . More... | |
Integer | gcd (const Integer &y) const |
Return the greatest common divisor of this integer with another. More... | |
Integer | lcm (const Integer &y) const |
Return the least common multiple of this integer with another. More... | |
bool | divides (const Integer &y) const |
Return true if *this exactly divides y. More... | |
Integer | abs () const |
Return the absolute value of this integer. More... | |
std::string | toString (int base=10) const |
int | sgn () const |
bool | strictlyPositive () const |
bool | strictlyNegative () const |
bool | isZero () const |
bool | isOne () const |
bool | isNegativeOne () const |
long | getLong () const |
unsigned long | getUnsignedLong () const |
size_t | hash () const |
Computes the hash of the node from the first word of the numerator, the denominator. More... | |
bool | testBit (unsigned n) const |
Returns true iff bit n is set. More... | |
unsigned | isPow2 () const |
Returns k if the integer is equal to 2^(k-1) More... | |
size_t | length () const |
If x != 0, returns the unique n s.t. More... | |
Static Public Member Functions | |
static void | floorQR (Integer &q, Integer &r, const Integer &x, const Integer &y) |
Computes a floor quotient and remainder for x divided by y. More... | |
static void | euclidianQR (Integer &q, Integer &r, const Integer &x, const Integer &y) |
Computes a quoitent and remainder according to Boute's Euclidean definition. More... | |
static void | extendedGcd (Integer &g, Integer &s, Integer &t, const Integer &a, const Integer &b) |
static const Integer & | min (const Integer &a, const Integer &b) |
Returns a reference to the minimum of two integers. More... | |
static const Integer & | max (const Integer &a, const Integer &b) |
Returns a reference to the maximum of two integers. More... | |
static void | floorQR (Integer &q, Integer &r, const Integer &x, const Integer &y) |
Computes a floor quoient and remainder for x divided by y. More... | |
static void | euclidianQR (Integer &q, Integer &r, const Integer &x, const Integer &y) |
Computes a quoitent and remainder according to Boute's Euclidean definition. More... | |
static void | extendedGcd (Integer &g, Integer &s, Integer &t, const Integer &a, const Integer &b) |
static const Integer & | min (const Integer &a, const Integer &b) |
Returns a reference to the minimum of two integers. More... | |
static const Integer & | max (const Integer &a, const Integer &b) |
Returns a reference to the maximum of two integers. More... | |
Friends | |
class | CVC4::Rational |
Definition at line 33 of file integer_gmp_imp.h.
|
inline |
Constructs a rational with the value 0.
Definition at line 55 of file integer_gmp_imp.h.
|
inlineexplicit |
Constructs a Integer from a C string.
Throws std::invalid_argument if the string is not a valid rational. For more information about what is a valid rational string, see GMP's documentation for mpq_set_str().
Definition at line 63 of file integer_gmp_imp.h.
|
inlineexplicit |
Definition at line 64 of file integer_gmp_imp.h.
|
inline |
Definition at line 66 of file integer_gmp_imp.h.
|
inline |
Definition at line 68 of file integer_gmp_imp.h.
|
inline |
Definition at line 69 of file integer_gmp_imp.h.
|
inline |
Definition at line 70 of file integer_gmp_imp.h.
|
inline |
Definition at line 71 of file integer_gmp_imp.h.
|
inline |
Definition at line 78 of file integer_gmp_imp.h.
|
inline |
Constructs a rational with the value 0.
Definition at line 105 of file integer_cln_imp.h.
|
inlineexplicit |
Constructs a Integer from a C string.
Throws std::invalid_argument if the string is not a valid rational. For more information about what is a valid rational string, see GMP's documentation for mpq_set_str().
Definition at line 113 of file integer_cln_imp.h.
|
inlineexplicit |
Definition at line 117 of file integer_cln_imp.h.
|
inline |
Definition at line 121 of file integer_cln_imp.h.
|
inline |
Definition at line 123 of file integer_cln_imp.h.
|
inline |
Definition at line 124 of file integer_cln_imp.h.
|
inline |
Definition at line 125 of file integer_cln_imp.h.
|
inline |
Definition at line 126 of file integer_cln_imp.h.
|
inline |
Definition at line 133 of file integer_cln_imp.h.
|
inline |
Return the absolute value of this integer.
Definition at line 402 of file integer_cln_imp.h.
|
inline |
Return the absolute value of this integer.
Definition at line 412 of file integer_gmp_imp.h.
Definition at line 147 of file integer_gmp_imp.h.
Definition at line 200 of file integer_cln_imp.h.
|
inline |
Definition at line 159 of file integer_gmp_imp.h.
|
inline |
Definition at line 208 of file integer_cln_imp.h.
Definition at line 141 of file integer_gmp_imp.h.
Definition at line 196 of file integer_cln_imp.h.
Definition at line 153 of file integer_gmp_imp.h.
Definition at line 204 of file integer_cln_imp.h.
Returns the ceil(this / y)
Definition at line 248 of file integer_gmp_imp.h.
Returns the ceil(this / y)
Definition at line 276 of file integer_cln_imp.h.
Returns the ceil(this / y)
Definition at line 257 of file integer_gmp_imp.h.
Returns the ceil(this / y)
Definition at line 283 of file integer_cln_imp.h.
|
inline |
Returns y / 2^exp.
Definition at line 340 of file integer_gmp_imp.h.
Referenced by CVC4::BitVector::arithRightShift(), and CVC4::BitVector::logicalRightShift().
|
inline |
Definition at line 355 of file integer_cln_imp.h.
|
inline |
Return true if *this exactly divides y.
Definition at line 394 of file integer_cln_imp.h.
|
inline |
All non-zero integers z, z.divide(0) ! zero.divides(zero)
Definition at line 404 of file integer_gmp_imp.h.
Referenced by exactQuotient().
Returns the quoitent according to Boute's Euclidean definition.
See the documentation for euclidianQR.
Definition at line 301 of file integer_gmp_imp.h.
Returns the quoitent according to Boute's Euclidean definition.
See the documentation for euclidianQR.
Definition at line 326 of file integer_cln_imp.h.
Returns the remainfing according to Boute's Euclidean definition.
See the documentation for euclidianQR.
Definition at line 311 of file integer_gmp_imp.h.
Returns the remainfing according to Boute's Euclidean definition.
See the documentation for euclidianQR.
Definition at line 336 of file integer_cln_imp.h.
|
inlinestatic |
Computes a quoitent and remainder according to Boute's Euclidean definition.
euclidianDivideQuotient, euclidianDivideRemainder.
Boute, Raymond T. (April 1992). The Euclidean definition of the functions div and mod. ACM Transactions on Programming Languages and Systems (TOPLAS) ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
Definition at line 272 of file integer_gmp_imp.h.
References sgn(), and strictlyNegative().
|
inlinestatic |
Computes a quoitent and remainder according to Boute's Euclidean definition.
euclidianDivideQuotient, euclidianDivideRemainder.
Boute, Raymond T. (April 1992). The Euclidean definition of the functions div and mod. ACM Transactions on Programming Languages and Systems (TOPLAS) ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
Definition at line 296 of file integer_cln_imp.h.
References sgn(), and strictlyNegative().
If y divides *this, then exactQuotient returns (this/y)
Definition at line 321 of file integer_gmp_imp.h.
References CVC4::DebugCheckArgument(), and divides().
If y divides *this, then exactQuotient returns (this/y)
Definition at line 345 of file integer_cln_imp.h.
References CVC4::DebugCheckArgument(), and divides().
|
inlinestatic |
Definition at line 482 of file integer_gmp_imp.h.
|
inlinestatic |
Definition at line 530 of file integer_cln_imp.h.
|
inline |
See GMP Documentation.
Definition at line 209 of file integer_gmp_imp.h.
References div.
Referenced by CVC4::BitVector::arithRightShift(), and CVC4::BitVector::signExtend().
|
inline |
See CLN Documentation.
Definition at line 246 of file integer_cln_imp.h.
Returns the floor(this / y)
Definition at line 223 of file integer_gmp_imp.h.
Returns the floor(this / y)
Definition at line 254 of file integer_cln_imp.h.
Returns r == this - floor(this/y)*y.
Definition at line 232 of file integer_gmp_imp.h.
Returns r == this - floor(this/y)*y.
Definition at line 261 of file integer_cln_imp.h.
|
inlinestatic |
Computes a floor quotient and remainder for x divided by y.
Definition at line 241 of file integer_gmp_imp.h.
|
inlinestatic |
Computes a floor quoient and remainder for x divided by y.
Definition at line 267 of file integer_cln_imp.h.
Return the greatest common divisor of this integer with another.
Definition at line 378 of file integer_cln_imp.h.
Return the greatest common divisor of this integer with another.
Definition at line 385 of file integer_gmp_imp.h.
|
inline |
Definition at line 422 of file integer_gmp_imp.h.
References CVC4::CheckArgument().
|
inline |
Definition at line 460 of file integer_cln_imp.h.
References CVC4::CheckArgument().
|
inline |
Definition at line 429 of file integer_gmp_imp.h.
References CVC4::CheckArgument().
|
inline |
Definition at line 469 of file integer_cln_imp.h.
References CVC4::CheckArgument().
|
inline |
Computes the hash of the node from the first word of the numerator, the denominator.
Definition at line 441 of file integer_gmp_imp.h.
References CVC4::gmpz_hash().
Referenced by CVC4::DivisibleHashFunction::operator()(), CVC4::SubrangeBoundsHashFunction::operator()(), and CVC4::IntegerHashFunction::operator()().
|
inline |
Computes the hash of the node from the first word of the numerator, the denominator.
Definition at line 482 of file integer_cln_imp.h.
|
inline |
Definition at line 184 of file integer_gmp_imp.h.
|
inline |
Definition at line 221 of file integer_cln_imp.h.
|
inline |
Definition at line 367 of file integer_gmp_imp.h.
|
inline |
Definition at line 456 of file integer_cln_imp.h.
|
inline |
Definition at line 363 of file integer_gmp_imp.h.
|
inline |
Definition at line 452 of file integer_cln_imp.h.
|
inline |
Returns k if the integer is equal to 2^(k-1)
Definition at line 459 of file integer_gmp_imp.h.
|
inline |
Returns k if the integer is equal to 2^(k-1)
Definition at line 500 of file integer_cln_imp.h.
|
inline |
Definition at line 359 of file integer_gmp_imp.h.
|
inline |
Definition at line 448 of file integer_cln_imp.h.
Return the least common multiple of this integer with another.
Definition at line 386 of file integer_cln_imp.h.
Return the least common multiple of this integer with another.
Definition at line 394 of file integer_gmp_imp.h.
|
inline |
If x != 0, returns the smallest n s.t.
2^{n-1} <= abs(x) < 2^{n}. If x == 0, returns 1.
Definition at line 474 of file integer_gmp_imp.h.
|
inline |
If x != 0, returns the unique n s.t.
2^{n-1} <= abs(x) < 2^{n}. If x == 0, returns 1.
Definition at line 510 of file integer_cln_imp.h.
Returns a reference to the maximum of two integers.
Definition at line 494 of file integer_gmp_imp.h.
Referenced by CVC4::SubrangeBound::max().
Returns a reference to the maximum of two integers.
Definition at line 540 of file integer_cln_imp.h.
Returns a reference to the minimum of two integers.
Definition at line 489 of file integer_gmp_imp.h.
Referenced by CVC4::SubrangeBound::min().
Returns a reference to the minimum of two integers.
Definition at line 535 of file integer_cln_imp.h.
|
inline |
Returns y mod 2^exp.
Definition at line 331 of file integer_gmp_imp.h.
|
inline |
Definition at line 350 of file integer_cln_imp.h.
|
inline |
Return this*(2^pow).
Definition at line 168 of file integer_gmp_imp.h.
Referenced by CVC4::BitVector::leftShift().
|
inline |
Return this*(2^pow).
Definition at line 216 of file integer_cln_imp.h.
|
inline |
Returns the integer with the binary representation of size bits extended with amount 1's.
Definition at line 192 of file integer_gmp_imp.h.
References CVC4::DebugCheckArgument().
Referenced by CVC4::BitVector::arithRightShift(), and CVC4::BitVector::signExtend().
|
inline |
Definition at line 231 of file integer_cln_imp.h.
References CVC4::DebugCheckArgument().
|
inline |
Definition at line 95 of file integer_gmp_imp.h.
|
inline |
Definition at line 150 of file integer_cln_imp.h.
Definition at line 132 of file integer_gmp_imp.h.
Definition at line 187 of file integer_cln_imp.h.
Definition at line 135 of file integer_gmp_imp.h.
Definition at line 190 of file integer_cln_imp.h.
Definition at line 116 of file integer_gmp_imp.h.
Definition at line 171 of file integer_cln_imp.h.
Definition at line 119 of file integer_gmp_imp.h.
Definition at line 174 of file integer_cln_imp.h.
|
inline |
Definition at line 90 of file integer_gmp_imp.h.
Definition at line 124 of file integer_gmp_imp.h.
|
inline |
Definition at line 145 of file integer_cln_imp.h.
Definition at line 179 of file integer_cln_imp.h.
Definition at line 127 of file integer_gmp_imp.h.
Definition at line 182 of file integer_cln_imp.h.
|
inline |
Definition at line 99 of file integer_gmp_imp.h.
|
inline |
Definition at line 154 of file integer_cln_imp.h.
|
inline |
Definition at line 103 of file integer_gmp_imp.h.
|
inline |
Definition at line 158 of file integer_cln_imp.h.
Definition at line 80 of file integer_gmp_imp.h.
Definition at line 135 of file integer_cln_imp.h.
|
inline |
Definition at line 86 of file integer_gmp_imp.h.
|
inline |
Definition at line 141 of file integer_cln_imp.h.
|
inline |
Definition at line 107 of file integer_gmp_imp.h.
|
inline |
Definition at line 162 of file integer_cln_imp.h.
|
inline |
Definition at line 111 of file integer_gmp_imp.h.
|
inline |
Definition at line 166 of file integer_cln_imp.h.
|
inline |
Raise this Integer to the power exp
.
exp | the exponent |
Definition at line 364 of file integer_cln_imp.h.
|
inline |
Raise this Integer to the power exp
.
exp | the exponent |
Definition at line 376 of file integer_gmp_imp.h.
|
inline |
Returns the Integer obtained by setting the ith bit of the current Integer to 1.
Definition at line 178 of file integer_gmp_imp.h.
Referenced by CVC4::BitVector::setBit().
|
inline |
Definition at line 225 of file integer_cln_imp.h.
|
inline |
Definition at line 347 of file integer_gmp_imp.h.
Referenced by euclidianQR().
|
inline |
Definition at line 434 of file integer_cln_imp.h.
|
inline |
Definition at line 355 of file integer_gmp_imp.h.
Referenced by euclidianQR().
|
inline |
Definition at line 444 of file integer_cln_imp.h.
|
inline |
Definition at line 351 of file integer_gmp_imp.h.
|
inline |
Definition at line 440 of file integer_cln_imp.h.
|
inline |
Returns true iff bit n is set.
n | the bit to test (0 == least significant bit) |
Definition at line 451 of file integer_gmp_imp.h.
|
inline |
Returns true iff bit n is set.
n | the bit to test (0 == least significant bit) |
Definition at line 492 of file integer_cln_imp.h.
|
inline |
Definition at line 406 of file integer_cln_imp.h.
|
inline |
Definition at line 416 of file integer_gmp_imp.h.
Referenced by CVC4::Cardinality::Cardinality(), CVC4::CardinalityBeth::CardinalityBeth(), CVC4::SExpr::getValue(), and CVC4::operator<<().
|
inline |
Definition at line 204 of file integer_gmp_imp.h.
Referenced by CVC4::BitVector::arithRightShift(), CVC4::BitVector::leftShift(), and CVC4::BitVector::logicalRightShift().
|
inline |
Definition at line 240 of file integer_cln_imp.h.
|
friend |
Definition at line 498 of file integer_gmp_imp.h.