cvc4-1.4
rational_cln_imp.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__RATIONAL_H
21 #define __CVC4__RATIONAL_H
22 
23 #include <gmp.h>
24 #include <string>
25 #include <sstream>
26 #include <cassert>
27 #include <cln/rational.h>
28 #include <cln/input.h>
29 #include <cln/io.h>
30 #include <cln/output.h>
31 #include <cln/rational_io.h>
32 #include <cln/number_io.h>
33 #include <cln/dfloat.h>
34 #include <cln/real.h>
35 
36 #include "util/exception.h"
37 #include "util/integer.h"
38 
39 namespace CVC4 {
40 
42 public:
43  RationalFromDoubleException(double d) throw();
44 };
45 
62 private:
67  cln::cl_RA d_value;
68 
75  //Rational(const mpq_class& val) : d_value(val) { }
76  Rational(const cln::cl_RA& val) : d_value(val) { }
77 
78 public:
79 
86  static Rational fromDecimal(const std::string& dec);
87 
89  Rational() : d_value(0){
90  }
91 
98  explicit Rational(const char* s, unsigned base = 10) throw (std::invalid_argument){
99  cln::cl_read_flags flags;
100 
101  flags.syntax = cln::syntax_rational;
102  flags.lsyntax = cln::lsyntax_standard;
103  flags.rational_base = base;
104  try{
105  d_value = read_rational(flags, s, NULL, NULL);
106  }catch(...){
107  std::stringstream ss;
108  ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
109  throw std::invalid_argument(ss.str());
110  }
111  }
112  Rational(const std::string& s, unsigned base = 10) throw (std::invalid_argument){
113  cln::cl_read_flags flags;
114 
115  flags.syntax = cln::syntax_rational;
116  flags.lsyntax = cln::lsyntax_standard;
117  flags.rational_base = base;
118  try{
119  d_value = read_rational(flags, s.c_str(), NULL, NULL);
120  }catch(...){
121  std::stringstream ss;
122  ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
123  throw std::invalid_argument(ss.str());
124  }
125  }
126 
130  Rational(const Rational& q) : d_value(q.d_value) { }
131 
135  Rational(signed int n) : d_value((signed long int)n) { }
136  Rational(unsigned int n) : d_value((unsigned long int)n) { }
137  Rational(signed long int n) : d_value(n) { }
138  Rational(unsigned long int n) : d_value(n) { }
139 
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)) { }
143 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
144 
148  Rational(signed int n, signed int d) : d_value((signed long int)n) {
149  d_value /= cln::cl_I(d);
150  }
151  Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n) {
152  d_value /= cln::cl_I(d);
153  }
154  Rational(signed long int n, signed long int d) : d_value(n) {
155  d_value /= cln::cl_I(d);
156  }
157  Rational(unsigned long int n, unsigned long int d) : d_value(n) {
158  d_value /= cln::cl_I(d);
159  }
160 
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);
164  }
165  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) {
166  d_value /= cln::cl_I(d);
167  }
168 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
169 
170  Rational(const Integer& n, const Integer& d) :
171  d_value(n.get_cl_I())
172  {
173  d_value /= d.get_cl_I();
174  }
175  Rational(const Integer& n) : d_value(n.get_cl_I()){ }
176 
178 
179 
185  return Integer(cln::numerator(d_value));
186  }
187 
193  return Integer(cln::denominator(d_value));
194  }
195 
197  static Rational fromDouble(double d) throw(RationalFromDoubleException);
198 
204  double getDouble() const {
205  return cln::double_approx(d_value);
206  }
207 
208  Rational inverse() const {
209  return Rational(cln::recip(d_value));
210  }
211 
212  int cmp(const Rational& x) const {
213  //Don't use mpq_class's cmp() function.
214  //The name ends up conflicting with this function.
215  return cln::compare(d_value, x.d_value);
216  }
217 
218 
219  int sgn() const {
220  if(cln::zerop(d_value)){
221  return 0;
222  }else if(cln::minusp(d_value)){
223  return -1;
224  }else{
225  assert(cln::plusp(d_value));
226  return 1;
227  }
228  }
229 
230  bool isZero() const {
231  return cln::zerop(d_value);
232  }
233 
234  bool isOne() const {
235  return d_value == 1;
236  }
237 
238  bool isNegativeOne() const {
239  return d_value == -1;
240  }
241 
242  Rational abs() const {
243  if(sgn() < 0){
244  return -(*this);
245  }else{
246  return *this;
247  }
248  }
249 
250  bool isIntegral() const{
251  return getDenominator() == 1;
252  }
253 
254  Integer floor() const {
255  return Integer(cln::floor1(d_value));
256  }
257 
258  Integer ceiling() const {
259  return Integer(cln::ceiling1(d_value));
260  }
261 
263  return (*this) - Rational(floor());
264  }
265 
267  if(this == &x) return *this;
268  d_value = x.d_value;
269  return *this;
270  }
271 
273  return Rational(-(d_value));
274  }
275 
276  bool operator==(const Rational& y) const {
277  return d_value == y.d_value;
278  }
279 
280  bool operator!=(const Rational& y) const {
281  return d_value != y.d_value;
282  }
283 
284  bool operator< (const Rational& y) const {
285  return d_value < y.d_value;
286  }
287 
288  bool operator<=(const Rational& y) const {
289  return d_value <= y.d_value;
290  }
291 
292  bool operator> (const Rational& y) const {
293  return d_value > y.d_value;
294  }
295 
296  bool operator>=(const Rational& y) const {
297  return d_value >= y.d_value;
298  }
299 
300  Rational operator+(const Rational& y) const{
301  return Rational( d_value + y.d_value );
302  }
303  Rational operator-(const Rational& y) const {
304  return Rational( d_value - y.d_value );
305  }
306 
307  Rational operator*(const Rational& y) const {
308  return Rational( d_value * y.d_value );
309  }
310  Rational operator/(const Rational& y) const {
311  return Rational( d_value / y.d_value );
312  }
313 
315  d_value += y.d_value;
316  return (*this);
317  }
318 
320  d_value -= y.d_value;
321  return (*this);
322  }
323 
325  d_value *= y.d_value;
326  return (*this);
327  }
328 
330  d_value /= y.d_value;
331  return (*this);
332  }
333 
335  std::string toString(int base = 10) const {
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);
341  return ss.str();
342  }
343 
348  size_t hash() const {
349  return equal_hashcode(d_value);
350  }
351 
352  uint32_t complexity() const {
353  return getNumerator().length() + getDenominator().length();
354  }
355 
357  int absCmp(const Rational& q) const;
358 
359 };/* class Rational */
360 
362  inline size_t operator()(const CVC4::Rational& r) const {
363  return r.hash();
364  }
365 };/* struct RationalHashFunction */
366 
367 CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
368 
369 }/* CVC4 namespace */
370 
371 #endif /* __CVC4__RATIONAL_H */
372 
bool isIntegral() const
Rational(const Integer &n, const Integer &d)
int sgn() const
Rational & operator=(const Rational &x)
Integer ceiling() const
Rational(signed long int n)
Rational floor_frac() const
Rational & operator*=(const Rational &y)
Rational(unsigned int n)
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.
STL namespace.
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 inverse() const
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.
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Rational(const Integer &n)
size_t operator()(const CVC4::Rational &r) const
Rational abs() const
Rational & operator-=(const Rational &y)
bool isZero() const
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)
std::ostream & operator<<(std::ostream &out, const SubrangeBound &bound)
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)
Integer floor() const
std::string toString(int base=10) const
Returns a string representing the rational in the given base.
bool isOne() const
Rational operator/(const Rational &y) const