cvc4-1.3
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 
46 class CVC4_PUBLIC Rational {
47 private:
52  mpq_class d_value;
53 
60  Rational(const mpq_class& val) : d_value(val) { }
61 
62 public:
63 
70  static Rational fromDecimal(const std::string& dec);
71 
73  Rational() : d_value(0){
74  d_value.canonicalize();
75  }
76 
83  explicit Rational(const char* s, unsigned base = 10): d_value(s, base) {
84  d_value.canonicalize();
85  }
86  Rational(const std::string& s, unsigned base = 10) : d_value(s, base) {
87  d_value.canonicalize();
88  }
89 
93  Rational(const Rational& q) : d_value(q.d_value) {
94  d_value.canonicalize();
95  }
96 
100  Rational(signed int n) : d_value(n,1) {
101  d_value.canonicalize();
102  }
103  Rational(unsigned int n) : d_value(n,1) {
104  d_value.canonicalize();
105  }
106  Rational(signed long int n) : d_value(n,1) {
107  d_value.canonicalize();
108  }
109  Rational(unsigned long int n) : d_value(n,1) {
110  d_value.canonicalize();
111  }
112 
113 #ifdef CVC4_NEED_INT64_T_OVERLOADS
114  Rational(int64_t n) : d_value(static_cast<long>(n), 1) {
115  d_value.canonicalize();
116  }
117  Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) {
118  d_value.canonicalize();
119  }
120 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
121 
125  Rational(signed int n, signed int d) : d_value(n,d) {
126  d_value.canonicalize();
127  }
128  Rational(unsigned int n, unsigned int d) : d_value(n,d) {
129  d_value.canonicalize();
130  }
131  Rational(signed long int n, signed long int d) : d_value(n,d) {
132  d_value.canonicalize();
133  }
134  Rational(unsigned long int n, unsigned long int d) : d_value(n,d) {
135  d_value.canonicalize();
136  }
137 
138 #ifdef CVC4_NEED_INT64_T_OVERLOADS
139  Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) {
140  d_value.canonicalize();
141  }
142  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) {
143  d_value.canonicalize();
144  }
145 #endif /* CVC4_NEED_INT64_T_OVERLOADS */
146 
147  Rational(const Integer& n, const Integer& d) :
148  d_value(n.get_mpz(), d.get_mpz())
149  {
150  d_value.canonicalize();
151  }
152  Rational(const Integer& n) :
153  d_value(n.get_mpz())
154  {
155  d_value.canonicalize();
156  }
158 
164  return Integer(d_value.get_num());
165  }
166 
172  return Integer(d_value.get_den());
173  }
174 
176  static Rational fromDouble(double d){
177  Rational q;
178  mpq_set_d(q.d_value.get_mpq_t(), d);
179  return q;
180  }
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  if(this == &x) return *this;
239  d_value = x.d_value;
240  return *this;
241  }
242 
244  return Rational(-(d_value));
245  }
246 
247  bool operator==(const Rational& y) const {
248  return d_value == y.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  Rational operator+(const Rational& y) const{
272  return Rational( d_value + y.d_value );
273  }
274  Rational operator-(const Rational& y) const {
275  return Rational( d_value - y.d_value );
276  }
277 
278  Rational operator*(const Rational& y) const {
279  return Rational( d_value * y.d_value );
280  }
281  Rational operator/(const Rational& y) const {
282  return Rational( d_value / y.d_value );
283  }
284 
286  d_value += y.d_value;
287  return (*this);
288  }
290  d_value -= y.d_value;
291  return (*this);
292  }
293 
295  d_value *= y.d_value;
296  return (*this);
297  }
298 
300  d_value /= y.d_value;
301  return (*this);
302  }
303 
304  bool isIntegral() const{
305  return getDenominator() == 1;
306  }
307 
309  std::string toString(int base = 10) const {
310  return d_value.get_str(base);
311  }
312 
317  size_t hash() const {
318  size_t numeratorHash = gmpz_hash(d_value.get_num_mpz_t());
319  size_t denominatorHash = gmpz_hash(d_value.get_den_mpz_t());
320 
321  return numeratorHash xor denominatorHash;
322  }
323 
324  uint32_t complexity() const {
325  uint32_t numLen = getNumerator().length();
326  uint32_t denLen = getDenominator().length();
327  return numLen + denLen;
328  }
329 };/* class Rational */
330 
331 struct RationalHashFunction {
332  inline size_t operator()(const CVC4::Rational& r) const {
333  return r.hash();
334  }
335 };/* struct RationalHashFunction */
336 
337 CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
338 
339 }/* CVC4 namespace */
340 
341 #endif /* __CVC4__RATIONAL_H */
342 
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)
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
size_t gmpz_hash(const mpz_t toHash)
Hashes the gmp integer primitive in a word by word fashion.
Definition: gmp_util.h:28
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