Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Martin Brain, Mathias Preiner
4 : : * Copyright (c) 2013 University of Oxford
5 : : *
6 : : * This file is part of the cvc5 project.
7 : : *
8 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9 : : * in the top-level source directory and their institutional affiliations.
10 : : * All rights reserved. See the file COPYING in the top-level source
11 : : * directory for licensing information.
12 : : * ****************************************************************************
13 : : *
14 : : * A floating-point value.
15 : : *
16 : : * This file contains the data structures used by the constant and parametric
17 : : * types of the floating point theory.
18 : : */
19 : : #include "cvc5_public.h"
20 : :
21 : : #ifndef CVC5__FLOATINGPOINT_H
22 : : #define CVC5__FLOATINGPOINT_H
23 : :
24 : : #include <memory>
25 : :
26 : : #include "util/bitvector.h"
27 : : #include "util/floatingpoint_size.h"
28 : : #include "util/rational.h"
29 : : #include "util/roundingmode.h"
30 : :
31 : : /* -------------------------------------------------------------------------- */
32 : :
33 : : namespace cvc5::internal {
34 : :
35 : : /* -------------------------------------------------------------------------- */
36 : :
37 : : class FloatingPointLiteral;
38 : :
39 : : class FloatingPoint
40 : : {
41 : : public:
42 : : /**
43 : : * Wrappers to represent results of non-total functions (e.g., min/max).
44 : : * The Boolean flag is true if the result is defined, and false otherwise.
45 : : */
46 : : using PartialFloatingPoint = std::pair<FloatingPoint, bool>;
47 : : using PartialBitVector = std::pair<BitVector, bool>;
48 : : using PartialRational = std::pair<Rational, bool>;
49 : :
50 : : /**
51 : : * Get the number of exponent bits in the unpacked format corresponding to a
52 : : * given packed format. This is the unpacked counter-part of
53 : : * FloatingPointSize::exponentWidth().
54 : : */
55 : : static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
56 : : /**
57 : : * Get the number of exponent bits in the unpacked format corresponding to a
58 : : * given packed format. This is the unpacked counter-part of
59 : : * FloatingPointSize::significandWidth().
60 : : */
61 : : static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
62 : :
63 : : /** Constructors. */
64 : :
65 : : /** Create a FP value from its IEEE bit-vector representation. */
66 : : FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv);
67 : : FloatingPoint(const FloatingPointSize& size, const BitVector& bv);
68 : :
69 : : /**
70 : : * Create a FP value from a signed or unsigned bit-vector value with
71 : : * respect to given rounding mode.
72 : : */
73 : : FloatingPoint(const FloatingPointSize& size,
74 : : const RoundingMode& rm,
75 : : const BitVector& bv,
76 : : bool signedBV);
77 : :
78 : : /**
79 : : * Create a FP value from a rational value with respect to given rounding
80 : : * mode.
81 : : */
82 : : FloatingPoint(const FloatingPointSize& size,
83 : : const RoundingMode& rm,
84 : : const Rational& r);
85 : :
86 : : /** Copy constructor. */
87 : : FloatingPoint(const FloatingPoint& fp);
88 : :
89 : : /** Destructor. */
90 : : ~FloatingPoint();
91 : :
92 : : /**
93 : : * Create a FP NaN value of given size.
94 : : * size: The FP size (format).
95 : : */
96 : : static FloatingPoint makeNaN(const FloatingPointSize& size);
97 : : /**
98 : : * Create a FP infinity value of given size.
99 : : * size: The FP size (format).
100 : : * sign: True for -oo, false otherwise.
101 : : */
102 : : static FloatingPoint makeInf(const FloatingPointSize& size, bool sign);
103 : : /**
104 : : * Create a FP zero value of given size.
105 : : * size: The FP size (format).
106 : : * sign: True for -zero, false otherwise.
107 : : */
108 : : static FloatingPoint makeZero(const FloatingPointSize& size, bool sign);
109 : : /**
110 : : * Create the smallest subnormal FP value of given size.
111 : : * size: The FP size (format).
112 : : * sign: True for negative sign, false otherwise.
113 : : */
114 : : static FloatingPoint makeMinSubnormal(const FloatingPointSize& size,
115 : : bool sign);
116 : : /**
117 : : * Create the largest subnormal FP value of given size.
118 : : * size: The FP size (format).
119 : : * sign: True for negative sign, false otherwise.
120 : : */
121 : : static FloatingPoint makeMaxSubnormal(const FloatingPointSize& size,
122 : : bool sign);
123 : : /**
124 : : * Create the smallest normal FP value of given size.
125 : : * size: The FP size (format).
126 : : * sign: True for negative sign, false otherwise.
127 : : */
128 : : static FloatingPoint makeMinNormal(const FloatingPointSize& size, bool sign);
129 : : /**
130 : : * Create the largest normal FP value of given size.
131 : : * size: The FP size (format).
132 : : * sign: True for negative sign, false otherwise.
133 : : */
134 : : static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign);
135 : :
136 : : /** Return the size of this FP value. */
137 : : const FloatingPointSize& getSize() const;
138 : :
139 : : /** Get the wrapped floating-point value. */
140 : 437 : const FloatingPointLiteral* getLiteral(void) const { return d_fpl.get(); }
141 : :
142 : : /**
143 : : * Return a string representation of this floating-point.
144 : : *
145 : : * If printAsIndexed is true then it prints the bit-vector components of the
146 : : * FP value as indexed symbols, otherwise in binary notation.
147 : : */
148 : : std::string toString(bool printAsIndexed = false) const;
149 : :
150 : : /**
151 : : * Get the IEEE bit-vector representation of this floating-point value.
152 : : * Stores the sign bit in `sign`, the exponent in `exp` and the significand
153 : : * in `sig`.
154 : : */
155 : : void getIEEEBitvectors(BitVector& sign, BitVector& exp, BitVector& sig) const;
156 : :
157 : : /** Return the packed (IEEE-754) representation of this floating-point. */
158 : : BitVector pack(void) const;
159 : :
160 : : /** Floating-point absolute value. */
161 : : FloatingPoint absolute(void) const;
162 : : /** Floating-point negation. */
163 : : FloatingPoint negate(void) const;
164 : : /** Floating-point addition. */
165 : : FloatingPoint add(const RoundingMode& rm, const FloatingPoint& arg) const;
166 : : /** Floating-point subtraction. */
167 : : FloatingPoint sub(const RoundingMode& rm, const FloatingPoint& arg) const;
168 : : /** Floating-point multiplication. */
169 : : FloatingPoint mult(const RoundingMode& rm, const FloatingPoint& arg) const;
170 : : /** Floating-point division. */
171 : : FloatingPoint div(const RoundingMode& rm, const FloatingPoint& arg) const;
172 : : /** Floating-point fused multiplication and addition. */
173 : : FloatingPoint fma(const RoundingMode& rm,
174 : : const FloatingPoint& arg1,
175 : : const FloatingPoint& arg2) const;
176 : : /** Floating-point square root. */
177 : : FloatingPoint sqrt(const RoundingMode& rm) const;
178 : : /** Floating-point round to integral. */
179 : : FloatingPoint rti(const RoundingMode& rm) const;
180 : : /** Floating-point remainder. */
181 : : FloatingPoint rem(const FloatingPoint& arg) const;
182 : :
183 : : /**
184 : : * Floating-point max (total version).
185 : : * zeroCase: true to return the left (rather than the right operand) in case
186 : : * of max(-0,+0) or max(+0,-0).
187 : : */
188 : : FloatingPoint maxTotal(const FloatingPoint& arg, bool zeroCaseLeft) const;
189 : : /**
190 : : * Floating-point min (total version).
191 : : * zeroCase: true to return the left (rather than the right operand) in case
192 : : * of min(-0,+0) or min(+0,-0).
193 : : */
194 : : FloatingPoint minTotal(const FloatingPoint& arg, bool zeroCaseLeft) const;
195 : :
196 : : /**
197 : : * Floating-point max.
198 : : *
199 : : * Returns a partial floating-point, which is a pair of FloatingPoint and
200 : : * bool. The boolean flag is true if the result is defined, and false if it
201 : : * is undefined.
202 : : */
203 : : PartialFloatingPoint max(const FloatingPoint& arg) const;
204 : : /** Floating-point min.
205 : : *
206 : : * Returns a partial floating-point, which is a pair of FloatingPoint and
207 : : * bool. The boolean flag is true if the result is defined, and false if it
208 : : * is undefined.
209 : : */
210 : : PartialFloatingPoint min(const FloatingPoint& arg) const;
211 : :
212 : : /** Equality (NOT: fp.eq but =) over floating-point values. */
213 : : bool operator==(const FloatingPoint& fp) const;
214 : : /** Floating-point less or equal than. */
215 : : bool operator<=(const FloatingPoint& arg) const;
216 : : /** Floating-point less than. */
217 : : bool operator<(const FloatingPoint& arg) const;
218 : :
219 : : /** Get the exponent of this floating-point value. */
220 : : BitVector getExponent() const;
221 : : /** Get the significand of this floating-point value. */
222 : : BitVector getSignificand() const;
223 : : /** True if this value is a negative value. */
224 : : bool getSign() const;
225 : :
226 : : /** Return true if this floating-point represents a normal value. */
227 : : bool isNormal(void) const;
228 : : /** Return true if this floating-point represents a subnormal value. */
229 : : bool isSubnormal(void) const;
230 : : /** Return true if this floating-point represents a zero value. */
231 : : bool isZero(void) const;
232 : : /** Return true if this floating-point represents an infinite value. */
233 : : bool isInfinite(void) const;
234 : : /** Return true if this floating-point represents a NaN value. */
235 : : bool isNaN(void) const;
236 : : /** Return true if this floating-point represents a negative value. */
237 : : bool isNegative(void) const;
238 : : /** Return true if this floating-point represents a positive value. */
239 : : bool isPositive(void) const;
240 : :
241 : : /**
242 : : * Convert this floating-point to a floating-point of given size, with
243 : : * respect to given rounding mode.
244 : : */
245 : : FloatingPoint convert(const FloatingPointSize& target,
246 : : const RoundingMode& rm) const;
247 : :
248 : : /**
249 : : * Convert this floating-point to a bit-vector of given size, with
250 : : * respect to given rounding mode (total version).
251 : : * Returns given bit-vector 'undefinedCase' in the undefined case.
252 : : */
253 : : BitVector convertToBVTotal(BitVectorSize width,
254 : : const RoundingMode& rm,
255 : : bool signedBV,
256 : : BitVector undefinedCase) const;
257 : : /**
258 : : * Convert this floating-point to a rational, with respect to given rounding
259 : : * mode (total version).
260 : : * Returns given rational 'undefinedCase' in the undefined case.
261 : : */
262 : : Rational convertToRationalTotal(Rational undefinedCase) const;
263 : :
264 : : /**
265 : : * Convert this floating-point to a bit-vector of given size.
266 : : *
267 : : * Returns a partial bit-vector, which is a pair of BitVector and bool.
268 : : * The boolean flag is true if the result is defined, and false if it
269 : : * is undefined.
270 : : */
271 : : PartialBitVector convertToBV(BitVectorSize width,
272 : : const RoundingMode& rm,
273 : : bool signedBV) const;
274 : : /**
275 : : * Convert this floating-point to a Rational.
276 : : *
277 : : * Returns a partial Rational, which is a pair of Rational and bool.
278 : : * The boolean flag is true if the result is defined, and false if it
279 : : * is undefined.
280 : : */
281 : : PartialRational convertToRational(void) const;
282 : :
283 : : private:
284 : : /**
285 : : * Constructor.
286 : : *
287 : : * Note: This constructor takes ownership of 'fpl' and is not intended for
288 : : * public use.
289 : : */
290 : : FloatingPoint(FloatingPointLiteral* fpl);
291 : :
292 : : /** The floating-point literal of this floating-point value. */
293 : : std::unique_ptr<FloatingPointLiteral> d_fpl;
294 : :
295 : : }; /* class FloatingPoint */
296 : :
297 : : /**
298 : : * Hash function for floating-point values.
299 : : */
300 : : struct FloatingPointHashFunction
301 : : {
302 : 112509 : size_t operator()(const FloatingPoint& fp) const
303 : : {
304 : : FloatingPointSizeHashFunction fpshf;
305 : : BitVectorHashFunction bvhf;
306 : :
307 : 112509 : return fpshf(fp.getSize()) ^ bvhf(fp.pack());
308 : : }
309 : : }; /* struct FloatingPointHashFunction */
310 : :
311 : : /* -------------------------------------------------------------------------- */
312 : :
313 : : /**
314 : : * The parameter type for the conversions to floating point.
315 : : */
316 : : class FloatingPointConvertSort
317 : : {
318 : : public:
319 : : /** Constructors. */
320 : 501 : FloatingPointConvertSort(uint32_t _e, uint32_t _s) : d_fp_size(_e, _s) {}
321 : 4379 : FloatingPointConvertSort(const FloatingPointSize& fps) : d_fp_size(fps) {}
322 : :
323 : : /** Operator overload for comparison of conversion sorts. */
324 : 5117 : bool operator==(const FloatingPointConvertSort& fpcs) const
325 : : {
326 : 5117 : return d_fp_size == fpcs.d_fp_size;
327 : : }
328 : :
329 : : /** Return the size of this FP convert sort. */
330 : 11063 : FloatingPointSize getSize() const { return d_fp_size; }
331 : :
332 : : private:
333 : : /** The floating-point size of this sort. */
334 : : FloatingPointSize d_fp_size;
335 : : };
336 : :
337 : : /** Hash function for conversion sorts. */
338 : : template <uint32_t key>
339 : : struct FloatingPointConvertSortHashFunction
340 : : {
341 : 5720 : inline size_t operator()(const FloatingPointConvertSort& fpcs) const
342 : : {
343 : : FloatingPointSizeHashFunction f;
344 : 5720 : return f(fpcs.getSize()) ^ (0x00005300 | (key << 24));
345 : : }
346 : : }; /* struct FloatingPointConvertSortHashFunction */
347 : :
348 : : /**
349 : : * As different conversions are different parameterised kinds, there
350 : : * is a need for different (C++) types for each one.
351 : : */
352 : :
353 : : /**
354 : : * Conversion from floating-point to IEEE bit-vector (first bit represents the
355 : : * sign, the following exponent width bits the exponent, and the remaining bits
356 : : * the significand).
357 : : */
358 : : class FloatingPointToFPIEEEBitVector : public FloatingPointConvertSort
359 : : {
360 : : public:
361 : : /** Constructors. */
362 : 122 : FloatingPointToFPIEEEBitVector(uint32_t _e, uint32_t _s)
363 : 122 : : FloatingPointConvertSort(_e, _s)
364 : : {
365 : 122 : }
366 : 4348 : FloatingPointToFPIEEEBitVector(const FloatingPointConvertSort& old)
367 : 4348 : : FloatingPointConvertSort(old)
368 : : {
369 : 4348 : }
370 : : };
371 : :
372 : : /**
373 : : * Conversion from floating-point to another floating-point (of possibly
374 : : * different size).
375 : : */
376 : : class FloatingPointToFPFloatingPoint : public FloatingPointConvertSort
377 : : {
378 : : public:
379 : : /** Constructors. */
380 : 27 : FloatingPointToFPFloatingPoint(uint32_t _e, uint32_t _s)
381 : 27 : : FloatingPointConvertSort(_e, _s)
382 : : {
383 : 27 : }
384 : : FloatingPointToFPFloatingPoint(const FloatingPointConvertSort& old)
385 : : : FloatingPointConvertSort(old)
386 : : {
387 : : }
388 : : };
389 : :
390 : : /**
391 : : * Conversion from floating-point to Real.
392 : : */
393 : : class FloatingPointToFPReal : public FloatingPointConvertSort
394 : : {
395 : : public:
396 : : /** Constructors. */
397 : 129 : FloatingPointToFPReal(uint32_t _e, uint32_t _s)
398 : 129 : : FloatingPointConvertSort(_e, _s)
399 : : {
400 : 129 : }
401 : 31 : FloatingPointToFPReal(const FloatingPointConvertSort& old)
402 : 31 : : FloatingPointConvertSort(old)
403 : : {
404 : 31 : }
405 : : };
406 : :
407 : : /**
408 : : * Conversion from floating-point to signed bit-vector value.
409 : : */
410 : : class FloatingPointToFPSignedBitVector : public FloatingPointConvertSort
411 : : {
412 : : public:
413 : : /** Constructors. */
414 : 75 : FloatingPointToFPSignedBitVector(uint32_t _e, uint32_t _s)
415 : 75 : : FloatingPointConvertSort(_e, _s)
416 : : {
417 : 75 : }
418 : : FloatingPointToFPSignedBitVector(const FloatingPointConvertSort& old)
419 : : : FloatingPointConvertSort(old)
420 : : {
421 : : }
422 : : };
423 : :
424 : : /**
425 : : * Conversion from floating-point to unsigned bit-vector value.
426 : : */
427 : : class FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort
428 : : {
429 : : public:
430 : : /** Constructors. */
431 : 148 : FloatingPointToFPUnsignedBitVector(uint32_t _e, uint32_t _s)
432 : 148 : : FloatingPointConvertSort(_e, _s)
433 : : {
434 : 148 : }
435 : 36 : FloatingPointToFPUnsignedBitVector(const FloatingPointConvertSort& old)
436 : 36 : : FloatingPointConvertSort(old)
437 : : {
438 : 36 : }
439 : : };
440 : :
441 : : /**
442 : : * Base type for floating-point to bit-vector conversion.
443 : : */
444 : : class FloatingPointToBV
445 : : {
446 : : public:
447 : : /** Constructors. */
448 : 42 : FloatingPointToBV(uint32_t s) : d_bv_size(s) {}
449 : 142 : FloatingPointToBV(const FloatingPointToBV& old) : d_bv_size(old.d_bv_size) {}
450 : : FloatingPointToBV(const BitVectorSize& old) : d_bv_size(old) {}
451 : :
452 : : /** Return the bit-width of the bit-vector to convert to. */
453 : 246 : operator uint32_t() const { return d_bv_size; }
454 : :
455 : : /** The bit-width of the bit-vector to converto to. */
456 : : BitVectorSize d_bv_size;
457 : : };
458 : :
459 : : /**
460 : : * Conversion from floating-point to unsigned bit-vector value.
461 : : */
462 : : class FloatingPointToUBV : public FloatingPointToBV
463 : : {
464 : : public:
465 : 22 : FloatingPointToUBV(uint32_t _s) : FloatingPointToBV(_s) {}
466 : : FloatingPointToUBV(const FloatingPointToBV& old) : FloatingPointToBV(old) {}
467 : : };
468 : :
469 : : /**
470 : : * Conversion from floating-point to signed bit-vector value.
471 : : */
472 : : class FloatingPointToSBV : public FloatingPointToBV
473 : : {
474 : : public:
475 : 20 : FloatingPointToSBV(uint32_t _s) : FloatingPointToBV(_s) {}
476 : : FloatingPointToSBV(const FloatingPointToBV& old) : FloatingPointToBV(old) {}
477 : : };
478 : :
479 : : /**
480 : : * Conversion from floating-point to unsigned bit-vector value (total version).
481 : : */
482 : : class FloatingPointToUBVTotal : public FloatingPointToBV
483 : : {
484 : : public:
485 : 0 : FloatingPointToUBVTotal(uint32_t _s) : FloatingPointToBV(_s) {}
486 : 18 : FloatingPointToUBVTotal(const FloatingPointToBV& old) : FloatingPointToBV(old)
487 : : {
488 : 18 : }
489 : : };
490 : :
491 : : /**
492 : : * Conversion from floating-point to signed bit-vector value (total version).
493 : : */
494 : : class FloatingPointToSBVTotal : public FloatingPointToBV
495 : : {
496 : : public:
497 : 0 : FloatingPointToSBVTotal(uint32_t _s) : FloatingPointToBV(_s) {}
498 : 13 : FloatingPointToSBVTotal(const FloatingPointToBV& old) : FloatingPointToBV(old)
499 : : {
500 : 13 : }
501 : : };
502 : :
503 : : /**
504 : : * Hash function for floating-point to bit-vector conversions.
505 : : */
506 : : template <uint32_t key>
507 : : struct FloatingPointToBVHashFunction
508 : : {
509 : 217 : inline size_t operator()(const FloatingPointToBV& fptbv) const
510 : : {
511 : : UnsignedHashFunction<cvc5::internal::BitVectorSize> f;
512 : 217 : return (key ^ 0x46504256) ^ f(fptbv.d_bv_size);
513 : : }
514 : : }; /* struct FloatingPointToBVHashFunction */
515 : :
516 : : /* Note: It is not possible to pack a number without a size to pack to,
517 : : * thus it is difficult to implement output stream operator overloads for
518 : : * FloatingPointLiteral in a sensible way. Use FloatingPoint instead. */
519 : :
520 : : /** Output stream operator overloading for floating-point values. */
521 : : std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp);
522 : :
523 : : /** Output stream operator overloading for floating-point formats. */
524 : : std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps);
525 : :
526 : : /** Output stream operator overloading for floating-point conversion sorts. */
527 : : std::ostream& operator<<(std::ostream& os,
528 : : const FloatingPointConvertSort& fpcs);
529 : :
530 : : } // namespace cvc5::internal
531 : :
532 : : #endif /* CVC5__FLOATINGPOINT_H */
|
