cvc4-1.3
CVC4::Rational Class Reference

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

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

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 56 of file rational_cln_imp.h.

Constructor & Destructor Documentation

CVC4::Rational::Rational ( )
inline

Constructs a rational with the value 0/1.

Definition at line 84 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 93 of file rational_cln_imp.h.

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

Definition at line 107 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 125 of file rational_cln_imp.h.

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

Constructs a canonical Rational from a numerator.

Definition at line 130 of file rational_cln_imp.h.

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

Definition at line 131 of file rational_cln_imp.h.

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

Definition at line 132 of file rational_cln_imp.h.

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

Definition at line 133 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 143 of file rational_cln_imp.h.

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

Definition at line 146 of file rational_cln_imp.h.

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

Definition at line 149 of file rational_cln_imp.h.

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

Definition at line 152 of file rational_cln_imp.h.

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

Definition at line 165 of file rational_cln_imp.h.

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

Definition at line 170 of file rational_cln_imp.h.

CVC4::Rational::~Rational ( )
inline

Definition at line 172 of file rational_cln_imp.h.

CVC4::Rational::Rational ( )
inline

Constructs a rational with the value 0/1.

Definition at line 73 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 83 of file rational_gmp_imp.h.

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

Definition at line 86 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 93 of file rational_gmp_imp.h.

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

Constructs a canonical Rational from a numerator.

Definition at line 100 of file rational_gmp_imp.h.

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

Definition at line 103 of file rational_gmp_imp.h.

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

Definition at line 106 of file rational_gmp_imp.h.

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

Definition at line 109 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 125 of file rational_gmp_imp.h.

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

Definition at line 128 of file rational_gmp_imp.h.

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

Definition at line 131 of file rational_gmp_imp.h.

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

Definition at line 134 of file rational_gmp_imp.h.

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

Definition at line 147 of file rational_gmp_imp.h.

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

Definition at line 152 of file rational_gmp_imp.h.

CVC4::Rational::~Rational ( )
inline

Definition at line 157 of file rational_gmp_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.

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

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

Definition at line 348 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.

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

Return an exact rational for a double d.

Definition at line 176 of file rational_gmp_imp.h.

static Rational CVC4::Rational::fromDouble ( double  d)
inlinestatic

Return an exact rational for a double d.

Definition at line 192 of file rational_cln_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 171 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 187 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.

Referenced by CVC4::SExpr::getValue().

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 163 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 179 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 317 of file rational_gmp_imp.h.

References CVC4::gmpz_hash().

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

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

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

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

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

Definition at line 320 of file rational_cln_imp.h.

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

Definition at line 271 of file rational_gmp_imp.h.

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

Definition at line 296 of file rational_cln_imp.h.

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

Definition at line 285 of file rational_gmp_imp.h.

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

Definition at line 310 of file rational_cln_imp.h.

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

Definition at line 243 of file rational_gmp_imp.h.

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

Definition at line 268 of file rational_cln_imp.h.

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

Definition at line 274 of file rational_gmp_imp.h.

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

Definition at line 299 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 315 of file rational_cln_imp.h.

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

Definition at line 281 of file rational_gmp_imp.h.

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

Definition at line 306 of file rational_cln_imp.h.

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

Definition at line 299 of file rational_gmp_imp.h.

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

Definition at line 325 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.

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.

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

Definition at line 237 of file rational_gmp_imp.h.

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

Definition at line 262 of file rational_cln_imp.h.

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

Definition at line 247 of file rational_gmp_imp.h.

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

Definition at line 272 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.

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.

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 309 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 331 of file rational_cln_imp.h.


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