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 : :
16 : : #include "util/floatingpoint.h"
17 : :
18 : : #include <math.h>
19 : :
20 : : #include "base/check.h"
21 : : #include "util/floatingpoint_literal.h"
22 : : #include "util/integer.h"
23 : :
24 : : /* -------------------------------------------------------------------------- */
25 : :
26 : : namespace cvc5::internal {
27 : :
28 : : /* -------------------------------------------------------------------------- */
29 : :
30 : 198 : uint32_t FloatingPoint::getUnpackedExponentWidth(FloatingPointSize& size)
31 : : {
32 : 198 : return FloatingPointLiteral::getUnpackedExponentWidth(size);
33 : : }
34 : :
35 : 198 : uint32_t FloatingPoint::getUnpackedSignificandWidth(FloatingPointSize& size)
36 : : {
37 : 198 : return FloatingPointLiteral::getUnpackedSignificandWidth(size);
38 : : }
39 : :
40 : 6074 : FloatingPoint::FloatingPoint(uint32_t d_exp_size,
41 : : uint32_t d_sig_size,
42 : 6074 : const BitVector& bv)
43 : 6074 : : d_fpl(FloatingPointLiteral::create(d_exp_size, d_sig_size, bv))
44 : : {
45 : 6074 : }
46 : :
47 : 34 : FloatingPoint::FloatingPoint(const FloatingPointSize& size, const BitVector& bv)
48 : 34 : : d_fpl(FloatingPointLiteral::create(size, bv))
49 : : {
50 : 34 : }
51 : :
52 : 165 : FloatingPoint::FloatingPoint(const FloatingPointSize& size,
53 : : const RoundingMode& rm,
54 : : const BitVector& bv,
55 : 165 : bool signedBV)
56 : 165 : : d_fpl(FloatingPointLiteral::create(size, rm, bv, signedBV))
57 : : {
58 : 165 : }
59 : :
60 : 14093 : FloatingPoint::FloatingPoint(std::unique_ptr<FloatingPointLiteral>&& fpl)
61 : 14093 : : d_fpl(std::move(fpl))
62 : : {
63 : 14093 : }
64 : :
65 : 77 : FloatingPoint::FloatingPoint(const FloatingPointSize& size,
66 : : const RoundingMode& rm,
67 : 77 : const Rational& r)
68 : 77 : : d_fpl(FloatingPointLiteral::createFromRational(size, rm, r))
69 : : {
70 : 77 : }
71 : :
72 : 28194 : FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fpl(fp.d_fpl->clone())
73 : : {
74 : 28194 : }
75 : :
76 : 2 : FloatingPoint::FloatingPoint(FloatingPoint&& fp) noexcept
77 : 2 : : d_fpl(std::move(fp.d_fpl))
78 : : {
79 : 2 : }
80 : :
81 : 0 : FloatingPoint& FloatingPoint::operator=(const FloatingPoint& other)
82 : : {
83 [ - - ]: 0 : if (this != &other)
84 : : {
85 : 0 : d_fpl = other.d_fpl->clone();
86 : : }
87 : 0 : return *this;
88 : : }
89 : :
90 : 1 : FloatingPoint& FloatingPoint::operator=(FloatingPoint&& other) noexcept
91 : : {
92 [ + - ]: 1 : if (this != &other)
93 : : {
94 : 1 : d_fpl = std::move(other.d_fpl);
95 : : }
96 : 1 : return *this;
97 : : }
98 : :
99 : 48593 : FloatingPoint::~FloatingPoint() {}
100 : :
101 : 76798 : const FloatingPointSize& FloatingPoint::getSize() const
102 : : {
103 : 76798 : return d_fpl->getSize();
104 : : }
105 : :
106 : 237 : FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size)
107 : : {
108 : 474 : return FloatingPoint(FloatingPointLiteral::create(
109 : 474 : size, FloatingPointLiteral::SpecialConstKind::FPNAN));
110 : : }
111 : :
112 : 392 : FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign)
113 : : {
114 : 784 : return FloatingPoint(FloatingPointLiteral::create(
115 : 784 : size, FloatingPointLiteral::SpecialConstKind::FPINF, sign));
116 : : }
117 : :
118 : 430 : FloatingPoint FloatingPoint::makeZero(const FloatingPointSize& size, bool sign)
119 : : {
120 : 860 : return FloatingPoint(FloatingPointLiteral::create(
121 : 860 : size, FloatingPointLiteral::SpecialConstKind::FPZERO, sign));
122 : : }
123 : :
124 : 8 : FloatingPoint FloatingPoint::makeMinSubnormal(const FloatingPointSize& size,
125 : : bool sign)
126 : : {
127 [ + + ]: 8 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
128 : 8 : BitVector bvexp = BitVector::mkZero(size.packedExponentWidth());
129 : 8 : BitVector bvsig = BitVector::mkOne(size.packedSignificandWidth());
130 : 24 : return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
131 : 8 : }
132 : :
133 : 8 : FloatingPoint FloatingPoint::makeMaxSubnormal(const FloatingPointSize& size,
134 : : bool sign)
135 : : {
136 [ + + ]: 8 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
137 : 8 : BitVector bvexp = BitVector::mkZero(size.packedExponentWidth());
138 : 8 : BitVector bvsig = BitVector::mkOnes(size.packedSignificandWidth());
139 : 24 : return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
140 : 8 : }
141 : :
142 : 8 : FloatingPoint FloatingPoint::makeMinNormal(const FloatingPointSize& size,
143 : : bool sign)
144 : : {
145 [ + + ]: 8 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
146 : 8 : BitVector bvexp = BitVector::mkOne(size.packedExponentWidth());
147 : 8 : BitVector bvsig = BitVector::mkZero(size.packedSignificandWidth());
148 : 24 : return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
149 : 8 : }
150 : :
151 : 8 : FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size,
152 : : bool sign)
153 : : {
154 [ + + ]: 8 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
155 : 8 : BitVector bvexp = BitVector::mkOnes(size.packedExponentWidth());
156 : 8 : bvexp.setBit(0, false);
157 : 8 : BitVector bvsig = BitVector::mkOnes(size.packedSignificandWidth());
158 : 24 : return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
159 : 8 : }
160 : :
161 : 222 : FloatingPoint FloatingPoint::absolute(void) const
162 : : {
163 : 444 : return FloatingPoint(d_fpl->absolute());
164 : : }
165 : :
166 : 672 : FloatingPoint FloatingPoint::negate(void) const
167 : : {
168 : 1344 : return FloatingPoint(d_fpl->negate());
169 : : }
170 : :
171 : 4736 : FloatingPoint FloatingPoint::add(const RoundingMode& rm,
172 : : const FloatingPoint& arg) const
173 : : {
174 : 9472 : return FloatingPoint(d_fpl->add(rm, *arg.d_fpl));
175 : : }
176 : :
177 : 0 : FloatingPoint FloatingPoint::sub(const RoundingMode& rm,
178 : : const FloatingPoint& arg) const
179 : : {
180 : 0 : return FloatingPoint(d_fpl->sub(rm, *arg.d_fpl));
181 : : }
182 : :
183 : 2418 : FloatingPoint FloatingPoint::mult(const RoundingMode& rm,
184 : : const FloatingPoint& arg) const
185 : : {
186 : 4836 : return FloatingPoint(d_fpl->mult(rm, *arg.d_fpl));
187 : : }
188 : :
189 : 2 : FloatingPoint FloatingPoint::fma(const RoundingMode& rm,
190 : : const FloatingPoint& arg1,
191 : : const FloatingPoint& arg2) const
192 : : {
193 : 4 : return FloatingPoint(d_fpl->fma(rm, *arg1.d_fpl, *arg2.d_fpl));
194 : : }
195 : :
196 : 2605 : FloatingPoint FloatingPoint::div(const RoundingMode& rm,
197 : : const FloatingPoint& arg) const
198 : : {
199 : 5210 : return FloatingPoint(d_fpl->div(rm, *arg.d_fpl));
200 : : }
201 : :
202 : 1180 : FloatingPoint FloatingPoint::sqrt(const RoundingMode& rm) const
203 : : {
204 : 2360 : return FloatingPoint(d_fpl->sqrt(rm));
205 : : }
206 : :
207 : 210 : FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const
208 : : {
209 : 420 : return FloatingPoint(d_fpl->rti(rm));
210 : : }
211 : :
212 : 525 : FloatingPoint FloatingPoint::rem(const FloatingPoint& arg) const
213 : : {
214 : 1050 : return FloatingPoint(d_fpl->rem(*arg.d_fpl));
215 : : }
216 : :
217 : 424 : FloatingPoint FloatingPoint::maxTotal(const FloatingPoint& arg,
218 : : bool zeroCaseLeft) const
219 : : {
220 : 848 : return FloatingPoint(d_fpl->maxTotal(*arg.d_fpl, zeroCaseLeft));
221 : : }
222 : :
223 : 18 : FloatingPoint FloatingPoint::minTotal(const FloatingPoint& arg,
224 : : bool zeroCaseLeft) const
225 : : {
226 : 36 : return FloatingPoint(d_fpl->minTotal(*arg.d_fpl, zeroCaseLeft));
227 : : }
228 : :
229 : : // Suppress clang-analyzer-core.uninitialized.Assign for the
230 : : // following functions as a workaround for a false positive
231 : : // in clang-tidy 18.
232 : : // NOLINTBEGIN(clang-analyzer-core.uninitialized.Assign)
233 : 212 : FloatingPoint::PartialFloatingPoint FloatingPoint::max(
234 : : const FloatingPoint& arg) const
235 : : {
236 : 212 : FloatingPoint tmp(maxTotal(arg, true));
237 : 636 : return PartialFloatingPoint(tmp, tmp == maxTotal(arg, false));
238 : 212 : }
239 : :
240 : 8 : FloatingPoint::PartialFloatingPoint FloatingPoint::min(
241 : : const FloatingPoint& arg) const
242 : : {
243 : 8 : FloatingPoint tmp(minTotal(arg, true));
244 : 24 : return PartialFloatingPoint(tmp, tmp == minTotal(arg, false));
245 : 8 : }
246 : : // NOLINTEND(clang-analyzer-core.uninitialized.Assign)
247 : :
248 : 26009 : bool FloatingPoint::operator==(const FloatingPoint& fp) const
249 : : {
250 : 26009 : return *d_fpl == *fp.d_fpl;
251 : : }
252 : :
253 : 45 : bool FloatingPoint::operator<=(const FloatingPoint& fp) const
254 : : {
255 : 45 : return *d_fpl <= *fp.d_fpl;
256 : : }
257 : :
258 : 42 : bool FloatingPoint::operator<(const FloatingPoint& fp) const
259 : : {
260 : 42 : return *d_fpl < *fp.d_fpl;
261 : : }
262 : :
263 : 26 : BitVector FloatingPoint::getUnpackedExponent() const
264 : : {
265 : 26 : return d_fpl->getUnpackedExponent();
266 : : }
267 : :
268 : 26 : BitVector FloatingPoint::getUnpackedSignificand() const
269 : : {
270 : 26 : return d_fpl->getUnpackedSignificand();
271 : : }
272 : :
273 : 26 : bool FloatingPoint::getSign() const { return d_fpl->getSign(); }
274 : :
275 : 42 : bool FloatingPoint::isNormal(void) const { return d_fpl->isNormal(); }
276 : :
277 : 29 : bool FloatingPoint::isSubnormal(void) const { return d_fpl->isSubnormal(); }
278 : :
279 : 514 : bool FloatingPoint::isZero(void) const { return d_fpl->isZero(); }
280 : :
281 : 249 : bool FloatingPoint::isInfinite(void) const { return d_fpl->isInfinite(); }
282 : :
283 : 260 : bool FloatingPoint::isNaN(void) const { return d_fpl->isNaN(); }
284 : :
285 : 112 : bool FloatingPoint::isNegative(void) const { return d_fpl->isNegative(); }
286 : :
287 : 113 : bool FloatingPoint::isPositive(void) const { return d_fpl->isPositive(); }
288 : :
289 : 22 : FloatingPoint FloatingPoint::convert(const FloatingPointSize& target,
290 : : const RoundingMode& rm) const
291 : : {
292 : 44 : return FloatingPoint(d_fpl->convert(target, rm));
293 : : }
294 : :
295 : 12 : BitVector FloatingPoint::convertToBVTotal(BitVectorSize width,
296 : : const RoundingMode& rm,
297 : : bool signedBV,
298 : : BitVector undefinedCase) const
299 : : {
300 [ + + ]: 12 : if (signedBV)
301 : : {
302 : 4 : return d_fpl->convertToSBVTotal(width, rm, undefinedCase);
303 : : }
304 : 8 : return d_fpl->convertToUBVTotal(width, rm, undefinedCase);
305 : : }
306 : :
307 : 33 : Rational FloatingPoint::convertToRationalTotal(Rational undefinedCase) const
308 : : {
309 : 33 : PartialRational p(convertToRational());
310 : :
311 [ + + ]: 66 : return p.second ? p.first : undefinedCase;
312 : 33 : }
313 : :
314 : 0 : FloatingPoint::PartialBitVector FloatingPoint::convertToBV(
315 : : BitVectorSize width, const RoundingMode& rm, bool signedBV) const
316 : : {
317 : 0 : BitVector tmp(convertToBVTotal(width, rm, signedBV, BitVector(width, 0U)));
318 : : BitVector confirm(
319 : 0 : convertToBVTotal(width, rm, signedBV, BitVector(width, 1U)));
320 : :
321 : 0 : return PartialBitVector(tmp, tmp == confirm);
322 : 0 : }
323 : :
324 : 41 : FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const
325 : : {
326 : 41 : return d_fpl->convertToRational();
327 : : }
328 : :
329 : 40931 : BitVector FloatingPoint::pack(void) const { return d_fpl->pack(); }
330 : :
331 : 570 : void FloatingPoint::getIEEEBitvectors(BitVector& sign,
332 : : BitVector& exp,
333 : : BitVector& sig) const
334 : : {
335 : : // retrieve BV value
336 : 570 : BitVector bv(pack());
337 : : uint32_t largestSignificandBit =
338 : 570 : getSize().significandWidth() - 2; // -1 for -inclusive, -1 for hidden
339 : : uint32_t largestExponentBit =
340 : 570 : (getSize().exponentWidth() - 1) + (largestSignificandBit + 1);
341 : 570 : sign = bv.extract(largestExponentBit + 1, largestExponentBit + 1);
342 : 570 : exp = bv.extract(largestExponentBit, largestSignificandBit + 1);
343 : 570 : sig = bv.extract(largestSignificandBit, 0);
344 : 570 : }
345 : :
346 : 551 : std::string FloatingPoint::toString(bool printAsIndexed) const
347 : : {
348 : 551 : std::string str;
349 : : // retrive BV value
350 [ + + ]: 4408 : BitVector v[3];
351 : 551 : getIEEEBitvectors(v[0], v[1], v[2]);
352 : 551 : str.append("(fp ");
353 [ + + ]: 2204 : for (uint32_t i = 0; i < 3; ++i)
354 : : {
355 [ - + ]: 1653 : if (printAsIndexed)
356 : : {
357 : 0 : str.append("(_ bv");
358 : 0 : str.append(v[i].getValue().toString());
359 : 0 : str.append(" ");
360 : 0 : str.append(std::to_string(v[i].getSize()));
361 : 0 : str.append(")");
362 : : }
363 : : else
364 : : {
365 : 1653 : str.append("#b");
366 : 1653 : str.append(v[i].toString());
367 : : }
368 [ + + ]: 1653 : if (i < 2)
369 : : {
370 : 1102 : str.append(" ");
371 : : }
372 : : }
373 : 551 : str.append(")");
374 : 1102 : return str;
375 [ + + ][ - - ]: 2204 : }
376 : :
377 : 0 : std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp)
378 : : {
379 : : // print in binary notation
380 : 0 : return os << fp.toString();
381 : : }
382 : :
383 : 0 : std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps)
384 : : {
385 : 0 : return os << "(_ FloatingPoint " << fps.exponentWidth() << " "
386 : 0 : << fps.significandWidth() << ")";
387 : : }
388 : :
389 : 0 : std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs)
390 : : {
391 : 0 : return os << "(_ to_fp " << fpcs.getSize().exponentWidth() << " "
392 : 0 : << fpcs.getSize().significandWidth() << ")";
393 : : }
394 : : } // namespace cvc5::internal
|
