GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/integer_cln_imp.cpp Lines: 219 239 91.6 %
Date: 2021-09-15 Branches: 224 535 41.9 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Aina Niemetz, Tim King, Gereon Kremer
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * A multiprecision integer constant; wraps a CLN multiprecision integer.
14
 */
15
#include <sstream>
16
#include <string>
17
18
#include "base/cvc5config.h"
19
#include "util/integer.h"
20
21
#ifndef CVC5_CLN_IMP
22
#error "This source should only ever be built if CVC5_CLN_IMP is on !"
23
#endif /* CVC5_CLN_IMP */
24
25
#include "base/check.h"
26
27
using namespace std;
28
29
namespace cvc5 {
30
31
signed int Integer::s_fastSignedIntMin = -(1 << 29);
32
signed int Integer::s_fastSignedIntMax = (1 << 29) - 1;
33
signed long Integer::s_slowSignedIntMin =
34
    (signed long)std::numeric_limits<signed int>::min();
35
signed long Integer::s_slowSignedIntMax =
36
    (signed long)std::numeric_limits<signed int>::max();
37
38
unsigned int Integer::s_fastUnsignedIntMax = (1 << 29) - 1;
39
unsigned long Integer::s_slowUnsignedIntMax =
40
    (unsigned long)std::numeric_limits<unsigned int>::max();
41
42
unsigned long Integer::s_signedLongMin =
43
    std::numeric_limits<signed long>::min();
44
unsigned long Integer::s_signedLongMax =
45
    std::numeric_limits<signed long>::max();
46
unsigned long Integer::s_unsignedLongMax =
47
    std::numeric_limits<unsigned long>::max();
48
49
23520841
Integer& Integer::operator=(const Integer& x)
50
{
51
23520841
  if (this == &x) return *this;
52
23520841
  d_value = x.d_value;
53
23520841
  return *this;
54
}
55
56
268468556
bool Integer::operator==(const Integer& y) const
57
{
58
268468556
  return d_value == y.d_value;
59
}
60
61
726983
Integer Integer::operator-() const { return Integer(-(d_value)); }
62
63
891283
bool Integer::operator!=(const Integer& y) const
64
{
65
891283
  return d_value != y.d_value;
66
}
67
68
924482
bool Integer::operator<(const Integer& y) const { return d_value < y.d_value; }
69
70
179855
bool Integer::operator<=(const Integer& y) const
71
{
72
179855
  return d_value <= y.d_value;
73
}
74
75
459204
bool Integer::operator>(const Integer& y) const { return d_value > y.d_value; }
76
77
684991
bool Integer::operator>=(const Integer& y) const
78
{
79
684991
  return d_value >= y.d_value;
80
}
81
82
2776197
Integer Integer::operator+(const Integer& y) const
83
{
84
2776197
  return Integer(d_value + y.d_value);
85
}
86
87
66299
Integer& Integer::operator+=(const Integer& y)
88
{
89
66299
  d_value += y.d_value;
90
66299
  return *this;
91
}
92
93
1343675
Integer Integer::operator-(const Integer& y) const
94
{
95
1343675
  return Integer(d_value - y.d_value);
96
}
97
98
9187
Integer& Integer::operator-=(const Integer& y)
99
{
100
9187
  d_value -= y.d_value;
101
9187
  return *this;
102
}
103
104
1301775
Integer Integer::operator*(const Integer& y) const
105
{
106
1301775
  return Integer(d_value * y.d_value);
107
}
108
109
9972
Integer& Integer::operator*=(const Integer& y)
110
{
111
9972
  d_value *= y.d_value;
112
9972
  return *this;
113
}
114
115
293283
Integer Integer::bitwiseOr(const Integer& y) const
116
{
117
293283
  return Integer(cln::logior(d_value, y.d_value));
118
}
119
120
206487
Integer Integer::bitwiseAnd(const Integer& y) const
121
{
122
206487
  return Integer(cln::logand(d_value, y.d_value));
123
}
124
125
597
Integer Integer::bitwiseXor(const Integer& y) const
126
{
127
597
  return Integer(cln::logxor(d_value, y.d_value));
128
}
129
130
1151514
Integer Integer::bitwiseNot() const { return Integer(cln::lognot(d_value)); }
131
132
1511826
Integer Integer::multiplyByPow2(uint32_t pow) const
133
{
134
3023652
  cln::cl_I ipow(pow);
135
3023652
  return Integer(d_value << ipow);
136
}
137
138
56547
bool Integer::isBitSet(uint32_t i) const
139
{
140
56547
  return !extractBitRange(1, i).isZero();
141
}
142
143
1969
void Integer::setBit(uint32_t i, bool value)
144
{
145
3938
  cln::cl_I mask(1);
146
1969
  mask = mask << i;
147
1969
  if (value)
148
  {
149
1941
    d_value = cln::logior(d_value, mask);
150
  }
151
  else
152
  {
153
28
    mask = cln::lognot(mask);
154
28
    d_value = cln::logand(d_value, mask);
155
  }
156
1969
}
157
158
630494
Integer Integer::oneExtend(uint32_t size, uint32_t amount) const
159
{
160
630494
  DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
161
630494
  cln::cl_byte range(amount, size);
162
1260988
  cln::cl_I allones = (cln::cl_I(1) << (size + amount)) - 1;  // 2^size - 1
163
1260988
  Integer temp(allones);
164
165
1260988
  return Integer(cln::deposit_field(allones, d_value, range));
166
}
167
168
1533952
uint32_t Integer::toUnsignedInt() const { return cln::cl_I_to_uint(d_value); }
169
170
1708922
Integer Integer::extractBitRange(uint32_t bitCount, uint32_t low) const
171
{
172
1708922
  cln::cl_byte range(bitCount, low);
173
1708922
  return Integer(cln::ldb(d_value, range));
174
}
175
176
26691
Integer Integer::floorDivideQuotient(const Integer& y) const
177
{
178
26691
  return Integer(cln::floor1(d_value, y.d_value));
179
}
180
181
28898
Integer Integer::floorDivideRemainder(const Integer& y) const
182
{
183
28898
  return Integer(cln::floor2(d_value, y.d_value).remainder);
184
}
185
186
4573
void Integer::floorQR(Integer& q,
187
                      Integer& r,
188
                      const Integer& x,
189
                      const Integer& y)
190
{
191
9146
  cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value);
192
4573
  q.d_value = res.quotient;
193
4573
  r.d_value = res.remainder;
194
4573
}
195
196
Integer Integer::ceilingDivideQuotient(const Integer& y) const
197
{
198
  return Integer(cln::ceiling1(d_value, y.d_value));
199
}
200
201
Integer Integer::ceilingDivideRemainder(const Integer& y) const
202
{
203
  return Integer(cln::ceiling2(d_value, y.d_value).remainder);
204
}
205
206
3413
void Integer::euclidianQR(Integer& q,
207
                          Integer& r,
208
                          const Integer& x,
209
                          const Integer& y)
210
{
211
  // compute the floor and then fix the value up if needed.
212
3413
  floorQR(q, r, x, y);
213
214
3413
  if (r.strictlyNegative())
215
  {
216
    // if r < 0
217
    // abs(r) < abs(y)
218
    // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
219
    // n = y * q + r
220
    // n = y * q - abs(y) + r + abs(y)
221
8
    if (r.sgn() >= 0)
222
    {
223
      // y = abs(y)
224
      // n = y * q - y + r + y
225
      // n = y * (q-1) + (r+y)
226
      q -= 1;
227
      r += y;
228
    }
229
    else
230
    {
231
      // y = -abs(y)
232
      // n = y * q + y + r - y
233
      // n = y * (q+1) + (r-y)
234
8
      q += 1;
235
8
      r -= y;
236
    }
237
  }
238
3413
}
239
240
301
Integer Integer::euclidianDivideQuotient(const Integer& y) const
241
{
242
602
  Integer q, r;
243
301
  euclidianQR(q, r, *this, y);
244
602
  return q;
245
}
246
247
3096
Integer Integer::euclidianDivideRemainder(const Integer& y) const
248
{
249
6192
  Integer q, r;
250
3096
  euclidianQR(q, r, *this, y);
251
6192
  return r;
252
}
253
254
Integer Integer::exactQuotient(const Integer& y) const
255
{
256
  DebugCheckArgument(y.divides(*this), y);
257
  return Integer(cln::exquo(d_value, y.d_value));
258
}
259
260
11842591
Integer Integer::modByPow2(uint32_t exp) const
261
{
262
11842591
  cln::cl_byte range(exp, 0);
263
11842591
  return Integer(cln::ldb(d_value, range));
264
}
265
266
7454
Integer Integer::divByPow2(uint32_t exp) const { return d_value >> exp; }
267
268
26698
Integer Integer::pow(unsigned long int exp) const
269
{
270
26698
  if (exp == 0)
271
  {
272
182
    return Integer(1);
273
  }
274
  else
275
  {
276
26516
    Assert(exp > 0);
277
53032
    cln::cl_I result = cln::expt_pos(d_value, exp);
278
26516
    return Integer(result);
279
  }
280
}
281
282
4057095
Integer Integer::gcd(const Integer& y) const
283
{
284
8114190
  cln::cl_I result = cln::gcd(d_value, y.d_value);
285
8114190
  return Integer(result);
286
}
287
288
16141192
Integer Integer::lcm(const Integer& y) const
289
{
290
32282384
  cln::cl_I result = cln::lcm(d_value, y.d_value);
291
32282384
  return Integer(result);
292
}
293
294
2564
Integer Integer::modAdd(const Integer& y, const Integer& m) const
295
{
296
5128
  cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
297
5128
  cln::cl_MI xm = ry->canonhom(d_value);
298
5128
  cln::cl_MI ym = ry->canonhom(y.d_value);
299
5128
  cln::cl_MI res = xm + ym;
300
5128
  return Integer(ry->retract(res));
301
}
302
303
2558
Integer Integer::modMultiply(const Integer& y, const Integer& m) const
304
{
305
5116
  cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
306
5116
  cln::cl_MI xm = ry->canonhom(d_value);
307
5116
  cln::cl_MI ym = ry->canonhom(y.d_value);
308
5116
  cln::cl_MI res = xm * ym;
309
5116
  return Integer(ry->retract(res));
310
}
311
312
466
Integer Integer::modInverse(const Integer& m) const
313
{
314
466
  PrettyCheckArgument(m > 0, m, "m must be greater than zero");
315
932
  cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
316
932
  cln::cl_MI xm = ry->canonhom(d_value);
317
  /* normalize to modulo m for coprime check */
318
932
  cln::cl_I x = ry->retract(xm);
319
466
  if (x == 0 || cln::gcd(x, m.d_value) != 1)
320
  {
321
26
    return Integer(-1);
322
  }
323
880
  cln::cl_MI res = cln::recip(xm);
324
440
  return Integer(ry->retract(res));
325
}
326
327
55351
bool Integer::divides(const Integer& y) const
328
{
329
110702
  cln::cl_I result = cln::rem(y.d_value, d_value);
330
110702
  return cln::zerop(result);
331
}
332
333
8705807
Integer Integer::abs() const { return d_value >= 0 ? *this : -*this; }
334
335
4550
std::string Integer::toString(int base) const
336
{
337
9100
  std::stringstream ss;
338
4550
  switch (base)
339
  {
340
242
    case 2: fprintbinary(ss, d_value); break;
341
    case 8: fprintoctal(ss, d_value); break;
342
4286
    case 10: fprintdecimal(ss, d_value); break;
343
22
    case 16: fprinthexadecimal(ss, d_value); break;
344
    default: throw Exception("Unhandled base in Integer::toString()");
345
  }
346
4550
  std::string output = ss.str();
347
28572
  for (unsigned i = 0; i <= output.length(); ++i)
348
  {
349
24022
    if (isalpha(output[i]))
350
    {
351
18
      output.replace(i, 1, 1, tolower(output[i]));
352
    }
353
  }
354
355
9100
  return output;
356
}
357
358
1572052
int Integer::sgn() const
359
{
360
3144104
  cln::cl_I sgn = cln::signum(d_value);
361
3144104
  return cln::cl_I_to_int(sgn);
362
}
363
364
28
bool Integer::strictlyPositive() const { return cln::plusp(d_value); }
365
366
104700
bool Integer::strictlyNegative() const { return cln::minusp(d_value); }
367
368
56613
bool Integer::isZero() const { return cln::zerop(d_value); }
369
370
23076475
bool Integer::isOne() const { return d_value == 1; }
371
372
bool Integer::isNegativeOne() const { return d_value == -1; }
373
374
221825
void Integer::parseInt(const std::string& s, unsigned base)
375
{
376
  cln::cl_read_flags flags;
377
221825
  flags.syntax = cln::syntax_integer;
378
221825
  flags.lsyntax = cln::lsyntax_standard;
379
221825
  flags.rational_base = base;
380
221825
  if (base == 0)
381
  {
382
    // infer base in a manner consistent with GMP
383
16
    if (s[0] == '0')
384
    {
385
10
      flags.lsyntax = cln::lsyntax_commonlisp;
386
20
      std::string st = s;
387
10
      if (s[1] == 'X' || s[1] == 'x')
388
      {
389
4
        st.replace(0, 2, "#x");
390
      }
391
6
      else if (s[1] == 'B' || s[1] == 'b')
392
      {
393
4
        st.replace(0, 2, "#b");
394
      }
395
      else
396
      {
397
2
        st.replace(0, 1, "#o");
398
      }
399
10
      readInt(flags, st, base);
400
8
      return;
401
    }
402
    else
403
    {
404
6
      flags.rational_base = 10;
405
    }
406
  }
407
221815
  readInt(flags, s, base);
408
}
409
410
221825
void Integer::readInt(const cln::cl_read_flags& flags,
411
                      const std::string& s,
412
                      unsigned base)
413
{
414
  try
415
  {
416
    // Removing leading zeroes, CLN has a bug for these inputs up to and
417
    // including CLN v1.3.2.
418
    // See
419
    // http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a
420
    // for details.
421
221825
    size_t pos = s.find_first_not_of('0');
422
221825
    if (pos == std::string::npos)
423
    {
424
45887
      d_value = cln::read_integer(flags, "0", NULL, NULL);
425
    }
426
    else
427
    {
428
175938
      const char* cstr = s.c_str();
429
175938
      const char* start = cstr + pos;
430
175938
      const char* end = cstr + s.length();
431
175938
      d_value = cln::read_integer(flags, start, end, NULL);
432
    }
433
  }
434
194
  catch (...)
435
  {
436
194
    std::stringstream ss;
437
97
    ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
438
97
    throw std::invalid_argument(ss.str());
439
  }
440
221728
}
441
442
48
bool Integer::fitsSignedInt() const
443
{
444
  // http://www.ginac.de/CLN/cln.html#Conversions
445
  // TODO improve performance
446
48
  Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
447
48
  Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
448
48
  Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
449
450
144
  return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax)
451
240
         && (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
452
}
453
454
1292793
bool Integer::fitsUnsignedInt() const
455
{
456
  // TODO improve performance
457
1292793
  Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
458
1292793
  return sgn() >= 0
459
5171172
         && (d_value <= s_fastUnsignedIntMax
460
2585588
             || d_value <= s_slowUnsignedIntMax);
461
}
462
463
48
signed int Integer::getSignedInt() const
464
{
465
  // ensure there isn't overflow
466
96
  CheckArgument(
467
48
      fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
468
48
  return cln::cl_I_to_int(d_value);
469
}
470
471
13122
unsigned int Integer::getUnsignedInt() const
472
{
473
  // ensure there isn't overflow
474
13122
  CheckArgument(fitsUnsignedInt(),
475
                this,
476
                "Overflow detected in Integer::getUnsignedInt()");
477
13122
  return cln::cl_I_to_uint(d_value);
478
}
479
480
bool Integer::fitsSignedLong() const
481
{
482
  return d_value <= s_signedLongMax && d_value >= s_signedLongMin;
483
}
484
485
bool Integer::fitsUnsignedLong() const
486
{
487
  return sgn() >= 0 && d_value <= s_unsignedLongMax;
488
}
489
490
2392
long Integer::getLong() const
491
{
492
  // ensure there isn't overflow
493
2394
  CheckArgument(d_value <= std::numeric_limits<long>::max(),
494
                this,
495
                "Overflow detected in Integer::getLong()");
496
2390
  CheckArgument(d_value >= std::numeric_limits<long>::min(),
497
                this,
498
                "Overflow detected in Integer::getLong()");
499
2390
  return cln::cl_I_to_long(d_value);
500
}
501
502
400
unsigned long Integer::getUnsignedLong() const
503
{
504
  // ensure there isn't overflow
505
402
  CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(),
506
                this,
507
                "Overflow detected in Integer::getUnsignedLong()");
508
398
  CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(),
509
                this,
510
                "Overflow detected in Integer::getUnsignedLong()");
511
398
  return cln::cl_I_to_ulong(d_value);
512
}
513
514
2996558
size_t Integer::hash() const { return equal_hashcode(d_value); }
515
516
94
bool Integer::testBit(unsigned n) const { return cln::logbitp(n, d_value); }
517
518
407366
unsigned Integer::isPow2() const
519
{
520
407366
  if (d_value <= 0) return 0;
521
  // power2p returns n such that d_value = 2^(n-1)
522
396380
  return cln::power2p(d_value);
523
}
524
525
276985
size_t Integer::length() const
526
{
527
276985
  int s = sgn();
528
276985
  if (s == 0)
529
  {
530
39314
    return 1;
531
  }
532
237671
  else if (s < 0)
533
  {
534
102077
    size_t len = cln::integer_length(d_value);
535
    /*If this is -2^n, return len+1 not len to stay consistent with the
536
     * definition above! From CLN's documentation of integer_length: This is
537
     * the smallest n >= 0 such that -2^n <= x < 2^n. If x > 0, this is the
538
     * unique n > 0 such that 2^(n-1) <= x < 2^n.
539
     */
540
102077
    size_t ord2 = cln::ord2(d_value);
541
102077
    return (len == ord2) ? (len + 1) : len;
542
  }
543
  else
544
  {
545
135594
    return cln::integer_length(d_value);
546
  }
547
}
548
549
46
void Integer::extendedGcd(
550
    Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b)
551
{
552
46
  g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
553
46
}
554
555
const Integer& Integer::min(const Integer& a, const Integer& b)
556
{
557
  return (a <= b) ? a : b;
558
}
559
560
const Integer& Integer::max(const Integer& a, const Integer& b)
561
{
562
  return (a >= b) ? a : b;
563
}
564
565
3559
std::ostream& operator<<(std::ostream& os, const Integer& n)
566
{
567
3559
  return os << n.toString();
568
}
569
29577
}  // namespace cvc5