GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/rational_cln_imp.h Lines: 96 105 91.4 %
Date: 2021-03-22 Branches: 46 106 43.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file rational_cln_imp.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Gereon Kremer, Morgan Deters
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Multiprecision rational constants; wraps a CLN multiprecision
13
 ** rational.
14
 **
15
 ** Multiprecision rational constants; wraps a CLN multiprecision rational.
16
 **/
17
18
#include "cvc4_public.h"
19
20
#ifndef CVC4__RATIONAL_H
21
#define CVC4__RATIONAL_H
22
23
#include <cln/dfloat.h>
24
#include <cln/input.h>
25
#include <cln/io.h>
26
#include <cln/number_io.h>
27
#include <cln/output.h>
28
#include <cln/rational.h>
29
#include <cln/rational_io.h>
30
#include <cln/real.h>
31
32
#include <sstream>
33
#include <string>
34
35
#include "base/exception.h"
36
#include "cvc4_export.h"  // remove when Cvc language support is removed
37
#include "util/integer.h"
38
#include "util/maybe.h"
39
40
namespace CVC4 {
41
42
/**
43
 ** A multi-precision rational constant.
44
 ** This stores the rational as a pair of multi-precision integers,
45
 ** one for the numerator and one for the denominator.
46
 ** The number is always stored so that the gcd of the numerator and denominator
47
 ** is 1.  (This is referred to as referred to as canonical form in GMP's
48
 ** literature.) A consequence is that that the numerator and denominator may be
49
 ** different than the values used to construct the Rational.
50
 **
51
 ** NOTE: The correct way to create a Rational from an int is to use one of the
52
 ** int numerator/int denominator constructors with the denominator 1.  Trying
53
 ** to construct a Rational with a single int, e.g., Rational(0), will put you
54
 ** in danger of invoking the char* constructor, from whence you will segfault.
55
 **/
56
57
class CVC4_EXPORT Rational
58
{
59
 public:
60
  /**
61
   * Constructs a Rational from a cln::cl_RA object.
62
   * Does a deep copy.
63
   */
64
126997524
  Rational(const cln::cl_RA& val) : d_value(val) {}
65
66
  /**
67
   * Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
68
   *
69
   * @param dec a string encoding a decimal number in the format
70
   * <code>[0-9]*\.[0-9]*</code>
71
   */
72
  static Rational fromDecimal(const std::string& dec);
73
74
  /** Constructs a rational with the value 0/1. */
75
3968551
  Rational() : d_value(0) {}
76
  /**
77
   * Constructs a Rational from a C string in a given base (defaults to 10).
78
   *
79
   * Throws std::invalid_argument if the string is not a valid rational.
80
   * For more information about what is a valid rational string,
81
   * see CLN's documentation for read_rational.
82
   */
83
44
  explicit Rational(const char* s, unsigned base = 10)
84
44
  {
85
    cln::cl_read_flags flags;
86
87
44
    flags.syntax = cln::syntax_rational;
88
44
    flags.lsyntax = cln::lsyntax_standard;
89
44
    flags.rational_base = base;
90
    try
91
    {
92
44
      d_value = read_rational(flags, s, NULL, NULL);
93
    }
94
    catch (...)
95
    {
96
      std::stringstream ss;
97
      ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
98
      throw std::invalid_argument(ss.str());
99
    }
100
44
  }
101
357863
  Rational(const std::string& s, unsigned base = 10)
102
357889
  {
103
    cln::cl_read_flags flags;
104
105
357863
    flags.syntax = cln::syntax_rational;
106
357863
    flags.lsyntax = cln::lsyntax_standard;
107
357863
    flags.rational_base = base;
108
    try
109
    {
110
357863
      d_value = read_rational(flags, s.c_str(), NULL, NULL);
111
    }
112
52
    catch (...)
113
    {
114
52
      std::stringstream ss;
115
26
      ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
116
26
      throw std::invalid_argument(ss.str());
117
    }
118
357837
  }
119
120
  /**
121
   * Creates a Rational from another Rational, q, by performing a deep copy.
122
   */
123
116933892
  Rational(const Rational& q) : d_value(q.d_value) {}
124
125
  /**
126
   * Constructs a canonical Rational from a numerator.
127
   */
128
481122801
  Rational(signed int n) : d_value((signed long int)n) {}
129
1800414
  Rational(unsigned int n) : d_value((unsigned long int)n) {}
130
37671
  Rational(signed long int n) : d_value(n) {}
131
53608
  Rational(unsigned long int n) : d_value(n) {}
132
133
#ifdef CVC4_NEED_INT64_T_OVERLOADS
134
  Rational(int64_t n) : d_value(static_cast<long>(n)) {}
135
  Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) {}
136
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
137
138
  /**
139
   * Constructs a canonical Rational from a numerator and denominator.
140
   */
141
15237853
  Rational(signed int n, signed int d) : d_value((signed long int)n)
142
  {
143
15237853
    d_value /= cln::cl_I(d);
144
15237853
  }
145
8
  Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n)
146
  {
147
8
    d_value /= cln::cl_I(d);
148
8
  }
149
18
  Rational(signed long int n, signed long int d) : d_value(n)
150
  {
151
18
    d_value /= cln::cl_I(d);
152
18
  }
153
2
  Rational(unsigned long int n, unsigned long int d) : d_value(n)
154
  {
155
2
    d_value /= cln::cl_I(d);
156
2
  }
157
158
#ifdef CVC4_NEED_INT64_T_OVERLOADS
159
  Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n))
160
  {
161
    d_value /= cln::cl_I(d);
162
  }
163
  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n))
164
  {
165
    d_value /= cln::cl_I(d);
166
  }
167
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
168
169
1184043
  Rational(const Integer& n, const Integer& d) : d_value(n.get_cl_I())
170
  {
171
1184043
    d_value /= d.get_cl_I();
172
1184043
  }
173
3222059
  Rational(const Integer& n) : d_value(n.get_cl_I()) {}
174
175
750916353
  ~Rational() {}
176
177
  /**
178
   * Returns a copy of d_value to enable public access of CLN data.
179
   */
180
  const cln::cl_RA& getValue() const { return d_value; }
181
182
  /**
183
   * Returns the value of numerator of the Rational.
184
   * Note that this makes a deep copy of the numerator.
185
   */
186
14686953
  Integer getNumerator() const { return Integer(cln::numerator(d_value)); }
187
188
  /**
189
   * Returns the value of denominator of the Rational.
190
   * Note that this makes a deep copy of the denominator.
191
   */
192
250022986
  Integer getDenominator() const { return Integer(cln::denominator(d_value)); }
193
194
  /** Return an exact rational for a double d. */
195
  static Maybe<Rational> fromDouble(double d);
196
197
  /**
198
   * Get a double representation of this Rational, which is
199
   * approximate: truncation may occur, overflow may result in
200
   * infinity, and underflow may result in zero.
201
   */
202
7
  double getDouble() const { return cln::double_approx(d_value); }
203
204
565335
  Rational inverse() const { return Rational(cln::recip(d_value)); }
205
206
75446304
  int cmp(const Rational& x) const
207
  {
208
    // Don't use mpq_class's cmp() function.
209
    // The name ends up conflicting with this function.
210
75446304
    return cln::compare(d_value, x.d_value);
211
  }
212
213
  int sgn() const;
214
215
232991618
  bool isZero() const { return cln::zerop(d_value); }
216
217
8295403
  bool isOne() const { return d_value == 1; }
218
219
29837
  bool isNegativeOne() const { return d_value == -1; }
220
221
326562
  Rational abs() const
222
  {
223
326562
    if (sgn() < 0)
224
    {
225
68492
      return -(*this);
226
    }
227
    else
228
    {
229
258070
      return *this;
230
    }
231
  }
232
233
236233293
  bool isIntegral() const { return getDenominator() == 1; }
234
235
2134
  Integer floor() const { return Integer(cln::floor1(d_value)); }
236
237
201184
  Integer ceiling() const { return Integer(cln::ceiling1(d_value)); }
238
239
  Rational floor_frac() const { return (*this) - Rational(floor()); }
240
241
71418857
  Rational& operator=(const Rational& x)
242
  {
243
71418857
    if (this == &x) return *this;
244
71418857
    d_value = x.d_value;
245
71418857
    return *this;
246
  }
247
248
3447173
  Rational operator-() const { return Rational(-(d_value)); }
249
250
450943831
  bool operator==(const Rational& y) const { return d_value == y.d_value; }
251
252
54840362
  bool operator!=(const Rational& y) const { return d_value != y.d_value; }
253
254
398182
  bool operator<(const Rational& y) const { return d_value < y.d_value; }
255
256
25537607
  bool operator<=(const Rational& y) const { return d_value <= y.d_value; }
257
258
137310
  bool operator>(const Rational& y) const { return d_value > y.d_value; }
259
260
419380
  bool operator>=(const Rational& y) const { return d_value >= y.d_value; }
261
262
27103627
  Rational operator+(const Rational& y) const
263
  {
264
27103627
    return Rational(d_value + y.d_value);
265
  }
266
122023
  Rational operator-(const Rational& y) const
267
  {
268
122023
    return Rational(d_value - y.d_value);
269
  }
270
271
94479560
  Rational operator*(const Rational& y) const
272
  {
273
94479560
    return Rational(d_value * y.d_value);
274
  }
275
1279728
  Rational operator/(const Rational& y) const
276
  {
277
1279728
    return Rational(d_value / y.d_value);
278
  }
279
280
41345569
  Rational& operator+=(const Rational& y)
281
  {
282
41345569
    d_value += y.d_value;
283
41345569
    return (*this);
284
  }
285
286
  Rational& operator-=(const Rational& y)
287
  {
288
    d_value -= y.d_value;
289
    return (*this);
290
  }
291
292
4845616
  Rational& operator*=(const Rational& y)
293
  {
294
4845616
    d_value *= y.d_value;
295
4845616
    return (*this);
296
  }
297
298
556
  Rational& operator/=(const Rational& y)
299
  {
300
556
    d_value /= y.d_value;
301
556
    return (*this);
302
  }
303
304
  /** Returns a string representing the rational in the given base. */
305
729958
  std::string toString(int base = 10) const
306
  {
307
1459916
    cln::cl_print_flags flags;
308
729958
    flags.rational_base = base;
309
729958
    flags.rational_readably = false;
310
1459916
    std::stringstream ss;
311
729958
    print_rational(ss, flags, d_value);
312
1459916
    return ss.str();
313
  }
314
315
  /**
316
   * Computes the hash of the rational from hashes of the numerator and the
317
   * denominator.
318
   */
319
137630902
  size_t hash() const { return equal_hashcode(d_value); }
320
321
  uint32_t complexity() const
322
  {
323
    return getNumerator().length() + getDenominator().length();
324
  }
325
326
  /** Equivalent to calling (this->abs()).cmp(b.abs()) */
327
  int absCmp(const Rational& q) const;
328
329
 private:
330
  /**
331
   * Stores the value of the rational in a C++ CLN rational class.
332
   */
333
  cln::cl_RA d_value;
334
335
}; /* class Rational */
336
337
struct RationalHashFunction
338
{
339
137630902
  inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); }
340
}; /* struct RationalHashFunction */
341
342
std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT;
343
344
26676
}  // namespace CVC4
345
346
#endif /* CVC4__RATIONAL_H */