cvc4-1.4
rational_gmp_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 
26 #include "util/integer.h"
27 #include "util/exception.h"
28 
29 namespace CVC4 {
30 
32 public:
33  RationalFromDoubleException(double d) throw();
34 };
35 
52 private:
57  mpq_class d_value;
58 
65  Rational(const mpq_class& val) : d_value(val) { }
66 
67 public:
68 
75  static Rational fromDecimal(const std::string& dec);
76 
78  Rational() : d_value(0){
79  d_value.canonicalize();
80  }
81 
88  explicit Rational(const char* s, unsigned base = 10): d_value(s, base) {
89  d_value.canonicalize();
90  }
91  Rational(const std::string& s, unsigned base = 10) : d_value(s, base) {
92  d_value.canonicalize();
93  }
94 
98  Rational(const Rational& q) : d_value(q.d_value) {
99  d_value.canonicalize();
100  }
101 
105  Rational(signed int n) : d_value(n,1) {
106  d_value.canonicalize();
107  }
108  Rational(unsigned int n) : d_value(n,1) {
109  d_value.canonicalize();
110  }
111  Rational(signed long int n) : d_value(n,1) {
112  d_value.canonicalize();
113  }
114  Rational(unsigned long int n) : d_value(n,1) {
115  d_value.canonicalize();
116  }
117 
118 #ifdef CVC4_NEED_INT64_T_OVERLOADS
119  Rational(int64_t n) : d_value(static_cast<long>(n), 1) {
120  d_value.canonicalize();
121  }
122  Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) {
123  d_value.canonicalize();
124  }
125 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
126 
130  Rational(signed int n, signed int d) : d_value(n,d) {
131  d_value.canonicalize();
132  }
133  Rational(unsigned int n, unsigned int d) : d_value(n,d) {
134  d_value.canonicalize();
135  }
136  Rational(signed long int n, signed long int d) : d_value(n,d) {
137  d_value.canonicalize();
138  }
139  Rational(unsigned long int n, unsigned long int d) : d_value(n,d) {
140  d_value.canonicalize();
141  }
142 
143 #ifdef CVC4_NEED_INT64_T_OVERLOADS
144  Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) {
145  d_value.canonicalize();
146  }
147  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) {
148  d_value.canonicalize();
149  }
150 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
151 
152  Rational(const Integer& n, const Integer& d) :
153  d_value(n.get_mpz(), d.get_mpz())
154  {
155  d_value.canonicalize();
156  }
157  Rational(const Integer& n) :
158  d_value(n.get_mpz())
159  {
160  d_value.canonicalize();
161  }
163 
169  return Integer(d_value.get_num());
170  }
171 
177  return Integer(d_value.get_den());
178  }
179 
180  static Rational fromDouble(double d) throw(RationalFromDoubleException);
181 
187  double getDouble() const {
188  return d_value.get_d();
189  }
190 
191  Rational inverse() const {
192  return Rational(getDenominator(), getNumerator());
193  }
194 
195  int cmp(const Rational& x) const {
196  //Don't use mpq_class's cmp() function.
197  //The name ends up conflicting with this function.
198  return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t());
199  }
200 
201  int sgn() const {
202  return mpq_sgn(d_value.get_mpq_t());
203  }
204 
205  bool isZero() const {
206  return sgn() == 0;
207  }
208 
209  bool isOne() const {
210  return mpq_cmp_si(d_value.get_mpq_t(), 1, 1) == 0;
211  }
212 
213  bool isNegativeOne() const {
214  return mpq_cmp_si(d_value.get_mpq_t(), -1, 1) == 0;
215  }
216 
217  Rational abs() const {
218  if(sgn() < 0){
219  return -(*this);
220  }else{
221  return *this;
222  }
223  }
224 
225  Integer floor() const {
226  mpz_class q;
227  mpz_fdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
228  return Integer(q);
229  }
230 
231  Integer ceiling() const {
232  mpz_class q;
233  mpz_cdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
234  return Integer(q);
235  }
236 
238  return (*this) - Rational(floor());
239  }
240 
242  if(this == &x) return *this;
243  d_value = x.d_value;
244  return *this;
245  }
246 
248  return Rational(-(d_value));
249  }
250 
251  bool operator==(const Rational& y) const {
252  return d_value == y.d_value;
253  }
254 
255  bool operator!=(const Rational& y) const {
256  return d_value != y.d_value;
257  }
258 
259  bool operator< (const Rational& y) const {
260  return d_value < y.d_value;
261  }
262 
263  bool operator<=(const Rational& y) const {
264  return d_value <= y.d_value;
265  }
266 
267  bool operator> (const Rational& y) const {
268  return d_value > y.d_value;
269  }
270 
271  bool operator>=(const Rational& y) const {
272  return d_value >= y.d_value;
273  }
274 
275  Rational operator+(const Rational& y) const{
276  return Rational( d_value + y.d_value );
277  }
278  Rational operator-(const Rational& y) const {
279  return Rational( d_value - y.d_value );
280  }
281 
282  Rational operator*(const Rational& y) const {
283  return Rational( d_value * y.d_value );
284  }
285  Rational operator/(const Rational& y) const {
286  return Rational( d_value / y.d_value );
287  }
288 
290  d_value += y.d_value;
291  return (*this);
292  }
294  d_value -= y.d_value;
295  return (*this);
296  }
297 
299  d_value *= y.d_value;
300  return (*this);
301  }
302 
304  d_value /= y.d_value;
305  return (*this);
306  }
307 
308  bool isIntegral() const{
309  return getDenominator() == 1;
310  }
311 
313  std::string toString(int base = 10) const {
314  return d_value.get_str(base);
315  }
316 
321  size_t hash() const {
322  size_t numeratorHash = gmpz_hash(d_value.get_num_mpz_t());
323  size_t denominatorHash = gmpz_hash(d_value.get_den_mpz_t());
324 
325  return numeratorHash xor denominatorHash;
326  }
327 
328  uint32_t complexity() const {
329  uint32_t numLen = getNumerator().length();
330  uint32_t denLen = getDenominator().length();
331  return numLen + denLen;
332  }
333 
335  int absCmp(const Rational& q) const;
336 
337 };/* class Rational */
338 
340  inline size_t operator()(const CVC4::Rational& r) const {
341  return r.hash();
342  }
343 };/* struct RationalHashFunction */
344 
345 CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
346 
347 }/* CVC4 namespace */
348 
349 #endif /* __CVC4__RATIONAL_H */
350 
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)
Definition: kind.h:57
Rational & operator*=(const Rational &y)
Rational(unsigned int n)
Integer floor() const
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
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
size_t gmpz_hash(const mpz_t toHash)
Hashes the gmp integer primitive in a word by word fashion.
Definition: gmp_util.h:28
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.