cvc4-1.4
|
A multi-precision rational constant. More...
#include <rational_cln_imp.h>
Public Member Functions | |
Rational () | |
Constructs a rational with the value 0/1. More... | |
Rational (const char *s, unsigned base=10) throw (std::invalid_argument) | |
Constructs a Rational from a C string in a given base (defaults to 10). More... | |
Rational (const std::string &s, unsigned base=10) throw (std::invalid_argument) | |
Rational (const Rational &q) | |
Creates a Rational from another Rational, q, by performing a deep copy. More... | |
Rational (signed int n) | |
Constructs a canonical Rational from a numerator. More... | |
Rational (unsigned int n) | |
Rational (signed long int n) | |
Rational (unsigned long int n) | |
Rational (signed int n, signed int d) | |
Constructs a canonical Rational from a numerator and denominator. More... | |
Rational (unsigned int n, unsigned int d) | |
Rational (signed long int n, signed long int d) | |
Rational (unsigned long int n, unsigned long int d) | |
Rational (const Integer &n, const Integer &d) | |
Rational (const Integer &n) | |
~Rational () | |
Integer | getNumerator () const |
Returns the value of numerator of the Rational. More... | |
Integer | getDenominator () const |
Returns the value of denominator of the Rational. More... | |
double | getDouble () const |
Get a double representation of this Rational, which is approximate: truncation may occur, overflow may result in infinity, and underflow may result in zero. More... | |
Rational | inverse () const |
int | cmp (const Rational &x) const |
int | sgn () const |
bool | isZero () const |
bool | isOne () const |
bool | isNegativeOne () const |
Rational | abs () const |
bool | isIntegral () const |
Integer | floor () const |
Integer | ceiling () const |
Rational | floor_frac () const |
Rational & | operator= (const Rational &x) |
Rational | operator- () const |
bool | operator== (const Rational &y) const |
bool | operator!= (const Rational &y) const |
bool | operator< (const Rational &y) const |
bool | operator<= (const Rational &y) const |
bool | operator> (const Rational &y) const |
bool | operator>= (const Rational &y) const |
Rational | operator+ (const Rational &y) const |
Rational | operator- (const Rational &y) const |
Rational | operator* (const Rational &y) const |
Rational | operator/ (const Rational &y) const |
Rational & | operator+= (const Rational &y) |
Rational & | operator-= (const Rational &y) |
Rational & | operator*= (const Rational &y) |
Rational & | operator/= (const Rational &y) |
std::string | toString (int base=10) const |
Returns a string representing the rational in the given base. More... | |
size_t | hash () const |
Computes the hash of the rational from hashes of the numerator and the denominator. More... | |
uint32_t | complexity () const |
int | absCmp (const Rational &q) const |
Equivalent to calling (this->abs()).cmp(b.abs()) More... | |
Rational () | |
Constructs a rational with the value 0/1. More... | |
Rational (const char *s, unsigned base=10) | |
Constructs a Rational from a C string in a given base (defaults to 10). More... | |
Rational (const std::string &s, unsigned base=10) | |
Rational (const Rational &q) | |
Creates a Rational from another Rational, q, by performing a deep copy. More... | |
Rational (signed int n) | |
Constructs a canonical Rational from a numerator. More... | |
Rational (unsigned int n) | |
Rational (signed long int n) | |
Rational (unsigned long int n) | |
Rational (signed int n, signed int d) | |
Constructs a canonical Rational from a numerator and denominator. More... | |
Rational (unsigned int n, unsigned int d) | |
Rational (signed long int n, signed long int d) | |
Rational (unsigned long int n, unsigned long int d) | |
Rational (const Integer &n, const Integer &d) | |
Rational (const Integer &n) | |
~Rational () | |
Integer | getNumerator () const |
Returns the value of numerator of the Rational. More... | |
Integer | getDenominator () const |
Returns the value of denominator of the Rational. More... | |
double | getDouble () const |
Get a double representation of this Rational, which is approximate: truncation may occur, overflow may result in infinity, and underflow may result in zero. More... | |
Rational | inverse () const |
int | cmp (const Rational &x) const |
int | sgn () const |
bool | isZero () const |
bool | isOne () const |
bool | isNegativeOne () const |
Rational | abs () const |
Integer | floor () const |
Integer | ceiling () const |
Rational | floor_frac () const |
Rational & | operator= (const Rational &x) |
Rational | operator- () const |
bool | operator== (const Rational &y) const |
bool | operator!= (const Rational &y) const |
bool | operator< (const Rational &y) const |
bool | operator<= (const Rational &y) const |
bool | operator> (const Rational &y) const |
bool | operator>= (const Rational &y) const |
Rational | operator+ (const Rational &y) const |
Rational | operator- (const Rational &y) const |
Rational | operator* (const Rational &y) const |
Rational | operator/ (const Rational &y) const |
Rational & | operator+= (const Rational &y) |
Rational & | operator-= (const Rational &y) |
Rational & | operator*= (const Rational &y) |
Rational & | operator/= (const Rational &y) |
bool | isIntegral () const |
std::string | toString (int base=10) const |
Returns a string representing the rational in the given base. More... | |
size_t | hash () const |
Computes the hash of the rational from hashes of the numerator and the denominator. More... | |
uint32_t | complexity () const |
int | absCmp (const Rational &q) const |
Equivalent to calling (this->abs()).cmp(b.abs()) More... | |
Static Public Member Functions | |
static Rational | fromDecimal (const std::string &dec) |
Creates a rational from a decimal string (e.g., "1.5" ). More... | |
static Rational | fromDouble (double d) throw (RationalFromDoubleException) |
Return an exact rational for a double d. More... | |
static Rational | fromDecimal (const std::string &dec) |
Creates a rational from a decimal string (e.g., "1.5" ). More... | |
static Rational | fromDouble (double d) throw (RationalFromDoubleException) |
A multi-precision rational constant.
This stores the rational as a pair of multi-precision integers, one for the numerator and one for the denominator. The number is always stored so that the gcd of the numerator and denominator is 1. (This is referred to as referred to as canonical form in GMP's literature.) A consequence is that that the numerator and denominator may be different than the values used to construct the Rational.
NOTE: The correct way to create a Rational from an int is to use one of the int numerator/int denominator constructors with the denominator 1. Trying to construct a Rational with a single int, e.g., Rational(0), will put you in danger of invoking the char* constructor, from whence you will segfault.
Definition at line 61 of file rational_cln_imp.h.
|
inline |
Constructs a rational with the value 0/1.
Definition at line 89 of file rational_cln_imp.h.
|
inlineexplicit |
Constructs a Rational from a C string in a given base (defaults to 10).
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 98 of file rational_cln_imp.h.
|
inline |
Definition at line 112 of file rational_cln_imp.h.
|
inline |
Creates a Rational from another Rational, q, by performing a deep copy.
Definition at line 130 of file rational_cln_imp.h.
|
inline |
Constructs a canonical Rational from a numerator.
Definition at line 135 of file rational_cln_imp.h.
|
inline |
Definition at line 136 of file rational_cln_imp.h.
|
inline |
Definition at line 137 of file rational_cln_imp.h.
|
inline |
Definition at line 138 of file rational_cln_imp.h.
|
inline |
Constructs a canonical Rational from a numerator and denominator.
Definition at line 148 of file rational_cln_imp.h.
|
inline |
Definition at line 151 of file rational_cln_imp.h.
|
inline |
Definition at line 154 of file rational_cln_imp.h.
|
inline |
Definition at line 157 of file rational_cln_imp.h.
Definition at line 170 of file rational_cln_imp.h.
|
inline |
Definition at line 175 of file rational_cln_imp.h.
|
inline |
Definition at line 177 of file rational_cln_imp.h.
|
inline |
Constructs a rational with the value 0/1.
Definition at line 78 of file rational_gmp_imp.h.
|
inlineexplicit |
Constructs a Rational from a C string in a given base (defaults to 10).
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 88 of file rational_gmp_imp.h.
|
inline |
Definition at line 91 of file rational_gmp_imp.h.
|
inline |
Creates a Rational from another Rational, q, by performing a deep copy.
Definition at line 98 of file rational_gmp_imp.h.
|
inline |
Constructs a canonical Rational from a numerator.
Definition at line 105 of file rational_gmp_imp.h.
|
inline |
Definition at line 108 of file rational_gmp_imp.h.
|
inline |
Definition at line 111 of file rational_gmp_imp.h.
|
inline |
Definition at line 114 of file rational_gmp_imp.h.
|
inline |
Constructs a canonical Rational from a numerator and denominator.
Definition at line 130 of file rational_gmp_imp.h.
|
inline |
Definition at line 133 of file rational_gmp_imp.h.
|
inline |
Definition at line 136 of file rational_gmp_imp.h.
|
inline |
Definition at line 139 of file rational_gmp_imp.h.
Definition at line 152 of file rational_gmp_imp.h.
|
inline |
Definition at line 157 of file rational_gmp_imp.h.
|
inline |
Definition at line 162 of file rational_gmp_imp.h.
|
inline |
Definition at line 217 of file rational_gmp_imp.h.
|
inline |
Definition at line 242 of file rational_cln_imp.h.
int CVC4::Rational::absCmp | ( | const Rational & | q | ) | const |
Equivalent to calling (this->abs()).cmp(b.abs())
int CVC4::Rational::absCmp | ( | const Rational & | q | ) | const |
Equivalent to calling (this->abs()).cmp(b.abs())
|
inline |
Definition at line 231 of file rational_gmp_imp.h.
|
inline |
Definition at line 258 of file rational_cln_imp.h.
|
inline |
Definition at line 195 of file rational_gmp_imp.h.
|
inline |
Definition at line 212 of file rational_cln_imp.h.
References CVC3::compare().
|
inline |
Definition at line 328 of file rational_gmp_imp.h.
|
inline |
Definition at line 352 of file rational_cln_imp.h.
|
inline |
Definition at line 225 of file rational_gmp_imp.h.
|
inline |
Definition at line 254 of file rational_cln_imp.h.
|
inline |
Definition at line 237 of file rational_gmp_imp.h.
|
inline |
Definition at line 262 of file rational_cln_imp.h.
|
static |
Creates a rational from a decimal string (e.g., "1.5"
).
dec | a string encoding a decimal number in the format [0-9]*.[0-9]* |
|
static |
Creates a rational from a decimal string (e.g., "1.5"
).
dec | a string encoding a decimal number in the format [0-9]*.[0-9]* |
|
static |
|
static |
Return an exact rational for a double d.
|
inline |
Returns the value of denominator of the Rational.
Note that this makes a deep copy of the denominator.
Definition at line 176 of file rational_gmp_imp.h.
|
inline |
Returns the value of denominator of the Rational.
Note that this makes a deep copy of the denominator.
Definition at line 192 of file rational_cln_imp.h.
|
inline |
Get a double representation of this Rational, which is approximate: truncation may occur, overflow may result in infinity, and underflow may result in zero.
Definition at line 187 of file rational_gmp_imp.h.
|
inline |
Get a double representation of this Rational, which is approximate: truncation may occur, overflow may result in infinity, and underflow may result in zero.
Definition at line 204 of file rational_cln_imp.h.
|
inline |
Returns the value of numerator of the Rational.
Note that this makes a deep copy of the numerator.
Definition at line 168 of file rational_gmp_imp.h.
|
inline |
Returns the value of numerator of the Rational.
Note that this makes a deep copy of the numerator.
Definition at line 184 of file rational_cln_imp.h.
|
inline |
Computes the hash of the rational from hashes of the numerator and the denominator.
Definition at line 321 of file rational_gmp_imp.h.
References CVC4::gmpz_hash().
|
inline |
Computes the hash of the rational from hashes of the numerator and the denominator.
Definition at line 348 of file rational_cln_imp.h.
Referenced by CVC4::RationalHashFunction::operator()().
|
inline |
Definition at line 191 of file rational_gmp_imp.h.
|
inline |
Definition at line 208 of file rational_cln_imp.h.
|
inline |
Definition at line 250 of file rational_cln_imp.h.
|
inline |
Definition at line 308 of file rational_gmp_imp.h.
|
inline |
Definition at line 213 of file rational_gmp_imp.h.
|
inline |
Definition at line 238 of file rational_cln_imp.h.
|
inline |
Definition at line 209 of file rational_gmp_imp.h.
|
inline |
Definition at line 234 of file rational_cln_imp.h.
|
inline |
Definition at line 205 of file rational_gmp_imp.h.
|
inline |
Definition at line 230 of file rational_cln_imp.h.
|
inline |
Definition at line 255 of file rational_gmp_imp.h.
|
inline |
Definition at line 280 of file rational_cln_imp.h.
Definition at line 282 of file rational_gmp_imp.h.
Definition at line 307 of file rational_cln_imp.h.
Definition at line 298 of file rational_gmp_imp.h.
Definition at line 324 of file rational_cln_imp.h.
Definition at line 275 of file rational_gmp_imp.h.
Definition at line 300 of file rational_cln_imp.h.
Definition at line 289 of file rational_gmp_imp.h.
Definition at line 314 of file rational_cln_imp.h.
|
inline |
Definition at line 247 of file rational_gmp_imp.h.
|
inline |
Definition at line 272 of file rational_cln_imp.h.
Definition at line 278 of file rational_gmp_imp.h.
Definition at line 303 of file rational_cln_imp.h.
Definition at line 293 of file rational_gmp_imp.h.
Definition at line 319 of file rational_cln_imp.h.
Definition at line 285 of file rational_gmp_imp.h.
Definition at line 310 of file rational_cln_imp.h.
Definition at line 303 of file rational_gmp_imp.h.
Definition at line 329 of file rational_cln_imp.h.
|
inline |
Definition at line 259 of file rational_gmp_imp.h.
|
inline |
Definition at line 284 of file rational_cln_imp.h.
|
inline |
Definition at line 263 of file rational_gmp_imp.h.
|
inline |
Definition at line 288 of file rational_cln_imp.h.
Definition at line 241 of file rational_gmp_imp.h.
Definition at line 266 of file rational_cln_imp.h.
|
inline |
Definition at line 251 of file rational_gmp_imp.h.
|
inline |
Definition at line 276 of file rational_cln_imp.h.
|
inline |
Definition at line 267 of file rational_gmp_imp.h.
|
inline |
Definition at line 292 of file rational_cln_imp.h.
|
inline |
Definition at line 271 of file rational_gmp_imp.h.
|
inline |
Definition at line 296 of file rational_cln_imp.h.
|
inline |
Definition at line 201 of file rational_gmp_imp.h.
|
inline |
Definition at line 219 of file rational_cln_imp.h.
|
inline |
Returns a string representing the rational in the given base.
Definition at line 313 of file rational_gmp_imp.h.
|
inline |
Returns a string representing the rational in the given base.
Definition at line 335 of file rational_cln_imp.h.