cvc4-1.3
|
A multi-precision rational constant. More...
#include <rational_gmp_imp.h>
Public Member Functions | |
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 & | 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 |
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 & | 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 |
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) |
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) |
Return an exact rational for a double d. More... | |
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 46 of file rational_gmp_imp.h.
|
inline |
Constructs a rational with the value 0/1.
Definition at line 73 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 83 of file rational_gmp_imp.h.
|
inline |
Definition at line 86 of file rational_gmp_imp.h.
|
inline |
Creates a Rational from another Rational, q, by performing a deep copy.
Definition at line 93 of file rational_gmp_imp.h.
|
inline |
Constructs a canonical Rational from a numerator.
Definition at line 100 of file rational_gmp_imp.h.
|
inline |
Definition at line 103 of file rational_gmp_imp.h.
|
inline |
Definition at line 106 of file rational_gmp_imp.h.
|
inline |
Definition at line 109 of file rational_gmp_imp.h.
|
inline |
Constructs a canonical Rational from a numerator and denominator.
Definition at line 125 of file rational_gmp_imp.h.
|
inline |
Definition at line 128 of file rational_gmp_imp.h.
|
inline |
Definition at line 131 of file rational_gmp_imp.h.
|
inline |
Definition at line 134 of file rational_gmp_imp.h.
Definition at line 147 of file rational_gmp_imp.h.
|
inline |
Definition at line 152 of file rational_gmp_imp.h.
|
inline |
Definition at line 157 of file rational_gmp_imp.h.
|
inline |
Constructs a rational with the value 0/1.
Definition at line 84 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 93 of file rational_cln_imp.h.
|
inline |
Definition at line 107 of file rational_cln_imp.h.
|
inline |
Creates a Rational from another Rational, q, by performing a deep copy.
Definition at line 125 of file rational_cln_imp.h.
|
inline |
Constructs a canonical Rational from a numerator.
Definition at line 130 of file rational_cln_imp.h.
|
inline |
Definition at line 131 of file rational_cln_imp.h.
|
inline |
Definition at line 132 of file rational_cln_imp.h.
|
inline |
Definition at line 133 of file rational_cln_imp.h.
|
inline |
Constructs a canonical Rational from a numerator and denominator.
Definition at line 143 of file rational_cln_imp.h.
|
inline |
Definition at line 146 of file rational_cln_imp.h.
|
inline |
Definition at line 149 of file rational_cln_imp.h.
|
inline |
Definition at line 152 of file rational_cln_imp.h.
Definition at line 165 of file rational_cln_imp.h.
|
inline |
Definition at line 170 of file rational_cln_imp.h.
|
inline |
Definition at line 172 of file rational_cln_imp.h.
|
inline |
Definition at line 217 of file rational_gmp_imp.h.
|
inline |
Definition at line 242 of file rational_cln_imp.h.
|
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 324 of file rational_gmp_imp.h.
|
inline |
Definition at line 348 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.
|
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]* |
|
inlinestatic |
Return an exact rational for a double d.
Definition at line 176 of file rational_gmp_imp.h.
|
inlinestatic |
Return an exact rational for a double d.
Definition at line 192 of file rational_cln_imp.h.
|
inline |
Returns the value of denominator of the Rational.
Note that this makes a deep copy of the denominator.
Definition at line 171 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 187 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.
Referenced by CVC4::SExpr::getValue().
|
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 163 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 179 of file rational_cln_imp.h.
|
inline |
Computes the hash of the rational from hashes of the numerator and the denominator.
Definition at line 317 of file rational_gmp_imp.h.
References CVC4::gmpz_hash().
Referenced by CVC4::RationalHashFunction::operator()().
|
inline |
Computes the hash of the rational from hashes of the numerator and the denominator.
Definition at line 344 of file rational_cln_imp.h.
|
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 304 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 251 of file rational_gmp_imp.h.
|
inline |
Definition at line 276 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 294 of file rational_gmp_imp.h.
Definition at line 320 of file rational_cln_imp.h.
Definition at line 271 of file rational_gmp_imp.h.
Definition at line 296 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.
|
inline |
Definition at line 243 of file rational_gmp_imp.h.
|
inline |
Definition at line 268 of file rational_cln_imp.h.
Definition at line 274 of file rational_gmp_imp.h.
Definition at line 299 of file rational_cln_imp.h.
Definition at line 289 of file rational_gmp_imp.h.
Definition at line 315 of file rational_cln_imp.h.
Definition at line 281 of file rational_gmp_imp.h.
Definition at line 306 of file rational_cln_imp.h.
Definition at line 299 of file rational_gmp_imp.h.
Definition at line 325 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.
|
inline |
Definition at line 259 of file rational_gmp_imp.h.
|
inline |
Definition at line 284 of file rational_cln_imp.h.
Definition at line 237 of file rational_gmp_imp.h.
Definition at line 262 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.
|
inline |
Definition at line 263 of file rational_gmp_imp.h.
|
inline |
Definition at line 288 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 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 309 of file rational_gmp_imp.h.
|
inline |
Returns a string representing the rational in the given base.
Definition at line 331 of file rational_cln_imp.h.