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