20 #ifndef __CVC4__RATIONAL_H
21 #define __CVC4__RATIONAL_H
27 #include <cln/rational.h>
28 #include <cln/input.h>
30 #include <cln/output.h>
31 #include <cln/rational_io.h>
32 #include <cln/number_io.h>
33 #include <cln/dfloat.h>
37 #include "util/integer.h"
71 Rational(
const cln::cl_RA& val) : d_value(val) { }
81 static Rational fromDecimal(
const std::string& dec);
93 explicit Rational(
const char* s,
unsigned base = 10) throw (std::invalid_argument){
94 cln::cl_read_flags flags;
96 flags.syntax = cln::syntax_rational;
97 flags.lsyntax = cln::lsyntax_standard;
98 flags.rational_base = base;
100 d_value = read_rational(flags, s, NULL, NULL);
102 std::stringstream ss;
103 ss <<
"Rational() failed to parse value \"" <<s <<
"\" in base=" <<base;
104 throw std::invalid_argument(ss.str());
107 Rational(
const std::string& s,
unsigned base = 10) throw (std::invalid_argument){
108 cln::cl_read_flags flags;
110 flags.syntax = cln::syntax_rational;
111 flags.lsyntax = cln::lsyntax_standard;
112 flags.rational_base = base;
114 d_value = read_rational(flags, s.c_str(), NULL, NULL);
116 std::stringstream ss;
117 ss <<
"Rational() failed to parse value \"" <<s <<
"\" in base=" <<base;
118 throw std::invalid_argument(ss.str());
130 Rational(
signed int n) : d_value((signed long int)n) { }
131 Rational(
unsigned int n) : d_value((unsigned long int)n) { }
135 #ifdef CVC4_NEED_INT64_T_OVERLOADS
136 Rational(int64_t n) : d_value(static_cast<long>(n)) { }
137 Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) { }
143 Rational(
signed int n,
signed int d) : d_value((signed long int)n) {
144 d_value /= cln::cl_I(d);
146 Rational(
unsigned int n,
unsigned int d) : d_value((unsigned long int)n) {
147 d_value /= cln::cl_I(d);
149 Rational(
signed long int n,
signed long int d) : d_value(n) {
150 d_value /= cln::cl_I(d);
152 Rational(
unsigned long int n,
unsigned long int d) : d_value(n) {
153 d_value /= cln::cl_I(d);
156 #ifdef CVC4_NEED_INT64_T_OVERLOADS
157 Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) {
158 d_value /= cln::cl_I(d);
160 Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) {
161 d_value /= cln::cl_I(d);
166 d_value(n.get_cl_I())
168 d_value /= d.get_cl_I();
180 return Integer(cln::numerator(d_value));
188 return Integer(cln::denominator(d_value));
193 cln::cl_DF fromD = d;
195 q.d_value = cln::rationalize(fromD);
205 return cln::double_approx(d_value);
209 return Rational(cln::recip(d_value));
220 if(cln::zerop(d_value)){
222 }
else if(cln::minusp(d_value)){
225 assert(cln::plusp(d_value));
231 return cln::zerop(d_value);
239 return d_value == -1;
251 return getDenominator() == 1;
255 return Integer(cln::floor1(d_value));
259 return Integer(cln::ceiling1(d_value));
263 if(
this == &x)
return *
this;
273 return d_value == y.d_value;
277 return d_value != y.d_value;
281 return d_value < y.d_value;
285 return d_value <= y.d_value;
289 return d_value > y.d_value;
293 return d_value >= y.d_value;
297 return Rational( d_value + y.d_value );
300 return Rational( d_value - y.d_value );
304 return Rational( d_value * y.d_value );
307 return Rational( d_value / y.d_value );
311 d_value += y.d_value;
316 d_value -= y.d_value;
321 d_value *= y.d_value;
326 d_value /= y.d_value;
332 cln::cl_print_flags flags;
333 flags.rational_base = base;
334 flags.rational_readably =
false;
335 std::stringstream ss;
336 print_rational(ss, flags, d_value);
345 return equal_hashcode(d_value);
349 return getNumerator().length() + getDenominator().length();
Rational(const Integer &n, const Integer &d)
Rational & operator=(const Rational &x)
Rational(signed long int n)
Rational & operator*=(const Rational &y)
int compare(const Expr &e1, const Expr &e2)
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
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
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