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 
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)
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.
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
size_t gmpz_hash(const mpz_t toHash)
Hashes the gmp integer primitive in a word by word fashion.
Definition: gmp_util.h:28
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
std::ostream & operator<<(std::ostream &out, ModelFormatMode mode)
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