GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/integer_cln_imp.h Lines: 18 18 100.0 %
Date: 2021-03-22 Branches: 5 6 83.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file integer_cln_imp.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Tim King, Gereon Kremer
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 A multiprecision integer constant; wraps a CLN multiprecision
13
 ** integer.
14
 **
15
 ** A multiprecision integer constant; wraps a CLN multiprecision integer.
16
 **/
17
18
#include "cvc4_public.h"
19
20
#ifndef CVC4__INTEGER_H
21
#define CVC4__INTEGER_H
22
23
#include <cln/input.h>
24
#include <cln/integer.h>
25
#include <cln/integer_io.h>
26
#include <cln/modinteger.h>
27
28
#include <iostream>
29
#include <limits>
30
#include <sstream>
31
#include <string>
32
33
#include "base/exception.h"
34
#include "cvc4_export.h"  // remove when Cvc language support is removed
35
36
namespace CVC4 {
37
38
class Rational;
39
40
class CVC4_EXPORT Integer
41
{
42
  friend class CVC4::Rational;
43
44
 public:
45
  /**
46
   * Constructs an Integer by copying a CLN C++ primitive.
47
   */
48
324047005
  Integer(const cln::cl_I& val) : d_value(val) {}
49
50
  /** Constructs a rational with the value 0. */
51
136564
  Integer() : d_value(0) {}
52
53
  /**
54
   * Constructs a Integer from a C string.
55
   * Throws std::invalid_argument if the string is not a valid integer.
56
   */
57
8958
  explicit Integer(const char* sp, unsigned base = 10)
58
8974
  {
59
8974
    parseInt(std::string(sp), base);
60
8942
  }
61
62
  /**
63
   * Constructs a Integer from a C++ string.
64
   * Throws std::invalid_argument if the string is not a valid integer.
65
   */
66
238879
  explicit Integer(const std::string& s, unsigned base = 10)
67
238893
  {
68
238879
    parseInt(s, base);
69
238865
  }
70
71
37250937
  Integer(const Integer& q) : d_value(q.d_value) {}
72
73
257981865
  Integer(signed int z) : d_value((signed long int)z) {}
74
9095407
  Integer(unsigned int z) : d_value((unsigned long int)z) {}
75
39279
  Integer(signed long int z) : d_value(z) {}
76
8883
  Integer(unsigned long int z) : d_value(z) {}
77
78
#ifdef CVC4_NEED_INT64_T_OVERLOADS
79
  Integer(int64_t z) : d_value(static_cast<long>(z)) {}
80
  Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
81
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
82
83
  /** Destructor. */
84
628736935
  ~Integer() {}
85
86
  /** Returns a copy of d_value to enable public access of CLN data. */
87
  const cln::cl_I& getValue() const { return d_value; }
88
89
  /** Overload copy assignment operator. */
90
  Integer& operator=(const Integer& x);
91
92
  /** Overload equality comparison operator. */
93
  bool operator==(const Integer& y) const;
94
  /** Overload disequality comparison operator. */
95
  bool operator!=(const Integer& y) const;
96
  /** Overload less than comparison operator. */
97
  bool operator<(const Integer& y) const;
98
  /** Overload less than or equal comparison operator. */
99
  bool operator<=(const Integer& y) const;
100
  /** Overload greater than comparison operator. */
101
  bool operator>(const Integer& y) const;
102
  /** Overload greater than or equal comparison operator. */
103
  bool operator>=(const Integer& y) const;
104
105
  /** Overload negation operator. */
106
  Integer operator-() const;
107
  /** Overload addition operator. */
108
  Integer operator+(const Integer& y) const;
109
  /** Overload addition assignment operator. */
110
  Integer& operator+=(const Integer& y);
111
  /** Overload subtraction operator. */
112
  Integer operator-(const Integer& y) const;
113
  /** Overload subtraction assignment operator. */
114
  Integer& operator-=(const Integer& y);
115
  /** Overload multiplication operator. */
116
  Integer operator*(const Integer& y) const;
117
  /** Overload multiplication assignment operator. */
118
  Integer& operator*=(const Integer& y);
119
120
  /** Return the bit-wise or of this and the given Integer. */
121
  Integer bitwiseOr(const Integer& y) const;
122
  /** Return the bit-wise and of this and the given Integer. */
123
  Integer bitwiseAnd(const Integer& y) const;
124
  /** Return the bit-wise exclusive or of this and the given Integer. */
125
  Integer bitwiseXor(const Integer& y) const;
126
  /** Return the bit-wise not of this Integer. */
127
  Integer bitwiseNot() const;
128
129
  /** Return this*(2^pow). */
130
  Integer multiplyByPow2(uint32_t pow) const;
131
132
  /** Return true if bit at index 'i' is 1, and false otherwise. */
133
  bool isBitSet(uint32_t i) const;
134
135
  /** Set the ith bit of the current Integer to 'value'.  */
136
  void setBit(uint32_t i, bool value);
137
138
  /**
139
   * Returns the integer with the binary representation of 'size' bits
140
   * extended with 'amount' 1's.
141
   */
142
  Integer oneExtend(uint32_t size, uint32_t amount) const;
143
144
  /** Return a 32 bit unsigned integer representation of this Integer. */
145
  uint32_t toUnsignedInt() const;
146
147
  /**
148
   * Extract a range of bits from index 'low' to (excluding) 'low + bitCount'.
149
   * Note: corresponds to the extract operator of theory BV.
150
   */
151
  Integer extractBitRange(uint32_t bitCount, uint32_t low) const;
152
153
  /** Returns the floor(this / y). */
154
  Integer floorDivideQuotient(const Integer& y) const;
155
156
  /** Returns r == this - floor(this/y)*y. */
157
  Integer floorDivideRemainder(const Integer& y) const;
158
159
  /** Computes a floor quoient and remainder for x divided by y.  */
160
  static void floorQR(Integer& q,
161
                      Integer& r,
162
                      const Integer& x,
163
                      const Integer& y);
164
165
  /** Returns the ceil(this / y). */
166
  Integer ceilingDivideQuotient(const Integer& y) const;
167
168
  /** Returns the ceil(this / y). */
169
  Integer ceilingDivideRemainder(const Integer& y) const;
170
171
  /**
172
   * Computes a quoitent and remainder according to Boute's Euclidean
173
   * definition. euclidianDivideQuotient, euclidianDivideRemainder.
174
   *
175
   * Boute, Raymond T. (April 1992).
176
   * The Euclidean definition of the functions div and mod.
177
   * ACM Transactions on Programming Languages and Systems (TOPLAS)
178
   * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
179
   */
180
  static void euclidianQR(Integer& q,
181
                          Integer& r,
182
                          const Integer& x,
183
                          const Integer& y);
184
185
  /**
186
   * Returns the quoitent according to Boute's Euclidean definition.
187
   * See the documentation for euclidianQR.
188
   */
189
  Integer euclidianDivideQuotient(const Integer& y) const;
190
191
  /**
192
   * Returns the remainfing according to Boute's Euclidean definition.
193
   * See the documentation for euclidianQR.
194
   */
195
  Integer euclidianDivideRemainder(const Integer& y) const;
196
197
  /** If y divides *this, then exactQuotient returns (this/y). */
198
  Integer exactQuotient(const Integer& y) const;
199
200
  /** Return y mod 2^exp. */
201
  Integer modByPow2(uint32_t exp) const;
202
203
  /** Returns y / 2^exp. */
204
  Integer divByPow2(uint32_t exp) const;
205
206
  /**
207
   * Raise this Integer to the power <code>exp</code>.
208
   *
209
   * @param exp the exponent
210
   */
211
  Integer pow(unsigned long int exp) const;
212
213
  /** Return the greatest common divisor of this integer with another.  */
214
  Integer gcd(const Integer& y) const;
215
216
  /** Return the least common multiple of this integer with another.  */
217
  Integer lcm(const Integer& y) const;
218
219
  /** Compute addition of this Integer x + y modulo m.  */
220
  Integer modAdd(const Integer& y, const Integer& m) const;
221
222
  /** Compute multiplication of this Integer x * y modulo m.  */
223
  Integer modMultiply(const Integer& y, const Integer& m) const;
224
225
  /**
226
   * Compute modular inverse x^-1 of this Integer x modulo m with m > 0.
227
   * Returns a value x^-1 with 0 <= x^-1 < m such that x * x^-1 = 1 modulo m
228
   * if such an inverse exists, and -1 otherwise.
229
   *
230
   * Such an inverse only exists if
231
   *   - x is non-zero
232
   *   - x and m are coprime, i.e., if gcd (x, m) = 1
233
   *
234
   * Note that if x and m are coprime, then x^-1 > 0 if m > 1 and x^-1 = 0
235
   * if m = 1 (the zero ring).
236
   */
237
  Integer modInverse(const Integer& m) const;
238
239
  /** Return true if *this exactly divides y.  */
240
  bool divides(const Integer& y) const;
241
242
  /** Return the absolute value of this integer.  */
243
  Integer abs() const;
244
245
  /** Return a string representation of this Integer. */
246
  std::string toString(int base = 10) const;
247
248
  /** Return 1 if this is > 0, 0 if it is 0, and -1 if it is < 0. */
249
  int sgn() const;
250
251
  /** Return true if this is > 0. */
252
  bool strictlyPositive() const;
253
254
  /** Return true if this is < 0. */
255
  bool strictlyNegative() const;
256
257
  /** Return true if this is 0. */
258
  bool isZero() const;
259
260
  /** Return true if this is 1. */
261
  bool isOne() const;
262
263
  /** Return true if this is -1. */
264
  bool isNegativeOne() const;
265
266
  /** Return true if this Integer fits into a signed int. */
267
  bool fitsSignedInt() const;
268
269
  /** Return true if this Integer fits into an unsigned int. */
270
  bool fitsUnsignedInt() const;
271
272
  /** Return the signed int representation of this Integer. */
273
  int getSignedInt() const;
274
275
  /** Return the unsigned int representation of this Integer. */
276
  unsigned int getUnsignedInt() const;
277
278
  /** Return true if this Integer fits into a signed long. */
279
  bool fitsSignedLong() const;
280
281
  /** Return true if this Integer fits into an unsigned long. */
282
  bool fitsUnsignedLong() const;
283
284
  /** Return the signed long representation of this Integer. */
285
  long getLong() const;
286
287
  /** Return the unsigned long representation of this Integer. */
288
  unsigned long getUnsignedLong() const;
289
290
  /**
291
   * Computes the hash of the node from the first word of the
292
   * numerator, the denominator.
293
   */
294
  size_t hash() const;
295
296
  /**
297
   * Returns true iff bit n is set.
298
   *
299
   * @param n the bit to test (0 == least significant bit)
300
   * @return true if bit n is set in this integer; false otherwise
301
   */
302
  bool testBit(unsigned n) const;
303
304
  /**
305
   * Returns k if the integer is equal to 2^(k-1)
306
   * @return k if the integer is equal to 2^(k-1) and 0 otherwise
307
   */
308
  unsigned isPow2() const;
309
310
  /**
311
   * If x != 0, returns the unique n s.t. 2^{n-1} <= abs(x) < 2^{n}.
312
   * If x == 0, returns 1.
313
   */
314
  size_t length() const;
315
316
  /*   cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */
317
  /* This function ("extended gcd") returns the greatest common divisor g of a
318
   * and b and at the same time the representation of g as an integral linear
319
   * combination of a and b: u and v with u*a+v*b = g, g >= 0. u and v will be
320
   * normalized to be of smallest possible absolute value, in the following
321
   * sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy
322
   * the inequalities abs(u) <= abs(b)/(2*g), abs(v) <= abs(a)/(2*g). */
323
  static void extendedGcd(
324
      Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b);
325
326
  /** Returns a reference to the minimum of two integers. */
327
  static const Integer& min(const Integer& a, const Integer& b);
328
329
  /** Returns a reference to the maximum of two integers. */
330
  static const Integer& max(const Integer& a, const Integer& b);
331
332
 private:
333
  /**
334
   * Gets a reference to the cln data that backs up the integer.
335
   * Only accessible to friend classes.
336
   */
337
5590145
  const cln::cl_I& get_cl_I() const { return d_value; }
338
339
  /**
340
   * Helper for parseInt.
341
   * Throws a std::invalid_argument on invalid input `s` for the given base.
342
   */
343
  void readInt(const cln::cl_read_flags& flags,
344
               const std::string& s,
345
               unsigned base);
346
347
  /**
348
   * Parse string representation of integer into this Integer.
349
   * Throws a std::invalid_argument on invalid inputs.
350
   */
351
  void parseInt(const std::string& s, unsigned base);
352
353
  /**
354
   * The following constants are to help with CLN conversion in 32 bit.
355
   * See http://www.ginac.de/CLN/cln.html#Conversions.
356
   */
357
358
  /**  2^29 - 1 */
359
  static signed int s_fastSignedIntMax;
360
  /** -2^29 */
361
  static signed int s_fastSignedIntMin;
362
  /** 2^29 - 1 */
363
  static unsigned int s_fastUnsignedIntMax;
364
  /** std::numeric_limits<signed int>::max() */
365
  static signed long s_slowSignedIntMax;
366
  /** std::numeric_limits<signed int>::min() */
367
  static signed long s_slowSignedIntMin;
368
  /** std::numeric_limits<unsigned int>::max() */
369
  static unsigned long s_slowUnsignedIntMax;
370
  /** std::numeric_limits<signed long>::min() */
371
  static unsigned long s_signedLongMin;
372
  /** std::numeric_limits<signed long>::max() */
373
  static unsigned long s_signedLongMax;
374
  /** std::numeric_limits<unsigned long>::max() */
375
  static unsigned long s_unsignedLongMax;
376
377
  /** Value of the rational is stored in a C++ CLN integer class. */
378
  cln::cl_I d_value;
379
}; /* class Integer */
380
381
struct IntegerHashFunction
382
{
383
59838
  size_t operator()(const CVC4::Integer& i) const { return i.hash(); }
384
}; /* struct IntegerHashFunction */
385
386
std::ostream& operator<<(std::ostream& os, const Integer& n);
387
388
}  // namespace CVC4
389
390
#endif /* CVC4__INTEGER_H */