ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
bigint.hh
Go to the documentation of this file.
1// $Id: bigint.hh,v 1.12 2009-01-24 15:14:46 kroening Exp $
2
3// My own BigInt class, declaration.
4
5#ifndef BIGINT_HH
6#define BIGINT_HH
7
8#include <cstdint>
9#include <utility>
10
11// This one is pretty simple but has a fair divide implementation.
12// Though I'm not ambitious enough to do that FFT-like stuff.
13//
14// Desirable properties / design goals:
15//
16// - Highly configurable, should run on chips from 8 to 64 bits word size.
17// - Is relatively small.
18// - Is thread safe.
19// - Does not significantly pollute the global namespace.
20//
21// Deliberate omissions:
22//
23// - Support of the C++ iostream classes which I find obsolete.
24// (Of course there are conversions from/to strings.)
25// - Bitwise operations. A bitset is a different thing than a BigInt.
26//
27// Porting and configuration:
28//
29// - Somehow resolve the problem when your compiler has no `bool' yet.
30// - Choose appropriate elementary types to use for onedig_t, twodig_t,
31// llong_t, and ullong_t. Some possible variants are #ifdef'd below.
32// - Decide what to do on division by zero (in implementation file.)
33// - In allocainc.h, do whatever necessary to provide the alloca() function.
34//
35// That should be all. I saw this running on:
36//
37// - Linux/egcs-1.1.2 ... gcc-2.95.2
38// - Linux/Comeau C++ 4.2.42
39// - Linux/Fujitsu C++
40// - FreeBSD 3.1/gcc-2.7.2 ... 4.1/gcc-2.95.2, NetBSD 1.4.2/egcs-1.1.1
41// - FreeBSD 4.x/TenDRA 4.2-BETA
42// - AIX/xlC
43// - Sun Solaris 2.5 ... 8/Sparc/SunPRO CC 4.2 ... Forte 6.0
44// - Windows NT/i386/MS Visual-C 4.2 ... 6.0
45// - Windows NT/i386/Borland-C++ 5.0, 5.5 (also with Intel reference compiler)
46// - DEC-OSF1/DEC CXX 6.0
47// - DEC OpenVMS 6.2/VAX/DEC CXX 5.5 (without optimization)
48// - DEC OpenVMS 6.2 and 7.1/Alpha/DEC CXX 5.6
49//
50// Legal status:
51//
52// The copyright at this source is owned by Dirk Zoller,
53// e-mail: duz@sol-3.de
54//
55// You may however use and modify this without restriction.
56
57class BigInt
58{
59public:
60 // Decide about and publish configuration details:
61
62 // Choose digit type for best performance. Bigger is better as long
63 // as there are machine instructions for multiplying and dividing on
64 // twice the size of a digit, i.e. on twodig_t.
65#if defined __GNUG__ || defined __alpha // || defined __TenDRA__
66 // Or other true 64 bit CPU.
67 typedef unsigned onedig_t;
68 typedef unsigned long long twodig_t;
69#elif defined _MSC_VER // || defined __BORLANDC__ (works but is slower)
70 // Like GCC's long long this __int64 actually performs better than
71 // unsigned. Though not as much as is the case with gcc.
72 typedef unsigned onedig_t;
73 typedef unsigned __int64 twodig_t;
74#elif 1
75 // Majority (currently) of 32 bit CPUs.
76 typedef unsigned short onedig_t;
77 typedef unsigned twodig_t;
78#else
79 // Works on 8/16 bit CPUs just as well.
80 typedef unsigned char onedig_t;
81 typedef unsigned short twodig_t;
82#endif
83
84 // Choose largest integral type to use. Must be >= twodig_t.
85#if defined __GNUG__
86 typedef long long llong_t;
87 typedef unsigned long long ullong_t;
88#elif defined _MSC_VER // || defined __BORLANDC__
89 typedef __int64 llong_t;
90 typedef unsigned __int64 ullong_t;
91#else
92 typedef long llong_t;
93 typedef unsigned long ullong_t;
94#endif
95
96 // Maximum number of onedig_t digits which could also be represented
97 // by an elementary type.
98 enum
99 {
100 small = sizeof(ullong_t) / sizeof(onedig_t)
101 };
102
103private:
104 unsigned size; // Length of digit vector.
105 unsigned length; // Used places in digit vector.
106 onedig_t *digit; // Least significant first.
107 bool positive; // Signed magnitude representation.
108
109 // Create or resize this.
110 inline void allocate(unsigned digits);
111 inline void reallocate(unsigned digits);
112 inline void resize(unsigned digits);
113
114 // Adjust length (e.g. after subtraction).
115 inline void adjust();
116
117 // Assign to this.
118 void assign(llong_t);
119 void assign(ullong_t);
120
121 // Aux methods, only for internal use.
122 inline int ucompare(BigInt const &) const;
123 void add(onedig_t const *, unsigned, bool);
124 void mul(onedig_t const *, unsigned, bool);
125
126 // Auxiliary constructor used for temporary or static BigInt.
127 // Sets size=0 which indicates that ~BigInt must not delete[].
128 inline BigInt(onedig_t *, unsigned, bool);
129
130public:
131 ~BigInt();
132
133 BigInt();
134 BigInt(int);
135 BigInt(unsigned);
136
137 BigInt(long signed int x);
138 BigInt(long unsigned int x);
139
142 BigInt(BigInt const &);
143 BigInt(BigInt &&);
144 BigInt(char const *, onedig_t = 10);
145
146 BigInt &operator=(BigInt const &);
147 BigInt &operator=(BigInt &&);
148
149 // Input conversion from text.
150
151 char const *scan_on(char const *, onedig_t = 10);
152 char const *scan(char const *, onedig_t = 10);
153
154 // Output conversion into text.
155
156 // Return an upper bound for the number of digits the textual
157 // representation of this might have.
158 unsigned digits(onedig_t = 10) const;
159
160 // Convert into string, right adjusted in field of specified width.
161 // Returns pointer to start of number or NULL if field too small.
162 char *as_string(char *, unsigned, onedig_t = 10) const;
163
164 // Convert to/from a binary representation.
165
166 // Write and read in a compact byte-wise binary form. Effectively
167 // print in base 256 with the most significant digit first. Also
168 // read back from such a representation. Return success.
169 bool dump(unsigned char *, unsigned) const;
170 void load(unsigned char const *, unsigned);
171
172 // Conversions to elementary types.
173
174 bool is_int64() const;
175 bool is_uint64() const
176 {
177 return length <= small;
178 }
179
180 // disabled by DK: makes operators ambigous
181 // operator llong_t() const;
182 // operator ullong_t() const;
183 uint64_t to_uint64() const;
184 int64_t to_int64() const;
185
186#ifndef bool
187 // Like int: non-zero is true. Equivalent to !is_zero().
188 // operator bool() const { return length != 0; }
189#endif
190
191 // All comparisions are done with these primitives.
192
193 int compare(llong_t) const;
194 int compare(ullong_t) const;
195 int compare(BigInt const &) const;
196
197 // Eliminate need for explicit casts when comparing.
198
199 int compare(long n) const
200 {
201 return compare(static_cast<llong_t>(n));
202 }
203 int compare(unsigned long n) const
204 {
205 return compare(static_cast<ullong_t>(n));
206 }
207 int compare(int n) const
208 {
209 return compare(static_cast<llong_t>(n));
210 }
211 int compare(unsigned n) const
212 {
213 return compare(static_cast<ullong_t>(n));
214 }
215
216 // Tests. These are faster than comparing with 0 or of course %2.
217
218 bool is_zero() const
219 {
220 return length == 0;
221 }
222 bool is_positive() const
223 {
224 return positive;
225 }
226 bool is_negative() const
227 {
228 return !positive;
229 }
230 bool is_odd() const
231 {
232 return length != 0 && digit[0] & 1;
233 }
234 bool is_even() const
235 {
236 return !is_odd();
237 }
238
239 // Arithmetic.
240
241 BigInt &negate()
242 {
243 if (!is_zero())
244 positive = !positive;
245 return *this;
246 }
247
248 friend BigInt operator-(BigInt b)
249 {
250 b.negate();
251 return b;
252 }
253
254#define IN_PLACE_OPERATOR(TYPE) \
255 BigInt &operator+=(TYPE); \
256 BigInt &operator-=(TYPE); \
257 BigInt &operator*=(TYPE); \
258 BigInt &operator/=(TYPE); \
259 BigInt &operator%=(TYPE);
260
264#undef IN_PLACE_OPERATOR
265
266#define OVERLOAD_IN_PLACE_OPERATOR(FROM, TO) \
267 BigInt &operator+=(FROM x) \
268 { \
269 return operator+=(static_cast<TO>(x)); \
270 } \
271 BigInt &operator-=(FROM x) \
272 { \
273 return operator-=(static_cast<TO>(x)); \
274 } \
275 BigInt &operator*=(FROM x) \
276 { \
277 return operator*=(static_cast<TO>(x)); \
278 } \
279 BigInt &operator/=(FROM x) \
280 { \
281 return operator/=(static_cast<TO>(x)); \
282 } \
283 BigInt &operator%=(FROM x) \
284 { \
285 return operator%=(static_cast<TO>(x)); \
286 }
287
292#undef OVERLOAD_IN_PLACE_OPERATOR
293
294 BigInt &operator++()
295 {
296 return operator+=(1);
297 } // preincrement
298 BigInt &operator--()
299 {
300 return operator-=(1);
301 } // predecrement
302
303 static void div(BigInt const &, BigInt const &, BigInt &quot, BigInt &rem);
304
305 // Returns the largest x such that 2^x <= abs() or 0 if input is 0
306 // Not part of original BigInt.
307 unsigned floorPow2() const;
308
309 // Not part of original BigInt.
310 static BigInt power2(unsigned n)
311 {
312 BigInt b;
313 b.setPower2(n);
314 return b;
315 }
316
317 // Not part of original BigInt.
318 static BigInt power2m1(unsigned n)
319 {
320 BigInt b = power2(n);
321 --b;
322 return b;
323 }
324
325 void swap(BigInt &other)
326 {
327 std::swap(other.size, size);
328 std::swap(other.length, length);
329 std::swap(other.digit, digit);
330 std::swap(other.positive, positive);
331 }
332
333private:
334 // Sets the number to the power of two given by the exponent
335 // Not part of original BigInt.
336 void setPower2(unsigned exponent);
337};
338
339// Binary arithmetic operators
340
341inline BigInt operator+(const BigInt &lhs, const BigInt &rhs)
342{
343 return BigInt(lhs) += rhs;
344}
345inline BigInt operator-(const BigInt &lhs, const BigInt &rhs)
346{
347 return BigInt(lhs) -= rhs;
348}
349inline BigInt operator*(const BigInt &lhs, const BigInt &rhs)
350{
351 return BigInt(lhs) *= rhs;
352}
353inline BigInt operator/(const BigInt &lhs, const BigInt &rhs)
354{
355 return BigInt(lhs) /= rhs;
356}
357inline BigInt operator%(const BigInt &lhs, const BigInt &rhs)
358{
359 return BigInt(lhs) %= rhs;
360}
361
362// Because the operators `+` and `*` are associative, we can do fast math, no
363// matter which side the BigInt is on. For the rest of the operators, which
364// are non-associative, we can only get speedups if the primitive type is on
365// the RHS.
366#define BINARY_ARITHMETIC_OPERATORS(OTHER) \
367 inline BigInt operator+(const BigInt &lhs, OTHER rhs) \
368 { \
369 return BigInt(lhs) += rhs; \
370 } \
371 inline BigInt operator+(OTHER lhs, const BigInt &rhs) \
372 { \
373 return BigInt(rhs) += lhs; \
374 } \
375 inline BigInt operator*(const BigInt &lhs, OTHER rhs) \
376 { \
377 return BigInt(lhs) *= rhs; \
378 } \
379 inline BigInt operator*(OTHER lhs, const BigInt &rhs) \
380 { \
381 return BigInt(rhs) *= lhs; \
382 } \
383 inline BigInt operator-(const BigInt &lhs, OTHER rhs) \
384 { \
385 return BigInt(lhs) -= rhs; \
386 } \
387 inline BigInt operator/(const BigInt &lhs, OTHER rhs) \
388 { \
389 return BigInt(lhs) /= rhs; \
390 } \
391 inline BigInt operator%(const BigInt &lhs, OTHER rhs) \
392 { \
393 return BigInt(lhs) %= rhs; \
394 }
395
399BINARY_ARITHMETIC_OPERATORS(unsigned long)
402#undef BINARY_ARITHMETIC_OPERATORS
403
404// Binary comparison operators
405
406inline bool operator<(const BigInt &lhs, const BigInt &rhs)
407{
408 return lhs.compare(rhs) < 0;
409}
410inline bool operator>(const BigInt &lhs, const BigInt &rhs)
411{
412 return lhs.compare(rhs) > 0;
413}
414inline bool operator<=(const BigInt &lhs, const BigInt &rhs)
415{
416 return lhs.compare(rhs) <= 0;
417}
418inline bool operator>=(const BigInt &lhs, const BigInt &rhs)
419{
420 return lhs.compare(rhs) >= 0;
421}
422inline bool operator==(const BigInt &lhs, const BigInt &rhs)
423{
424 return lhs.compare(rhs) == 0;
425}
426inline bool operator!=(const BigInt &lhs, const BigInt &rhs)
427{
428 return lhs.compare(rhs) != 0;
429}
430
431// These operators are all associative, so we can define them all for
432// primitives on the LHS and RHS.
433#define COMPARISON_OPERATORS(OTHER) \
434 inline bool operator<(const BigInt &lhs, OTHER rhs) \
435 { \
436 return lhs.compare(rhs) < 0; \
437 } \
438 inline bool operator>(const BigInt &lhs, OTHER rhs) \
439 { \
440 return lhs.compare(rhs) > 0; \
441 } \
442 inline bool operator<=(const BigInt &lhs, OTHER rhs) \
443 { \
444 return lhs.compare(rhs) <= 0; \
445 } \
446 inline bool operator>=(const BigInt &lhs, OTHER rhs) \
447 { \
448 return lhs.compare(rhs) >= 0; \
449 } \
450 inline bool operator==(const BigInt &lhs, OTHER rhs) \
451 { \
452 return lhs.compare(rhs) == 0; \
453 } \
454 inline bool operator!=(const BigInt &lhs, OTHER rhs) \
455 { \
456 return lhs.compare(rhs) != 0; \
457 } \
458 inline bool operator<(OTHER lhs, const BigInt &rhs) \
459 { \
460 return -rhs.compare(lhs) < 0; \
461 } \
462 inline bool operator>(OTHER lhs, const BigInt &rhs) \
463 { \
464 return -rhs.compare(lhs) > 0; \
465 } \
466 inline bool operator<=(OTHER lhs, const BigInt &rhs) \
467 { \
468 return -rhs.compare(lhs) <= 0; \
469 } \
470 inline bool operator>=(OTHER lhs, const BigInt &rhs) \
471 { \
472 return -rhs.compare(lhs) >= 0; \
473 } \
474 inline bool operator==(OTHER lhs, const BigInt &rhs) \
475 { \
476 return -rhs.compare(lhs) == 0; \
477 } \
478 inline bool operator!=(OTHER lhs, const BigInt &rhs) \
479 { \
480 return -rhs.compare(lhs) != 0; \
481 }
482
486COMPARISON_OPERATORS(unsigned long)
488COMPARISON_OPERATORS(unsigned)
489#undef COMPARISON_OPERATORS
490
491#endif // ndef BIGINT_HH
BigInt::onedig_t onedig_t
Definition bigint.cpp:23
BigInt::llong_t llong_t
Definition bigint.cpp:21
BigInt::ullong_t ullong_t
Definition bigint.cpp:22
BigInt operator+(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:341
BigInt operator*(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:349
bool operator<(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:406
bool operator>(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:410
BigInt operator-(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:345
#define BINARY_ARITHMETIC_OPERATORS(OTHER)
Definition bigint.hh:366
#define OVERLOAD_IN_PLACE_OPERATOR(FROM, TO)
Definition bigint.hh:266
bool operator!=(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:426
bool operator<=(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:414
#define COMPARISON_OPERATORS(OTHER)
Definition bigint.hh:433
#define IN_PLACE_OPERATOR(TYPE)
Definition bigint.hh:254
BigInt operator%(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:357
bool operator==(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:422
BigInt operator/(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:353
bool operator>=(const BigInt &lhs, const BigInt &rhs)
Definition bigint.hh:418
Definition bigint.hh:58
bool is_uint64() const
Definition bigint.hh:175
void load(unsigned char const *, unsigned)
Definition bigint.cpp:605
BigInt & operator++()
Definition bigint.hh:294
int64_t to_int64() const
Definition bigint.cpp:670
long llong_t
Definition bigint.hh:92
int compare(unsigned long n) const
Definition bigint.hh:203
unsigned digits(onedig_t=10) const
Definition bigint.cpp:514
~BigInt()
Definition bigint.cpp:367
int compare(unsigned n) const
Definition bigint.hh:211
BigInt & operator=(BigInt const &)
Definition bigint.cpp:448
bool is_odd() const
Definition bigint.hh:230
bool dump(unsigned char *, unsigned) const
Definition bigint.cpp:560
char const * scan_on(char const *, onedig_t=10)
Definition bigint.cpp:461
int compare(long n) const
Definition bigint.hh:199
static BigInt power2(unsigned n)
Definition bigint.hh:310
bool is_int64() const
Definition bigint.cpp:635
bool is_even() const
Definition bigint.hh:234
unsigned short onedig_t
Definition bigint.hh:76
int compare(llong_t) const
Definition bigint.cpp:709
bool is_zero() const
Definition bigint.hh:218
int compare(int n) const
Definition bigint.hh:207
void swap(BigInt &other)
Definition bigint.hh:325
@ small
Definition bigint.hh:100
friend BigInt operator-(BigInt b)
Definition bigint.hh:248
char * as_string(char *, unsigned, onedig_t=10) const
Definition bigint.cpp:522
bool is_negative() const
Definition bigint.hh:226
static BigInt power2m1(unsigned n)
Definition bigint.hh:318
unsigned floorPow2() const
Definition bigint.cpp:1194
BigInt & negate()
Definition bigint.hh:241
BigInt(long unsigned int x)
bool is_positive() const
Definition bigint.hh:222
BigInt(long signed int x)
uint64_t to_uint64() const
Definition bigint.cpp:659
char const * scan(char const *, onedig_t=10)
Definition bigint.cpp:505
static void div(BigInt const &, BigInt const &, BigInt &quot, BigInt &rem)
Definition bigint.cpp:957
BigInt & operator--()
Definition bigint.hh:298
unsigned long ullong_t
Definition bigint.hh:93
BigInt()
Definition bigint.cpp:381
unsigned twodig_t
Definition bigint.hh:77
@ other
Definition converter_compare.cpp:887
guard2tc & operator-=(guard2tc &g1, const guard2tc &g2)
Definition irep2_guard.cpp:334
void add(int64_t *A, int64_t *B, int64_t *C, int64_t a_rows, int64_t a_cols, int64_t b_rows, int64_t b_cols)
Definition umath.c:23