1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 mpff.cpp
7
8 Abstract:
9
10 Multi precision fast floating point numbers.
11 The implementation is not compliant with the IEEE standard.
12 For a compliant implementation, see mpf.h
13
14 Author:
15
16 Leonardo de Moura (leonardo) 2012-09-12
17
18 Revision History:
19
20 --*/
21 #include<sstream>
22 #include<iomanip>
23 #include "util/mpff.h"
24 #include "util/mpn.h"
25 #include "util/mpz.h"
26 #include "util/mpq.h"
27 #include "util/bit_util.h"
28 #include "util/trace.h"
29
30 static_assert(sizeof(mpn_digit) == sizeof(unsigned), "");
31 static_assert(sizeof(unsigned) == 4, "unsigned haven't changed size for a while");
32
33 // MIN_MSW is an shorthand for 0x8000..00, i.e., the minimal most significand word.
34 #define MIN_MSW (1u << (sizeof(unsigned) * 8 - 1))
35
mpff_manager(unsigned prec,unsigned initial_capacity)36 mpff_manager::mpff_manager(unsigned prec, unsigned initial_capacity) {
37 SASSERT(initial_capacity > 0);
38 m_precision = prec;
39 m_precision_bits = prec * 8 * sizeof(unsigned);
40 m_capacity = initial_capacity;
41 m_to_plus_inf = false;
42 m_significands.resize(initial_capacity * prec, 0);
43 for (unsigned i = 0; i < MPFF_NUM_BUFFERS; i++)
44 m_buffers[i].resize(2 * prec, 0);
45 // Reserve space for zero
46 VERIFY(m_id_gen.mk() == 0);
47 set(m_one, 1);
48 }
49
~mpff_manager()50 mpff_manager::~mpff_manager() {
51 del(m_one);
52 }
53
expand()54 void mpff_manager::expand() {
55 m_capacity = 2*m_capacity;
56 m_significands.resize(m_capacity * m_precision, 0);
57 }
58
allocate(mpff & n)59 void mpff_manager::allocate(mpff & n) {
60 SASSERT(n.m_sig_idx == 0);
61 unsigned sig_idx = m_id_gen.mk();
62 ensure_capacity(sig_idx);
63 n.m_sig_idx = sig_idx;
64 DEBUG_CODE({
65 unsigned * s = sig(n);
66 for (unsigned i = 0; i < m_precision; i++) {
67 SASSERT(s[i] == 0);
68 }
69 });
70 }
71
to_buffer(unsigned idx,mpff const & n) const72 void mpff_manager::to_buffer(unsigned idx, mpff const & n) const {
73 SASSERT(idx < MPFF_NUM_BUFFERS);
74 svector<unsigned> & b = const_cast<mpff_manager*>(this)->m_buffers[idx];
75 unsigned * s = sig(n);
76 for (unsigned i = 0; i < m_precision; i++)
77 b[i] = s[i];
78 }
79
to_buffer_ext(unsigned idx,mpff const & n) const80 void mpff_manager::to_buffer_ext(unsigned idx, mpff const & n) const {
81 SASSERT(idx < MPFF_NUM_BUFFERS);
82 svector<unsigned> & b = const_cast<mpff_manager*>(this)->m_buffers[idx];
83 unsigned * s = sig(n);
84 unsigned j = m_precision;
85 for (unsigned i = 0; i < m_precision; i++, j++) {
86 b[i] = s[i];
87 b[j] = 0;
88 }
89 }
90
to_buffer_shifting(unsigned idx,mpff const & n) const91 void mpff_manager::to_buffer_shifting(unsigned idx, mpff const & n) const {
92 SASSERT(idx < MPFF_NUM_BUFFERS);
93 svector<unsigned> & b = const_cast<mpff_manager*>(this)->m_buffers[idx];
94 unsigned * s = sig(n);
95 unsigned j = m_precision;
96 for (unsigned i = 0; i < m_precision; i++, j++) {
97 b[i] = 0;
98 b[j] = s[i];
99 }
100 }
101
del(mpff & n)102 void mpff_manager::del(mpff & n) {
103 unsigned sig_idx = n.m_sig_idx;
104 if (sig_idx != 0) {
105 m_id_gen.recycle(sig_idx);
106 unsigned * s = sig(n);
107 for (unsigned i = 0; i < m_precision; i++)
108 s[i] = 0;
109 }
110 }
111
reset(mpff & n)112 void mpff_manager::reset(mpff & n) {
113 del(n);
114 n.m_sign = false;
115 n.m_sig_idx = 0;
116 n.m_exponent = 0;
117 SASSERT(check(n));
118 }
119
is_int(mpff const & n) const120 bool mpff_manager::is_int(mpff const & n) const {
121 if (n.m_exponent >= 0)
122 return true; // cheap case
123 if (n.m_exponent <= -static_cast<int>(m_precision_bits))
124 return false;
125 return !has_one_at_first_k_bits(m_precision, sig(n), -n.m_exponent);
126 }
127
is_int64(mpff const & n) const128 bool mpff_manager::is_int64(mpff const & n) const {
129 SASSERT(m_precision >= 2);
130 if (is_zero(n))
131 return true;
132 int max_exp = -static_cast<int>(sizeof(unsigned) * 8 * (m_precision - 2));
133 if (n.m_exponent < max_exp) {
134 return n.m_exponent > -static_cast<int>(m_precision_bits) &&
135 !has_one_at_first_k_bits(m_precision, sig(n), -n.m_exponent);
136 }
137 else if (n.m_exponent == max_exp) {
138 // handle INT64_MIN case
139 unsigned * s = sig(n);
140 return is_neg(n) && s[m_precision-1] == 0x80000000u && ::is_zero(m_precision-1, s);
141 }
142 else {
143 return false;
144 }
145 }
146
is_uint64(mpff const & n) const147 bool mpff_manager::is_uint64(mpff const & n) const {
148 SASSERT(m_precision >= 2);
149 if (is_zero(n))
150 return true;
151 return
152 n.m_sign == 0 &&
153 n.m_exponent <= -static_cast<int>(sizeof(unsigned) * 8 * (m_precision - 2)) &&
154 n.m_exponent > -static_cast<int>(m_precision_bits) &&
155 !has_one_at_first_k_bits(m_precision, sig(n), -n.m_exponent);
156 }
157
get_uint64(mpff const & a) const158 uint64_t mpff_manager::get_uint64(mpff const & a) const {
159 SASSERT(is_uint64(a));
160 if (is_zero(a)) return 0;
161 int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2);
162 SASSERT(exp >= 0);
163 uint64_t * s = reinterpret_cast<uint64_t*>(sig(a) + (m_precision - 2));
164 return *s >> exp;
165 }
166
get_int64(mpff const & a) const167 int64_t mpff_manager::get_int64(mpff const & a) const {
168 SASSERT(is_int64(a));
169 if (is_zero(a)) return 0;
170 int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2);
171 SASSERT(exp >= 0);
172 uint64_t * s = reinterpret_cast<uint64_t*>(sig(a) + (m_precision - 2));
173 // INT64_MIN case
174 if (exp == 0 && *s == 0x8000000000000000ull && is_neg(a)) {
175 return INT64_MIN;
176 }
177 else {
178 int64_t r = *s >> exp;
179 if (is_neg(a))
180 r = -r;
181 return r;
182 }
183 }
184
185 // Return true if n is 1 or -1
is_abs_one(mpff const & n) const186 bool mpff_manager::is_abs_one(mpff const & n) const {
187 // That is, check whether
188 // n.exponent == 1 - m_precision_bits
189 // n.significand == 0b10000...0 (that is, only the highest bit is set in the significand).
190 if (n.m_exponent != 1 - static_cast<int>(m_precision_bits))
191 return false;
192 unsigned * s = sig(n);
193 if (s[m_precision - 1] != 0x80000000u)
194 return false;
195 for (unsigned i = 0; i < m_precision - 1; i++)
196 if (s[i] != 0)
197 return false;
198 return true;
199 }
200
is_two(mpff const & n) const201 bool mpff_manager::is_two(mpff const & n) const {
202 // That is, check whether
203 // n.exponent = 2 - m_precision_bits
204 // n.significand == 0b10000...0 (that is, only the highest bit is set in the significand).
205 if (is_neg(n))
206 return false;
207 if (n.m_exponent != 2 - static_cast<int>(m_precision_bits))
208 return false;
209 unsigned * s = sig(n);
210 if (s[m_precision - 1] != 0x80000000u)
211 return false;
212 for (unsigned i = 0; i < m_precision - 1; i++)
213 if (s[i] != 0)
214 return false;
215 return true;
216 }
217
set(mpff & n,int v)218 void mpff_manager::set(mpff & n, int v) {
219 if (v == 0) {
220 reset(n);
221 }
222 else {
223 if (v < 0) {
224 set(n, static_cast<unsigned>(-v));
225 n.m_sign = 1;
226 }
227 else {
228 set(n, static_cast<unsigned>(v));
229 }
230 }
231 SASSERT(check(n));
232 }
233
set(mpff & n,unsigned v)234 void mpff_manager::set(mpff & n, unsigned v) {
235 if (v == 0) {
236 reset(n);
237 }
238 else {
239 allocate_if_needed(n);
240 n.m_sign = 0;
241 int num_leading_zeros = nlz_core(v);
242 n.m_exponent = static_cast<int>(8 * sizeof(unsigned)) - num_leading_zeros - static_cast<int>(m_precision_bits);
243 v <<= num_leading_zeros;
244 unsigned * s = sig(n);
245 s[m_precision - 1] = v;
246 for (unsigned i = 0; i < m_precision - 1; i++)
247 s[i] = 0;
248 }
249 SASSERT(check(n));
250 }
251
set(mpff & n,int64_t v)252 void mpff_manager::set(mpff & n, int64_t v) {
253 if (v == 0) {
254 reset(n);
255 }
256 else {
257 if (v < 0) {
258 set(n, 1 + static_cast<uint64_t>(-(1+v)));
259 n.m_sign = 1;
260 }
261 else {
262 set(n, static_cast<uint64_t>(v));
263 }
264 }
265 SASSERT(check(n));
266 SASSERT(get_int64(n) == v);
267 }
268
set(mpff & n,uint64_t v)269 void mpff_manager::set(mpff & n, uint64_t v) {
270 #ifdef Z3DEBUG
271 uint64_t old_v = v;
272 #endif
273 if (v == 0) {
274 reset(n);
275 }
276 else {
277 allocate_if_needed(n);
278 n.m_sign = 0;
279 unsigned * _v = reinterpret_cast<unsigned*>(&v);
280 int num_leading_zeros = nlz(2, _v);
281 n.m_exponent = static_cast<int>(8 * sizeof(uint64_t)) - num_leading_zeros - static_cast<int>(m_precision_bits);
282 v <<= num_leading_zeros;
283 SASSERT(m_precision >= 2);
284 unsigned * s = sig(n);
285 s[m_precision-1] = _v[1];
286 s[m_precision-2] = _v[0];
287 for (unsigned i = 0; i < m_precision - 2; i++)
288 s[i] = 0;
289 }
290 SASSERT(check(n));
291 SASSERT(get_uint64(n) == old_v);
292 }
293
set(mpff & n,int num,unsigned den)294 void mpff_manager::set(mpff & n, int num, unsigned den) {
295 scoped_mpff a(*this), b(*this);
296 set(a, num);
297 set(b, den);
298 div(a, b, n);
299 SASSERT(check(n));
300 }
301
set(mpff & n,int64_t num,uint64_t den)302 void mpff_manager::set(mpff & n, int64_t num, uint64_t den) {
303 scoped_mpff a(*this), b(*this);
304 set(a, num);
305 set(b, den);
306 div(a, b, n);
307 SASSERT(check(n));
308 }
309
set(mpff & n,mpff const & v)310 void mpff_manager::set(mpff & n, mpff const & v) {
311 if (is_zero(v)) {
312 reset(n);
313 return;
314 }
315 if (&n == &v)
316 return;
317 allocate_if_needed(n);
318 n.m_sign = v.m_sign;
319 n.m_exponent = v.m_exponent;
320 unsigned * s1 = sig(n);
321 unsigned * s2 = sig(v);
322 for (unsigned i = 0; i < m_precision; i++)
323 s1[i] = s2[i];
324 SASSERT(check(n));
325 }
326
327 template<bool SYNCH>
set_core(mpff & n,mpz_manager<SYNCH> & m,mpz const & v)328 void mpff_manager::set_core(mpff & n, mpz_manager<SYNCH> & m, mpz const & v) {
329 TRACE("mpff", tout << "mpz->mpff\n"; m.display(tout, v); tout << "\n";);
330 if (m.is_int64(v)) {
331 TRACE("mpff", tout << "is_int64 " << m.get_int64(v) << "\n";);
332 set(n, m.get_int64(v));
333 }
334 else if (m.is_uint64(v)) {
335 TRACE("mpff", tout << "is_uint64\n";);
336 set(n, m.get_uint64(v));
337 }
338 else {
339 allocate_if_needed(n);
340 svector<unsigned> & w = m_set_buffer;
341 n.m_sign = m.decompose(v, w);
342 while (w.size() < m_precision) {
343 w.push_back(0);
344 }
345 TRACE("mpff", tout << "w words: "; for (unsigned i = 0; i < w.size(); i++) tout << w[i] << " "; tout << "\n";);
346 unsigned w_sz = w.size();
347 SASSERT(w_sz >= m_precision);
348 unsigned num_leading_zeros = nlz(w_sz, w.data());
349 shl(w_sz, w.data(), num_leading_zeros, w_sz, w.data());
350 unsigned * s = sig(n);
351 unsigned i = m_precision;
352 unsigned j = w_sz;
353 while (i > 0) {
354 --i;
355 --j;
356 s[i] = w[j];
357 }
358 n.m_exponent = j * 8 * sizeof(unsigned) - static_cast<int>(num_leading_zeros);
359 if ((n.m_sign == 1) != m_to_plus_inf) {
360 // must check whether it is precise or not
361 while (j > 0) {
362 --j;
363 if (w[j] != 0) {
364 // imprecision detected.
365 inc_significand(n);
366 }
367 }
368 // it is precise
369 }
370 }
371 TRACE("mpff", tout << "mpz->mpff result:\n"; display_raw(tout, n); tout << "\n";);
372 SASSERT(check(n));
373 }
374
set(mpff & n,unsynch_mpz_manager & m,mpz const & v)375 void mpff_manager::set(mpff & n, unsynch_mpz_manager & m, mpz const & v) {
376 set_core(n, m, v);
377 }
378
379 #ifndef SINGLE_THREAD
set(mpff & n,synch_mpz_manager & m,mpz const & v)380 void mpff_manager::set(mpff & n, synch_mpz_manager & m, mpz const & v) {
381 set_core(n, m, v);
382 }
383 #endif
384
385 template<bool SYNCH>
set_core(mpff & n,mpq_manager<SYNCH> & m,mpq const & v)386 void mpff_manager::set_core(mpff & n, mpq_manager<SYNCH> & m, mpq const & v) {
387 // TODO: improve precision?
388 scoped_mpff num(*this), den(*this);
389 set_core(num, m, v.numerator());
390 {
391 flet<bool> l(m_to_plus_inf, !m_to_plus_inf);
392 set_core(den, m, v.denominator());
393 }
394 div(num, den, n);
395 SASSERT(check(n));
396 }
397
set(mpff & n,unsynch_mpq_manager & m,mpq const & v)398 void mpff_manager::set(mpff & n, unsynch_mpq_manager & m, mpq const & v) {
399 set_core(n, m, v);
400 }
401
402 #ifndef SINGLE_THREAD
set(mpff & n,synch_mpq_manager & m,mpq const & v)403 void mpff_manager::set(mpff & n, synch_mpq_manager & m, mpq const & v) {
404 set_core(n, m, v);
405 }
406 #endif
407
eq(mpff const & a,mpff const & b) const408 bool mpff_manager::eq(mpff const & a, mpff const & b) const {
409 if (is_zero(a) && is_zero(b))
410 return true;
411 if (is_zero(a) || is_zero(b))
412 return false;
413 if (a.m_sign != b.m_sign ||
414 a.m_exponent != b.m_exponent)
415 return false;
416 unsigned * s1 = sig(a);
417 unsigned * s2 = sig(b);
418 for (unsigned i = 0; i < m_precision; i++)
419 if (s1[i] != s2[i])
420 return false;
421 return true;
422 }
423
lt(mpff const & a,mpff const & b) const424 bool mpff_manager::lt(mpff const & a, mpff const & b) const {
425 STRACE("mpff_trace", tout << "[mpff] ("; display(tout, a); tout << " < "; display(tout, b); tout << ") == ";);
426 if (is_zero(a)) {
427 if (is_zero(b) || is_neg(b)) {
428 STRACE("mpff_trace", tout << "(1 == 0)\n";);
429 return false;
430 }
431 else {
432 STRACE("mpff_trace", tout << "(1 == 1)\n";);
433 SASSERT(is_pos(b));
434 return true;
435 }
436 }
437 if (is_zero(b)) {
438 SASSERT(!is_zero(a));
439 if (is_neg(a)) {
440 STRACE("mpff_trace", tout << "(1 == 1)\n";);
441 return true;
442 }
443 else {
444 SASSERT(is_pos(a));
445 STRACE("mpff_trace", tout << "(1 == 0)\n";);
446 return false;
447 }
448 }
449 SASSERT(!is_zero(a));
450 SASSERT(!is_zero(b));
451 if (a.m_sign == 1) {
452 if (b.m_sign == 0) {
453 STRACE("mpff_trace", tout << "(1 == 1)\n";);
454 return true; // neg < pos
455 }
456 // case: neg neg
457 bool r =
458 b.m_exponent < a.m_exponent ||
459 (a.m_exponent == b.m_exponent && ::lt(m_precision, sig(b), sig(a)));
460 STRACE("mpff_trace", tout << "(" << r << " == 1)\n";);
461 return r;
462 }
463 else {
464 if (b.m_sign == 1) {
465 STRACE("mpff_trace", tout << "(1 == 0)\n";);
466 return false; // pos < neg
467 }
468 // case: pos pos
469 bool r =
470 a.m_exponent < b.m_exponent ||
471 (a.m_exponent == b.m_exponent && ::lt(m_precision, sig(a), sig(b)));
472 STRACE("mpff_trace", tout << "(" << r << " == 1)\n";);
473 return r;
474 }
475 }
476
inc_significand(unsigned * s,int64_t & exp)477 void mpff_manager::inc_significand(unsigned * s, int64_t & exp) {
478 if (!::inc(m_precision, s)) {
479 SASSERT(::is_zero(m_precision, s));
480 s[m_precision - 1] = MIN_MSW;
481 SASSERT(exp != INT64_MAX);
482 exp++;
483 }
484 }
485
inc_significand(mpff & a)486 void mpff_manager::inc_significand(mpff & a) {
487 unsigned * s = sig(a);
488 if (!::inc(m_precision, s)) {
489 // Overflow happened, a was of the form 0xFFFF...FF
490 // Now, it must be 0x000...000
491 SASSERT(::is_zero(m_precision, s));
492 // Set it to 0x80000...000, and increment exponent by 1.
493 s[m_precision - 1] = MIN_MSW;
494 if (a.m_exponent == INT_MAX)
495 throw overflow_exception();
496 a.m_exponent++;
497 }
498 }
499
dec_significand(mpff & a)500 void mpff_manager::dec_significand(mpff & a) {
501 SASSERT(!is_minus_epsilon(a) && !is_zero(a) && !is_plus_epsilon(a));
502 unsigned * s = sig(a);
503 for (unsigned i = 0; i < m_precision - 1; i++) {
504 s[i]--;
505 if (s[i] != UINT_MAX)
506 return;
507 }
508 s[m_precision - 1]--;
509 if (s[m_precision - 1] < MIN_MSW) {
510 s[m_precision - 1] = UINT_MAX;
511 a.m_exponent--;
512 }
513 }
514
min_significand(mpff const & a) const515 bool mpff_manager::min_significand(mpff const & a) const {
516 unsigned * s = sig(a);
517 return s[m_precision - 1] == MIN_MSW && ::is_zero(m_precision - 1, s);
518 }
519
is_minus_epsilon(mpff const & a) const520 bool mpff_manager::is_minus_epsilon(mpff const & a) const {
521 return a.m_sign == 1 && a.m_exponent == INT_MIN && min_significand(a);
522 }
523
is_plus_epsilon(mpff const & a) const524 bool mpff_manager::is_plus_epsilon(mpff const & a) const {
525 return a.m_sign == 0 && a.m_exponent == INT_MIN && min_significand(a);
526 }
527
set_min_significand(mpff & a)528 void mpff_manager::set_min_significand(mpff & a) {
529 // Since the most significand bit of the most significand word must be 1 in our representation,
530 // we have that 0x8000..00 is the minimal significand
531 unsigned * s = sig(a);
532 s[m_precision - 1] = MIN_MSW;
533 for (unsigned i = 0; i < m_precision - 1; i++)
534 s[i] = 0;
535 }
536
set_max_significand(mpff & a)537 void mpff_manager::set_max_significand(mpff & a) {
538 SASSERT(!is_zero(a));
539 unsigned * s = sig(a);
540 for (unsigned i = 0; i < m_precision; i++)
541 s[i] = UINT_MAX;
542 }
543
set_plus_epsilon(mpff & n)544 void mpff_manager::set_plus_epsilon(mpff & n) {
545 allocate_if_needed(n);
546 n.m_sign = 0;
547 n.m_exponent = INT_MIN;
548 set_min_significand(n);
549 SASSERT(check(n));
550 }
551
set_minus_epsilon(mpff & n)552 void mpff_manager::set_minus_epsilon(mpff & n) {
553 set_plus_epsilon(n);
554 n.m_sign = 1;
555 SASSERT(check(n));
556 }
557
set_max(mpff & n)558 void mpff_manager::set_max(mpff & n) {
559 allocate_if_needed(n);
560 n.m_sign = 0;
561 n.m_exponent = INT_MAX;
562 set_max_significand(n);
563 SASSERT(check(n));
564 }
565
set_min(mpff & n)566 void mpff_manager::set_min(mpff & n) {
567 set_max(n);
568 n.m_sign = 1;
569 SASSERT(check(n));
570 }
571
next(mpff & a)572 void mpff_manager::next(mpff & a) {
573 if (is_zero(a)) {
574 set_plus_epsilon(a);
575 }
576 else if (is_minus_epsilon(a)) {
577 reset(a);
578 }
579 else if (a.m_sign == 0) {
580 inc_significand(a);
581 }
582 else {
583 dec_significand(a);
584 }
585 SASSERT(check(a));
586 }
587
prev(mpff & a)588 void mpff_manager::prev(mpff & a) {
589 if (is_zero(a)) {
590 set_minus_epsilon(a);
591 }
592 else if (is_plus_epsilon(a)) {
593 reset(a);
594 }
595 else if (a.m_sign == 0) {
596 dec_significand(a);
597 }
598 else {
599 inc_significand(a);
600 }
601 SASSERT(check(a));
602 }
603
set_big_exponent(mpff & a,int64_t e)604 void mpff_manager::set_big_exponent(mpff & a, int64_t e) {
605 SASSERT(e > INT_MAX || e < INT_MIN);
606 if (e > INT_MAX) {
607 if (a.m_sign == 1) {
608 if (m_to_plus_inf)
609 set_min(a);
610 else
611 throw overflow_exception();
612 }
613 else {
614 if (m_to_plus_inf)
615 throw overflow_exception();
616 else
617 set_max(a);
618 }
619 }
620 else {
621 SASSERT(e < INT_MIN);
622 if (a.m_sign == 1) {
623 if (m_to_plus_inf)
624 reset(a);
625 else
626 set_minus_epsilon(a);
627 }
628 else {
629 if (m_to_plus_inf)
630 set_plus_epsilon(a);
631 else
632 reset(a);
633 }
634 }
635 }
636
add_sub(bool is_sub,mpff const & a,mpff const & b,mpff & c)637 void mpff_manager::add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c) {
638 if (is_zero(a)) {
639 set(c, b);
640 if (is_sub)
641 neg(c);
642 return;
643 }
644
645 if (is_zero(b)) {
646 set(c, a);
647 return;
648 }
649
650 TRACE("mpff", tout << (is_sub ? "sub" : "add") << "("; display(tout, a); tout << ", "; display(tout, b); tout << ")\n";);
651
652 // Remark: any result returned by sig(...) may be invalid after a call to allocate_if_needed()
653 // So, we must invoke allocate_if_needed(c) before we invoke sig(a) and sig(b).
654 allocate_if_needed(c);
655
656 bool sgn_a, sgn_b;
657 int exp_a, exp_b;
658 unsigned * sig_a, * sig_b;
659
660 if (a.m_exponent >= b.m_exponent) {
661 sgn_a = a.m_sign != 0;
662 sgn_b = b.m_sign != 0;
663 exp_a = a.m_exponent;
664 exp_b = b.m_exponent;
665 sig_a = sig(a);
666 sig_b = sig(b);
667 if (is_sub)
668 sgn_b = !sgn_b;
669 }
670 else {
671 sgn_a = b.m_sign != 0;
672 sgn_b = a.m_sign != 0;
673 exp_a = b.m_exponent;
674 exp_b = a.m_exponent;
675 sig_a = sig(b);
676 sig_b = sig(a);
677 if (is_sub)
678 sgn_a = !sgn_a;
679 }
680
681 SASSERT(exp_a >= exp_b);
682
683 unsigned * n_sig_b; // normalized sig_b
684
685 // Make sure that a and b have the same exponent.
686 if (exp_a > exp_b) {
687 unsigned shift = (unsigned)exp_a - (unsigned)exp_b;
688 n_sig_b = m_buffers[0].data();
689 shr(m_precision, sig_b, shift, m_precision, n_sig_b);
690 if (sgn_b != m_to_plus_inf && has_one_at_first_k_bits(m_precision, sig_b, shift)) {
691 // Precision was lost when normalizing the significand.
692 // The current rounding mode forces us to bump the significand.
693 // Remark: an overflow cannot happen when incrementing the significand.
694 VERIFY(::inc(m_precision, n_sig_b));
695 }
696 }
697 else {
698 SASSERT(exp_a == exp_b);
699 n_sig_b = sig_b;
700 }
701
702 // Compute c
703 if (sgn_a == sgn_b) {
704 c.m_sign = sgn_a;
705 unsigned * sig_r = m_buffers[1].data();
706 size_t r_sz;
707 m_mpn_manager.add(sig_a, m_precision, n_sig_b, m_precision, sig_r, m_precision + 1, &r_sz);
708 SASSERT(r_sz <= m_precision + 1);
709 unsigned num_leading_zeros = nlz(m_precision + 1, sig_r);
710 SASSERT(num_leading_zeros >= sizeof(unsigned) * 8 - 1); // num_leading_zeros >= 31
711 SASSERT(num_leading_zeros < sizeof(unsigned) * 8 * (m_precision + 1)); // result is not zero.
712 unsigned * sig_c = sig(c);
713 if (num_leading_zeros == sizeof(unsigned) * 8) {
714 // no shift is needed
715 c.m_exponent = exp_a;
716 for (unsigned i = 0; i < m_precision; i++)
717 sig_c[i] = sig_r[i];
718 }
719 else if (num_leading_zeros == sizeof(unsigned) * 8 - 1) {
720 // shift 1 right
721 bool _inc_significand = ((c.m_sign == 1) != m_to_plus_inf) && has_one_at_first_k_bits(m_precision*2, sig_r, 1);
722 int64_t exp_c = exp_a;
723 exp_c++;
724 shr(m_precision + 1, sig_r, 1, m_precision, sig_c);
725 if (_inc_significand)
726 inc_significand(sig_c, exp_c);
727 set_exponent(c, exp_c);
728 }
729 else {
730 SASSERT(num_leading_zeros > sizeof(unsigned) * 8);
731 num_leading_zeros -= sizeof(unsigned) * 8; // remove 1 word bits.
732 // Now, we can assume sig_r has size m_precision
733 SASSERT(num_leading_zeros > 0);
734 // shift left num_leading_zeros
735 int64_t exp_c = exp_a;
736 exp_c -= num_leading_zeros;
737 shl(m_precision, sig_r, num_leading_zeros, m_precision, sig_c);
738 set_exponent(c, exp_c);
739 }
740 }
741 else {
742 unsigned borrow;
743 SASSERT(sgn_a != sgn_b);
744 unsigned * sig_c = sig(c);
745 if (::lt(m_precision, sig_a, n_sig_b)) {
746 c.m_sign = sgn_b;
747 m_mpn_manager.sub(n_sig_b, m_precision, sig_a, m_precision, sig_c, &borrow);
748 }
749 else {
750 c.m_sign = sgn_a;
751 m_mpn_manager.sub(sig_a, m_precision, n_sig_b, m_precision, sig_c, &borrow);
752 }
753 SASSERT(borrow == 0);
754 unsigned num_leading_zeros = nlz(m_precision, sig_c);
755 if (num_leading_zeros == m_precision_bits) {
756 reset(c);
757 }
758 else if (num_leading_zeros > 0) {
759 int64_t exp_c = exp_a;
760 exp_c -= num_leading_zeros;
761 shl(m_precision, sig_c, num_leading_zeros, m_precision, sig_c);
762 set_exponent(c, exp_c);
763 }
764 else {
765 SASSERT(num_leading_zeros == 0);
766 c.m_exponent = exp_a;
767 }
768 }
769 TRACE("mpff", tout << "result: "; display(tout, c); tout << "\n";);
770 SASSERT(check(c));
771 }
772
add(mpff const & a,mpff const & b,mpff & c)773 void mpff_manager::add(mpff const & a, mpff const & b, mpff & c) {
774 STRACE("mpff_trace", tout << "[mpff] "; display(tout, a); tout << " + "; display(tout, b); tout << " " << (m_to_plus_inf ? "<=" : ">=") << " ";);
775 add_sub(false, a, b, c);
776 STRACE("mpff_trace", display(tout, c); tout << "\n";);
777 }
778
sub(mpff const & a,mpff const & b,mpff & c)779 void mpff_manager::sub(mpff const & a, mpff const & b, mpff & c) {
780 STRACE("mpff_trace", tout << "[mpff] "; display(tout, a); tout << " - "; display(tout, b); tout << " " << (m_to_plus_inf ? "<=" : ">=") << " ";);
781 add_sub(true, a, b, c);
782 STRACE("mpff_trace", display(tout, c); tout << "\n";);
783 }
784
mul(mpff const & a,mpff const & b,mpff & c)785 void mpff_manager::mul(mpff const & a, mpff const & b, mpff & c) {
786 STRACE("mpff_trace", tout << "[mpff] ("; display(tout, a); tout << ") * ("; display(tout, b); tout << ") " << (m_to_plus_inf ? "<=" : ">=") << " ";);
787 if (is_zero(a) || is_zero(b)) {
788 reset(c);
789 }
790 else {
791 allocate_if_needed(c);
792 TRACE("mpff", tout << "mul("; display(tout, a); tout << ", "; display(tout, b); tout << ")\n";);
793 c.m_sign = a.m_sign ^ b.m_sign;
794 // use int64_t to make sure we do not have overflows
795 int64_t exp_a = a.m_exponent;
796 int64_t exp_b = b.m_exponent;
797 int64_t exp_c = exp_a + exp_b;
798 // store result in m_buffers[0]
799 unsigned * r = m_buffers[0].data();
800 m_mpn_manager.mul(sig(a), m_precision, sig(b), m_precision, r);
801 // r has 2*m_precision_bits bits
802 unsigned num_leading_zeros = nlz(m_precision*2, r);
803 SASSERT(num_leading_zeros <= m_precision_bits);
804 TRACE("mpff", tout << "num_leading_zeros: " << num_leading_zeros << "\n";);
805 // We must shift right (m_precision_bits - num_leading_zeros)
806 // If r does not have a 1 bit in the first (m_precision_bits - num_leading_zeros), then the result is precise.
807 unsigned shift = m_precision_bits - num_leading_zeros;
808 // Imprecision == "lost digits"
809 // If c.m_sign --> result became bigger (e.g., -3.1 --> -3)
810 // If !c.m_sign --> result became smaller (e.g., 3.1 --> 3)
811 // Thus, when we are imprecise, we only need to bump the significand when:
812 // 1) !c.m_sign && m_to_plus_inf
813 // 2) c.m_sign && !m_to_plus_inf
814 bool _inc_significand = ((c.m_sign == 1) != m_to_plus_inf) && has_one_at_first_k_bits(m_precision*2, r, shift);
815 TRACE("mpff",
816 tout << "c.m_sign: " << c.m_sign << ", m_to_plus_inf: " << m_to_plus_inf
817 << "\nhas_one_at_first_k_bits: " << has_one_at_first_k_bits(m_precision*2, r, shift) << "\n";
818 tout << "_inc_significand: " << _inc_significand << "\n";);
819 exp_c += shift;
820 unsigned * s_c = sig(c);
821 shr(m_precision*2, r, shift, m_precision, s_c);
822 if (_inc_significand)
823 inc_significand(s_c, exp_c);
824 set_exponent(c, exp_c);
825 TRACE("mpff", tout << "result: "; display(tout, c); tout << "\n";);
826 SASSERT(check(c));
827 }
828 STRACE("mpff_trace", display(tout, c); tout << "\n";);
829 }
830
div(mpff const & a,mpff const & b,mpff & c)831 void mpff_manager::div(mpff const & a, mpff const & b, mpff & c) {
832 if (is_zero(b))
833 throw div0_exception();
834 STRACE("mpff_trace", tout << "[mpff] ("; display(tout, a); tout << ") / ("; display(tout, b); tout << ") " << (m_to_plus_inf ? "<=" : ">=") << " ";);
835 if (is_zero(a)) {
836 reset(c);
837 }
838 #if 1
839 else if (is_two(b)) {
840 set(c, a);
841 int64_t exp_c = a.m_exponent;
842 exp_c--;
843 set_exponent(c, exp_c);
844 }
845 #endif
846 else {
847 allocate_if_needed(c);
848 c.m_sign = a.m_sign ^ b.m_sign;
849 // use int64_t to make sure we do not have overflows
850 int64_t exp_a = a.m_exponent;
851 int64_t exp_b = b.m_exponent;
852 int64_t exp_c = exp_a - exp_b;
853
854 exp_c -= m_precision_bits; // we will multiplying (shifting) a by 2^m_precision_bits.
855 // copy a to buffer 0, and shift by m_precision_bits
856 to_buffer_shifting(0, a);
857 unsigned * _a = m_buffers[0].data();
858 unsigned * q = m_buffers[1].data();
859 unsigned q_sz = m_precision + 1; // 2*m_precision - m_precision + 1
860 unsigned * r = m_buffers[2].data();
861 unsigned r_sz = m_precision;
862 SASSERT(!::is_zero(2*m_precision, _a));
863 SASSERT(!::is_zero(m_precision, sig(b)));
864 SASSERT(nlz(2*m_precision, _a) == 0);
865 // Thus it is always the case that _a > b since size(a) = 2*size(b)
866 // Actually, a is much bigger than b.
867 // b is at most 2^m_precision_bits - 1
868 // a is at least 2^(2*m_precision_bits - 1)
869 // Thus the quotient of a/b cannot be zero
870 // Actually, quotient of a/b must be >= 2^(2*m_precision_bits - 1)/(2^m_precision_bits - 1)
871 m_mpn_manager.div(_a, 2 * m_precision,
872 sig(b), m_precision,
873 q,
874 r);
875 TRACE("mpff_div",
876 unsigned j = q_sz;
877 while (j > 0) { --j; tout << std::hex << std::setfill('0') << std::setw(2*sizeof(unsigned)) << q[j]; tout << " "; }
878 tout << std::dec << "\n";);
879 SASSERT(!::is_zero(q_sz, q));
880 unsigned num_leading_zeros = nlz(q_sz, q);
881 SASSERT(num_leading_zeros < q_sz * 8 * sizeof(unsigned));
882 unsigned q_bits = q_sz * 8 * sizeof(unsigned);
883 SASSERT(num_leading_zeros < q_bits);
884 unsigned actual_q_bits = q_bits - num_leading_zeros;
885 bool _inc_significand;
886 unsigned * s_c = sig(c);
887 if (actual_q_bits > m_precision_bits) {
888 unsigned shift = actual_q_bits - m_precision_bits;
889 // We are imprecise if the remainder is != 0 or if we lost a bit when shifting.
890 // See comment in mul(...)
891 _inc_significand =
892 ((c.m_sign == 1) != m_to_plus_inf) &&
893 (has_one_at_first_k_bits(q_sz, q, shift) ||
894 !::is_zero(r_sz, r));
895 exp_c += shift;
896 shr(q_sz, q, shift, m_precision, s_c);
897 }
898 else {
899 // We are imprecise only if the remainder is != 0
900 _inc_significand =
901 ((c.m_sign == 1) != m_to_plus_inf) &&
902 !::is_zero(r_sz, r);
903 if (actual_q_bits < m_precision_bits) {
904 unsigned shift = m_precision_bits - actual_q_bits;
905 exp_c -= shift;
906 shl(q_sz, q, shift, m_precision, s_c);
907 }
908 else {
909 SASSERT(actual_q_bits == m_precision_bits);
910 ::copy(q_sz, q, m_precision, s_c);
911 }
912 }
913 if (_inc_significand)
914 inc_significand(s_c, exp_c);
915 set_exponent(c, exp_c);
916 SASSERT(check(c));
917 }
918 STRACE("mpff_trace", display(tout, c); tout << "\n";);
919 }
920
floor(mpff & n)921 void mpff_manager::floor(mpff & n) {
922 if (n.m_exponent >= 0)
923 return;
924 STRACE("mpff_trace", tout << "[mpff] Floor["; display(tout, n); tout << "] == ";);
925 if (n.m_exponent <= -static_cast<int>(m_precision_bits)) {
926 // number is between (-1, 1)
927 if (n.m_sign == 0)
928 reset(n);
929 else
930 set(n, -1);
931 }
932 else {
933 unsigned * s = sig(n);
934 if (n.m_sign == 1 && has_one_at_first_k_bits(m_precision, s, -n.m_exponent)) {
935 shr(m_precision, s, -n.m_exponent, m_precision, s);
936 VERIFY(::inc(m_precision, s));
937 int num_leading_zeros = nlz(m_precision, s);
938 SASSERT(num_leading_zeros == -n.m_exponent || num_leading_zeros == -n.m_exponent - 1);
939 if (num_leading_zeros != -n.m_exponent) {
940 shl(m_precision, s, -n.m_exponent - 1, m_precision, s);
941 n.m_exponent++;
942 }
943 else {
944 shl(m_precision, s, -n.m_exponent, m_precision, s) ;
945 }
946 }
947 else {
948 // reset first n.m_exponent bits
949 shr(m_precision, s, -n.m_exponent, m_precision, s);
950 shl(m_precision, s, -n.m_exponent, m_precision, s);
951 }
952 }
953 SASSERT(check(n));
954 STRACE("mpff_trace", display(tout, n); tout << "\n";);
955 }
956
ceil(mpff & n)957 void mpff_manager::ceil(mpff & n) {
958 if (n.m_exponent >= 0)
959 return;
960 STRACE("mpff_trace", tout << "[mpff] Ceiling["; display(tout, n); tout << "] == ";);
961 if (n.m_exponent <= -static_cast<int>(m_precision_bits)) {
962 // number is between (-1, 1)
963 if (n.m_sign == 0)
964 set(n, 1);
965 else
966 reset(n);
967 }
968 else {
969 unsigned * s = sig(n);
970 if (n.m_sign == 0 && has_one_at_first_k_bits(m_precision, s, -n.m_exponent)) {
971 shr(m_precision, s, -n.m_exponent, m_precision, s);
972 VERIFY(::inc(m_precision, s));
973 int num_leading_zeros = nlz(m_precision, s);
974 SASSERT(num_leading_zeros == -n.m_exponent || num_leading_zeros == -n.m_exponent - 1);
975 if (num_leading_zeros != -n.m_exponent) {
976 shl(m_precision, s, -n.m_exponent - 1, m_precision, s);
977 n.m_exponent++;
978 }
979 else {
980 shl(m_precision, s, -n.m_exponent, m_precision, s) ;
981 }
982 }
983 else {
984 // reset first n.m_exponent bits
985 shr(m_precision, s, -n.m_exponent, m_precision, s);
986 shl(m_precision, s, -n.m_exponent, m_precision, s);
987 }
988 }
989 SASSERT(check(n));
990 STRACE("mpff_trace", display(tout, n); tout << "\n";);
991 }
992
power(mpff const & a,unsigned p,mpff & b)993 void mpff_manager::power(mpff const & a, unsigned p, mpff & b) {
994 #ifdef _TRACE
995 scoped_mpff _a(*this); _a = a;
996 unsigned _p = p;
997 #endif
998 #define SMALL_POWER 8
999 SASSERT(check(a));
1000 if (is_zero(a)) {
1001 SASSERT(p != 0);
1002 reset(b);
1003 }
1004 else if (p == 0) {
1005 set(b, 1);
1006 }
1007 else if (p == 1) {
1008 set(b, a);
1009 }
1010 else if (p == 2) {
1011 mul(a, a, b);
1012 }
1013 else if (p <= SMALL_POWER && &a != &b) {
1014 SASSERT(p > 2);
1015 --p;
1016 set(b, a);
1017 while (p > 0) {
1018 --p;
1019 mul(a, b, b);
1020 }
1021 }
1022 else {
1023 unsigned * s = sig(a);
1024 if (s[m_precision - 1] == 0x80000000u && ::is_zero(m_precision - 1, s)) {
1025 allocate_if_needed(b);
1026 if (p % 2 == 0)
1027 b.m_sign = 0;
1028 else
1029 b.m_sign = a.m_sign;
1030 int64_t exp = a.m_exponent;
1031 exp *= p;
1032 if (exp > INT_MAX || exp < INT_MIN)
1033 throw overflow_exception();
1034 exp += (m_precision_bits - 1)*(p - 1);
1035 if (exp > INT_MAX || exp < INT_MIN)
1036 throw overflow_exception();
1037 unsigned * r = sig(b);
1038 r[m_precision - 1] = 0x80000000u;
1039 for (unsigned i = 0; i < m_precision - 1; i++)
1040 r[i] = 0;
1041 b.m_exponent = static_cast<int>(exp);
1042 }
1043 else {
1044 unsigned mask = 1;
1045 scoped_mpff pw(*this);
1046 set(pw, a);
1047 set(b, 1);
1048 while (mask <= p) {
1049 if (mask & p)
1050 mul(b, pw, b);
1051 mul(pw, pw, pw);
1052 mask = mask << 1;
1053 }
1054 }
1055 }
1056 STRACE("mpff_trace", tout << "[mpff] ("; display(tout, _a); tout << ") ^ " << _p << (m_to_plus_inf ? "<=" : ">="); display(tout, b); tout << "\n";);
1057 TRACE("mpff_power", display_raw(tout, b); tout << "\n";);
1058 SASSERT(check(b));
1059 }
1060
is_power_of_two(mpff const & a,unsigned & k) const1061 bool mpff_manager::is_power_of_two(mpff const & a, unsigned & k) const {
1062 if (!is_power_of_two(a))
1063 return false;
1064 int64_t exp = a.m_exponent + m_precision_bits - 1;
1065 SASSERT(exp >= 0);
1066 k = static_cast<unsigned>(exp);
1067 return true;
1068 }
1069
is_power_of_two(mpff const & a) const1070 bool mpff_manager::is_power_of_two(mpff const & a) const {
1071 unsigned * s = sig(a);
1072 return is_pos(a) && a.m_exponent > -static_cast<int>(m_precision_bits) && s[m_precision - 1] == 0x80000000u && ::is_zero(m_precision - 1, s);
1073 }
1074
1075 template<bool SYNCH>
significand_core(mpff const & n,mpz_manager<SYNCH> & m,mpz & t)1076 void mpff_manager::significand_core(mpff const & n, mpz_manager<SYNCH> & m, mpz & t) {
1077 m.set_digits(t, m_precision, sig(n));
1078 }
1079
significand(mpff const & n,unsynch_mpz_manager & m,mpz & t)1080 void mpff_manager::significand(mpff const & n, unsynch_mpz_manager & m, mpz & t) {
1081 significand_core(n, m, t);
1082 }
1083
1084 #ifndef SINGLE_THREAD
significand(mpff const & n,synch_mpz_manager & m,mpz & t)1085 void mpff_manager::significand(mpff const & n, synch_mpz_manager & m, mpz & t) {
1086 significand_core(n, m, t);
1087 }
1088 #endif
1089
1090 template<bool SYNCH>
to_mpz_core(mpff const & n,mpz_manager<SYNCH> & m,mpz & t)1091 void mpff_manager::to_mpz_core(mpff const & n, mpz_manager<SYNCH> & m, mpz & t) {
1092 SASSERT(is_int(n));
1093 int exp = n.m_exponent;
1094 if (exp < 0) {
1095 SASSERT(exp > -static_cast<int>(m_precision_bits));
1096 to_buffer(0, n);
1097 unsigned * b = m_buffers[0].data();
1098 shr(m_precision, b, -exp, m_precision, b);
1099 m.set_digits(t, m_precision, b);
1100 }
1101 else {
1102 m.set_digits(t, m_precision, sig(n));
1103 if (exp > 0) {
1104 _scoped_numeral<mpz_manager<SYNCH> > p(m);
1105 m.set(p, 2);
1106 m.power(p, exp, p);
1107 m.mul(t, p, t);
1108 }
1109 }
1110 if (is_neg(n))
1111 m.neg(t);
1112 }
1113
to_mpz(mpff const & n,unsynch_mpz_manager & m,mpz & t)1114 void mpff_manager::to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t) {
1115 to_mpz_core(n, m, t);
1116 }
1117
1118 #ifndef SINGLE_THREAD
to_mpz(mpff const & n,synch_mpz_manager & m,mpz & t)1119 void mpff_manager::to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t) {
1120 to_mpz_core(n, m, t);
1121 }
1122 #endif
1123
1124 template<bool SYNCH>
to_mpq_core(mpff const & n,mpq_manager<SYNCH> & m,mpq & t)1125 void mpff_manager::to_mpq_core(mpff const & n, mpq_manager<SYNCH> & m, mpq & t) {
1126 int exp = n.m_exponent;
1127 TRACE("mpff_to_mpq", tout << "to_mpq: "; display(tout, n); tout << "\nexp: " << exp << "\n";);
1128 if (exp < 0 && exp > -static_cast<int>(m_precision_bits) && !has_one_at_first_k_bits(m_precision, sig(n), -n.m_exponent)) {
1129 to_buffer(0, n);
1130 unsigned * b = m_buffers[0].data();
1131 shr(m_precision, b, -exp, m_precision, b);
1132 m.set(t, m_precision, b);
1133 }
1134 else {
1135 m.set(t, m_precision, sig(n));
1136 if (exp != 0) {
1137 _scoped_numeral<mpq_manager<SYNCH> > p(m);
1138 m.set(p, 2);
1139 unsigned abs_exp;
1140 if (exp < 0) {
1141 // Avoid -INT_MIN == INT_MIN issue. It is not really useful, since we will run out of memory anyway.
1142 if (exp == INT_MIN)
1143 abs_exp = static_cast<unsigned>(-static_cast<int64_t>(INT_MIN));
1144 else
1145 abs_exp = -exp;
1146 }
1147 else {
1148 abs_exp = exp;
1149 }
1150 m.power(p, abs_exp, p);
1151 if (exp < 0)
1152 m.div(t, p, t);
1153 else
1154 m.mul(t, p, t);
1155 }
1156 }
1157 if (is_neg(n))
1158 m.neg(t);
1159 }
1160
to_mpq(mpff const & n,unsynch_mpq_manager & m,mpq & t)1161 void mpff_manager::to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t) {
1162 to_mpq_core(n, m, t);
1163 }
1164
1165 #ifndef SINGLE_THREAD
to_mpq(mpff const & n,synch_mpq_manager & m,mpq & t)1166 void mpff_manager::to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t) {
1167 to_mpq_core(n, m, t);
1168 }
1169 #endif
1170
display_raw(std::ostream & out,mpff const & n) const1171 void mpff_manager::display_raw(std::ostream & out, mpff const & n) const {
1172 if (is_neg(n))
1173 out << "-";
1174 unsigned * s = sig(n);
1175 unsigned i = m_precision;
1176 while(i > 0) {
1177 --i;
1178 out << std::hex << std::setfill('0') << std::setw(2 * sizeof(unsigned)) << s[i];
1179 }
1180 out << "*2^" << std::dec << n.m_exponent;
1181 }
1182
display(std::ostream & out,mpff const & n) const1183 void mpff_manager::display(std::ostream & out, mpff const & n) const {
1184 if (is_neg(n))
1185 out << "-";
1186 to_buffer_ext(0, n);
1187 svector<unsigned> & u_buffer = const_cast<mpff_manager*>(this)->m_buffers[0];
1188 int num_trailing_zeros = ntz(m_precision, u_buffer.data());
1189 int shift = 0;
1190 int64_t exp = n.m_exponent; // use int64_t to avoid -INT_MIN == INT_MIN issue
1191 if (exp < 0) {
1192 if (num_trailing_zeros >= -exp) {
1193 shift = static_cast<int>(-exp);
1194 exp = 0;
1195 }
1196 else {
1197 shift = num_trailing_zeros;
1198 exp += num_trailing_zeros;
1199 }
1200 }
1201 if (shift > 0)
1202 shr(m_precision, u_buffer.data(), shift, u_buffer.data());
1203 sbuffer<char, 1024> str_buffer(11*m_precision, 0);
1204 out << m_mpn_manager.to_string(u_buffer.data(), m_precision, str_buffer.begin(), str_buffer.size());
1205 if (exp > 0) {
1206 if (exp <= 63) {
1207 uint64_t _exp = 1;
1208 _exp <<= exp;
1209 out << "*" << _exp;
1210 }
1211 else {
1212 out << "*2";
1213 if (exp > 1) {
1214 out << "^";
1215 out << exp;
1216 }
1217 }
1218 }
1219 else if (exp < 0) {
1220 exp = -exp;
1221 if (exp <= 63) {
1222 uint64_t _exp = 1;
1223 _exp <<= exp;
1224 out << "/" << _exp;
1225 }
1226 else {
1227 out << "/2";
1228 if (exp > 1) {
1229 out << "^";
1230 out << exp;
1231 }
1232 }
1233 }
1234 }
1235
display_decimal(std::ostream & out,mpff const & n,unsigned prec,unsigned min_exponent)1236 void mpff_manager::display_decimal(std::ostream & out, mpff const & n, unsigned prec, unsigned min_exponent) {
1237 // The result in scientific notation when n.m_exponent >= min_exponent or n.m_exponent <= - min_exponent - m_precision_bits
1238 int64_t exp = n.m_exponent;
1239 if (exp >= min_exponent || exp <= -static_cast<int64_t>(min_exponent) - m_precision_bits || is_int(n)) {
1240 display(out, n);
1241 return;
1242 }
1243 if (is_neg(n))
1244 out << "-";
1245 unsigned word_sz = 8 * sizeof(unsigned);
1246 if (exp >= 0) {
1247 sbuffer<unsigned, 1024> buffer;
1248 unsigned num_extra_words = 1 + static_cast<unsigned>(exp/word_sz);
1249 unsigned shift = word_sz - exp%word_sz;
1250 for (unsigned i = 0; i < num_extra_words; i++)
1251 buffer.push_back(0);
1252 unsigned * s = sig(n);
1253 for (unsigned i = 0; i < m_precision; i++)
1254 buffer.push_back(s[i]);
1255 shr(buffer.size(), buffer.data(), shift, buffer.size(), buffer.data());
1256 sbuffer<char, 1024> str_buffer(11*buffer.size(), 0);
1257 out << m_mpn_manager.to_string(buffer.data(), buffer.size(), str_buffer.begin(), str_buffer.size());
1258 }
1259 else {
1260 sbuffer<unsigned, 1024> buffer1, buffer2;
1261 sbuffer<unsigned> buffer3;
1262 exp = -exp;
1263 unsigned num_words = 1 + static_cast<unsigned>(exp/word_sz);
1264 unsigned num_extra_words = m_precision < num_words ? num_words - m_precision : 0;
1265 num_extra_words++;
1266 unsigned * s = sig(n);
1267 for (unsigned i = 0; i < m_precision; i++) {
1268 buffer1.push_back(s[i]);
1269 buffer2.push_back(0);
1270 buffer3.push_back(0);
1271 }
1272 for (unsigned i = 0; i < num_extra_words; i++) {
1273 buffer1.push_back(0);
1274 buffer2.push_back(0);
1275 }
1276 unsigned ten = 10;
1277 sbuffer<unsigned, 1024> pw_buffer;
1278 pw_buffer.resize(num_words, 0);
1279 pw_buffer[0] = 1;
1280 shl(num_words, pw_buffer.data(), static_cast<unsigned>(exp), num_words, pw_buffer.data());
1281 if (num_words > m_precision) {
1282 out << "0";
1283 }
1284 else {
1285 m_mpn_manager.div(buffer1.data(), m_precision,
1286 pw_buffer.data(), num_words,
1287 buffer3.data(),
1288 buffer2.data());
1289 sbuffer<char, 1024> str_buffer(11*buffer3.size(), 0);
1290 out << m_mpn_manager.to_string(buffer3.data(), buffer3.size(), str_buffer.begin(), str_buffer.size());
1291 SASSERT(!::is_zero(buffer2.size(), buffer2.data())); // otherwise n is an integer
1292 ::copy(buffer2.size(), buffer2.data(), buffer1.size(), buffer1.data());
1293 }
1294 out << ".";
1295 // buffer1 contain the fractional part
1296 unsigned i = 0;
1297 unsigned sz1 = buffer1.size();
1298 while (sz1 > 0 && buffer1[sz1-1] == 0)
1299 --sz1;
1300 SASSERT(sz1 > 0); // otherwise the number is an integer
1301 while (sz1 > 0) {
1302 if (i >= prec) {
1303 out << "?";
1304 return;
1305 }
1306 i = i + 1;
1307 m_mpn_manager.mul(buffer1.data(), sz1, &ten, 1, buffer2.data());
1308 unsigned sz2 = sz1 + 1;
1309 while (sz2 > 0 && buffer2[sz2-1] == 0)
1310 --sz2;
1311 SASSERT(sz2 > 0);
1312 if (num_words > sz2) {
1313 out << "0";
1314 sz1 = sz2;
1315 ::copy(sz2, buffer2.data(), sz1, buffer1.data());
1316 SASSERT(sz1 == 0 || !::is_zero(sz1, buffer1.data()));
1317 }
1318 else {
1319 m_mpn_manager.div(buffer2.data(), sz2,
1320 pw_buffer.data(), num_words,
1321 buffer3.data(),
1322 buffer1.data());
1323 out << buffer3[0];
1324 sz1 = num_words;
1325 while (sz1 > 0 && buffer1[sz1-1] == 0)
1326 --sz1;
1327 SASSERT(sz1 == 0 || !::is_zero(sz1, buffer1.data()));
1328 }
1329 }
1330 }
1331 }
1332
display_smt2(std::ostream & out,mpff const & n,bool decimal) const1333 void mpff_manager::display_smt2(std::ostream & out, mpff const & n, bool decimal) const {
1334 if (is_neg(n))
1335 out << "(- ";
1336 to_buffer_ext(0, n);
1337 svector<unsigned> & u_buffer = const_cast<mpff_manager*>(this)->m_buffers[0];
1338 int num_trailing_zeros = ntz(m_precision, u_buffer.data());
1339 int shift = 0;
1340 int64_t exp = n.m_exponent;
1341 if (exp < 0) {
1342 if (num_trailing_zeros >= -exp) {
1343 shift = static_cast<int>(-exp);
1344 exp = 0;
1345 }
1346 else {
1347 shift = num_trailing_zeros;
1348 exp += num_trailing_zeros;
1349 }
1350 }
1351 if (shift > 0)
1352 shr(m_precision, u_buffer.data(), shift, u_buffer.data());
1353
1354 if (exp > 0)
1355 out << "(* ";
1356 else if (exp < 0)
1357 out << "(/ ";
1358
1359 sbuffer<char, 1024> str_buffer(11*m_precision, 0);
1360 out << m_mpn_manager.to_string(u_buffer.data(), m_precision, str_buffer.begin(), str_buffer.size());
1361 if (decimal) out << ".0";
1362
1363 if (exp != 0) {
1364 if (exp < 0) exp = -exp;
1365 if (exp <= 63) {
1366 uint64_t _exp = 1;
1367 _exp <<= exp;
1368 out << _exp;
1369 if (decimal) out << ".0";
1370 }
1371 else {
1372 out << " (^ 2";
1373 if (decimal) out << ".0";
1374 out << " " << exp;
1375 if (decimal) out << ".0";
1376 out << ")";
1377 }
1378 out << ")";
1379 }
1380 if (is_neg(n))
1381 out << ")";
1382 }
1383
to_string(mpff const & a) const1384 std::string mpff_manager::to_string(mpff const & a) const {
1385 std::ostringstream buffer;
1386 display(buffer, a);
1387 return buffer.str();
1388 }
1389
to_rational_string(mpff const & a) const1390 std::string mpff_manager::to_rational_string(mpff const & a) const {
1391 // The exponent may be too big to encode without using 2^
1392 return to_string(a);
1393 }
1394
prev_power_of_two(mpff const & a)1395 unsigned mpff_manager::prev_power_of_two(mpff const & a) {
1396 if (!is_pos(a))
1397 return 0;
1398 if (a.m_exponent <= -static_cast<int>(m_precision_bits))
1399 return 0; // Number is smaller than 1
1400 SASSERT(static_cast<int64_t>(a.m_exponent) + static_cast<int64_t>(m_precision_bits) - 1 >= 0);
1401 SASSERT(static_cast<int64_t>(a.m_exponent) + static_cast<int64_t>(m_precision_bits) - 1 <= static_cast<int64_t>(static_cast<uint64_t>(UINT_MAX)));
1402 return m_precision_bits + a.m_exponent - 1;
1403 }
1404
check(mpff const & n) const1405 bool mpff_manager::check(mpff const & n) const {
1406 // n is zero or the most significand bit of the most significand word is 1.
1407 unsigned * s = sig(n);
1408 (void)s;
1409 SASSERT(is_zero(n) || (s[m_precision - 1] & MIN_MSW) != 0);
1410 // if n is zero, then the sign must be 0
1411 SASSERT(!is_zero(n) || n.m_sign == 0);
1412 // if n is zero, then all bits must be 0.
1413 SASSERT(!is_zero(n) || ::is_zero(m_precision, sig(n)));
1414 // if n is zero, then exponent must be 0.
1415 SASSERT(!is_zero(n) || n.m_exponent == 0);
1416 return true;
1417 }
1418