cvc4-1.4
CVC4::Rational Class Reference

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 floor_frac () const
 
Rationaloperator= (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
 
Rationaloperator+= (const Rational &y)
 
Rationaloperator-= (const Rational &y)
 
Rationaloperator*= (const Rational &y)
 
Rationaloperator/= (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...
 
 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
 
Rationaloperator= (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
 
Rationaloperator+= (const Rational &y)
 
Rationaloperator-= (const Rational &y)
 
Rationaloperator*= (const Rational &y)
 
Rationaloperator/= (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...
 

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)
 
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...
 

Detailed Description

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 51 of file rational_gmp_imp.h.

Constructor & Destructor Documentation

CVC4::Rational::Rational ( )
inline

Constructs a rational with the value 0/1.

Definition at line 78 of file rational_gmp_imp.h.

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

CVC4::Rational::Rational ( const std::string &  s,
unsigned  base = 10 
)
inline

Definition at line 91 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( const Rational q)
inline

Creates a Rational from another Rational, q, by performing a deep copy.

Definition at line 98 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( signed int  n)
inline

Constructs a canonical Rational from a numerator.

Definition at line 105 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( unsigned int  n)
inline

Definition at line 108 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( signed long int  n)
inline

Definition at line 111 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( unsigned long int  n)
inline

Definition at line 114 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( signed int  n,
signed int  d 
)
inline

Constructs a canonical Rational from a numerator and denominator.

Definition at line 130 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( unsigned int  n,
unsigned int  d 
)
inline

Definition at line 133 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( signed long int  n,
signed long int  d 
)
inline

Definition at line 136 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( unsigned long int  n,
unsigned long int  d 
)
inline

Definition at line 139 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( const Integer n,
const Integer d 
)
inline

Definition at line 152 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( const Integer n)
inline

Definition at line 157 of file rational_gmp_imp.h.

CVC4::Rational::~Rational ( )
inline

Definition at line 162 of file rational_gmp_imp.h.

CVC4::Rational::Rational ( )
inline

Constructs a rational with the value 0/1.

Definition at line 89 of file rational_cln_imp.h.

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

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

Definition at line 112 of file rational_cln_imp.h.

CVC4::Rational::Rational ( const Rational q)
inline

Creates a Rational from another Rational, q, by performing a deep copy.

Definition at line 130 of file rational_cln_imp.h.

CVC4::Rational::Rational ( signed int  n)
inline

Constructs a canonical Rational from a numerator.

Definition at line 135 of file rational_cln_imp.h.

CVC4::Rational::Rational ( unsigned int  n)
inline

Definition at line 136 of file rational_cln_imp.h.

CVC4::Rational::Rational ( signed long int  n)
inline

Definition at line 137 of file rational_cln_imp.h.

CVC4::Rational::Rational ( unsigned long int  n)
inline

Definition at line 138 of file rational_cln_imp.h.

CVC4::Rational::Rational ( signed int  n,
signed int  d 
)
inline

Constructs a canonical Rational from a numerator and denominator.

Definition at line 148 of file rational_cln_imp.h.

CVC4::Rational::Rational ( unsigned int  n,
unsigned int  d 
)
inline

Definition at line 151 of file rational_cln_imp.h.

CVC4::Rational::Rational ( signed long int  n,
signed long int  d 
)
inline

Definition at line 154 of file rational_cln_imp.h.

CVC4::Rational::Rational ( unsigned long int  n,
unsigned long int  d 
)
inline

Definition at line 157 of file rational_cln_imp.h.

CVC4::Rational::Rational ( const Integer n,
const Integer d 
)
inline

Definition at line 170 of file rational_cln_imp.h.

CVC4::Rational::Rational ( const Integer n)
inline

Definition at line 175 of file rational_cln_imp.h.

CVC4::Rational::~Rational ( )
inline

Definition at line 177 of file rational_cln_imp.h.

Member Function Documentation

Rational CVC4::Rational::abs ( ) const
inline

Definition at line 217 of file rational_gmp_imp.h.

Rational CVC4::Rational::abs ( ) const
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())

Integer CVC4::Rational::ceiling ( ) const
inline

Definition at line 231 of file rational_gmp_imp.h.

Integer CVC4::Rational::ceiling ( ) const
inline

Definition at line 258 of file rational_cln_imp.h.

int CVC4::Rational::cmp ( const Rational x) const
inline

Definition at line 195 of file rational_gmp_imp.h.

int CVC4::Rational::cmp ( const Rational x) const
inline

Definition at line 212 of file rational_cln_imp.h.

References CVC3::compare().

uint32_t CVC4::Rational::complexity ( ) const
inline

Definition at line 328 of file rational_gmp_imp.h.

uint32_t CVC4::Rational::complexity ( ) const
inline

Definition at line 352 of file rational_cln_imp.h.

Integer CVC4::Rational::floor ( ) const
inline

Definition at line 225 of file rational_gmp_imp.h.

Integer CVC4::Rational::floor ( ) const
inline

Definition at line 254 of file rational_cln_imp.h.

Rational CVC4::Rational::floor_frac ( ) const
inline

Definition at line 237 of file rational_gmp_imp.h.

Rational CVC4::Rational::floor_frac ( ) const
inline

Definition at line 262 of file rational_cln_imp.h.

static Rational CVC4::Rational::fromDecimal ( const std::string &  dec)
static

Creates a rational from a decimal string (e.g., "1.5").

Parameters
deca string encoding a decimal number in the format [0-9]*.[0-9]*
static Rational CVC4::Rational::fromDecimal ( const std::string &  dec)
static

Creates a rational from a decimal string (e.g., "1.5").

Parameters
deca string encoding a decimal number in the format [0-9]*.[0-9]*
static Rational CVC4::Rational::fromDouble ( double  d)
throw (RationalFromDoubleException
)
static
static Rational CVC4::Rational::fromDouble ( double  d)
throw (RationalFromDoubleException
)
static

Return an exact rational for a double d.

Integer CVC4::Rational::getDenominator ( ) const
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.

Integer CVC4::Rational::getDenominator ( ) const
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.

double CVC4::Rational::getDouble ( ) const
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.

double CVC4::Rational::getDouble ( ) const
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.

Integer CVC4::Rational::getNumerator ( ) const
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.

Integer CVC4::Rational::getNumerator ( ) const
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.

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

Referenced by CVC4::RationalHashFunction::operator()().

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

Rational CVC4::Rational::inverse ( ) const
inline

Definition at line 191 of file rational_gmp_imp.h.

Rational CVC4::Rational::inverse ( ) const
inline

Definition at line 208 of file rational_cln_imp.h.

bool CVC4::Rational::isIntegral ( ) const
inline

Definition at line 250 of file rational_cln_imp.h.

bool CVC4::Rational::isIntegral ( ) const
inline

Definition at line 308 of file rational_gmp_imp.h.

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

Definition at line 213 of file rational_gmp_imp.h.

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

Definition at line 238 of file rational_cln_imp.h.

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

Definition at line 209 of file rational_gmp_imp.h.

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

Definition at line 234 of file rational_cln_imp.h.

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

Definition at line 205 of file rational_gmp_imp.h.

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

Definition at line 230 of file rational_cln_imp.h.

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

Definition at line 255 of file rational_gmp_imp.h.

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

Definition at line 280 of file rational_cln_imp.h.

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

Definition at line 282 of file rational_gmp_imp.h.

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

Definition at line 307 of file rational_cln_imp.h.

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

Definition at line 298 of file rational_gmp_imp.h.

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

Definition at line 324 of file rational_cln_imp.h.

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

Definition at line 275 of file rational_gmp_imp.h.

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

Definition at line 300 of file rational_cln_imp.h.

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

Definition at line 289 of file rational_gmp_imp.h.

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

Definition at line 314 of file rational_cln_imp.h.

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

Definition at line 247 of file rational_gmp_imp.h.

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

Definition at line 272 of file rational_cln_imp.h.

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

Definition at line 278 of file rational_gmp_imp.h.

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

Definition at line 303 of file rational_cln_imp.h.

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

Definition at line 293 of file rational_gmp_imp.h.

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

Definition at line 319 of file rational_cln_imp.h.

Rational CVC4::Rational::operator/ ( const Rational y) const
inline

Definition at line 285 of file rational_gmp_imp.h.

Rational CVC4::Rational::operator/ ( const Rational y) const
inline

Definition at line 310 of file rational_cln_imp.h.

Rational& CVC4::Rational::operator/= ( const Rational y)
inline

Definition at line 303 of file rational_gmp_imp.h.

Rational& CVC4::Rational::operator/= ( const Rational y)
inline

Definition at line 329 of file rational_cln_imp.h.

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

Definition at line 259 of file rational_gmp_imp.h.

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

Definition at line 284 of file rational_cln_imp.h.

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

Definition at line 263 of file rational_gmp_imp.h.

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

Definition at line 288 of file rational_cln_imp.h.

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

Definition at line 241 of file rational_gmp_imp.h.

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

Definition at line 266 of file rational_cln_imp.h.

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

Definition at line 251 of file rational_gmp_imp.h.

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

Definition at line 276 of file rational_cln_imp.h.

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

Definition at line 267 of file rational_gmp_imp.h.

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

Definition at line 292 of file rational_cln_imp.h.

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

Definition at line 271 of file rational_gmp_imp.h.

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

Definition at line 296 of file rational_cln_imp.h.

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

Definition at line 201 of file rational_gmp_imp.h.

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

Definition at line 219 of file rational_cln_imp.h.

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

Returns a string representing the rational in the given base.

Definition at line 313 of file rational_gmp_imp.h.

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

Returns a string representing the rational in the given base.

Definition at line 335 of file rational_cln_imp.h.


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