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" 41 class CVC4_PUBLIC RationalFromDoubleException :
public Exception {
43 RationalFromDoubleException(
double d)
throw();
76 Rational(
const cln::cl_RA& val) : d_value(val) { }
86 static Rational fromDecimal(
const std::string& dec);
98 explicit Rational(
const char* s,
unsigned base = 10) throw (
std::invalid_argument){
99 cln::cl_read_flags flags;
101 flags.syntax = cln::syntax_rational;
102 flags.lsyntax = cln::lsyntax_standard;
103 flags.rational_base = base;
105 d_value = read_rational(flags, s, NULL, NULL);
107 std::stringstream ss;
108 ss <<
"Rational() failed to parse value \"" <<s <<
"\" in base=" <<base;
109 throw std::invalid_argument(ss.str());
112 Rational(
const std::string& s,
unsigned base = 10) throw (
std::invalid_argument){
113 cln::cl_read_flags flags;
115 flags.syntax = cln::syntax_rational;
116 flags.lsyntax = cln::lsyntax_standard;
117 flags.rational_base = base;
119 d_value = read_rational(flags, s.c_str(), NULL, NULL);
121 std::stringstream ss;
122 ss <<
"Rational() failed to parse value \"" <<s <<
"\" in base=" <<base;
123 throw std::invalid_argument(ss.str());
135 Rational(
signed int n) : d_value((signed long int)n) { }
136 Rational(
unsigned int n) : d_value((unsigned long int)n) { }
140 #ifdef CVC4_NEED_INT64_T_OVERLOADS 141 Rational(int64_t n) : d_value(static_cast<long>(n)) { }
142 Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) { }
148 Rational(
signed int n,
signed int d) : d_value((signed long int)n) {
149 d_value /= cln::cl_I(d);
151 Rational(
unsigned int n,
unsigned int d) : d_value((unsigned long int)n) {
152 d_value /= cln::cl_I(d);
154 Rational(
signed long int n,
signed long int d) : d_value(n) {
155 d_value /= cln::cl_I(d);
157 Rational(
unsigned long int n,
unsigned long int d) : d_value(n) {
158 d_value /= cln::cl_I(d);
161 #ifdef CVC4_NEED_INT64_T_OVERLOADS 162 Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) {
163 d_value /= cln::cl_I(d);
165 Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) {
166 d_value /= cln::cl_I(d);
171 d_value(n.get_cl_I())
173 d_value /= d.get_cl_I();
185 return Integer(cln::numerator(d_value));
193 return Integer(cln::denominator(d_value));
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));
267 if(
this == &x)
return *
this;
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 d_value >= y.d_value;
301 return Rational( d_value + y.d_value );
304 return Rational( d_value - y.d_value );
308 return Rational( d_value * y.d_value );
311 return Rational( d_value / y.d_value );
315 d_value += y.d_value;
320 d_value -= y.d_value;
325 d_value *= y.d_value;
330 d_value /= y.d_value;
336 cln::cl_print_flags flags;
337 flags.rational_base = base;
338 flags.rational_readably =
false;
339 std::stringstream ss;
340 print_rational(ss, flags, d_value);
349 return equal_hashcode(d_value);
353 return getNumerator().length() + getDenominator().length();
357 int absCmp(
const Rational& q)
const;
Rational(const Integer &n, const Integer &d)
bool operator!=(const Rational &y) const
Rational & operator=(const Rational &x)
Rational(signed long int n)
Rational & operator*=(const Rational &y)
int compare(const Expr &e1, const Expr &e2)
Rational operator-() const
Rational & operator+=(const Rational &y)
Rational & operator/=(const Rational &y)
Integer getNumerator() const
Returns the value of numerator of the Rational.
A multi-precision rational constant.
std::ostream & operator<<(std::ostream &, const Command &)
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 floor_frac() const
Rational(unsigned long int n, unsigned long int d)
bool operator<=(const Rational &y) const
Rational(signed int n)
Constructs a canonical Rational from a numerator.
bool isNegativeOne() const
Rational(const char *s, unsigned base=10)
Constructs a Rational from a C string in a given base (defaults to 10).
Rational operator*(const Rational &y) const
size_t operator()(const CVC4::Rational &r) const
Rational operator/(const Rational &y) const
Rational(const Integer &n)
Rational operator-(const Rational &y) const
Rational & operator-=(const Rational &y)
Macros that should be defined everywhere during the building of the libraries and driver binary...
size_t hash() const
Computes the hash of the rational from hashes of the numerator and the denominator.
Rational operator+(const Rational &y) const
Rational(const std::string &s, unsigned base=10)
double getDouble() const
Get a double representation of this Rational, which is approximate: truncation may occur...
uint32_t complexity() const
Rational(unsigned int n, unsigned int d)
bool operator>=(const Rational &y) const
Rational(signed long int n, signed long int d)
Rational(const Rational &q)
Creates a Rational from another Rational, q, by performing a deep copy.
bool operator==(const Rational &y) const
Rational(unsigned long int n)
Integer getDenominator() const
Returns the value of denominator of the Rational.
int cmp(const Rational &x) const
std::string toString(int base=10) const
Returns a string representing the rational in the given base.