PPL  1.2
Float_inlines.hh
Go to the documentation of this file.
1 /* IEC 559 floating point format related functions.
2  Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3  Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4 
5 This file is part of the Parma Polyhedra Library (PPL).
6 
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11 
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16 
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20 
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23 
24 #ifndef PPL_Float_inlines_hh
25 #define PPL_Float_inlines_hh 1
26 
27 #include "Variable_defs.hh"
28 #include "Linear_Form_defs.hh"
29 #include "assertions.hh"
30 #include <climits>
31 
32 namespace Parma_Polyhedra_Library {
33 
34 inline int
36  if (word == NEG_INF) {
37  return -1;
38  }
39  if (word == POS_INF) {
40  return 1;
41  }
42  return 0;
43 }
44 
45 inline bool
47  return (word & ~SGN_MASK) > POS_INF;
48 }
49 
50 inline int
52  if (word == NEG_ZERO) {
53  return -1;
54  }
55  if (word == POS_ZERO) {
56  return 1;
57  }
58  return 0;
59 }
60 
61 inline void
63  word ^= SGN_MASK;
64 }
65 
66 inline bool
68  return (word & SGN_MASK) != 0;
69 }
70 
71 inline void
73  --word;
74 }
75 
76 inline void
78  ++word;
79 }
80 
81 inline void
83  word = WRD_MAX;
84  if (negative) {
85  word |= SGN_MASK;
86  }
87 }
88 
89 inline void
90 float_ieee754_half::build(bool negative, mpz_t mantissa, int exponent) {
91  word = static_cast<uint16_t>(mpz_get_ui(mantissa)
92  & ((1UL << MANTISSA_BITS) - 1));
93  if (negative) {
94  word |= SGN_MASK;
95  }
96  const int exponent_repr = exponent + EXPONENT_BIAS;
97  PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
98  word |= static_cast<uint16_t>(exponent_repr) << MANTISSA_BITS;
99 }
100 
101 inline int
103  if (word == NEG_INF) {
104  return -1;
105  }
106  if (word == POS_INF) {
107  return 1;
108  }
109  return 0;
110 }
111 
112 inline bool
114  return (word & ~SGN_MASK) > POS_INF;
115 }
116 
117 inline int
119  if (word == NEG_ZERO) {
120  return -1;
121  }
122  if (word == POS_ZERO) {
123  return 1;
124  }
125  return 0;
126 }
127 
128 inline void
130  word ^= SGN_MASK;
131 }
132 
133 inline bool
135  return (word & SGN_MASK) != 0;
136 }
137 
138 inline void
140  --word;
141 }
142 
143 inline void
145  ++word;
146 }
147 
148 inline void
150  word = WRD_MAX;
151  if (negative) {
152  word |= SGN_MASK;
153  }
154 }
155 
156 inline void
157 float_ieee754_single::build(bool negative, mpz_t mantissa, int exponent) {
158  word = static_cast<uint32_t>(mpz_get_ui(mantissa)
159  & ((1UL << MANTISSA_BITS) - 1));
160  if (negative) {
161  word |= SGN_MASK;
162  }
163  const int exponent_repr = exponent + EXPONENT_BIAS;
164  PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
165  word |= static_cast<uint32_t>(exponent_repr) << MANTISSA_BITS;
166 }
167 
168 inline int
170  if (lsp != LSP_INF) {
171  return 0;
172  }
173  if (msp == MSP_NEG_INF) {
174  return -1;
175  }
176  if (msp == MSP_POS_INF) {
177  return 1;
178  }
179  return 0;
180 }
181 
182 inline bool
184  const uint32_t a = msp & ~MSP_SGN_MASK;
185  return a > MSP_POS_INF || (a == MSP_POS_INF && lsp != LSP_INF);
186 }
187 
188 inline int
190  if (lsp != LSP_ZERO) {
191  return 0;
192  }
193  if (msp == MSP_NEG_ZERO) {
194  return -1;
195  }
196  if (msp == MSP_POS_ZERO) {
197  return 1;
198  }
199  return 0;
200 }
201 
202 inline void
204  msp ^= MSP_SGN_MASK;
205 }
206 
207 inline bool
209  return (msp & MSP_SGN_MASK) != 0;
210 }
211 
212 inline void
214  if (lsp == 0) {
215  --msp;
216  lsp = LSP_MAX;
217  }
218  else {
219  --lsp;
220  }
221 }
222 
223 inline void
225  if (lsp == LSP_MAX) {
226  ++msp;
227  lsp = 0;
228  }
229  else {
230  ++lsp;
231  }
232 }
233 
234 inline void
236  msp = MSP_MAX;
237  lsp = LSP_MAX;
238  if (negative) {
239  msp |= MSP_SGN_MASK;
240  }
241 }
242 
243 inline void
244 float_ieee754_double::build(bool negative, mpz_t mantissa, int exponent) {
245  unsigned long m;
246 #if ULONG_MAX == 0xffffffffUL
247  lsp = mpz_get_ui(mantissa);
248  mpz_tdiv_q_2exp(mantissa, mantissa, 32);
249  m = mpz_get_ui(mantissa);
250 #else
251  m = mpz_get_ui(mantissa);
252  lsp = static_cast<uint32_t>(m & LSP_MAX);
253  m >>= 32;
254 #endif
255  msp = static_cast<uint32_t>(m & ((1UL << (MANTISSA_BITS - 32)) - 1));
256  if (negative) {
257  msp |= MSP_SGN_MASK;
258  }
259  const int exponent_repr = exponent + EXPONENT_BIAS;
260  PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
261  msp |= static_cast<uint32_t>(exponent_repr) << (MANTISSA_BITS - 32);
262 }
263 
264 inline int
266  if (word == NEG_INF) {
267  return -1;
268  }
269  if (word == POS_INF) {
270  return 1;
271  }
272  return 0;
273 }
274 
275 inline bool
277  return (word & ~SGN_MASK) > POS_INF;
278 }
279 
280 inline int
282  if (word == NEG_ZERO) {
283  return -1;
284  }
285  if (word == POS_ZERO) {
286  return 1;
287  }
288  return 0;
289 }
290 
291 inline void
293  word ^= SGN_MASK;
294 }
295 
296 inline bool
298  return (word & SGN_MASK) != 0;
299 }
300 
301 inline void
303  --word;
304 }
305 
306 inline void
308  ++word;
309 }
310 
311 inline void
313  word = WRD_MAX;
314  if (negative) {
315  word |= SGN_MASK;
316  }
317 }
318 
319 inline void
320 float_ibm_single::build(bool negative, mpz_t mantissa, int exponent) {
321  word = static_cast<uint32_t>(mpz_get_ui(mantissa)
322  & ((1UL << MANTISSA_BITS) - 1));
323  if (negative) {
324  word |= SGN_MASK;
325  }
326  const int exponent_repr = exponent + EXPONENT_BIAS;
327  PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
328  word |= static_cast<uint32_t>(exponent_repr) << MANTISSA_BITS;
329 }
330 
331 inline int
333  if (lsp != LSP_INF) {
334  return 0;
335  }
336  const uint32_t a = msp & MSP_NEG_INF;
337  if (a == MSP_NEG_INF) {
338  return -1;
339  }
340  if (a == MSP_POS_INF) {
341  return 1;
342  }
343  return 0;
344 }
345 
346 inline bool
348  return (msp & MSP_POS_INF) == MSP_POS_INF
349  && lsp != LSP_INF;
350 }
351 
352 inline int
354  if (lsp != LSP_ZERO) {
355  return 0;
356  }
357  const uint32_t a = msp & MSP_NEG_INF;
358  if (a == MSP_NEG_ZERO) {
359  return -1;
360  }
361  if (a == MSP_POS_ZERO) {
362  return 1;
363  }
364  return 0;
365 }
366 
367 inline void
369  msp ^= MSP_SGN_MASK;
370 }
371 
372 inline bool
374  return (msp & MSP_SGN_MASK) != 0;
375 }
376 
377 inline void
379  if ((lsp & LSP_DMAX) == 0) {
380  --msp;
381  lsp = ((msp & MSP_NEG_INF) == 0) ? LSP_DMAX : LSP_NMAX;
382  }
383  else {
384  --lsp;
385  }
386 }
387 
388 inline void
390  if ((lsp & LSP_DMAX) == LSP_DMAX) {
391  ++msp;
392  lsp = LSP_DMAX + 1;
393  }
394  else {
395  ++lsp;
396  }
397 }
398 
399 inline void
401  msp = MSP_MAX;
402  lsp = LSP_NMAX;
403  if (negative) {
404  msp |= MSP_SGN_MASK;
405  }
406 }
407 
408 inline void
410  mpz_t mantissa, int exponent) {
411 #if ULONG_MAX == 0xffffffffUL
412  mpz_export(&lsp, 0, -1, sizeof(lsp), 0, 0, mantissa);
413 #else
414  lsp = mpz_get_ui(mantissa);
415 #endif
416  msp = (negative ? MSP_SGN_MASK : 0);
417  const int exponent_repr = exponent + EXPONENT_BIAS;
418  PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
419  msp |= static_cast<uint32_t>(exponent_repr);
420 }
421 
422 inline int
424  if (lsp != LSP_INF) {
425  return 0;
426  }
427  if (msp == MSP_NEG_INF) {
428  return -1;
429  }
430  if (msp == MSP_POS_INF) {
431  return 1;
432  }
433  return 0;
434 }
435 
436 inline bool
438  return (msp & ~MSP_SGN_MASK) == MSP_POS_INF
439  && lsp != LSP_INF;
440 }
441 
442 inline int
444  if (lsp != LSP_ZERO) {
445  return 0;
446  }
447  if (msp == MSP_NEG_ZERO) {
448  return -1;
449  }
450  if (msp == MSP_POS_ZERO) {
451  return 1;
452  }
453  return 0;
454 }
455 
456 inline void
458  msp ^= MSP_SGN_MASK;
459 }
460 
461 inline bool
463  return (msp & MSP_SGN_MASK) != 0;
464 }
465 
466 inline void
468  if (lsp == 0) {
469  --msp;
470  lsp = LSP_MAX;
471  }
472  else {
473  --lsp;
474  }
475 }
476 
477 inline void
479  if (lsp == LSP_MAX) {
480  ++msp;
481  lsp = 0;
482  }
483  else {
484  ++lsp;
485  }
486 }
487 
488 inline void
490  msp = MSP_MAX;
491  lsp = LSP_MAX;
492  if (negative) {
493  msp |= MSP_SGN_MASK;
494  }
495 }
496 
497 inline void
498 float_ieee754_quad::build(bool negative, mpz_t mantissa, int exponent) {
499  uint64_t parts[2];
500  mpz_export(parts, 0, -1, sizeof(parts[0]), 0, 0, mantissa);
501  lsp = parts[0];
502  msp = parts[1];
503  msp &= ((static_cast<uint64_t>(1) << (MANTISSA_BITS - 64)) - 1);
504  if (negative) {
505  msp |= MSP_SGN_MASK;
506  }
507  const int exponent_repr = exponent + EXPONENT_BIAS;
508  PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
509  msp |= static_cast<uint64_t>(exponent_repr) << (MANTISSA_BITS - 64);
510 }
511 
512 inline bool
514  return f1 < f2;
515 }
516 
517 inline unsigned int
518 msb_position(unsigned long long v) {
519  return static_cast<unsigned int>(sizeof_to_bits(sizeof(v))) - 1U - clz(v);
520 }
521 
522 template <typename FP_Interval_Type>
523 inline void
525  Linear_Form<FP_Interval_Type> >& lf_store,
526  const Variable var,
527  const Linear_Form<FP_Interval_Type>& lf) {
528  // Assign the new linear form for var.
529  lf_store[var.id()] = lf;
530  // Now invalidate all linear forms in which var occurs.
531  discard_occurrences(lf_store, var);
532 }
533 
534 #if PPL_SUPPORTED_FLOAT
535 inline
536 Float<float>::Float() {
537 }
538 
539 inline
540 Float<float>::Float(float v) {
541  u.number = v;
542 }
543 
544 inline float
546  return u.number;
547 }
548 #endif
549 
550 #if PPL_SUPPORTED_DOUBLE
551 inline
552 Float<double>::Float() {
553 }
554 
555 inline
556 Float<double>::Float(double v) {
557  u.number = v;
558 }
559 
560 inline double
562  return u.number;
563 }
564 #endif
565 
566 #if PPL_SUPPORTED_LONG_DOUBLE
567 inline
568 Float<long double>::Float() {
569 }
570 
571 inline
572 Float<long double>::Float(long double v) {
573  u.number = v;
574 }
575 
576 inline long double
578  return u.number;
579 }
580 #endif
581 
582 } // namespace Parma_Polyhedra_Library
583 
584 #endif // !defined(PPL_Float_inlines_hh)
static const unsigned int MANTISSA_BITS
Definition: Float_defs.hh:93
void affine_form_image(std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, const Variable var, const Linear_Form< FP_Interval_Type > &lf)
size_t dimension_type
An unsigned integral type for representing space dimensions.
static const unsigned int MANTISSA_BITS
Definition: Float_defs.hh:171
void discard_occurrences(std::map< dimension_type, Linear_Form< FP_Interval_Type > > &lf_store, Variable var)
void build(bool negative, mpz_t mantissa, int exponent)
unsigned int msb_position(unsigned long long v)
If v is nonzero, returns the position of the most significant bit in a.
dimension_type id() const
Returns the index of the Cartesian axis associated to the variable.
A dimension of the vector space.
bool is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2)
void build(bool negative, mpz_t mantissa, int exponent)
#define sizeof_to_bits(size)
Definition: compiler.hh:80
A linear form with interval coefficients.
static const unsigned int EXPONENT_BITS
Definition: Float_defs.hh:92
void build(bool negative, mpz_t mantissa, int exponent)
static const unsigned int EXPONENT_BITS
Definition: Float_defs.hh:59
static const unsigned int MANTISSA_BITS
Definition: Float_defs.hh:263
void build(bool negative, mpz_t mantissa, int exponent)
The entire library is confined to this namespace.
Definition: version.hh:61
static const unsigned int EXPONENT_BITS
Definition: Float_defs.hh:170
unsigned int clz(unsigned int u)
Definition: compiler.hh:143
void build(bool negative, mpz_t mantissa, int exponent)
void build(bool negative, mpz_t mantissa, int exponent)
static const unsigned int EXPONENT_BITS
Definition: Float_defs.hh:262
static const unsigned int MANTISSA_BITS
Definition: Float_defs.hh:60