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 |
|
|
16 |
|
#include <cln/input.h> |
17 |
|
#include <cln/integer_io.h> |
18 |
|
#include <cln/modinteger.h> |
19 |
|
|
20 |
|
#include <iostream> |
21 |
|
#include <sstream> |
22 |
|
#include <string> |
23 |
|
|
24 |
|
#include "base/cvc5config.h" |
25 |
|
#include "util/integer.h" |
26 |
|
|
27 |
|
#ifndef CVC5_CLN_IMP |
28 |
|
#error "This source should only ever be built if CVC5_CLN_IMP is on !" |
29 |
|
#endif /* CVC5_CLN_IMP */ |
30 |
|
|
31 |
|
#include "base/check.h" |
32 |
|
|
33 |
|
using namespace std; |
34 |
|
|
35 |
|
namespace cvc5 { |
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 |
26459509 |
Integer& Integer::operator=(const Integer& x) |
56 |
|
{ |
57 |
26459509 |
if (this == &x) return *this; |
58 |
26459509 |
d_value = x.d_value; |
59 |
26459509 |
return *this; |
60 |
|
} |
61 |
|
|
62 |
399398305 |
bool Integer::operator==(const Integer& y) const |
63 |
|
{ |
64 |
399398305 |
return d_value == y.d_value; |
65 |
|
} |
66 |
|
|
67 |
653532 |
Integer Integer::operator-() const { return Integer(-(d_value)); } |
68 |
|
|
69 |
1121516 |
bool Integer::operator!=(const Integer& y) const |
70 |
|
{ |
71 |
1121516 |
return d_value != y.d_value; |
72 |
|
} |
73 |
|
|
74 |
1196140 |
bool Integer::operator<(const Integer& y) const { return d_value < y.d_value; } |
75 |
|
|
76 |
225400 |
bool Integer::operator<=(const Integer& y) const |
77 |
|
{ |
78 |
225400 |
return d_value <= y.d_value; |
79 |
|
} |
80 |
|
|
81 |
591698 |
bool Integer::operator>(const Integer& y) const { return d_value > y.d_value; } |
82 |
|
|
83 |
873499 |
bool Integer::operator>=(const Integer& y) const |
84 |
|
{ |
85 |
873499 |
return d_value >= y.d_value; |
86 |
|
} |
87 |
|
|
88 |
3607646 |
Integer Integer::operator+(const Integer& y) const |
89 |
|
{ |
90 |
3607646 |
return Integer(d_value + y.d_value); |
91 |
|
} |
92 |
|
|
93 |
68420 |
Integer& Integer::operator+=(const Integer& y) |
94 |
|
{ |
95 |
68420 |
d_value += y.d_value; |
96 |
68420 |
return *this; |
97 |
|
} |
98 |
|
|
99 |
1832298 |
Integer Integer::operator-(const Integer& y) const |
100 |
|
{ |
101 |
1832298 |
return Integer(d_value - y.d_value); |
102 |
|
} |
103 |
|
|
104 |
9235 |
Integer& Integer::operator-=(const Integer& y) |
105 |
|
{ |
106 |
9235 |
d_value -= y.d_value; |
107 |
9235 |
return *this; |
108 |
|
} |
109 |
|
|
110 |
1859189 |
Integer Integer::operator*(const Integer& y) const |
111 |
|
{ |
112 |
1859189 |
return Integer(d_value * y.d_value); |
113 |
|
} |
114 |
|
|
115 |
10082 |
Integer& Integer::operator*=(const Integer& y) |
116 |
|
{ |
117 |
10082 |
d_value *= y.d_value; |
118 |
10082 |
return *this; |
119 |
|
} |
120 |
|
|
121 |
417481 |
Integer Integer::bitwiseOr(const Integer& y) const |
122 |
|
{ |
123 |
417481 |
return Integer(cln::logior(d_value, y.d_value)); |
124 |
|
} |
125 |
|
|
126 |
284169 |
Integer Integer::bitwiseAnd(const Integer& y) const |
127 |
|
{ |
128 |
284169 |
return Integer(cln::logand(d_value, y.d_value)); |
129 |
|
} |
130 |
|
|
131 |
801 |
Integer Integer::bitwiseXor(const Integer& y) const |
132 |
|
{ |
133 |
801 |
return Integer(cln::logxor(d_value, y.d_value)); |
134 |
|
} |
135 |
|
|
136 |
1388232 |
Integer Integer::bitwiseNot() const { return Integer(cln::lognot(d_value)); } |
137 |
|
|
138 |
1971068 |
Integer Integer::multiplyByPow2(uint32_t pow) const |
139 |
|
{ |
140 |
3942136 |
cln::cl_I ipow(pow); |
141 |
3942136 |
return Integer(d_value << ipow); |
142 |
|
} |
143 |
|
|
144 |
92144 |
bool Integer::isBitSet(uint32_t i) const |
145 |
|
{ |
146 |
92144 |
return !extractBitRange(1, i).isZero(); |
147 |
|
} |
148 |
|
|
149 |
2715 |
void Integer::setBit(uint32_t i, bool value) |
150 |
|
{ |
151 |
5430 |
cln::cl_I mask(1); |
152 |
2715 |
mask = mask << i; |
153 |
2715 |
if (value) |
154 |
|
{ |
155 |
2687 |
d_value = cln::logior(d_value, mask); |
156 |
|
} |
157 |
|
else |
158 |
|
{ |
159 |
28 |
mask = cln::lognot(mask); |
160 |
28 |
d_value = cln::logand(d_value, mask); |
161 |
|
} |
162 |
2715 |
} |
163 |
|
|
164 |
837079 |
Integer Integer::oneExtend(uint32_t size, uint32_t amount) const |
165 |
|
{ |
166 |
837079 |
DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); |
167 |
837079 |
cln::cl_byte range(amount, size); |
168 |
1674158 |
cln::cl_I allones = (cln::cl_I(1) << (size + amount)) - 1; // 2^size - 1 |
169 |
1674158 |
Integer temp(allones); |
170 |
|
|
171 |
1674158 |
return Integer(cln::deposit_field(allones, d_value, range)); |
172 |
|
} |
173 |
|
|
174 |
1532086 |
uint32_t Integer::toUnsignedInt() const { return cln::cl_I_to_uint(d_value); } |
175 |
|
|
176 |
2200982 |
Integer Integer::extractBitRange(uint32_t bitCount, uint32_t low) const |
177 |
|
{ |
178 |
2200982 |
cln::cl_byte range(bitCount, low); |
179 |
2200982 |
return Integer(cln::ldb(d_value, range)); |
180 |
|
} |
181 |
|
|
182 |
53002 |
Integer Integer::floorDivideQuotient(const Integer& y) const |
183 |
|
{ |
184 |
53002 |
return Integer(cln::floor1(d_value, y.d_value)); |
185 |
|
} |
186 |
|
|
187 |
57441 |
Integer Integer::floorDivideRemainder(const Integer& y) const |
188 |
|
{ |
189 |
57441 |
return Integer(cln::floor2(d_value, y.d_value).remainder); |
190 |
|
} |
191 |
|
|
192 |
4664 |
void Integer::floorQR(Integer& q, |
193 |
|
Integer& r, |
194 |
|
const Integer& x, |
195 |
|
const Integer& y) |
196 |
|
{ |
197 |
9328 |
cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value); |
198 |
4664 |
q.d_value = res.quotient; |
199 |
4664 |
r.d_value = res.remainder; |
200 |
4664 |
} |
201 |
|
|
202 |
|
Integer Integer::ceilingDivideQuotient(const Integer& y) const |
203 |
|
{ |
204 |
|
return Integer(cln::ceiling1(d_value, y.d_value)); |
205 |
|
} |
206 |
|
|
207 |
|
Integer Integer::ceilingDivideRemainder(const Integer& y) const |
208 |
|
{ |
209 |
|
return Integer(cln::ceiling2(d_value, y.d_value).remainder); |
210 |
|
} |
211 |
|
|
212 |
3464 |
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 |
3464 |
floorQR(q, r, x, y); |
219 |
|
|
220 |
3464 |
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 |
8 |
if (r.sgn() >= 0) |
228 |
|
{ |
229 |
|
// y = abs(y) |
230 |
|
// n = y * q - y + r + y |
231 |
|
// n = y * (q-1) + (r+y) |
232 |
|
q -= 1; |
233 |
|
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 |
8 |
q += 1; |
241 |
8 |
r -= y; |
242 |
|
} |
243 |
|
} |
244 |
3464 |
} |
245 |
|
|
246 |
315 |
Integer Integer::euclidianDivideQuotient(const Integer& y) const |
247 |
|
{ |
248 |
630 |
Integer q, r; |
249 |
315 |
euclidianQR(q, r, *this, y); |
250 |
630 |
return q; |
251 |
|
} |
252 |
|
|
253 |
3133 |
Integer Integer::euclidianDivideRemainder(const Integer& y) const |
254 |
|
{ |
255 |
6266 |
Integer q, r; |
256 |
3133 |
euclidianQR(q, r, *this, y); |
257 |
6266 |
return r; |
258 |
|
} |
259 |
|
|
260 |
|
Integer Integer::exactQuotient(const Integer& y) const |
261 |
|
{ |
262 |
|
DebugCheckArgument(y.divides(*this), y); |
263 |
|
return Integer(cln::exquo(d_value, y.d_value)); |
264 |
|
} |
265 |
|
|
266 |
14655323 |
Integer Integer::modByPow2(uint32_t exp) const |
267 |
|
{ |
268 |
14655323 |
cln::cl_byte range(exp, 0); |
269 |
14655323 |
return Integer(cln::ldb(d_value, range)); |
270 |
|
} |
271 |
|
|
272 |
9186 |
Integer Integer::divByPow2(uint32_t exp) const { return d_value >> exp; } |
273 |
|
|
274 |
28737 |
Integer Integer::pow(unsigned long int exp) const |
275 |
|
{ |
276 |
28737 |
if (exp == 0) |
277 |
|
{ |
278 |
176 |
return Integer(1); |
279 |
|
} |
280 |
|
else |
281 |
|
{ |
282 |
28561 |
Assert(exp > 0); |
283 |
57122 |
cln::cl_I result = cln::expt_pos(d_value, exp); |
284 |
28561 |
return Integer(result); |
285 |
|
} |
286 |
|
} |
287 |
|
|
288 |
3513805 |
Integer Integer::gcd(const Integer& y) const |
289 |
|
{ |
290 |
7027610 |
cln::cl_I result = cln::gcd(d_value, y.d_value); |
291 |
7027610 |
return Integer(result); |
292 |
|
} |
293 |
|
|
294 |
15599249 |
Integer Integer::lcm(const Integer& y) const |
295 |
|
{ |
296 |
31198498 |
cln::cl_I result = cln::lcm(d_value, y.d_value); |
297 |
31198498 |
return Integer(result); |
298 |
|
} |
299 |
|
|
300 |
2564 |
Integer Integer::modAdd(const Integer& y, const Integer& m) const |
301 |
|
{ |
302 |
5128 |
cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value); |
303 |
5128 |
cln::cl_MI xm = ry->canonhom(d_value); |
304 |
5128 |
cln::cl_MI ym = ry->canonhom(y.d_value); |
305 |
5128 |
cln::cl_MI res = xm + ym; |
306 |
5128 |
return Integer(ry->retract(res)); |
307 |
|
} |
308 |
|
|
309 |
2559 |
Integer Integer::modMultiply(const Integer& y, const Integer& m) const |
310 |
|
{ |
311 |
5118 |
cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value); |
312 |
5118 |
cln::cl_MI xm = ry->canonhom(d_value); |
313 |
5118 |
cln::cl_MI ym = ry->canonhom(y.d_value); |
314 |
5118 |
cln::cl_MI res = xm * ym; |
315 |
5118 |
return Integer(ry->retract(res)); |
316 |
|
} |
317 |
|
|
318 |
466 |
Integer Integer::modInverse(const Integer& m) const |
319 |
|
{ |
320 |
466 |
PrettyCheckArgument(m > 0, m, "m must be greater than zero"); |
321 |
932 |
cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value); |
322 |
932 |
cln::cl_MI xm = ry->canonhom(d_value); |
323 |
|
/* normalize to modulo m for coprime check */ |
324 |
932 |
cln::cl_I x = ry->retract(xm); |
325 |
466 |
if (x == 0 || cln::gcd(x, m.d_value) != 1) |
326 |
|
{ |
327 |
26 |
return Integer(-1); |
328 |
|
} |
329 |
880 |
cln::cl_MI res = cln::recip(xm); |
330 |
440 |
return Integer(ry->retract(res)); |
331 |
|
} |
332 |
|
|
333 |
66402 |
bool Integer::divides(const Integer& y) const |
334 |
|
{ |
335 |
132804 |
cln::cl_I result = cln::rem(y.d_value, d_value); |
336 |
132804 |
return cln::zerop(result); |
337 |
|
} |
338 |
|
|
339 |
9002157 |
Integer Integer::abs() const { return d_value >= 0 ? *this : -*this; } |
340 |
|
|
341 |
54770 |
std::string Integer::toString(int base) const |
342 |
|
{ |
343 |
109540 |
std::stringstream ss; |
344 |
54770 |
switch (base) |
345 |
|
{ |
346 |
29326 |
case 2: fprintbinary(ss, d_value); break; |
347 |
|
case 8: fprintoctal(ss, d_value); break; |
348 |
25422 |
case 10: fprintdecimal(ss, d_value); break; |
349 |
22 |
case 16: fprinthexadecimal(ss, d_value); break; |
350 |
|
default: throw Exception("Unhandled base in Integer::toString()"); |
351 |
|
} |
352 |
54770 |
std::string output = ss.str(); |
353 |
235268 |
for (unsigned i = 0; i <= output.length(); ++i) |
354 |
|
{ |
355 |
180498 |
if (isalpha(output[i])) |
356 |
|
{ |
357 |
18 |
output.replace(i, 1, 1, tolower(output[i])); |
358 |
|
} |
359 |
|
} |
360 |
|
|
361 |
109540 |
return output; |
362 |
|
} |
363 |
|
|
364 |
1535121 |
int Integer::sgn() const |
365 |
|
{ |
366 |
3070242 |
cln::cl_I sgn = cln::signum(d_value); |
367 |
3070242 |
return cln::cl_I_to_int(sgn); |
368 |
|
} |
369 |
|
|
370 |
65 |
bool Integer::strictlyPositive() const { return cln::plusp(d_value); } |
371 |
|
|
372 |
111445 |
bool Integer::strictlyNegative() const { return cln::minusp(d_value); } |
373 |
|
|
374 |
92210 |
bool Integer::isZero() const { return cln::zerop(d_value); } |
375 |
|
|
376 |
23769143 |
bool Integer::isOne() const { return d_value == 1; } |
377 |
|
|
378 |
|
bool Integer::isNegativeOne() const { return d_value == -1; } |
379 |
|
|
380 |
247790 |
void Integer::parseInt(const std::string& s, unsigned base) |
381 |
|
{ |
382 |
|
cln::cl_read_flags flags; |
383 |
247790 |
flags.syntax = cln::syntax_integer; |
384 |
247790 |
flags.lsyntax = cln::lsyntax_standard; |
385 |
247790 |
flags.rational_base = base; |
386 |
247790 |
if (base == 0) |
387 |
|
{ |
388 |
|
// infer base in a manner consistent with GMP |
389 |
16 |
if (s[0] == '0') |
390 |
|
{ |
391 |
10 |
flags.lsyntax = cln::lsyntax_commonlisp; |
392 |
20 |
std::string st = s; |
393 |
10 |
if (s[1] == 'X' || s[1] == 'x') |
394 |
|
{ |
395 |
4 |
st.replace(0, 2, "#x"); |
396 |
|
} |
397 |
6 |
else if (s[1] == 'B' || s[1] == 'b') |
398 |
|
{ |
399 |
4 |
st.replace(0, 2, "#b"); |
400 |
|
} |
401 |
|
else |
402 |
|
{ |
403 |
2 |
st.replace(0, 1, "#o"); |
404 |
|
} |
405 |
10 |
readInt(flags, st, base); |
406 |
8 |
return; |
407 |
|
} |
408 |
|
else |
409 |
|
{ |
410 |
6 |
flags.rational_base = 10; |
411 |
|
} |
412 |
|
} |
413 |
247780 |
readInt(flags, s, base); |
414 |
|
} |
415 |
|
|
416 |
247790 |
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 |
247790 |
size_t pos = s.find_first_not_of('0'); |
428 |
247790 |
if (pos == std::string::npos) |
429 |
|
{ |
430 |
48586 |
d_value = cln::read_integer(flags, "0", NULL, NULL); |
431 |
|
} |
432 |
|
else |
433 |
|
{ |
434 |
199204 |
const char* cstr = s.c_str(); |
435 |
199204 |
const char* start = cstr + pos; |
436 |
199204 |
const char* end = cstr + s.length(); |
437 |
199204 |
d_value = cln::read_integer(flags, start, end, NULL); |
438 |
|
} |
439 |
|
} |
440 |
194 |
catch (...) |
441 |
|
{ |
442 |
194 |
std::stringstream ss; |
443 |
97 |
ss << "Integer() failed to parse value \"" << s << "\" in base " << base; |
444 |
97 |
throw std::invalid_argument(ss.str()); |
445 |
|
} |
446 |
247693 |
} |
447 |
|
|
448 |
48 |
bool Integer::fitsSignedInt() const |
449 |
|
{ |
450 |
|
// http://www.ginac.de/CLN/cln.html#Conversions |
451 |
|
// TODO improve performance |
452 |
48 |
Assert(s_slowSignedIntMin <= s_fastSignedIntMin); |
453 |
48 |
Assert(s_fastSignedIntMin <= s_fastSignedIntMax); |
454 |
48 |
Assert(s_fastSignedIntMax <= s_slowSignedIntMax); |
455 |
|
|
456 |
144 |
return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) |
457 |
240 |
&& (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax); |
458 |
|
} |
459 |
|
|
460 |
1206611 |
bool Integer::fitsUnsignedInt() const |
461 |
|
{ |
462 |
|
// TODO improve performance |
463 |
1206611 |
Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax); |
464 |
1206611 |
return sgn() >= 0 |
465 |
4826444 |
&& (d_value <= s_fastUnsignedIntMax |
466 |
2413224 |
|| d_value <= s_slowUnsignedIntMax); |
467 |
|
} |
468 |
|
|
469 |
48 |
signed int Integer::getSignedInt() const |
470 |
|
{ |
471 |
|
// ensure there isn't overflow |
472 |
96 |
CheckArgument( |
473 |
48 |
fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()"); |
474 |
48 |
return cln::cl_I_to_int(d_value); |
475 |
|
} |
476 |
|
|
477 |
13231 |
unsigned int Integer::getUnsignedInt() const |
478 |
|
{ |
479 |
|
// ensure there isn't overflow |
480 |
13231 |
CheckArgument(fitsUnsignedInt(), |
481 |
|
this, |
482 |
|
"Overflow detected in Integer::getUnsignedInt()"); |
483 |
13231 |
return cln::cl_I_to_uint(d_value); |
484 |
|
} |
485 |
|
|
486 |
|
bool Integer::fitsSignedLong() const |
487 |
|
{ |
488 |
|
return d_value <= s_signedLongMax && d_value >= s_signedLongMin; |
489 |
|
} |
490 |
|
|
491 |
|
bool Integer::fitsUnsignedLong() const |
492 |
|
{ |
493 |
|
return sgn() >= 0 && d_value <= s_unsignedLongMax; |
494 |
|
} |
495 |
|
|
496 |
2433 |
long Integer::getLong() const |
497 |
|
{ |
498 |
|
// ensure there isn't overflow |
499 |
2435 |
CheckArgument(d_value <= std::numeric_limits<long>::max(), |
500 |
|
this, |
501 |
|
"Overflow detected in Integer::getLong()"); |
502 |
2431 |
CheckArgument(d_value >= std::numeric_limits<long>::min(), |
503 |
|
this, |
504 |
|
"Overflow detected in Integer::getLong()"); |
505 |
2431 |
return cln::cl_I_to_long(d_value); |
506 |
|
} |
507 |
|
|
508 |
451 |
unsigned long Integer::getUnsignedLong() const |
509 |
|
{ |
510 |
|
// ensure there isn't overflow |
511 |
453 |
CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), |
512 |
|
this, |
513 |
|
"Overflow detected in Integer::getUnsignedLong()"); |
514 |
449 |
CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), |
515 |
|
this, |
516 |
|
"Overflow detected in Integer::getUnsignedLong()"); |
517 |
449 |
return cln::cl_I_to_ulong(d_value); |
518 |
|
} |
519 |
|
|
520 |
3694888 |
size_t Integer::hash() const { return equal_hashcode(d_value); } |
521 |
|
|
522 |
70 |
bool Integer::testBit(unsigned n) const { return cln::logbitp(n, d_value); } |
523 |
|
|
524 |
536462 |
unsigned Integer::isPow2() const |
525 |
|
{ |
526 |
536462 |
if (d_value <= 0) return 0; |
527 |
|
// power2p returns n such that d_value = 2^(n-1) |
528 |
514962 |
return cln::power2p(d_value); |
529 |
|
} |
530 |
|
|
531 |
327620 |
size_t Integer::length() const |
532 |
|
{ |
533 |
327620 |
int s = sgn(); |
534 |
327620 |
if (s == 0) |
535 |
|
{ |
536 |
41074 |
return 1; |
537 |
|
} |
538 |
286546 |
else if (s < 0) |
539 |
|
{ |
540 |
128347 |
size_t len = cln::integer_length(d_value); |
541 |
|
/*If this is -2^n, return len+1 not len to stay consistent with the |
542 |
|
* definition above! From CLN's documentation of integer_length: This is |
543 |
|
* the smallest n >= 0 such that -2^n <= x < 2^n. If x > 0, this is the |
544 |
|
* unique n > 0 such that 2^(n-1) <= x < 2^n. |
545 |
|
*/ |
546 |
128347 |
size_t ord2 = cln::ord2(d_value); |
547 |
128347 |
return (len == ord2) ? (len + 1) : len; |
548 |
|
} |
549 |
|
else |
550 |
|
{ |
551 |
158199 |
return cln::integer_length(d_value); |
552 |
|
} |
553 |
|
} |
554 |
|
|
555 |
48 |
void Integer::extendedGcd( |
556 |
|
Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b) |
557 |
|
{ |
558 |
48 |
g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value); |
559 |
48 |
} |
560 |
|
|
561 |
|
const Integer& Integer::min(const Integer& a, const Integer& b) |
562 |
|
{ |
563 |
|
return (a <= b) ? a : b; |
564 |
|
} |
565 |
|
|
566 |
|
const Integer& Integer::max(const Integer& a, const Integer& b) |
567 |
|
{ |
568 |
|
return (a >= b) ? a : b; |
569 |
|
} |
570 |
|
|
571 |
24682 |
std::ostream& operator<<(std::ostream& os, const Integer& n) |
572 |
|
{ |
573 |
24682 |
return os << n.toString(); |
574 |
|
} |
575 |
31137 |
} // namespace cvc5 |