1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 mpff.h
7
8 Abstract:
9
10 Multi precision fast floating point numbers.
11 The implementation is not compliant with the IEEE standard.
12 For an IEEE compliant implementation, see mpf.h
13
14 There are only two rounding modes: towards plus or minus inf.
15
16 Author:
17
18 Leonardo de Moura (leonardo) 2012-09-12
19
20 Revision History:
21
22 --*/
23 #pragma once
24
25 #include "util/id_gen.h"
26 #include "util/util.h"
27 #include "util/vector.h"
28 #include "util/z3_exception.h"
29 #include "util/scoped_numeral.h"
30 #include "util/scoped_numeral_vector.h"
31 #include "util/mpn.h"
32
33 class mpff_manager;
34
35 class mpff {
36 friend class mpff_manager;
37 unsigned m_sign:1;
38 unsigned m_sig_idx:31; // position where the significand is stored in the mpff_manager.
39 int m_exponent;
40 public:
mpff()41 mpff():
42 m_sign(0),
43 m_sig_idx(0),
44 m_exponent(0) {
45 }
46
swap(mpff & other)47 void swap(mpff & other) {
48 unsigned sign = m_sign; m_sign = other.m_sign; other.m_sign = sign;
49 unsigned sig_idx = m_sig_idx; m_sig_idx = other.m_sig_idx; other.m_sig_idx = sig_idx;
50 std::swap(m_exponent, other.m_exponent);
51 }
52 };
53
swap(mpff & m1,mpff & m2)54 inline void swap(mpff & m1, mpff & m2) { m1.swap(m2); }
55
56 class mpz;
57 class mpq;
58 template<bool SYNCH> class mpz_manager;
59 template<bool SYNCH> class mpq_manager;
60 #ifndef SINGLE_THREAD
61 typedef mpz_manager<true> synch_mpz_manager;
62 typedef mpq_manager<true> synch_mpq_manager;
63 #else
64 typedef mpz_manager<false> synch_mpz_manager;
65 typedef mpq_manager<false> synch_mpq_manager;
66 #endif
67 typedef mpz_manager<false> unsynch_mpz_manager;
68 typedef mpq_manager<false> unsynch_mpq_manager;
69
70 class mpff_manager {
71 // Some restrictions on mpff numbers
72 //
73 // - The exponent is always a machine integer. The main point is that 2^(2^31) is a huge number,
74 // we will not even be able to convert the mpff into mpq. Formulas that need this kind of huge number
75 // are usually out-of-reach for Z3.
76 //
77 // - The significand size is measured in words of 32-bit. The number of words is always even.
78 // This decision makes sure that the size (in bits) of mpff numbers is always a multiple of 64.
79 // Thus mpff objs can be easily packed in 64-bit machines.
80 //
81 // - The smallest mpff numeral has 128-bits total. mpff structure has always 64-bits.
82 // The minimal size for the significand is 64-bits.
83 //
84 // - All mpff numerals in a given manager use the same number of words for storing the significand.
85 // This is different from the mpf_manager where the same manager can be used to manipulate floating point numbers
86 // of different precision.
87 //
88 // - In the encoding used for mpff numbers, the most significand bit of the most significand word is always 1.
89 // The only exception is the number zero.
90 // For example, assuming we are using 64-bits for the significand, the number 1 is encoded as
91 // (sign = 0, significand = 0x800..0, exponent = -63)
92 // Note that, in this representation, the smallest positive integer is:
93 // (sign = 0, significand = 0x800..0, exponent = INT_MIN)
94 // instead of
95 // (sign = 0, significand = 0x000..1, exponent = INT_MIN)
96 //
97 // Remarks:
98 //
99 // - All values of type int, unsigned, int64_t and uint64_t can be precisely represented as mpff numerals.
100 //
101 // - Hardware float and double values (corresponding to rationals) can also be precisely represented as mpff numerals.
102 // That is, NaN, +oo and -oo are not supported by this module.
103 //
104 // - An exception (mpff_manager::exception) is thrown if overflow occurs. This can happen because the exponent is
105 // represented as a machine integer.
106 //
107 // - There are only two rounding modes: towards plus infinity and towards minus infinity.
108 // The rounding mode can be dynamically modified.
109 //
110 // - The mpff numerals are stored in a dynamic array.
111 // Type mpff is just an index (unsigned) into this array.
112
113 unsigned m_precision; //!< Number of words in the significand. Must be an even number.
114 unsigned m_precision_bits; //!< Number of bits in the significand. Must be 32*m_precision.
115 mutable unsigned_vector m_significands; //!< Array containing all significands.
116 unsigned m_capacity; //!< Number of significands that can be stored in m_significands.
117 bool m_to_plus_inf; //!< If True, then round to plus infinity, otherwise to minus infinity
118 id_gen m_id_gen;
119 static const unsigned MPFF_NUM_BUFFERS = 4;
120 svector<unsigned> m_buffers[MPFF_NUM_BUFFERS];
121 svector<unsigned> m_set_buffer;
122 mpff m_one;
123 mpn_manager m_mpn_manager;
124
sig(mpff const & n)125 unsigned * sig(mpff const & n) const { return m_significands.data() + (n.m_sig_idx * m_precision); }
126
ensure_capacity(unsigned sig_idx)127 void ensure_capacity(unsigned sig_idx) {
128 while (sig_idx >= m_capacity)
129 expand();
130 }
131
132 void expand();
133
allocate_if_needed(mpff & n)134 void allocate_if_needed(mpff & n) {
135 if (n.m_sig_idx == 0)
136 allocate(n);
137 }
138
139 void allocate(mpff & n);
140
141 // copy n to buffer idx.
142 void to_buffer(unsigned idx, mpff const & n) const;
143 // copy n to buffer idx and add m_precision zeros.
144 void to_buffer_ext(unsigned idx, mpff const & n) const;
145 // copy (and shift by m_precision_bits) n to buffer idx
146 void to_buffer_shifting(unsigned idx, mpff const & n) const;
147
148 void inc_significand(unsigned * s, int64_t & exp);
149 void inc_significand(mpff & a);
150 void dec_significand(mpff & a);
151 bool min_significand(mpff const & a) const;
152 void set_min_significand(mpff & a);
153 void set_max_significand(mpff & a);
154 void set_big_exponent(mpff & a, int64_t e);
set_exponent(mpff & a,int64_t e)155 void set_exponent(mpff & a, int64_t e) {
156 if (e > INT_MAX || e < INT_MIN)
157 set_big_exponent(a, e);
158 else
159 a.m_exponent = static_cast<int>(e);
160 }
161
162 template<bool SYNCH>
163 void set_core(mpff & n, mpz_manager<SYNCH> & m, mpz const & v);
164
165 template<bool SYNCH>
166 void set_core(mpff & n, mpq_manager<SYNCH> & m, mpq const & v);
167
168 template<bool SYNCH>
169 void to_mpz_core(mpff const & n, mpz_manager<SYNCH> & m, mpz & t);
170
171 template<bool SYNCH>
172 void to_mpq_core(mpff const & n, mpq_manager<SYNCH> & m, mpq & t);
173
174 template<bool SYNCH>
175 void significand_core(mpff const & n, mpz_manager<SYNCH> & m, mpz & r);
176
177 void add_sub(bool is_sub, mpff const & a, mpff const & b, mpff & c);
178
179 public:
180 typedef mpff numeral;
precise()181 static bool precise() { return false; }
field()182 static bool field() { return true; }
183
184 class exception : public z3_exception {
msg()185 char const * msg() const override { return "multi-precision floating point (mpff) exception"; }
186 };
187
188 class overflow_exception : public exception {
msg()189 char const * msg() const override { return "multi-precision floating point (mpff) overflow"; }
190 };
191
192 class div0_exception : public exception {
msg()193 char const * msg() const override { return "multi-precision floating point (mpff) division by zero"; }
194 };
195
196 mpff_manager(unsigned prec = 2, unsigned initial_capacity = 1024);
197 ~mpff_manager();
198
round_to_plus_inf()199 void round_to_plus_inf() { m_to_plus_inf = true; }
round_to_minus_inf()200 void round_to_minus_inf() { m_to_plus_inf = false; }
set_rounding(bool to_plus_inf)201 void set_rounding(bool to_plus_inf) { m_to_plus_inf = to_plus_inf; }
rounding_to_plus_inf()202 bool rounding_to_plus_inf() const { return m_to_plus_inf; }
203
204 /**
205 \brief Return the exponent of n.
206 */
exponent(mpff const & n)207 static int exponent(mpff const & n) { return n.m_exponent; }
208
209 /**
210 \brief Update the exponent of n.
211
212 \remark It is a NOOP if n is zero.
213 */
set_exponent(mpff & n,int exp)214 void set_exponent(mpff & n, int exp) { if (is_zero(n)) return; n.m_exponent = exp; SASSERT(check(n)); }
215
216 /**
217 \brief Return the significand as a mpz numeral.
218 */
219 void significand(mpff const & n, unsynch_mpz_manager & m, mpz & r);
220 #ifndef SINGLE_THREAD
221 void significand(mpff const & n, synch_mpz_manager & m, mpz & r);
222 #endif
223
224 /**
225 \brief Return true if n is negative
226 */
sign(mpff const & n)227 static bool sign(mpff const & n) { return is_neg(n); }
228
229 /**
230 \brief Set n to zero.
231 */
232 void reset(mpff & n);
233
234 /**
235 \brief Return true if n is an integer.
236 */
237 bool is_int(mpff const & n) const;
238
239 /**
240 \brief Return true if n is zero.
241 */
is_zero(mpff const & n)242 static bool is_zero(mpff const & n) { return n.m_sig_idx == 0; }
243
244 /**
245 \brief Return true if n is positive.
246 */
is_pos(mpff const & n)247 static bool is_pos(mpff const & n) { return n.m_sign == 0 && !is_zero(n); }
248
249 /**
250 \brief Return true if n is negative.
251 */
is_neg(mpff const & n)252 static bool is_neg(mpff const & n) { return n.m_sign != 0; }
253
254 /**
255 \brief Return true if n is non positive.
256 */
is_nonpos(mpff const & n)257 static bool is_nonpos(mpff const & n) { return !is_pos(n); }
258
259 /**
260 \brief Return true if n is non negative.
261 */
is_nonneg(mpff const & n)262 static bool is_nonneg(mpff const & n) { return !is_neg(n); }
263
264 /**
265 \brief Return true if the absolute value of n is 1.
266 */
267 bool is_abs_one(mpff const & n) const;
268
269 /**
270 \brief Return true if n is one.
271 */
is_one(mpff const & n)272 bool is_one(mpff const & n) const { return is_pos(n) && is_abs_one(n); }
273
274 /**
275 \brief Return true if n is minus one.
276 */
is_minus_one(mpff const & n)277 bool is_minus_one(mpff const & n) const { return is_neg(n) && is_abs_one(n); }
278
279 /**
280 \brief Return true if n is two.
281 */
282 bool is_two(mpff const & n) const;
283
284 /**
285 \brief Return true if \c a is the smallest representable negative number.
286 */
287 bool is_minus_epsilon(mpff const & a) const;
288
289 /**
290 \brief Return true if \c a is the smallest representable positive number.
291 */
292 bool is_plus_epsilon(mpff const & a) const;
293
294 /**
295 \brief Return true if \c a is an integer and fits in an int64_t machine integer.
296 */
297 bool is_int64(mpff const & a) const;
298
299 /**
300 \brief Return true if \c a is a non-negative integer and fits in an int64_t machine integer.
301 */
302 bool is_uint64(mpff const & a) const;
303
304 /**
305 \brief Delete the resources associated with n.
306 */
307 void del(mpff & n);
308
309 /**
310 \brief a <- -a
311 */
neg(mpff & a)312 static void neg(mpff & a) { if (!is_zero(a)) a.m_sign = !a.m_sign; }
313
314 /**
315 \brief a <- |a|
316 */
abs(mpff & a)317 static void abs(mpff & a) { a.m_sign = 0; }
318
swap(mpff & a,mpff & b)319 static void swap(mpff & a, mpff & b) { a.swap(b); }
320
321 /**
322 \brief c <- a + b
323 */
324 void add(mpff const & a, mpff const & b, mpff & c);
325
326 /**
327 \brief c <- a - b
328 */
329 void sub(mpff const & a, mpff const & b, mpff & c);
330
331 /**
332 \brief a <- a + 1
333 */
inc(mpff & a)334 void inc(mpff & a) { add(a, m_one, a); }
335
336 /**
337 \brief a <- a - 1
338 */
dec(mpff & a)339 void dec(mpff & a) { sub(a, m_one, a); }
340
341 /**
342 \brief c <- a * b
343 */
344 void mul(mpff const & a, mpff const & b, mpff & c);
345
346 /**
347 \brief c <- a / b
348
349 \pre !is_zero(b)
350 */
351 void div(mpff const & a, mpff const & b, mpff & c);
352
353 /**
354 \brief a <- 1/a
355
356 \pre !is_zero(a);
357 */
inv(mpff & a)358 void inv(mpff & a) { div(m_one, a, a); }
inv(mpff const & a,mpff & b)359 void inv(mpff const & a, mpff & b) { set(b, a); inv(b); }
360
361 /**
362 \brief b <- a^k
363 */
364 void power(mpff const & a, unsigned k, mpff & b);
365
366 /**
367 \brief Return true if \c a is a power of 2. That is, a is equal to 2^k for some k >= 0.
368 */
369 bool is_power_of_two(mpff const & a, unsigned & k) const;
370 bool is_power_of_two(mpff const & a) const;
371
372 bool eq(mpff const & a, mpff const & b) const;
neq(mpff const & a,mpff const & b)373 bool neq(mpff const & a, mpff const & b) const { return !eq(a, b); }
374 bool lt(mpff const & a, mpff const & b) const;
gt(mpff const & a,mpff const & b)375 bool gt(mpff const & a, mpff const & b) const { return lt(b, a); }
le(mpff const & a,mpff const & b)376 bool le(mpff const & a, mpff const & b) const { return !lt(b, a); }
ge(mpff const & a,mpff const & b)377 bool ge(mpff const & a, mpff const & b) const { return !lt(a, b); }
378
379 void set(mpff & n, int v);
380 void set(mpff & n, unsigned v);
381 void set(mpff & n, int64_t v);
382 void set(mpff & n, uint64_t v);
383 void set(mpff & n, int num, unsigned den);
384 void set(mpff & n, int64_t num, uint64_t den);
385 void set(mpff & n, mpff const & v);
386 void set(mpff & n, unsynch_mpz_manager & m, mpz const & v);
387 void set(mpff & n, unsynch_mpq_manager & m, mpq const & v);
388 #ifndef SINGLE_THREAD
389 void set(mpff & n, synch_mpq_manager & m, mpq const & v);
390 void set(mpff & n, synch_mpz_manager & m, mpz const & v);
391 #endif
392 void set_plus_epsilon(mpff & n);
393 void set_minus_epsilon(mpff & n);
394 void set_max(mpff & n);
395 void set_min(mpff & n);
396
397 /**
398 \brief n <- floor(n)
399 */
400 void floor(mpff & n);
floor(mpff const & n,mpff & o)401 void floor(mpff const & n, mpff & o) { set(o, n); floor(o); }
402
403 /**
404 \brief n <- ceil(n)
405 */
406 void ceil(mpff & n);
ceil(mpff const & n,mpff & o)407 void ceil(mpff const & n, mpff & o) { set(o, n); ceil(o); }
408
409 /**
410 \brief Update \c a to the next representable float.
411
412 Throws an exception if \c a is the maximal representable float.
413 */
414 void next(mpff & a);
415 /**
416 \brief Update \c a to the previous representable float.
417
418 Throws an exception if \c a is the minimal representable float.
419 */
420 void prev(mpff & a);
421
422 /**
423 \brief Convert n into a mpz numeral.
424
425 \pre is_int(n)
426
427 \remark if exponent(n) is too big, we may run out of memory.
428 */
429 void to_mpz(mpff const & n, unsynch_mpz_manager & m, mpz & t);
430
431 #ifndef SINGLE_THREAD
432 /**
433 \brief Convert n into a mpz numeral.
434
435 \pre is_int(n)
436
437 \remark if exponent(n) is too big, we may run out of memory.
438 */
439 void to_mpz(mpff const & n, synch_mpz_manager & m, mpz & t);
440 #endif
441
442
443 /**
444 \brief Convert n into a mpq numeral.
445
446 \remark if exponent(n) is too big, we may run out of memory.
447 */
448 void to_mpq(mpff const & n, unsynch_mpq_manager & m, mpq & t);
449
450 #ifndef SINGLE_THREAD
451 /**
452 \brief Convert n into a mpq numeral.
453
454 \remark if exponent(n) is too big, we may run out of memory.
455 */
456 void to_mpq(mpff const & n, synch_mpq_manager & m, mpq & t);
457 #endif
458
459 /**
460 \brief Return n as an int64.
461
462 \pre is_int64(n)
463 */
464 int64_t get_int64(mpff const & n) const;
465
466 /**
467 \brief Return n as an uint64.
468
469 \pre is_uint64(n)
470 */
471 uint64_t get_uint64(mpff const & n) const;
472
473 /**
474 \brief Return the biggest k s.t. 2^k <= a.
475
476 \remark Return 0 if a is not positive.
477 */
478 unsigned prev_power_of_two(mpff const & a);
479
480 void display_raw(std::ostream & out, mpff const & n) const;
481 void display(std::ostream & out, mpff const & n) const;
display_pp(std::ostream & out,mpff const & n)482 void display_pp(std::ostream & out, mpff const & n) const { display(out, n); }
483 void display_decimal(std::ostream & out, mpff const & n, unsigned prec=32, unsigned max_power=128);
484 void display_smt2(std::ostream & out, mpff const & n, bool decimal=true) const;
485
486 std::string to_string(mpff const & a) const;
487 std::string to_rational_string(mpff const & a) const;
488
489 bool check(mpff const & n) const;
490 };
491
492 typedef _scoped_numeral<mpff_manager> scoped_mpff;
493 typedef _scoped_numeral_vector<mpff_manager> scoped_mpff_vector;
494
495