Branch data Line data Source code
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-2025 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 : :
16 : : #include <cln/input.h>
17 : : #include <cln/integer_io.h>
18 : : #include <cln/modinteger.h>
19 : : #include <cln/numtheory.h>
20 : :
21 : : #include <iostream>
22 : : #include <sstream>
23 : : #include <string>
24 : :
25 : : #include "base/cvc5config.h"
26 : : #include "util/integer.h"
27 : :
28 : : #ifndef CVC5_CLN_IMP
29 : : #error "This source should only ever be built if CVC5_CLN_IMP is on !"
30 : : #endif /* CVC5_CLN_IMP */
31 : :
32 : : #include "base/check.h"
33 : :
34 : : using namespace std;
35 : :
36 : : namespace cvc5::internal {
37 : :
38 : : signed int Integer::s_fastSignedIntMin = -(1 << 29);
39 : : signed int Integer::s_fastSignedIntMax = (1 << 29) - 1;
40 : : signed long Integer::s_slowSignedIntMin =
41 : : (signed long)std::numeric_limits<signed int>::min();
42 : : signed long Integer::s_slowSignedIntMax =
43 : : (signed long)std::numeric_limits<signed int>::max();
44 : :
45 : : unsigned int Integer::s_fastUnsignedIntMax = (1 << 29) - 1;
46 : : unsigned long Integer::s_slowUnsignedIntMax =
47 : : (unsigned long)std::numeric_limits<unsigned int>::max();
48 : :
49 : : unsigned long Integer::s_signedLongMin =
50 : : std::numeric_limits<signed long>::min();
51 : : unsigned long Integer::s_signedLongMax =
52 : : std::numeric_limits<signed long>::max();
53 : : unsigned long Integer::s_unsignedLongMax =
54 : : std::numeric_limits<unsigned long>::max();
55 : :
56 : 57064200 : Integer& Integer::operator=(const Integer& x)
57 : : {
58 [ - + ]: 57064200 : if (this == &x) return *this;
59 : 57064200 : d_value = x.d_value;
60 : 57064200 : return *this;
61 : : }
62 : :
63 : 32286800 : bool Integer::operator==(const Integer& y) const
64 : : {
65 : 32286800 : return d_value == y.d_value;
66 : : }
67 : :
68 : 5551380 : Integer Integer::operator-() const { return Integer(-(d_value)); }
69 : :
70 : 1103360 : bool Integer::operator!=(const Integer& y) const
71 : : {
72 : 1103360 : return d_value != y.d_value;
73 : : }
74 : :
75 : 9017720 : bool Integer::operator<(const Integer& y) const { return d_value < y.d_value; }
76 : :
77 : 5537960 : bool Integer::operator<=(const Integer& y) const
78 : : {
79 : 5537960 : return d_value <= y.d_value;
80 : : }
81 : :
82 : 7951440 : bool Integer::operator>(const Integer& y) const { return d_value > y.d_value; }
83 : :
84 : 12360100 : bool Integer::operator>=(const Integer& y) const
85 : : {
86 : 12360100 : return d_value >= y.d_value;
87 : : }
88 : :
89 : 36062000 : Integer Integer::operator+(const Integer& y) const
90 : : {
91 : 72124100 : return Integer(d_value + y.d_value);
92 : : }
93 : :
94 : 112194 : Integer& Integer::operator+=(const Integer& y)
95 : : {
96 : 112194 : d_value += y.d_value;
97 : 112194 : return *this;
98 : : }
99 : :
100 : 2675910 : Integer Integer::operator-(const Integer& y) const
101 : : {
102 : 5351820 : return Integer(d_value - y.d_value);
103 : : }
104 : :
105 : 3126 : Integer& Integer::operator-=(const Integer& y)
106 : : {
107 : 3126 : d_value -= y.d_value;
108 : 3126 : return *this;
109 : : }
110 : :
111 : 12535700 : Integer Integer::operator*(const Integer& y) const
112 : : {
113 : 25071500 : return Integer(d_value * y.d_value);
114 : : }
115 : :
116 : 5214 : Integer& Integer::operator*=(const Integer& y)
117 : : {
118 : 5214 : d_value *= y.d_value;
119 : 5214 : return *this;
120 : : }
121 : :
122 : 520030 : Integer Integer::bitwiseOr(const Integer& y) const
123 : : {
124 : 1040060 : return Integer(cln::logior(d_value, y.d_value));
125 : : }
126 : :
127 : 1727000 : Integer Integer::bitwiseAnd(const Integer& y) const
128 : : {
129 : 3454000 : return Integer(cln::logand(d_value, y.d_value));
130 : : }
131 : :
132 : 2965 : Integer Integer::bitwiseXor(const Integer& y) const
133 : : {
134 : 5930 : return Integer(cln::logxor(d_value, y.d_value));
135 : : }
136 : :
137 : 28679900 : Integer Integer::bitwiseNot() const { return Integer(cln::lognot(d_value)); }
138 : :
139 : 27529000 : Integer Integer::multiplyByPow2(uint32_t pow) const
140 : : {
141 : 27529000 : cln::cl_I ipow(pow);
142 : 82587100 : return Integer(d_value << ipow);
143 : : }
144 : :
145 : 136943 : bool Integer::isBitSet(uint32_t i) const
146 : : {
147 : 136943 : return !extractBitRange(1, i).isZero();
148 : : }
149 : :
150 : 2269 : void Integer::setBit(uint32_t i, bool value)
151 : : {
152 : 4538 : cln::cl_I mask(1);
153 : 2269 : mask = mask << i;
154 [ + + ]: 2269 : if (value)
155 : : {
156 : 2255 : d_value = cln::logior(d_value, mask);
157 : : }
158 : : else
159 : : {
160 : 14 : mask = cln::lognot(mask);
161 : 14 : d_value = cln::logand(d_value, mask);
162 : : }
163 : 2269 : }
164 : :
165 : 1498680 : Integer Integer::oneExtend(uint32_t size, uint32_t amount) const
166 : : {
167 [ - + ][ - + ]: 1498680 : Assert((*this) < Integer(1).multiplyByPow2(size));
[ - - ]
168 : 1498680 : cln::cl_byte range(amount, size);
169 : 4496040 : cln::cl_I allones = (cln::cl_I(1) << (size + amount)) - 1; // 2^size - 1
170 : 1498680 : Integer temp(allones);
171 : :
172 : 4496040 : return Integer(cln::deposit_field(allones, d_value, range));
173 : : }
174 : :
175 : 26250000 : uint32_t Integer::toUnsignedInt() const { return cln::cl_I_to_uint(d_value); }
176 : :
177 : 26791200 : Integer Integer::extractBitRange(uint32_t bitCount, uint32_t low) const
178 : : {
179 : 26791200 : cln::cl_byte range(bitCount, low);
180 : 53582300 : return Integer(cln::ldb(d_value, range));
181 : : }
182 : :
183 : 60935 : Integer Integer::floorDivideQuotient(const Integer& y) const
184 : : {
185 : 121870 : return Integer(cln::floor1(d_value, y.d_value));
186 : : }
187 : :
188 : 158648 : Integer Integer::floorDivideRemainder(const Integer& y) const
189 : : {
190 : 317296 : return Integer(cln::floor2(d_value, y.d_value).remainder);
191 : : }
192 : :
193 : 164299 : void Integer::floorQR(Integer& q,
194 : : Integer& r,
195 : : const Integer& x,
196 : : const Integer& y)
197 : : {
198 : 328598 : cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value);
199 : 164299 : q.d_value = res.quotient;
200 : 164299 : r.d_value = res.remainder;
201 : 164299 : }
202 : :
203 : 0 : Integer Integer::ceilingDivideQuotient(const Integer& y) const
204 : : {
205 : 0 : return Integer(cln::ceiling1(d_value, y.d_value));
206 : : }
207 : :
208 : 0 : Integer Integer::ceilingDivideRemainder(const Integer& y) const
209 : : {
210 : 0 : return Integer(cln::ceiling2(d_value, y.d_value).remainder);
211 : : }
212 : :
213 : 162823 : void Integer::euclidianQR(Integer& q,
214 : : Integer& r,
215 : : const Integer& x,
216 : : const Integer& y)
217 : : {
218 : : // compute the floor and then fix the value up if needed.
219 : 162823 : floorQR(q, r, x, y);
220 : :
221 [ + + ]: 162823 : if (r.strictlyNegative())
222 : : {
223 : : // if r < 0
224 : : // abs(r) < abs(y)
225 : : // - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
226 : : // n = y * q + r
227 : : // n = y * q - abs(y) + r + abs(y)
228 [ - + ]: 30 : if (r.sgn() >= 0)
229 : : {
230 : : // y = abs(y)
231 : : // n = y * q - y + r + y
232 : : // n = y * (q-1) + (r+y)
233 : 0 : q -= 1;
234 : 0 : r += y;
235 : : }
236 : : else
237 : : {
238 : : // y = -abs(y)
239 : : // n = y * q + y + r - y
240 : : // n = y * (q+1) + (r-y)
241 : 30 : q += 1;
242 : 30 : r -= y;
243 : : }
244 : : }
245 : 162823 : }
246 : :
247 : 1783 : Integer Integer::euclidianDivideQuotient(const Integer& y) const
248 : : {
249 : 3566 : Integer q, r;
250 : 1783 : euclidianQR(q, r, *this, y);
251 : 3566 : return q;
252 : : }
253 : :
254 : 161032 : Integer Integer::euclidianDivideRemainder(const Integer& y) const
255 : : {
256 : 322064 : Integer q, r;
257 : 161032 : euclidianQR(q, r, *this, y);
258 : 322064 : return r;
259 : : }
260 : :
261 : 0 : Integer Integer::exactQuotient(const Integer& y) const
262 : : {
263 : 0 : Assert(y.divides(*this));
264 : 0 : return Integer(cln::exquo(d_value, y.d_value));
265 : : }
266 : :
267 : 98529300 : Integer Integer::modByPow2(uint32_t exp) const
268 : : {
269 : 98529300 : cln::cl_byte range(exp, 0);
270 : 197059000 : return Integer(cln::ldb(d_value, range));
271 : : }
272 : :
273 : 453350 : Integer Integer::divByPow2(uint32_t exp) const { return d_value >> exp; }
274 : :
275 : 153214 : Integer Integer::pow(uint32_t exp) const
276 : : {
277 [ + + ]: 153214 : if (exp == 0)
278 : : {
279 : 452 : return Integer(1);
280 : : }
281 : : else
282 : : {
283 [ - + ][ - + ]: 152762 : Assert(exp > 0);
[ - - ]
284 : 305524 : cln::cl_I result = cln::expt_pos(d_value, exp);
285 : 152762 : return Integer(result);
286 : : }
287 : : }
288 : :
289 : 5219230 : Integer Integer::gcd(const Integer& y) const
290 : : {
291 : 10438500 : cln::cl_I result = cln::gcd(d_value, y.d_value);
292 : 10438500 : return Integer(result);
293 : : }
294 : :
295 : 17722000 : Integer Integer::lcm(const Integer& y) const
296 : : {
297 : 35444100 : cln::cl_I result = cln::lcm(d_value, y.d_value);
298 : 35444100 : return Integer(result);
299 : : }
300 : :
301 : 7815 : Integer Integer::modAdd(const Integer& y, const Integer& m) const
302 : : {
303 : 15630 : cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
304 : 15630 : cln::cl_MI xm = ry->canonhom(d_value);
305 : 15630 : cln::cl_MI ym = ry->canonhom(y.d_value);
306 : 7815 : cln::cl_MI res = xm + ym;
307 : 23445 : return Integer(ry->retract(res));
308 : : }
309 : :
310 : 8791 : Integer Integer::modMultiply(const Integer& y, const Integer& m) const
311 : : {
312 : 17582 : cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
313 : 17582 : cln::cl_MI xm = ry->canonhom(d_value);
314 : 17582 : cln::cl_MI ym = ry->canonhom(y.d_value);
315 : 8791 : cln::cl_MI res = xm * ym;
316 : 26373 : return Integer(ry->retract(res));
317 : : }
318 : :
319 : 429 : Integer Integer::modInverse(const Integer& m) const
320 : : {
321 [ - + ][ - + ]: 429 : Assert(m > 0) << "m must be greater than zero";
[ - - ]
322 : 858 : cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
323 : 858 : cln::cl_MI xm = ry->canonhom(d_value);
324 : : /* normalize to modulo m for coprime check */
325 : 858 : cln::cl_I x = ry->retract(xm);
326 : 429 : if (x == 0 || cln::gcd(x, m.d_value) != 1)
327 : : {
328 : 13 : return Integer(-1);
329 : : }
330 : 416 : cln::cl_MI res = cln::recip(xm);
331 : 832 : return Integer(ry->retract(res));
332 : : }
333 : :
334 : 56893 : bool Integer::divides(const Integer& y) const
335 : : {
336 : 113786 : cln::cl_I result = cln::rem(y.d_value, d_value);
337 : 113786 : return cln::zerop(result);
338 : : }
339 : :
340 [ + + ]: 27984400 : Integer Integer::abs() const { return d_value >= 0 ? *this : -*this; }
341 : :
342 : 309748 : std::string Integer::toString(int base) const
343 : : {
344 : 619496 : std::stringstream ss;
345 [ + - ][ + + ]: 309748 : switch (base)
[ - ]
346 : : {
347 : 173816 : case 2: fprintbinary(ss, d_value); break;
348 : 0 : case 8: fprintoctal(ss, d_value); break;
349 : 135466 : case 10: fprintdecimal(ss, d_value); break;
350 : 466 : case 16: fprinthexadecimal(ss, d_value); break;
351 : 0 : default: throw Exception("Unhandled base in Integer::toString()");
352 : : }
353 : 309748 : std::string output = ss.str();
354 [ + + ]: 2271160 : for (unsigned i = 0; i <= output.length(); ++i)
355 : : {
356 [ + + ]: 1961420 : if (isalpha(output[i]))
357 : : {
358 : 464 : output.replace(i, 1, 1, tolower(output[i]));
359 : : }
360 : : }
361 : :
362 : 619496 : return output;
363 : : }
364 : :
365 : 19460700 : int Integer::sgn() const
366 : : {
367 : 38921400 : cln::cl_I sgn = cln::signum(d_value);
368 : 38921400 : return cln::cl_I_to_int(sgn);
369 : : }
370 : :
371 : 61 : bool Integer::strictlyPositive() const { return cln::plusp(d_value); }
372 : :
373 : 382754 : bool Integer::strictlyNegative() const { return cln::minusp(d_value); }
374 : :
375 : 7169810 : bool Integer::isZero() const { return cln::zerop(d_value); }
376 : :
377 : 24116800 : bool Integer::isOne() const { return d_value == 1; }
378 : :
379 : 0 : bool Integer::isNegativeOne() const { return d_value == -1; }
380 : :
381 : 587993 : void Integer::parseInt(const std::string& s, unsigned base)
382 : : {
383 : : cln::cl_read_flags flags;
384 : 587993 : flags.syntax = cln::syntax_integer;
385 : 587993 : flags.lsyntax = cln::lsyntax_standard;
386 : 587993 : flags.rational_base = base;
387 [ + + ]: 587993 : if (base == 0)
388 : : {
389 : : // infer base in a manner consistent with GMP
390 [ + + ]: 8 : if (s[0] == '0')
391 : : {
392 : 5 : flags.lsyntax = cln::lsyntax_commonlisp;
393 : 6 : std::string st = s;
394 [ + - ][ + + ]: 5 : if (s[1] == 'X' || s[1] == 'x')
[ + + ]
395 : : {
396 : 2 : st.replace(0, 2, "#x");
397 : : }
398 [ + - ][ + + ]: 3 : else if (s[1] == 'B' || s[1] == 'b')
[ + + ]
399 : : {
400 : 2 : st.replace(0, 2, "#b");
401 : : }
402 : : else
403 : : {
404 : 1 : st.replace(0, 1, "#o");
405 : : }
406 : 5 : readInt(flags, st, base);
407 : 4 : return;
408 : : }
409 : : else
410 : : {
411 : 3 : flags.rational_base = 10;
412 : : }
413 : : }
414 : 587988 : readInt(flags, s, base);
415 : : }
416 : :
417 : 587993 : void Integer::readInt(const cln::cl_read_flags& flags,
418 : : const std::string& s,
419 : : unsigned base)
420 : : {
421 : : try
422 : : {
423 : : // Removing leading zeroes, CLN has a bug for these inputs up to and
424 : : // including CLN v1.3.2.
425 : : // See
426 : : // http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a
427 : : // for details.
428 : 587993 : size_t pos = s.find_first_not_of('0');
429 [ + + ]: 587993 : if (pos == std::string::npos)
430 : : {
431 : 119802 : d_value = cln::read_integer(flags, "0", NULL, NULL);
432 : : }
433 : : else
434 : : {
435 : 468191 : const char* cstr = s.c_str();
436 : 468191 : const char* start = cstr + pos;
437 : 468191 : const char* end = cstr + s.length();
438 : 468191 : d_value = cln::read_integer(flags, start, end, NULL);
439 : : }
440 : : }
441 : 798 : catch (...)
442 : : {
443 : 798 : std::stringstream ss;
444 : 399 : ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
445 : 399 : throw std::invalid_argument(ss.str());
446 : : }
447 : 587594 : }
448 : :
449 : 782 : bool Integer::fitsSignedInt() const
450 : : {
451 : : // http://www.ginac.de/CLN/cln.html#Conversions
452 : : // TODO improve performance
453 [ - + ][ - + ]: 782 : Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
[ - - ]
454 [ - + ][ - + ]: 782 : Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
[ - - ]
455 [ - + ][ - + ]: 782 : Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
[ - - ]
456 : :
457 : 782 : return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax)
458 : 1564 : && (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
459 : : }
460 : :
461 : 19124400 : bool Integer::fitsUnsignedInt() const
462 : : {
463 : : // TODO improve performance
464 [ - + ][ - + ]: 19124400 : Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
[ - - ]
465 : 38248700 : return sgn() >= 0
466 [ + + ][ + + ]: 38249500 : && (d_value <= s_fastUnsignedIntMax
[ - - ]
467 [ + + ][ + + ]: 38249500 : || d_value <= s_slowUnsignedIntMax);
[ + + ][ - - ]
468 : : }
469 : :
470 : 782 : signed int Integer::getSignedInt() const
471 : : {
472 : : // ensure there isn't overflow
473 [ - + ][ - + ]: 782 : Assert(fitsSignedInt()) << "Overflow detected in Integer::getSignedInt()";
[ - - ]
474 : 782 : return cln::cl_I_to_int(d_value);
475 : : }
476 : :
477 : 20517 : unsigned int Integer::getUnsignedInt() const
478 : : {
479 : : // ensure there isn't overflow
480 [ - + ][ - + ]: 20517 : Assert(fitsUnsignedInt()) << "Overflow detected in Integer::getUnsignedInt()";
[ - - ]
481 : 20517 : return cln::cl_I_to_uint(d_value);
482 : : }
483 : :
484 : 3509 : long Integer::getLong() const
485 : : {
486 : : // ensure there isn't overflow
487 [ - + ][ - + ]: 3509 : Assert(d_value <= std::numeric_limits<long>::max())
[ - - ]
488 : 0 : << "Overflow detected in Integer::getLong()";
489 [ - + ][ - + ]: 3509 : Assert(d_value >= std::numeric_limits<long>::min())
[ - - ]
490 : 0 : << "Overflow detected in Integer::getLong()";
491 : 3509 : return cln::cl_I_to_long(d_value);
492 : : }
493 : :
494 : 1099 : unsigned long Integer::getUnsignedLong() const
495 : : {
496 : : // ensure there isn't overflow
497 [ - + ][ - + ]: 1099 : Assert(d_value <= std::numeric_limits<unsigned long>::max())
[ - - ]
498 : 0 : << "Overflow detected in Integer::getUnsignedLong()";
499 [ - + ][ - + ]: 1099 : Assert(d_value >= std::numeric_limits<unsigned long>::min())
[ - - ]
500 : 0 : << "Overflow detected in Integer::getUnsignedLong()";
501 : 1099 : return cln::cl_I_to_ulong(d_value);
502 : : }
503 : :
504 : 1293 : int64_t Integer::getSigned64() const
505 : : {
506 : : if constexpr (sizeof(int64_t) == sizeof(signed long int))
507 : : {
508 : 1293 : return getLong();
509 : : }
510 : : else
511 : : {
512 : : if (std::numeric_limits<long>::min() <= d_value
513 : : && d_value <= std::numeric_limits<long>::max())
514 : : {
515 : : return getLong();
516 : : }
517 : : // ensure there isn't overflow
518 : : Assert(d_value <= std::numeric_limits<int64_t>::max())
519 : : << "Overflow detected in Integer::getSigned64()";
520 : : Assert(d_value >= std::numeric_limits<int64_t>::min())
521 : : << "Overflow detected in Integer::getSigned64()";
522 : : return std::stoll(toString());
523 : : }
524 : : }
525 : 1067 : uint64_t Integer::getUnsigned64() const
526 : : {
527 : : if constexpr (sizeof(uint64_t) == sizeof(unsigned long int))
528 : : {
529 : 1067 : return getUnsignedLong();
530 : : }
531 : : else
532 : : {
533 : : if (std::numeric_limits<unsigned long>::min() <= d_value
534 : : && d_value <= std::numeric_limits<unsigned long>::max())
535 : : {
536 : : return getUnsignedLong();
537 : : }
538 : : // ensure there isn't overflow
539 : : Assert(d_value <= std::numeric_limits<uint64_t>::max())
540 : : << "Overflow detected in Integer::getSigned64()";
541 : : Assert(d_value >= std::numeric_limits<uint64_t>::min())
542 : : << "Overflow detected in Integer::getSigned64()";
543 : : return std::stoull(toString());
544 : : }
545 : : }
546 : :
547 : 5089860 : size_t Integer::hash() const { return equal_hashcode(d_value); }
548 : :
549 : 10397 : bool Integer::testBit(unsigned n) const { return cln::logbitp(n, d_value); }
550 : :
551 : 194342 : unsigned Integer::isPow2() const
552 : : {
553 [ + + ]: 194342 : if (d_value <= 0) return 0;
554 : : // power2p returns n such that d_value = 2^(n-1)
555 : 178397 : return cln::power2p(d_value);
556 : : }
557 : :
558 : 286594 : size_t Integer::length() const
559 : : {
560 : 286594 : int s = sgn();
561 [ + + ]: 286594 : if (s == 0)
562 : : {
563 : 51205 : return 1;
564 : : }
565 [ + + ]: 235389 : else if (s < 0)
566 : : {
567 : 96293 : size_t len = cln::integer_length(d_value);
568 : : /*If this is -2^n, return len+1 not len to stay consistent with the
569 : : * definition above! From CLN's documentation of integer_length: This is
570 : : * the smallest n >= 0 such that -2^n <= x < 2^n. If x > 0, this is the
571 : : * unique n > 0 such that 2^(n-1) <= x < 2^n.
572 : : */
573 : 96293 : size_t ord2 = cln::ord2(d_value);
574 [ + + ]: 96293 : return (len == ord2) ? (len + 1) : len;
575 : : }
576 : : else
577 : : {
578 : 139096 : return cln::integer_length(d_value);
579 : : }
580 : : }
581 : :
582 : 75209 : bool Integer::isProbablePrime() const { return cln::isprobprime(d_value); }
583 : :
584 : 72 : void Integer::extendedGcd(
585 : : Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b)
586 : : {
587 : 72 : g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
588 : 72 : }
589 : :
590 : 0 : const Integer& Integer::min(const Integer& a, const Integer& b)
591 : : {
592 [ - - ]: 0 : return (a <= b) ? a : b;
593 : : }
594 : :
595 : 0 : const Integer& Integer::max(const Integer& a, const Integer& b)
596 : : {
597 [ - - ]: 0 : return (a >= b) ? a : b;
598 : : }
599 : :
600 : 122901 : std::ostream& operator<<(std::ostream& os, const Integer& n)
601 : : {
602 : 122901 : return os << n.toString();
603 : : }
604 : : } // namespace cvc5::internal
|
