cvc4-1.3
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 
57 private:
62  cln::cl_RA d_value;
63 
70  //Rational(const mpq_class& val) : d_value(val) { }
71  Rational(const cln::cl_RA& val) : d_value(val) { }
72 
73 public:
74 
81  static Rational fromDecimal(const std::string& dec);
82 
84  Rational() : d_value(0){
85  }
86 
93  explicit Rational(const char* s, unsigned base = 10) throw (std::invalid_argument){
94  cln::cl_read_flags flags;
95 
96  flags.syntax = cln::syntax_rational;
97  flags.lsyntax = cln::lsyntax_standard;
98  flags.rational_base = base;
99  try{
100  d_value = read_rational(flags, s, NULL, NULL);
101  }catch(...){
102  std::stringstream ss;
103  ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
104  throw std::invalid_argument(ss.str());
105  }
106  }
107  Rational(const std::string& s, unsigned base = 10) throw (std::invalid_argument){
108  cln::cl_read_flags flags;
109 
110  flags.syntax = cln::syntax_rational;
111  flags.lsyntax = cln::lsyntax_standard;
112  flags.rational_base = base;
113  try{
114  d_value = read_rational(flags, s.c_str(), NULL, NULL);
115  }catch(...){
116  std::stringstream ss;
117  ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
118  throw std::invalid_argument(ss.str());
119  }
120  }
121 
125  Rational(const Rational& q) : d_value(q.d_value) { }
126 
130  Rational(signed int n) : d_value((signed long int)n) { }
131  Rational(unsigned int n) : d_value((unsigned long int)n) { }
132  Rational(signed long int n) : d_value(n) { }
133  Rational(unsigned long int n) : d_value(n) { }
134 
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)) { }
138 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
139 
143  Rational(signed int n, signed int d) : d_value((signed long int)n) {
144  d_value /= cln::cl_I(d);
145  }
146  Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n) {
147  d_value /= cln::cl_I(d);
148  }
149  Rational(signed long int n, signed long int d) : d_value(n) {
150  d_value /= cln::cl_I(d);
151  }
152  Rational(unsigned long int n, unsigned long int d) : d_value(n) {
153  d_value /= cln::cl_I(d);
154  }
155 
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);
159  }
160  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) {
161  d_value /= cln::cl_I(d);
162  }
163 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
164 
165  Rational(const Integer& n, const Integer& d) :
166  d_value(n.get_cl_I())
167  {
168  d_value /= d.get_cl_I();
169  }
170  Rational(const Integer& n) : d_value(n.get_cl_I()){ }
171 
173 
174 
180  return Integer(cln::numerator(d_value));
181  }
182 
188  return Integer(cln::denominator(d_value));
189  }
190 
192  static Rational fromDouble(double d){
193  cln::cl_DF fromD = d;
194  Rational q;
195  q.d_value = cln::rationalize(fromD);
196  return q;
197  }
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  if(this == &x) return *this;
264  d_value = x.d_value;
265  return *this;
266  }
267 
269  return Rational(-(d_value));
270  }
271 
272  bool operator==(const Rational& y) const {
273  return d_value == y.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  Rational operator+(const Rational& y) const{
297  return Rational( d_value + y.d_value );
298  }
299  Rational operator-(const Rational& y) const {
300  return Rational( d_value - y.d_value );
301  }
302 
303  Rational operator*(const Rational& y) const {
304  return Rational( d_value * y.d_value );
305  }
306  Rational operator/(const Rational& y) const {
307  return Rational( d_value / y.d_value );
308  }
309 
311  d_value += y.d_value;
312  return (*this);
313  }
314 
316  d_value -= y.d_value;
317  return (*this);
318  }
319 
321  d_value *= y.d_value;
322  return (*this);
323  }
324 
326  d_value /= y.d_value;
327  return (*this);
328  }
329 
331  std::string toString(int base = 10) const {
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);
337  return ss.str();
338  }
339 
344  size_t hash() const {
345  return equal_hashcode(d_value);
346  }
347 
348  uint32_t complexity() const {
349  return getNumerator().length() + getDenominator().length();
350  }
351 
352 };/* class Rational */
353 
355  inline size_t operator()(const CVC4::Rational& r) const {
356  return r.hash();
357  }
358 };/* struct RationalHashFunction */
359 
360 CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
361 
362 }/* CVC4 namespace */
363 
364 #endif /* __CVC4__RATIONAL_H */
365 
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 & 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.
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 inverse() const
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
Definition: README:39
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
static Rational fromDouble(double d)
Return an exact rational for a double d.
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)
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