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