Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * A multiprecision integer constant; wraps a CLN multiprecision integer.
11 : : */
12 : :
13 : : #include <cln/input.h>
14 : : #include <cln/integer_io.h>
15 : : #include <cln/modinteger.h>
16 : : #include <cln/numtheory.h>
17 : :
18 : : #include <iostream>
19 : : #include <limits>
20 : : #include <sstream>
21 : : #include <string>
22 : :
23 : : #include "base/cvc5config.h"
24 : : #include "util/integer.h"
25 : :
26 : : #ifndef CVC5_CLN_IMP
27 : : #error "This source should only ever be built if CVC5_CLN_IMP is on !"
28 : : #endif /* CVC5_CLN_IMP */
29 : :
30 : : #include "base/check.h"
31 : : #include "util/random.h"
32 : :
33 : : using namespace std;
34 : :
35 : : namespace cvc5::internal {
36 : :
37 : : signed int Integer::s_fastSignedIntMin = -(1 << 29);
38 : : signed int Integer::s_fastSignedIntMax = (1 << 29) - 1;
39 : : signed long Integer::s_slowSignedIntMin =
40 : : (signed long)std::numeric_limits<signed int>::min();
41 : : signed long Integer::s_slowSignedIntMax =
42 : : (signed long)std::numeric_limits<signed int>::max();
43 : :
44 : : unsigned int Integer::s_fastUnsignedIntMax = (1 << 29) - 1;
45 : : unsigned long Integer::s_slowUnsignedIntMax =
46 : : (unsigned long)std::numeric_limits<unsigned int>::max();
47 : :
48 : : unsigned long Integer::s_signedLongMin =
49 : : std::numeric_limits<signed long>::min();
50 : : unsigned long Integer::s_signedLongMax =
51 : : std::numeric_limits<signed long>::max();
52 : : unsigned long Integer::s_unsignedLongMax =
53 : : std::numeric_limits<unsigned long>::max();
54 : :
55 : 43489915 : Integer& Integer::operator=(const Integer& x)
56 : : {
57 [ + + ]: 43489915 : if (this == &x) return *this;
58 : 43489393 : d_value = x.d_value;
59 : 43489393 : return *this;
60 : : }
61 : :
62 : 25947790 : bool Integer::operator==(const Integer& y) const
63 : : {
64 : 25947790 : return d_value == y.d_value;
65 : : }
66 : :
67 : 6212166 : Integer Integer::operator-() const { return Integer(-(d_value)); }
68 : :
69 : 1289479 : bool Integer::operator!=(const Integer& y) const
70 : : {
71 : 1289479 : return d_value != y.d_value;
72 : : }
73 : :
74 : 3957849 : bool Integer::operator<(const Integer& y) const { return d_value < y.d_value; }
75 : :
76 : 1757355 : bool Integer::operator<=(const Integer& y) const
77 : : {
78 : 1757355 : return d_value <= y.d_value;
79 : : }
80 : :
81 : 2671852 : bool Integer::operator>(const Integer& y) const { return d_value > y.d_value; }
82 : :
83 : 4306391 : bool Integer::operator>=(const Integer& y) const
84 : : {
85 : 4306391 : return d_value >= y.d_value;
86 : : }
87 : :
88 : 12231483 : Integer Integer::operator+(const Integer& y) const
89 : : {
90 : 24462966 : return Integer(d_value + y.d_value);
91 : : }
92 : :
93 : 124399 : Integer& Integer::operator+=(const Integer& y)
94 : : {
95 : 124399 : d_value += y.d_value;
96 : 124399 : return *this;
97 : : }
98 : :
99 : 2597399 : Integer Integer::operator-(const Integer& y) const
100 : : {
101 : 5194798 : return Integer(d_value - y.d_value);
102 : : }
103 : :
104 : 3177 : Integer& Integer::operator-=(const Integer& y)
105 : : {
106 : 3177 : d_value -= y.d_value;
107 : 3177 : return *this;
108 : : }
109 : :
110 : 4480810 : Integer Integer::operator*(const Integer& y) const
111 : : {
112 : 8961620 : return Integer(d_value * y.d_value);
113 : : }
114 : :
115 : 5463 : Integer& Integer::operator*=(const Integer& y)
116 : : {
117 : 5463 : d_value *= y.d_value;
118 : 5463 : return *this;
119 : : }
120 : :
121 : 328769 : Integer Integer::bitwiseOr(const Integer& y) const
122 : : {
123 : 657538 : return Integer(cln::logior(d_value, y.d_value));
124 : : }
125 : :
126 : 662683 : Integer Integer::bitwiseAnd(const Integer& y) const
127 : : {
128 : 1325366 : return Integer(cln::logand(d_value, y.d_value));
129 : : }
130 : :
131 : 3383 : Integer Integer::bitwiseXor(const Integer& y) const
132 : : {
133 : 6766 : return Integer(cln::logxor(d_value, y.d_value));
134 : : }
135 : :
136 : 9993884 : Integer Integer::bitwiseNot() const { return Integer(cln::lognot(d_value)); }
137 : :
138 : 9735132 : Integer Integer::multiplyByPow2(uint32_t pow) const
139 : : {
140 : 9735132 : cln::cl_I ipow(pow);
141 : 29205396 : return Integer(d_value << ipow);
142 : 9735132 : }
143 : :
144 : 154192 : bool Integer::isBitSet(uint32_t i) const
145 : : {
146 : 154192 : return !extractBitRange(1, i).isZero();
147 : : }
148 : :
149 : 2344 : void Integer::setBit(uint32_t i, bool value)
150 : : {
151 : 2344 : cln::cl_I mask(1);
152 : 2344 : mask = mask << i;
153 [ + + ]: 2344 : if (value)
154 : : {
155 : 2330 : d_value = cln::logior(d_value, mask);
156 : : }
157 : : else
158 : : {
159 : 14 : mask = cln::lognot(mask);
160 : 14 : d_value = cln::logand(d_value, mask);
161 : : }
162 : 2344 : }
163 : :
164 : 1521040 : Integer Integer::oneExtend(uint32_t size, uint32_t amount) const
165 : : {
166 [ - + ][ - + ]: 1521040 : Assert((*this) < Integer(1).multiplyByPow2(size));
[ - - ]
167 : 1521040 : cln::cl_byte range(amount, size);
168 : 3042080 : cln::cl_I allones = (cln::cl_I(1) << (size + amount)) - 1; // 2^size - 1
169 : 1521040 : Integer temp(allones);
170 : :
171 : 4563120 : return Integer(cln::deposit_field(allones, d_value, range));
172 : 1521040 : }
173 : :
174 : 45982514 : uint32_t Integer::toUnsignedInt() const { return cln::cl_I_to_uint(d_value); }
175 : :
176 : 9724464 : Integer Integer::extractBitRange(uint32_t bitCount, uint32_t low) const
177 : : {
178 : 9724464 : cln::cl_byte range(bitCount, low);
179 : 19448928 : return Integer(cln::ldb(d_value, range));
180 : : }
181 : :
182 : 54325 : Integer Integer::floorDivideQuotient(const Integer& y) const
183 : : {
184 : 108650 : return Integer(cln::floor1(d_value, y.d_value));
185 : : }
186 : :
187 : 153240 : Integer Integer::floorDivideRemainder(const Integer& y) const
188 : : {
189 : 306480 : return Integer(cln::floor2(d_value, y.d_value).remainder);
190 : : }
191 : :
192 : 242009 : void Integer::floorQR(Integer& q,
193 : : Integer& r,
194 : : const Integer& x,
195 : : const Integer& y)
196 : : {
197 : 242009 : cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value);
198 : 242009 : q.d_value = res.quotient;
199 : 242009 : r.d_value = res.remainder;
200 : 242009 : }
201 : :
202 : 0 : Integer Integer::ceilingDivideQuotient(const Integer& y) const
203 : : {
204 : 0 : return Integer(cln::ceiling1(d_value, y.d_value));
205 : : }
206 : :
207 : 0 : Integer Integer::ceilingDivideRemainder(const Integer& y) const
208 : : {
209 : 0 : return Integer(cln::ceiling2(d_value, y.d_value).remainder);
210 : : }
211 : :
212 : 237383 : void Integer::euclidianQR(Integer& q,
213 : : Integer& r,
214 : : const Integer& x,
215 : : const Integer& y)
216 : : {
217 : : // compute the floor and then fix the value up if needed.
218 : 237383 : floorQR(q, r, x, y);
219 : :
220 [ + + ]: 237383 : if (r.strictlyNegative())
221 : : {
222 : : // if r < 0
223 : : // abs(r) < abs(y)
224 : : // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
225 : : // n = y * q + r
226 : : // n = y * q - abs(y) + r + abs(y)
227 [ - + ]: 26 : if (r.sgn() >= 0)
228 : : {
229 : : // y = abs(y)
230 : : // n = y * q - y + r + y
231 : : // n = y * (q-1) + (r+y)
232 : 0 : q -= 1;
233 : 0 : r += y;
234 : : }
235 : : else
236 : : {
237 : : // y = -abs(y)
238 : : // n = y * q + y + r - y
239 : : // n = y * (q+1) + (r-y)
240 : 26 : q += 1;
241 : 26 : r -= y;
242 : : }
243 : : }
244 : 237383 : }
245 : :
246 : 1852 : Integer Integer::euclidianDivideQuotient(const Integer& y) const
247 : : {
248 : 1852 : Integer q, r;
249 : 1852 : euclidianQR(q, r, *this, y);
250 : 3704 : return q;
251 : 1852 : }
252 : :
253 : 235523 : Integer Integer::euclidianDivideRemainder(const Integer& y) const
254 : : {
255 : 235523 : Integer q, r;
256 : 235523 : euclidianQR(q, r, *this, y);
257 : 471046 : return r;
258 : 235523 : }
259 : :
260 : 0 : Integer Integer::exactQuotient(const Integer& y) const
261 : : {
262 : 0 : Assert(y.divides(*this));
263 : 0 : return Integer(cln::exquo(d_value, y.d_value));
264 : : }
265 : :
266 : 40320354 : Integer Integer::modByPow2(uint32_t exp) const
267 : : {
268 : 40320354 : cln::cl_byte range(exp, 0);
269 : 80640708 : return Integer(cln::ldb(d_value, range));
270 : : }
271 : :
272 : 154408 : Integer Integer::divByPow2(uint32_t exp) const { return d_value >> exp; }
273 : :
274 : 190656 : Integer Integer::pow(uint32_t exp) const
275 : : {
276 [ + + ]: 190656 : if (exp == 0)
277 : : {
278 : 481 : return Integer(1);
279 : : }
280 : : else
281 : : {
282 [ - + ][ - + ]: 190175 : Assert(exp > 0);
[ - - ]
283 : 190175 : cln::cl_I result = cln::expt_pos(d_value, exp);
284 : 190175 : return Integer(result);
285 : 190175 : }
286 : : }
287 : :
288 : 5696202 : Integer Integer::gcd(const Integer& y) const
289 : : {
290 : 5696202 : cln::cl_I result = cln::gcd(d_value, y.d_value);
291 : 11392404 : return Integer(result);
292 : 5696202 : }
293 : :
294 : 18731154 : Integer Integer::lcm(const Integer& y) const
295 : : {
296 : 18731154 : cln::cl_I result = cln::lcm(d_value, y.d_value);
297 : 37462308 : return Integer(result);
298 : 18731154 : }
299 : :
300 : 7960 : Integer Integer::modAdd(const Integer& y, const Integer& m) const
301 : : {
302 : 7960 : cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
303 : 7960 : cln::cl_MI xm = ry->canonhom(d_value);
304 : 7960 : cln::cl_MI ym = ry->canonhom(y.d_value);
305 : 7960 : cln::cl_MI res = xm + ym;
306 : 23880 : return Integer(ry->retract(res));
307 : 7960 : }
308 : :
309 : 8853 : Integer Integer::modMultiply(const Integer& y, const Integer& m) const
310 : : {
311 : 8853 : cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
312 : 8853 : cln::cl_MI xm = ry->canonhom(d_value);
313 : 8853 : cln::cl_MI ym = ry->canonhom(y.d_value);
314 : 8853 : cln::cl_MI res = xm * ym;
315 : 26559 : return Integer(ry->retract(res));
316 : 8853 : }
317 : :
318 : 512 : Integer Integer::modInverse(const Integer& m) const
319 : : {
320 [ - + ][ - + ]: 512 : Assert(m > 0) << "m must be greater than zero";
[ - - ]
321 : 512 : cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
322 : 512 : cln::cl_MI xm = ry->canonhom(d_value);
323 : : /* normalize to modulo m for coprime check */
324 : 512 : cln::cl_I x = ry->retract(xm);
325 : 512 : if (x == 0 || cln::gcd(x, m.d_value) != 1)
326 : : {
327 : 13 : return Integer(-1);
328 : : }
329 : 499 : cln::cl_MI res = cln::recip(xm);
330 : 998 : return Integer(ry->retract(res));
331 : 512 : }
332 : :
333 : 66380 : bool Integer::divides(const Integer& y) const
334 : : {
335 : 66380 : cln::cl_I result = cln::rem(y.d_value, d_value);
336 : 132760 : return cln::zerop(result);
337 : 66380 : }
338 : :
339 [ + + ]: 30147084 : Integer Integer::abs() const { return d_value >= 0 ? *this : -*this; }
340 : :
341 : 237379 : std::string Integer::toString(int base) const
342 : : {
343 : 237379 : std::stringstream ss;
344 [ + - ][ + + ]: 237379 : switch (base)
[ - ]
345 : : {
346 : 72917 : case 2: fprintbinary(ss, d_value); break;
347 : 0 : case 8: fprintoctal(ss, d_value); break;
348 : 163996 : case 10: fprintdecimal(ss, d_value); break;
349 : 466 : case 16: fprinthexadecimal(ss, d_value); break;
350 : 0 : default: throw Exception("Unhandled base in Integer::toString()");
351 : : }
352 : 237379 : std::string output = ss.str();
353 [ + + ]: 2311488 : for (unsigned i = 0; i <= output.length(); ++i)
354 : : {
355 [ + + ]: 2074109 : if (isalpha(output[i]))
356 : : {
357 : 464 : output.replace(i, 1, 1, tolower(output[i]));
358 : : }
359 : : }
360 : :
361 : 474758 : return output;
362 : 237379 : }
363 : :
364 : 44092953 : int Integer::sgn() const
365 : : {
366 : 44092953 : cln::cl_I sgn = cln::signum(d_value);
367 : 88185906 : return cln::cl_I_to_int(sgn);
368 : 44092953 : }
369 : :
370 : 61 : bool Integer::strictlyPositive() const { return cln::plusp(d_value); }
371 : :
372 : 458451 : bool Integer::strictlyNegative() const { return cln::minusp(d_value); }
373 : :
374 : 8850793 : bool Integer::isZero() const { return cln::zerop(d_value); }
375 : :
376 : 24376245 : bool Integer::isOne() const { return d_value == 1; }
377 : :
378 : 0 : bool Integer::isNegativeOne() const { return d_value == -1; }
379 : :
380 : 445414 : void Integer::parseInt(const std::string& s, unsigned base)
381 : : {
382 : : cln::cl_read_flags flags;
383 : 445414 : flags.syntax = cln::syntax_integer;
384 : 445414 : flags.lsyntax = cln::lsyntax_standard;
385 : 445414 : flags.rational_base = base;
386 [ + + ]: 445414 : if (base == 0)
387 : : {
388 : : // infer base in a manner consistent with GMP
389 [ + + ]: 8 : if (s[0] == '0')
390 : : {
391 : 5 : flags.lsyntax = cln::lsyntax_commonlisp;
392 : 5 : std::string st = s;
393 [ + - ][ + + ]: 5 : if (s[1] == 'X' || s[1] == 'x')
[ + + ]
394 : : {
395 : 2 : st.replace(0, 2, "#x");
396 : : }
397 [ + - ][ + + ]: 3 : else if (s[1] == 'B' || s[1] == 'b')
[ + + ]
398 : : {
399 : 2 : st.replace(0, 2, "#b");
400 : : }
401 : : else
402 : : {
403 : 1 : st.replace(0, 1, "#o");
404 : : }
405 : 5 : readInt(flags, st, base);
406 : 4 : return;
407 : 5 : }
408 : : else
409 : : {
410 : 3 : flags.rational_base = 10;
411 : : }
412 : : }
413 : 445409 : readInt(flags, s, base);
414 : : }
415 : :
416 : 445414 : void Integer::readInt(const cln::cl_read_flags& flags,
417 : : const std::string& s,
418 : : unsigned base)
419 : : {
420 : : try
421 : : {
422 : : // Removing leading zeroes, CLN has a bug for these inputs up to and
423 : : // including CLN v1.3.2.
424 : : // See
425 : : // http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a
426 : : // for details.
427 : 445414 : size_t pos = s.find_first_not_of('0');
428 [ + + ]: 445414 : if (pos == std::string::npos)
429 : : {
430 : 110233 : d_value = cln::read_integer(flags, "0", NULL, NULL);
431 : : }
432 : : else
433 : : {
434 : 335181 : const char* cstr = s.c_str();
435 : 335181 : const char* start = cstr + pos;
436 : 335181 : const char* end = cstr + s.length();
437 : 335181 : d_value = cln::read_integer(flags, start, end, NULL);
438 : : }
439 : : }
440 : 399 : catch (...)
441 : : {
442 : 399 : std::stringstream ss;
443 : 399 : ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
444 : 399 : throw std::invalid_argument(ss.str());
445 : 798 : }
446 : 445015 : }
447 : :
448 : 782 : bool Integer::fitsSignedInt() const
449 : : {
450 : : // http://www.ginac.de/CLN/cln.html#Conversions
451 : : // TODO improve performance
452 [ - + ][ - + ]: 782 : Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
[ - - ]
453 [ - + ][ - + ]: 782 : Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
[ - - ]
454 [ - + ][ - + ]: 782 : Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
[ - - ]
455 : :
456 : 782 : return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax)
457 : 1564 : && (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
458 : : }
459 : :
460 : 43689195 : bool Integer::fitsUnsignedInt() const
461 : : {
462 : : // TODO improve performance
463 [ - + ][ - + ]: 43689195 : Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
[ - - ]
464 : 87378390 : return sgn() >= 0
465 [ + + ][ + + ]: 87379148 : && (d_value <= s_fastUnsignedIntMax
[ - - ]
466 [ + + ][ + + ]: 87379148 : || d_value <= s_slowUnsignedIntMax);
[ + + ][ - - ]
467 : : }
468 : :
469 : 782 : signed int Integer::getSignedInt() const
470 : : {
471 : : // ensure there isn't overflow
472 [ - + ][ - + ]: 782 : Assert(fitsSignedInt()) << "Overflow detected in Integer::getSignedInt()";
[ - - ]
473 : 782 : return cln::cl_I_to_int(d_value);
474 : : }
475 : :
476 : 20613 : unsigned int Integer::getUnsignedInt() const
477 : : {
478 : : // ensure there isn't overflow
479 [ - + ][ - + ]: 20613 : Assert(fitsUnsignedInt()) << "Overflow detected in Integer::getUnsignedInt()";
[ - - ]
480 : 20613 : return cln::cl_I_to_uint(d_value);
481 : : }
482 : :
483 : 3509 : long Integer::getLong() const
484 : : {
485 : : // ensure there isn't overflow
486 [ - + ][ - + ]: 3509 : Assert(d_value <= std::numeric_limits<long>::max())
[ - - ]
487 : 0 : << "Overflow detected in Integer::getLong()";
488 [ - + ][ - + ]: 3509 : Assert(d_value >= std::numeric_limits<long>::min())
[ - - ]
489 : 0 : << "Overflow detected in Integer::getLong()";
490 : 3509 : return cln::cl_I_to_long(d_value);
491 : : }
492 : :
493 : 1099 : unsigned long Integer::getUnsignedLong() const
494 : : {
495 : : // ensure there isn't overflow
496 [ - + ][ - + ]: 1099 : Assert(d_value <= std::numeric_limits<unsigned long>::max())
[ - - ]
497 : 0 : << "Overflow detected in Integer::getUnsignedLong()";
498 [ - + ][ - + ]: 1099 : Assert(d_value >= std::numeric_limits<unsigned long>::min())
[ - - ]
499 : 0 : << "Overflow detected in Integer::getUnsignedLong()";
500 : 1099 : return cln::cl_I_to_ulong(d_value);
501 : : }
502 : :
503 : 1293 : int64_t Integer::getSigned64() const
504 : : {
505 : : if constexpr (sizeof(int64_t) == sizeof(signed long int))
506 : : {
507 : 1293 : return getLong();
508 : : }
509 : : else
510 : : {
511 : : if (std::numeric_limits<long>::min() <= d_value
512 : : && d_value <= std::numeric_limits<long>::max())
513 : : {
514 : : return getLong();
515 : : }
516 : : // ensure there isn't overflow
517 : : Assert(d_value <= std::numeric_limits<int64_t>::max())
518 : : << "Overflow detected in Integer::getSigned64()";
519 : : Assert(d_value >= std::numeric_limits<int64_t>::min())
520 : : << "Overflow detected in Integer::getSigned64()";
521 : : return std::stoll(toString());
522 : : }
523 : : }
524 : 1067 : uint64_t Integer::getUnsigned64() const
525 : : {
526 : : if constexpr (sizeof(uint64_t) == sizeof(unsigned long int))
527 : : {
528 : 1067 : return getUnsignedLong();
529 : : }
530 : : else
531 : : {
532 : : if (std::numeric_limits<unsigned long>::min() <= d_value
533 : : && d_value <= std::numeric_limits<unsigned long>::max())
534 : : {
535 : : return getUnsignedLong();
536 : : }
537 : : // ensure there isn't overflow
538 : : Assert(d_value <= std::numeric_limits<uint64_t>::max())
539 : : << "Overflow detected in Integer::getSigned64()";
540 : : Assert(d_value >= std::numeric_limits<uint64_t>::min())
541 : : << "Overflow detected in Integer::getSigned64()";
542 : : return std::stoull(toString());
543 : : }
544 : : }
545 : :
546 : 5591498 : size_t Integer::hash() const { return equal_hashcode(d_value); }
547 : :
548 : 15467 : bool Integer::testBit(unsigned n) const { return cln::logbitp(n, d_value); }
549 : :
550 : 196363 : unsigned Integer::isPow2() const
551 : : {
552 [ + + ]: 196363 : if (d_value <= 0) return 0;
553 : : // power2p returns n such that d_value = 2^(n-1)
554 : 179722 : return cln::power2p(d_value);
555 : : }
556 : :
557 : 331770 : size_t Integer::length() const
558 : : {
559 : 331770 : int s = sgn();
560 [ + + ]: 331770 : if (s == 0)
561 : : {
562 : 57152 : return 1;
563 : : }
564 [ + + ]: 274618 : else if (s < 0)
565 : : {
566 : 113824 : size_t len = cln::integer_length(d_value);
567 : : /*If this is -2^n, return len+1 not len to stay consistent with the
568 : : * definition above! From CLN's documentation of integer_length: This is
569 : : * the smallest n >= 0 such that -2^n <= x < 2^n. If x > 0, this is the
570 : : * unique n > 0 such that 2^(n-1) <= x < 2^n.
571 : : */
572 : 113824 : size_t ord2 = cln::ord2(d_value);
573 [ + + ]: 113824 : return (len == ord2) ? (len + 1) : len;
574 : : }
575 : : else
576 : : {
577 : 160794 : return cln::integer_length(d_value);
578 : : }
579 : : }
580 : :
581 : 76248 : bool Integer::isProbablePrime() const { return cln::isprobprime(d_value); }
582 : :
583 : 282 : void Integer::extendedGcd(
584 : : Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b)
585 : : {
586 : 282 : g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
587 : 282 : }
588 : :
589 : 0 : const Integer& Integer::min(const Integer& a, const Integer& b)
590 : : {
591 [ - - ]: 0 : return (a <= b) ? a : b;
592 : : }
593 : :
594 : 0 : const Integer& Integer::max(const Integer& a, const Integer& b)
595 : : {
596 [ - - ]: 0 : return (a >= b) ? a : b;
597 : : }
598 : :
599 : 247 : Integer Integer::mkRandom(uint32_t nbits)
600 : : {
601 [ - + ][ - + ]: 247 : Assert(nbits > 0);
[ - - ]
602 : 247 : Random& rnd = Random::getRandom();
603 : 247 : cln::cl_I max(2);
604 : 247 : max = cln::expt_pos(max, nbits);
605 : 247 : cln::cl_I res = cln::random_I(*rnd.getCLNRandstate(), max);
606 : 494 : return Integer(res);
607 : 247 : }
608 : :
609 : 151699 : std::ostream& operator<<(std::ostream& os, const Integer& n)
610 : : {
611 : 151699 : return os << n.toString();
612 : : }
613 : : } // namespace cvc5::internal
|
