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 
Rational(const Integer &n, const Integer &d)
bool isZero() const
bool operator!=(const Rational &y) const
Rational & operator=(const Rational &x)
Rational(signed long int n)
Rational & operator*=(const Rational &y)
Rational(unsigned int n)
Integer floor() const
int compare(const Expr &e1, const Expr &e2)
bool isIntegral() const
Rational operator-() const
Rational & operator+=(const Rational &y)
Rational & operator/=(const Rational &y)
Integer getNumerator() const
Returns the value of numerator of the Rational.
Integer ceiling() const
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&#39;s exception base class and some associated utilities.
Rational abs() const
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
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Rational(const Integer &n)
Rational operator-(const Rational &y) const
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:568
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
bool isOne() const
Rational inverse() 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.