20 #ifndef __CVC4__RATIONAL_H
21 #define __CVC4__RATIONAL_H
26 #include "util/integer.h"
60 Rational(
const mpq_class& val) : d_value(val) { }
70 static Rational fromDecimal(
const std::string& dec);
74 d_value.canonicalize();
83 explicit Rational(
const char* s,
unsigned base = 10): d_value(s, base) {
84 d_value.canonicalize();
86 Rational(
const std::string& s,
unsigned base = 10) : d_value(s, base) {
87 d_value.canonicalize();
94 d_value.canonicalize();
101 d_value.canonicalize();
104 d_value.canonicalize();
107 d_value.canonicalize();
110 d_value.canonicalize();
113 #ifdef CVC4_NEED_INT64_T_OVERLOADS
114 Rational(int64_t n) : d_value(static_cast<long>(n), 1) {
115 d_value.canonicalize();
117 Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) {
118 d_value.canonicalize();
125 Rational(
signed int n,
signed int d) : d_value(n,d) {
126 d_value.canonicalize();
128 Rational(
unsigned int n,
unsigned int d) : d_value(n,d) {
129 d_value.canonicalize();
131 Rational(
signed long int n,
signed long int d) : d_value(n,d) {
132 d_value.canonicalize();
134 Rational(
unsigned long int n,
unsigned long int d) : d_value(n,d) {
135 d_value.canonicalize();
138 #ifdef CVC4_NEED_INT64_T_OVERLOADS
139 Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) {
140 d_value.canonicalize();
142 Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) {
143 d_value.canonicalize();
148 d_value(n.get_mpz(), d.get_mpz())
150 d_value.canonicalize();
155 d_value.canonicalize();
164 return Integer(d_value.get_num());
172 return Integer(d_value.get_den());
178 mpq_set_d(q.d_value.get_mpq_t(), d);
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());
238 if(
this == &x)
return *
this;
248 return d_value == y.d_value;
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 Rational( d_value + y.d_value );
275 return Rational( d_value - y.d_value );
279 return Rational( d_value * y.d_value );
282 return Rational( d_value / y.d_value );
286 d_value += y.d_value;
290 d_value -= y.d_value;
295 d_value *= y.d_value;
300 d_value /= y.d_value;
305 return getDenominator() == 1;
310 return d_value.get_str(base);
318 size_t numeratorHash =
gmpz_hash(d_value.get_num_mpz_t());
319 size_t denominatorHash =
gmpz_hash(d_value.get_den_mpz_t());
321 return numeratorHash xor denominatorHash;
325 uint32_t numLen = getNumerator().length();
326 uint32_t denLen = getDenominator().length();
327 return numLen + denLen;
Rational(const Integer &n, const Integer &d)
Rational & operator=(const Rational &x)
Rational(signed long int n)
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.
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
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)
static Rational fromDouble(double d)
Return an exact rational for a double d.
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