cvc4-1.3
CVC4::Integer Class Reference

#include <integer_cln_imp.h>

Public Member Functions

 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 ()
 
Integeroperator= (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
 
Integeroperator+= (const Integer &y)
 
Integer operator- (const Integer &y) const
 
Integeroperator-= (const Integer &y)
 
Integer operator* (const Integer &y) const
 
Integeroperator*= (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...
 
 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 ()
 
Integeroperator= (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
 
Integeroperator+= (const Integer &y)
 
Integer operator- (const Integer &y) const
 
Integeroperator-= (const Integer &y)
 
Integer operator* (const Integer &y) const
 
Integeroperator*= (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...
 

Static Public Member Functions

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 Integermin (const Integer &a, const Integer &b)
 Returns a reference to the minimum of two integers. More...
 
static const Integermax (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 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 Integermin (const Integer &a, const Integer &b)
 Returns a reference to the minimum of two integers. More...
 
static const Integermax (const Integer &a, const Integer &b)
 Returns a reference to the maximum of two integers. More...
 

Friends

class CVC4::Rational
 

Detailed Description

Definition at line 38 of file integer_cln_imp.h.

Constructor & Destructor Documentation

CVC4::Integer::Integer ( )
inline

Constructs a rational with the value 0.

Definition at line 105 of file integer_cln_imp.h.

CVC4::Integer::Integer ( const char *  sp,
unsigned  base = 10 
)
throw (std::invalid_argument
)
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.

CVC4::Integer::Integer ( const std::string &  s,
unsigned  base = 10 
)
throw (std::invalid_argument
)
inlineexplicit

Definition at line 117 of file integer_cln_imp.h.

CVC4::Integer::Integer ( const Integer q)
inline

Definition at line 121 of file integer_cln_imp.h.

CVC4::Integer::Integer ( signed int  z)
inline

Definition at line 123 of file integer_cln_imp.h.

CVC4::Integer::Integer ( unsigned int  z)
inline

Definition at line 124 of file integer_cln_imp.h.

CVC4::Integer::Integer ( signed long int  z)
inline

Definition at line 125 of file integer_cln_imp.h.

CVC4::Integer::Integer ( unsigned long int  z)
inline

Definition at line 126 of file integer_cln_imp.h.

CVC4::Integer::~Integer ( )
inline

Definition at line 133 of file integer_cln_imp.h.

CVC4::Integer::Integer ( )
inline

Constructs a rational with the value 0.

Definition at line 55 of file integer_gmp_imp.h.

CVC4::Integer::Integer ( const char *  s,
unsigned  base = 10 
)
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.

CVC4::Integer::Integer ( const std::string &  s,
unsigned  base = 10 
)
inlineexplicit

Definition at line 64 of file integer_gmp_imp.h.

CVC4::Integer::Integer ( const Integer q)
inline

Definition at line 66 of file integer_gmp_imp.h.

CVC4::Integer::Integer ( signed int  z)
inline

Definition at line 68 of file integer_gmp_imp.h.

CVC4::Integer::Integer ( unsigned int  z)
inline

Definition at line 69 of file integer_gmp_imp.h.

CVC4::Integer::Integer ( signed long int  z)
inline

Definition at line 70 of file integer_gmp_imp.h.

CVC4::Integer::Integer ( unsigned long int  z)
inline

Definition at line 71 of file integer_gmp_imp.h.

CVC4::Integer::~Integer ( )
inline

Definition at line 78 of file integer_gmp_imp.h.

Member Function Documentation

Integer CVC4::Integer::abs ( ) const
inline

Return the absolute value of this integer.

Definition at line 402 of file integer_cln_imp.h.

Integer CVC4::Integer::abs ( ) const
inline

Return the absolute value of this integer.

Definition at line 412 of file integer_gmp_imp.h.

Integer CVC4::Integer::bitwiseAnd ( const Integer y) const
inline

Definition at line 147 of file integer_gmp_imp.h.

Integer CVC4::Integer::bitwiseAnd ( const Integer y) const
inline

Definition at line 200 of file integer_cln_imp.h.

Integer CVC4::Integer::bitwiseNot ( ) const
inline

Definition at line 159 of file integer_gmp_imp.h.

Integer CVC4::Integer::bitwiseNot ( ) const
inline

Definition at line 208 of file integer_cln_imp.h.

Integer CVC4::Integer::bitwiseOr ( const Integer y) const
inline

Definition at line 141 of file integer_gmp_imp.h.

Integer CVC4::Integer::bitwiseOr ( const Integer y) const
inline

Definition at line 196 of file integer_cln_imp.h.

Integer CVC4::Integer::bitwiseXor ( const Integer y) const
inline

Definition at line 153 of file integer_gmp_imp.h.

Integer CVC4::Integer::bitwiseXor ( const Integer y) const
inline

Definition at line 204 of file integer_cln_imp.h.

Integer CVC4::Integer::ceilingDivideQuotient ( const Integer y) const
inline

Returns the ceil(this / y)

Definition at line 248 of file integer_gmp_imp.h.

Integer CVC4::Integer::ceilingDivideQuotient ( const Integer y) const
inline

Returns the ceil(this / y)

Definition at line 276 of file integer_cln_imp.h.

Integer CVC4::Integer::ceilingDivideRemainder ( const Integer y) const
inline

Returns the ceil(this / y)

Definition at line 257 of file integer_gmp_imp.h.

Integer CVC4::Integer::ceilingDivideRemainder ( const Integer y) const
inline

Returns the ceil(this / y)

Definition at line 283 of file integer_cln_imp.h.

Integer CVC4::Integer::divByPow2 ( uint32_t  exp) const
inline

Returns y / 2^exp.

Definition at line 340 of file integer_gmp_imp.h.

Integer CVC4::Integer::divByPow2 ( uint32_t  exp) const
inline
bool CVC4::Integer::divides ( const Integer y) const
inline

Return true if *this exactly divides y.

Definition at line 394 of file integer_cln_imp.h.

Referenced by exactQuotient().

bool CVC4::Integer::divides ( const Integer y) const
inline

All non-zero integers z, z.divide(0) ! zero.divides(zero)

Definition at line 404 of file integer_gmp_imp.h.

Integer CVC4::Integer::euclidianDivideQuotient ( const Integer y) const
inline

Returns the quoitent according to Boute's Euclidean definition.

See the documentation for euclidianQR.

Definition at line 301 of file integer_gmp_imp.h.

Integer CVC4::Integer::euclidianDivideQuotient ( const Integer y) const
inline

Returns the quoitent according to Boute's Euclidean definition.

See the documentation for euclidianQR.

Definition at line 326 of file integer_cln_imp.h.

Integer CVC4::Integer::euclidianDivideRemainder ( const Integer y) const
inline

Returns the remainfing according to Boute's Euclidean definition.

See the documentation for euclidianQR.

Definition at line 311 of file integer_gmp_imp.h.

Integer CVC4::Integer::euclidianDivideRemainder ( const Integer y) const
inline

Returns the remainfing according to Boute's Euclidean definition.

See the documentation for euclidianQR.

Definition at line 336 of file integer_cln_imp.h.

static void CVC4::Integer::euclidianQR ( Integer q,
Integer r,
const Integer x,
const Integer y 
)
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().

static void CVC4::Integer::euclidianQR ( Integer q,
Integer r,
const Integer x,
const Integer y 
)
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().

Integer CVC4::Integer::exactQuotient ( const Integer y) const
inline

If y divides *this, then exactQuotient returns (this/y)

Definition at line 321 of file integer_gmp_imp.h.

References CVC4::DebugCheckArgument(), and divides().

Integer CVC4::Integer::exactQuotient ( const Integer y) const
inline

If y divides *this, then exactQuotient returns (this/y)

Definition at line 345 of file integer_cln_imp.h.

References CVC4::DebugCheckArgument(), and divides().

static void CVC4::Integer::extendedGcd ( Integer g,
Integer s,
Integer t,
const Integer a,
const Integer b 
)
inlinestatic

Definition at line 482 of file integer_gmp_imp.h.

static void CVC4::Integer::extendedGcd ( Integer g,
Integer s,
Integer t,
const Integer a,
const Integer b 
)
inlinestatic

Definition at line 530 of file integer_cln_imp.h.

Integer CVC4::Integer::extractBitRange ( uint32_t  bitCount,
uint32_t  low 
) const
inline

See GMP Documentation.

Definition at line 209 of file integer_gmp_imp.h.

References div.

Integer CVC4::Integer::extractBitRange ( uint32_t  bitCount,
uint32_t  low 
) const
inline

See CLN Documentation.

Definition at line 246 of file integer_cln_imp.h.

Referenced by CVC4::BitVector::arithRightShift(), and CVC4::BitVector::signExtend().

Integer CVC4::Integer::floorDivideQuotient ( const Integer y) const
inline

Returns the floor(this / y)

Definition at line 223 of file integer_gmp_imp.h.

Integer CVC4::Integer::floorDivideQuotient ( const Integer y) const
inline

Returns the floor(this / y)

Definition at line 254 of file integer_cln_imp.h.

Integer CVC4::Integer::floorDivideRemainder ( const Integer y) const
inline

Returns r == this - floor(this/y)*y.

Definition at line 232 of file integer_gmp_imp.h.

Integer CVC4::Integer::floorDivideRemainder ( const Integer y) const
inline

Returns r == this - floor(this/y)*y.

Definition at line 261 of file integer_cln_imp.h.

static void CVC4::Integer::floorQR ( Integer q,
Integer r,
const Integer x,
const Integer y 
)
inlinestatic

Computes a floor quotient and remainder for x divided by y.

Definition at line 241 of file integer_gmp_imp.h.

static void CVC4::Integer::floorQR ( Integer q,
Integer r,
const Integer x,
const Integer y 
)
inlinestatic

Computes a floor quoient and remainder for x divided by y.

Definition at line 267 of file integer_cln_imp.h.

Integer CVC4::Integer::gcd ( const Integer y) const
inline

Return the greatest common divisor of this integer with another.

Definition at line 378 of file integer_cln_imp.h.

Integer CVC4::Integer::gcd ( const Integer y) const
inline

Return the greatest common divisor of this integer with another.

Definition at line 385 of file integer_gmp_imp.h.

long CVC4::Integer::getLong ( ) const
inline

Definition at line 422 of file integer_gmp_imp.h.

References CVC4::CheckArgument().

long CVC4::Integer::getLong ( ) const
inline

Definition at line 460 of file integer_cln_imp.h.

References CVC4::CheckArgument().

unsigned long CVC4::Integer::getUnsignedLong ( ) const
inline

Definition at line 429 of file integer_gmp_imp.h.

References CVC4::CheckArgument().

unsigned long CVC4::Integer::getUnsignedLong ( ) const
inline

Definition at line 469 of file integer_cln_imp.h.

References CVC4::CheckArgument().

size_t CVC4::Integer::hash ( ) const
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().

size_t CVC4::Integer::hash ( ) const
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.

Referenced by CVC4::DivisibleHashFunction::operator()(), CVC4::SubrangeBoundsHashFunction::operator()(), and CVC4::IntegerHashFunction::operator()().

bool CVC4::Integer::isBitSet ( uint32_t  i) const
inline

Definition at line 184 of file integer_gmp_imp.h.

bool CVC4::Integer::isBitSet ( uint32_t  i) const
inline

Definition at line 221 of file integer_cln_imp.h.

bool CVC4::Integer::isNegativeOne ( ) const
inline

Definition at line 367 of file integer_gmp_imp.h.

bool CVC4::Integer::isNegativeOne ( ) const
inline

Definition at line 456 of file integer_cln_imp.h.

bool CVC4::Integer::isOne ( ) const
inline

Definition at line 363 of file integer_gmp_imp.h.

bool CVC4::Integer::isOne ( ) const
inline

Definition at line 452 of file integer_cln_imp.h.

unsigned CVC4::Integer::isPow2 ( ) const
inline

Returns k if the integer is equal to 2^(k-1)

Returns
k if the integer is equal to 2^(k-1) and 0 otherwise

Definition at line 459 of file integer_gmp_imp.h.

unsigned CVC4::Integer::isPow2 ( ) const
inline

Returns k if the integer is equal to 2^(k-1)

Returns
k if the integer is equal to 2^(k-1) and 0 otherwise

Definition at line 500 of file integer_cln_imp.h.

bool CVC4::Integer::isZero ( ) const
inline

Definition at line 359 of file integer_gmp_imp.h.

bool CVC4::Integer::isZero ( ) const
inline

Definition at line 448 of file integer_cln_imp.h.

Integer CVC4::Integer::lcm ( const Integer y) const
inline

Return the least common multiple of this integer with another.

Definition at line 386 of file integer_cln_imp.h.

Integer CVC4::Integer::lcm ( const Integer y) const
inline

Return the least common multiple of this integer with another.

Definition at line 394 of file integer_gmp_imp.h.

size_t CVC4::Integer::length ( ) const
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.

size_t CVC4::Integer::length ( ) const
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.

static const Integer& CVC4::Integer::max ( const Integer a,
const Integer b 
)
inlinestatic

Returns a reference to the maximum of two integers.

Definition at line 494 of file integer_gmp_imp.h.

static const Integer& CVC4::Integer::max ( const Integer a,
const Integer b 
)
inlinestatic

Returns a reference to the maximum of two integers.

Definition at line 540 of file integer_cln_imp.h.

Referenced by CVC4::SubrangeBound::max().

static const Integer& CVC4::Integer::min ( const Integer a,
const Integer b 
)
inlinestatic

Returns a reference to the minimum of two integers.

Definition at line 489 of file integer_gmp_imp.h.

static const Integer& CVC4::Integer::min ( const Integer a,
const Integer b 
)
inlinestatic

Returns a reference to the minimum of two integers.

Definition at line 535 of file integer_cln_imp.h.

Referenced by CVC4::SubrangeBound::min().

Integer CVC4::Integer::modByPow2 ( uint32_t  exp) const
inline

Returns y mod 2^exp.

Definition at line 331 of file integer_gmp_imp.h.

Integer CVC4::Integer::modByPow2 ( uint32_t  exp) const
inline

Definition at line 350 of file integer_cln_imp.h.

Integer CVC4::Integer::multiplyByPow2 ( uint32_t  pow) const
inline

Return this*(2^pow).

Definition at line 168 of file integer_gmp_imp.h.

Integer CVC4::Integer::multiplyByPow2 ( uint32_t  pow) const
inline

Return this*(2^pow).

Definition at line 216 of file integer_cln_imp.h.

Referenced by CVC4::BitVector::leftShift().

Integer CVC4::Integer::oneExtend ( uint32_t  size,
uint32_t  amount 
) const
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().

Integer CVC4::Integer::oneExtend ( uint32_t  size,
uint32_t  amount 
) const
inline
bool CVC4::Integer::operator!= ( const Integer y) const
inline

Definition at line 95 of file integer_gmp_imp.h.

bool CVC4::Integer::operator!= ( const Integer y) const
inline

Definition at line 150 of file integer_cln_imp.h.

Integer CVC4::Integer::operator* ( const Integer y) const
inline

Definition at line 132 of file integer_gmp_imp.h.

Integer CVC4::Integer::operator* ( const Integer y) const
inline

Definition at line 187 of file integer_cln_imp.h.

Integer& CVC4::Integer::operator*= ( const Integer y)
inline

Definition at line 135 of file integer_gmp_imp.h.

Integer& CVC4::Integer::operator*= ( const Integer y)
inline

Definition at line 190 of file integer_cln_imp.h.

Integer CVC4::Integer::operator+ ( const Integer y) const
inline

Definition at line 116 of file integer_gmp_imp.h.

Integer CVC4::Integer::operator+ ( const Integer y) const
inline

Definition at line 171 of file integer_cln_imp.h.

Integer& CVC4::Integer::operator+= ( const Integer y)
inline

Definition at line 119 of file integer_gmp_imp.h.

Integer& CVC4::Integer::operator+= ( const Integer y)
inline

Definition at line 174 of file integer_cln_imp.h.

Integer CVC4::Integer::operator- ( ) const
inline

Definition at line 90 of file integer_gmp_imp.h.

Integer CVC4::Integer::operator- ( const Integer y) const
inline

Definition at line 124 of file integer_gmp_imp.h.

Integer CVC4::Integer::operator- ( ) const
inline

Definition at line 145 of file integer_cln_imp.h.

Integer CVC4::Integer::operator- ( const Integer y) const
inline

Definition at line 179 of file integer_cln_imp.h.

Integer& CVC4::Integer::operator-= ( const Integer y)
inline

Definition at line 127 of file integer_gmp_imp.h.

Integer& CVC4::Integer::operator-= ( const Integer y)
inline

Definition at line 182 of file integer_cln_imp.h.

bool CVC4::Integer::operator< ( const Integer y) const
inline

Definition at line 99 of file integer_gmp_imp.h.

bool CVC4::Integer::operator< ( const Integer y) const
inline

Definition at line 154 of file integer_cln_imp.h.

bool CVC4::Integer::operator<= ( const Integer y) const
inline

Definition at line 103 of file integer_gmp_imp.h.

bool CVC4::Integer::operator<= ( const Integer y) const
inline

Definition at line 158 of file integer_cln_imp.h.

Integer& CVC4::Integer::operator= ( const Integer x)
inline

Definition at line 80 of file integer_gmp_imp.h.

Integer& CVC4::Integer::operator= ( const Integer x)
inline

Definition at line 135 of file integer_cln_imp.h.

bool CVC4::Integer::operator== ( const Integer y) const
inline

Definition at line 86 of file integer_gmp_imp.h.

bool CVC4::Integer::operator== ( const Integer y) const
inline

Definition at line 141 of file integer_cln_imp.h.

bool CVC4::Integer::operator> ( const Integer y) const
inline

Definition at line 107 of file integer_gmp_imp.h.

bool CVC4::Integer::operator> ( const Integer y) const
inline

Definition at line 162 of file integer_cln_imp.h.

bool CVC4::Integer::operator>= ( const Integer y) const
inline

Definition at line 111 of file integer_gmp_imp.h.

bool CVC4::Integer::operator>= ( const Integer y) const
inline

Definition at line 166 of file integer_cln_imp.h.

Integer CVC4::Integer::pow ( unsigned long int  exp) const
inline

Raise this Integer to the power exp.

Parameters
expthe exponent

Definition at line 364 of file integer_cln_imp.h.

Integer CVC4::Integer::pow ( unsigned long int  exp) const
inline

Raise this Integer to the power exp.

Parameters
expthe exponent

Definition at line 376 of file integer_gmp_imp.h.

Integer CVC4::Integer::setBit ( uint32_t  i) const
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.

Integer CVC4::Integer::setBit ( uint32_t  i) const
inline

Definition at line 225 of file integer_cln_imp.h.

Referenced by CVC4::BitVector::setBit().

int CVC4::Integer::sgn ( ) const
inline

Definition at line 347 of file integer_gmp_imp.h.

int CVC4::Integer::sgn ( ) const
inline

Definition at line 434 of file integer_cln_imp.h.

Referenced by euclidianQR().

bool CVC4::Integer::strictlyNegative ( ) const
inline

Definition at line 355 of file integer_gmp_imp.h.

bool CVC4::Integer::strictlyNegative ( ) const
inline

Definition at line 444 of file integer_cln_imp.h.

Referenced by euclidianQR().

bool CVC4::Integer::strictlyPositive ( ) const
inline

Definition at line 351 of file integer_gmp_imp.h.

bool CVC4::Integer::strictlyPositive ( ) const
inline

Definition at line 440 of file integer_cln_imp.h.

bool CVC4::Integer::testBit ( unsigned  n) const
inline

Returns true iff bit n is set.

Parameters
nthe bit to test (0 == least significant bit)
Returns
true if bit n is set in this integer; false otherwise

Definition at line 451 of file integer_gmp_imp.h.

bool CVC4::Integer::testBit ( unsigned  n) const
inline

Returns true iff bit n is set.

Parameters
nthe bit to test (0 == least significant bit)
Returns
true if bit n is set in this integer; false otherwise

Definition at line 492 of file integer_cln_imp.h.

std::string CVC4::Integer::toString ( int  base = 10) const
inline
std::string CVC4::Integer::toString ( int  base = 10) const
inline

Definition at line 416 of file integer_gmp_imp.h.

uint32_t CVC4::Integer::toUnsignedInt ( ) const
inline

Definition at line 204 of file integer_gmp_imp.h.

uint32_t CVC4::Integer::toUnsignedInt ( ) const
inline

Friends And Related Function Documentation

Definition at line 544 of file integer_cln_imp.h.


The documentation for this class was generated from the following files: