20 #ifndef __CVC4__RATIONAL_H
21 #define __CVC4__RATIONAL_H
26 #include "util/integer.h"
31 class CVC4_PUBLIC RationalFromDoubleException :
public Exception {
33 RationalFromDoubleException(
double d)
throw();
65 Rational(
const mpq_class& val) : d_value(val) { }
75 static Rational fromDecimal(
const std::string& dec);
79 d_value.canonicalize();
88 explicit Rational(
const char* s,
unsigned base = 10): d_value(s, base) {
89 d_value.canonicalize();
91 Rational(
const std::string& s,
unsigned base = 10) : d_value(s, base) {
92 d_value.canonicalize();
99 d_value.canonicalize();
106 d_value.canonicalize();
109 d_value.canonicalize();
112 d_value.canonicalize();
115 d_value.canonicalize();
118 #ifdef CVC4_NEED_INT64_T_OVERLOADS
119 Rational(int64_t n) : d_value(static_cast<long>(n), 1) {
120 d_value.canonicalize();
122 Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) {
123 d_value.canonicalize();
130 Rational(
signed int n,
signed int d) : d_value(n,d) {
131 d_value.canonicalize();
133 Rational(
unsigned int n,
unsigned int d) : d_value(n,d) {
134 d_value.canonicalize();
136 Rational(
signed long int n,
signed long int d) : d_value(n,d) {
137 d_value.canonicalize();
139 Rational(
unsigned long int n,
unsigned long int d) : d_value(n,d) {
140 d_value.canonicalize();
143 #ifdef CVC4_NEED_INT64_T_OVERLOADS
144 Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) {
145 d_value.canonicalize();
147 Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) {
148 d_value.canonicalize();
153 d_value(n.get_mpz(), d.get_mpz())
155 d_value.canonicalize();
160 d_value.canonicalize();
169 return Integer(d_value.get_num());
177 return Integer(d_value.get_den());
188 return d_value.get_d();
192 return Rational(getDenominator(), getNumerator());
198 return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t());
202 return mpq_sgn(d_value.get_mpq_t());
210 return mpq_cmp_si(d_value.get_mpq_t(), 1, 1) == 0;
214 return mpq_cmp_si(d_value.get_mpq_t(), -1, 1) == 0;
227 mpz_fdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
233 mpz_cdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
242 if(
this == &x)
return *
this;
252 return d_value == y.d_value;
256 return d_value != y.d_value;
260 return d_value < y.d_value;
264 return d_value <= y.d_value;
268 return d_value > y.d_value;
272 return d_value >= y.d_value;
276 return Rational( d_value + y.d_value );
279 return Rational( d_value - y.d_value );
283 return Rational( d_value * y.d_value );
286 return Rational( d_value / y.d_value );
290 d_value += y.d_value;
294 d_value -= y.d_value;
299 d_value *= y.d_value;
304 d_value /= y.d_value;
309 return getDenominator() == 1;
314 return d_value.get_str(base);
322 size_t numeratorHash =
gmpz_hash(d_value.get_num_mpz_t());
323 size_t denominatorHash =
gmpz_hash(d_value.get_den_mpz_t());
325 return numeratorHash xor denominatorHash;
329 uint32_t numLen = getNumerator().length();
330 uint32_t denLen = getDenominator().length();
331 return numLen + denLen;
335 int absCmp(
const Rational& q)
const;
339 struct RationalHashFunction {
Rational(const Integer &n, const Integer &d)
Rational & operator=(const Rational &x)
Rational(signed long int n)
Rational floor_frac() const
Rational & operator*=(const Rational &y)
bool operator!=(const Rational &y) const
Rational & operator+=(const Rational &y)
Rational & operator/=(const Rational &y)
Integer getDenominator() const
Returns the value of denominator of the Rational.
A multi-precision rational constant.
Rational()
Constructs a rational with the value 0/1.
Rational(signed int n, signed int d)
Constructs a canonical Rational from a numerator and denominator.
CVC4's exception base class and some associated utilities.
Rational(unsigned long int n, unsigned long int d)
Rational(signed int n)
Constructs a canonical Rational from a numerator.
Rational operator-() const
bool operator==(const Rational &y) const
Rational(const char *s, unsigned base=10)
Constructs a Rational from a C string in a given base (defaults to 10).
bool isNegativeOne() const
size_t hash() const
Computes the hash of the rational from hashes of the numerator and the denominator.
Rational(const Integer &n)
size_t operator()(const CVC4::Rational &r) const
size_t gmpz_hash(const mpz_t toHash)
Hashes the gmp integer primitive in a word by word fashion.
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
Rational & operator-=(const Rational &y)
Integer getNumerator() const
Returns the value of numerator of the Rational.
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool operator>=(const Rational &y) const
int cmp(const Rational &x) const
Rational(const std::string &s, unsigned base=10)
Rational operator-(const Rational &y) const
Rational(unsigned int n, unsigned int d)
Rational(signed long int n, signed long int d)
bool operator<=(const Rational &y) const
uint32_t complexity() const
Rational(const Rational &q)
Creates a Rational from another Rational, q, by performing a deep copy.
Rational operator+(const Rational &y) const
Rational operator*(const Rational &y) const
double getDouble() const
Get a double representation of this Rational, which is approximate: truncation may occur...
Rational(unsigned long int n)
std::string toString(int base=10) const
Returns a string representing the rational in the given base.
Rational operator/(const Rational &y) const