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 : : * SymFPU glue code for floating-point values.
11 : : */
12 : : #include "util/floatingpoint_literal_symfpu.h"
13 : :
14 : : #include <limits>
15 : :
16 : : #include "base/check.h"
17 : : #include "symfpu/core/add.h"
18 : : #include "symfpu/core/classify.h"
19 : : #include "symfpu/core/compare.h"
20 : : #include "symfpu/core/convert.h"
21 : : #include "symfpu/core/divide.h"
22 : : #include "symfpu/core/fma.h"
23 : : #include "symfpu/core/ite.h"
24 : : #include "symfpu/core/multiply.h"
25 : : #include "symfpu/core/packing.h"
26 : : #include "symfpu/core/remainder.h"
27 : : #include "symfpu/core/sign.h"
28 : : #include "symfpu/core/sqrt.h"
29 : : #include "util/floatingpoint_literal.h"
30 : : #include "util/rational.h"
31 : :
32 : : /* -------------------------------------------------------------------------- */
33 : :
34 : : namespace symfpu {
35 : :
36 : : #define CVC5_LIT_ITE_DFN(T) \
37 : : template <> \
38 : : struct ite<cvc5::internal::symfpuLiteral::Cvc5Prop, T> \
39 : : { \
40 : : static const T& iteOp(const cvc5::internal::symfpuLiteral::Cvc5Prop& cond, \
41 : : const T& l, \
42 : : const T& r) \
43 : : { \
44 : : return cond ? l : r; \
45 : : } \
46 : : }
47 : :
48 : : CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::rm);
49 [ + + ]: 681529 : CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::prop);
50 [ + + ]: 426731 : CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::sbv);
51 [ + + ]: 500543 : CVC5_LIT_ITE_DFN(cvc5::internal::symfpuLiteral::traits::ubv);
52 : :
53 : : #undef CVC5_LIT_ITE_DFN
54 : : } // namespace symfpu
55 : :
56 : : /* -------------------------------------------------------------------------- */
57 : :
58 : : namespace cvc5::internal {
59 : :
60 : : /* -------------------------------------------------------------------------- */
61 : :
62 : : namespace {
63 : 34744 : const FloatingPointLiteralSymFPU& asSymFPU(const FloatingPointLiteral& lit)
64 : : {
65 [ + - ][ - + ]: 34744 : Assert(dynamic_cast<const FloatingPointLiteralSymFPU*>(&lit) != nullptr);
[ - + ][ - - ]
66 : 34744 : return static_cast<const FloatingPointLiteralSymFPU&>(lit);
67 : : }
68 : : } // namespace
69 : :
70 : 5683 : FloatingPointLiteralSymFPU::FloatingPointLiteralSymFPU(uint32_t exp_size,
71 : : uint32_t sig_size,
72 : 5683 : const BitVector& bv)
73 : : : FloatingPointLiteral(exp_size, sig_size),
74 : 11366 : d_symuf(
75 : : new SymFPUUnpackedFloatLiteral(symfpu::unpack<symfpuLiteral::traits>(
76 : 11366 : symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv)))
77 : : {
78 : 5683 : }
79 : :
80 : 80 : FloatingPointLiteralSymFPU::FloatingPointLiteralSymFPU(
81 : : const FloatingPointSize& size,
82 : 80 : CVC5_UNUSED FloatingPointLiteralSymFPU::SpecialConstKind kind)
83 : : : FloatingPointLiteral(size),
84 : 80 : d_symuf(new SymFPUUnpackedFloatLiteral(
85 : 80 : SymFPUUnpackedFloatLiteral::makeNaN(size)))
86 : : {
87 [ - + ][ - + ]: 80 : Assert(kind == FloatingPointLiteralSymFPU::SpecialConstKind::FPNAN);
[ - - ]
88 : 80 : }
89 : :
90 : 227 : FloatingPointLiteralSymFPU::FloatingPointLiteralSymFPU(
91 : : const FloatingPointSize& size,
92 : : FloatingPointLiteralSymFPU::SpecialConstKind kind,
93 : 227 : bool sign)
94 : : : FloatingPointLiteral(size),
95 [ - - ]: 227 : d_symuf(new SymFPUUnpackedFloatLiteral(
96 : : kind == FloatingPointLiteralSymFPU::SpecialConstKind::FPINF
97 : : ? SymFPUUnpackedFloatLiteral::makeInf(size, sign)
98 [ + + ]: 227 : : SymFPUUnpackedFloatLiteral::makeZero(size, sign)))
99 : : {
100 [ + + ][ + - ]: 227 : Assert(kind == FloatingPointLiteralSymFPU::SpecialConstKind::FPINF
[ - + ][ - + ]
[ - - ]
101 : : || kind == FloatingPointLiteralSymFPU::SpecialConstKind::FPZERO);
102 : 227 : }
103 : :
104 : 34 : FloatingPointLiteralSymFPU::FloatingPointLiteralSymFPU(
105 : 34 : const FloatingPointSize& size, const BitVector& bv)
106 : : : FloatingPointLiteral(size),
107 : 68 : d_symuf(new SymFPUUnpackedFloatLiteral(
108 : 68 : symfpu::unpack<symfpuLiteral::traits>(size, bv)))
109 : : {
110 : 34 : }
111 : :
112 : 165 : FloatingPointLiteralSymFPU::FloatingPointLiteralSymFPU(
113 : : const FloatingPointSize& size,
114 : : const RoundingMode& rm,
115 : : const BitVector& bv,
116 : 165 : bool signedBV)
117 : 165 : : FloatingPointLiteral(size)
118 : : {
119 [ + + ]: 165 : if (signedBV)
120 : : {
121 [ + + ]: 12 : if (bv.getSize() == 1)
122 : : {
123 : : SymFPUUnpackedFloatLiteral uf =
124 : 2 : symfpu::convertUBVToFloat<symfpuLiteral::traits>(size, rm, bv);
125 : : /* We need special handling for bit-vectors of size one since symFPU does
126 : : * not allow conversions from signed bit-vectors of size one. */
127 [ + + ]: 2 : if (bv.is_one())
128 : : {
129 : 1 : d_symuf.reset(new SymFPUUnpackedFloatLiteral(
130 : 1 : symfpu::negate<symfpuLiteral::traits>(size, uf)));
131 : : }
132 : : else
133 : : {
134 : 1 : d_symuf.reset(new SymFPUUnpackedFloatLiteral(uf));
135 : : }
136 : 2 : }
137 : : else
138 : : {
139 : 20 : d_symuf.reset(new SymFPUUnpackedFloatLiteral(
140 : 10 : symfpu::convertSBVToFloat<symfpuLiteral::traits>(size, rm, bv)));
141 : : }
142 : : }
143 : : else
144 : : {
145 : 306 : d_symuf.reset(new SymFPUUnpackedFloatLiteral(
146 : 153 : symfpu::convertUBVToFloat<symfpuLiteral::traits>(size, rm, bv)));
147 : : }
148 : 165 : }
149 : :
150 : 27274 : FloatingPointLiteralSymFPU::FloatingPointLiteralSymFPU(
151 : 27274 : const FloatingPointLiteralSymFPU& other)
152 : : : FloatingPointLiteral(other.getSize()),
153 : 27274 : d_symuf(new SymFPUUnpackedFloatLiteral(*other.d_symuf))
154 : : {
155 : 27274 : }
156 : :
157 : 0 : FloatingPointLiteralSymFPU::FloatingPointLiteralSymFPU(
158 : 0 : FloatingPointLiteralSymFPU&& other) noexcept
159 : 0 : : FloatingPointLiteral(other.getSize()), d_symuf(std::move(other.d_symuf))
160 : : {
161 : 0 : }
162 : :
163 : 0 : FloatingPointLiteralSymFPU& FloatingPointLiteralSymFPU::operator=(
164 : : const FloatingPointLiteralSymFPU& other)
165 : : {
166 [ - - ]: 0 : if (this != &other)
167 : : {
168 : 0 : d_fp_size = other.d_fp_size;
169 : 0 : d_symuf.reset(new SymFPUUnpackedFloatLiteral(*other.d_symuf));
170 : : }
171 : 0 : return *this;
172 : : }
173 : :
174 : 0 : FloatingPointLiteralSymFPU& FloatingPointLiteralSymFPU::operator=(
175 : : FloatingPointLiteralSymFPU&& other) noexcept
176 : : {
177 [ - - ]: 0 : if (this != &other)
178 : : {
179 : 0 : d_fp_size = other.d_fp_size;
180 : 0 : d_symuf = std::move(other.d_symuf);
181 : : }
182 : 0 : return *this;
183 : : }
184 : :
185 : 93284 : FloatingPointLiteralSymFPU::~FloatingPointLiteralSymFPU() {}
186 : :
187 : : /* -------------------------------------------------------------------------- */
188 : :
189 : 61 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::fromUnpacked(
190 : : const FloatingPointSize& size,
191 : : bool sign,
192 : : const BitVector& exp,
193 : : const BitVector& sig)
194 : : {
195 : : return std::unique_ptr<FloatingPointLiteral>(
196 : 61 : new FloatingPointLiteralSymFPU(size, sign, exp, sig));
197 : : }
198 : :
199 : 77 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::fromRational(
200 : : const FloatingPointSize& size, const RoundingMode& rm, const Rational& r)
201 : : {
202 : 77 : Rational two(2, 1);
203 : :
204 [ + + ]: 77 : if (r.isZero())
205 : : {
206 : : // In keeping with the SMT-LIB standard
207 : : return std::unique_ptr<FloatingPointLiteral>(
208 : 16 : new FloatingPointLiteralSymFPU(size, SpecialConstKind::FPZERO, false));
209 : : }
210 : :
211 [ - + ]: 61 : uint32_t negative = (r.sgn() < 0) ? 1 : 0;
212 : 61 : Rational rabs(r.abs());
213 : :
214 : : // Compute the exponent
215 : 61 : Integer exp(0U);
216 : 61 : Integer inc(1U);
217 : 61 : Rational working(1, 1);
218 : :
219 [ + + ]: 61 : if (rabs != working)
220 : : {
221 [ + + ]: 50 : if (rabs < working)
222 : : {
223 [ + + ]: 78 : while (rabs < working)
224 : : {
225 : 58 : exp -= inc;
226 : 58 : working /= two;
227 : : }
228 : : }
229 : : else
230 : : {
231 [ + + ]: 130 : while (rabs >= working)
232 : : {
233 : 100 : exp += inc;
234 : 100 : working *= two;
235 : : }
236 : 30 : exp -= inc;
237 : 30 : working /= two;
238 : : }
239 : : }
240 : :
241 [ - + ][ - + ]: 61 : Assert(working <= rabs);
[ - - ]
242 [ - + ][ - + ]: 61 : Assert(rabs < working * two);
[ - - ]
243 : :
244 : : // Work out the number of bits required to represent the exponent for a
245 : : // normal number
246 : 61 : uint32_t expBits = 2; // No point starting with an invalid amount
247 : :
248 : 61 : Integer doubleInt(2);
249 [ + + ]: 61 : if (exp.strictlyPositive())
250 : : {
251 : : // 1 more than exactly representable with expBits
252 : 30 : Integer representable(4);
253 [ + + ]: 34 : while (representable <= exp)
254 : : { // hence <=
255 : 4 : representable *= doubleInt;
256 : 4 : ++expBits;
257 : : }
258 : 30 : }
259 [ + + ]: 31 : else if (exp.strictlyNegative())
260 : : {
261 : 20 : Integer representable(-4); // Exactly representable with expBits + sign
262 : : // but -2^n and -(2^n - 1) are both subnormal
263 [ + + ]: 30 : while ((representable + doubleInt) > exp)
264 : : {
265 : 10 : representable *= doubleInt;
266 : 10 : ++expBits;
267 : : }
268 : 20 : }
269 : 61 : ++expBits; // To allow for sign
270 : :
271 : 61 : BitVector exactExp(expBits, exp);
272 : :
273 : : // Compute the significand.
274 : 61 : uint32_t sigBits = size.significandWidth() + 2; // guard and sticky bits
275 : 61 : BitVector sig(sigBits, 0U);
276 : 61 : BitVector one(sigBits, 1U);
277 : 61 : Rational workingSig(0, 1);
278 [ + + ]: 2140 : for (uint32_t i = 0; i < sigBits - 1; ++i)
279 : : {
280 : 2079 : Rational mid(workingSig + working);
281 : :
282 [ + + ]: 2079 : if (mid <= rabs)
283 : : {
284 : 502 : sig = sig.setBit(0, true);
285 : 502 : workingSig = mid;
286 : : }
287 : :
288 : 2079 : sig = sig.leftShift(one);
289 : 2079 : working /= two;
290 : 2079 : }
291 : :
292 : : // Compute the sticky bit
293 : 61 : Rational remainder(rabs - workingSig);
294 [ - + ][ - + ]: 61 : Assert(Rational(0, 1) <= remainder);
[ - - ]
295 : :
296 [ + + ]: 61 : if (!remainder.isZero())
297 : : {
298 : 20 : sig = sig.setBit(0, true);
299 : : }
300 : :
301 : : // Build an exact float
302 : 61 : FloatingPointSize exactFormat(expBits, sigBits);
303 : :
304 : : // A small subtlety... if the format has expBits the unpacked format
305 : : // may have more to allow subnormals to be normalised.
306 : : // Thus...
307 : : uint32_t extension =
308 : 61 : SymFPUUnpackedFloatLiteral::exponentWidth(exactFormat) - expBits;
309 : :
310 : : auto exactFloat =
311 : 61 : fromUnpacked(exactFormat, negative, exactExp.signExtend(extension), sig);
312 : :
313 : : // Then cast...
314 : 61 : return exactFloat->convert(size, rm);
315 : 77 : }
316 : :
317 : : /* -------------------------------------------------------------------------- */
318 : : /* FloatingPointLiteral interface */
319 : : /* -------------------------------------------------------------------------- */
320 : :
321 : 27274 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::clone() const
322 : : {
323 : : return std::unique_ptr<FloatingPointLiteral>(
324 : 27274 : new FloatingPointLiteralSymFPU(*this));
325 : : }
326 : :
327 : 35663 : BitVector FloatingPointLiteralSymFPU::pack(void) const
328 : : {
329 : 35663 : BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, *d_symuf));
330 : 35663 : return bv;
331 : : }
332 : :
333 : : /* -------------------------------------------------------------------------- */
334 : :
335 : 222 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::absolute()
336 : : const
337 : : {
338 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
339 : 222 : d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, *d_symuf)));
340 : : }
341 : :
342 : 676 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::negate() const
343 : : {
344 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
345 : 676 : d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, *d_symuf)));
346 : : }
347 : :
348 : 4740 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::add(
349 : : const RoundingMode& rm, const FloatingPointLiteral& arg) const
350 : : {
351 : 4740 : const auto& a = asSymFPU(arg);
352 [ - + ][ - + ]: 4740 : Assert(d_fp_size == a.d_fp_size);
[ - - ]
353 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
354 : 4740 : d_fp_size,
355 : 4740 : symfpu::add<symfpuLiteral::traits>(
356 : 9480 : d_fp_size, rm, *d_symuf, *a.d_symuf, true)));
357 : : }
358 : :
359 : 0 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::sub(
360 : : const RoundingMode& rm, const FloatingPointLiteral& arg) const
361 : : {
362 : 0 : const auto& a = asSymFPU(arg);
363 : 0 : Assert(d_fp_size == a.d_fp_size);
364 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
365 : 0 : d_fp_size,
366 : 0 : symfpu::add<symfpuLiteral::traits>(
367 : 0 : d_fp_size, rm, *d_symuf, *a.d_symuf, false)));
368 : : }
369 : :
370 : 2418 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::mult(
371 : : const RoundingMode& rm, const FloatingPointLiteral& arg) const
372 : : {
373 : 2418 : const auto& a = asSymFPU(arg);
374 [ - + ][ - + ]: 2418 : Assert(d_fp_size == a.d_fp_size);
[ - - ]
375 : : return std::unique_ptr<FloatingPointLiteral>(
376 : 2418 : new FloatingPointLiteralSymFPU(d_fp_size,
377 : 2418 : symfpu::multiply<symfpuLiteral::traits>(
378 : 4836 : d_fp_size, rm, *d_symuf, *a.d_symuf)));
379 : : }
380 : :
381 : 2615 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::div(
382 : : const RoundingMode& rm, const FloatingPointLiteral& arg) const
383 : : {
384 : 2615 : const auto& a = asSymFPU(arg);
385 [ - + ][ - + ]: 2615 : Assert(d_fp_size == a.d_fp_size);
[ - - ]
386 : : return std::unique_ptr<FloatingPointLiteral>(
387 : 2615 : new FloatingPointLiteralSymFPU(d_fp_size,
388 : 2615 : symfpu::divide<symfpuLiteral::traits>(
389 : 5230 : d_fp_size, rm, *d_symuf, *a.d_symuf)));
390 : : }
391 : :
392 : 2 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::fma(
393 : : const RoundingMode& rm,
394 : : const FloatingPointLiteral& arg1,
395 : : const FloatingPointLiteral& arg2) const
396 : : {
397 : 2 : const auto& a1 = asSymFPU(arg1);
398 : 2 : const auto& a2 = asSymFPU(arg2);
399 [ - + ][ - + ]: 2 : Assert(d_fp_size == a1.d_fp_size);
[ - - ]
400 [ - + ][ - + ]: 2 : Assert(d_fp_size == a2.d_fp_size);
[ - - ]
401 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
402 : 2 : d_fp_size,
403 : 2 : symfpu::fma<symfpuLiteral::traits>(
404 : 4 : d_fp_size, rm, *d_symuf, *a1.d_symuf, *a2.d_symuf)));
405 : : }
406 : :
407 : 1180 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::sqrt(
408 : : const RoundingMode& rm) const
409 : : {
410 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
411 : 1180 : d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, *d_symuf)));
412 : : }
413 : :
414 : 210 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::rti(
415 : : const RoundingMode& rm) const
416 : : {
417 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
418 : 210 : d_fp_size,
419 : 210 : symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, *d_symuf)));
420 : : }
421 : :
422 : 525 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::rem(
423 : : const FloatingPointLiteral& arg) const
424 : : {
425 : 525 : const auto& a = asSymFPU(arg);
426 [ - + ][ - + ]: 525 : Assert(d_fp_size == a.d_fp_size);
[ - - ]
427 : : return std::unique_ptr<FloatingPointLiteral>(
428 : 525 : new FloatingPointLiteralSymFPU(d_fp_size,
429 : 525 : symfpu::remainder<symfpuLiteral::traits>(
430 : 1050 : d_fp_size, *d_symuf, *a.d_symuf)));
431 : : }
432 : :
433 : : /* -------------------------------------------------------------------------- */
434 : :
435 : 426 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::maxTotal(
436 : : const FloatingPointLiteral& arg, bool zeroCaseLeft) const
437 : : {
438 : 426 : const auto& a = asSymFPU(arg);
439 [ - + ][ - + ]: 426 : Assert(d_fp_size == a.d_fp_size);
[ - - ]
440 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
441 : 426 : d_fp_size,
442 : 426 : symfpu::max<symfpuLiteral::traits>(
443 : 852 : d_fp_size, *d_symuf, *a.d_symuf, zeroCaseLeft)));
444 : : }
445 : :
446 : 18 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::minTotal(
447 : : const FloatingPointLiteral& arg, bool zeroCaseLeft) const
448 : : {
449 : 18 : const auto& a = asSymFPU(arg);
450 [ - + ][ - + ]: 18 : Assert(d_fp_size == a.d_fp_size);
[ - - ]
451 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
452 : 18 : d_fp_size,
453 : 18 : symfpu::min<symfpuLiteral::traits>(
454 : 36 : d_fp_size, *d_symuf, *a.d_symuf, zeroCaseLeft)));
455 : : }
456 : :
457 : : /* -------------------------------------------------------------------------- */
458 : :
459 : 23909 : bool FloatingPointLiteralSymFPU::operator==(
460 : : const FloatingPointLiteral& fp) const
461 : : {
462 : 23909 : const auto& other = asSymFPU(fp);
463 : 23909 : return ((d_fp_size == other.d_fp_size)
464 [ + - ][ + + ]: 47818 : && symfpu::smtlibEqual<symfpuLiteral::traits>(
465 : 47818 : d_fp_size, *d_symuf, *other.d_symuf));
466 : : }
467 : :
468 : 47 : bool FloatingPointLiteralSymFPU::operator<=(
469 : : const FloatingPointLiteral& arg) const
470 : : {
471 : 47 : const auto& a = asSymFPU(arg);
472 [ - + ][ - + ]: 47 : Assert(d_fp_size == a.d_fp_size);
[ - - ]
473 : 94 : return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
474 : 47 : d_fp_size, *d_symuf, *a.d_symuf);
475 : : }
476 : :
477 : 42 : bool FloatingPointLiteralSymFPU::operator<(
478 : : const FloatingPointLiteral& arg) const
479 : : {
480 : 42 : const auto& a = asSymFPU(arg);
481 [ - + ][ - + ]: 42 : Assert(d_fp_size == a.d_fp_size);
[ - - ]
482 : 84 : return symfpu::lessThan<symfpuLiteral::traits>(
483 : 42 : d_fp_size, *d_symuf, *a.d_symuf);
484 : : }
485 : :
486 : : /* -------------------------------------------------------------------------- */
487 : :
488 : 42 : BitVector FloatingPointLiteralSymFPU::getUnpackedExponent() const
489 : : {
490 : 42 : return d_symuf->exponent;
491 : : }
492 : :
493 : 42 : BitVector FloatingPointLiteralSymFPU::getUnpackedSignificand() const
494 : : {
495 : 42 : return d_symuf->significand;
496 : : }
497 : :
498 : 42 : bool FloatingPointLiteralSymFPU::getSign() const { return d_symuf->sign; }
499 : :
500 : : /* -------------------------------------------------------------------------- */
501 : :
502 : 42 : bool FloatingPointLiteralSymFPU::isNormal(void) const
503 : : {
504 : 42 : return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, *d_symuf);
505 : : }
506 : :
507 : 29 : bool FloatingPointLiteralSymFPU::isSubnormal(void) const
508 : : {
509 : 29 : return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, *d_symuf);
510 : : }
511 : :
512 : 387 : bool FloatingPointLiteralSymFPU::isZero(void) const
513 : : {
514 : 387 : return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, *d_symuf);
515 : : }
516 : :
517 : 120 : bool FloatingPointLiteralSymFPU::isInfinite(void) const
518 : : {
519 : 120 : return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, *d_symuf);
520 : : }
521 : :
522 : 239 : bool FloatingPointLiteralSymFPU::isNaN(void) const
523 : : {
524 : 239 : return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, *d_symuf);
525 : : }
526 : :
527 : 24 : bool FloatingPointLiteralSymFPU::isNegative(void) const
528 : : {
529 : 24 : return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, *d_symuf);
530 : : }
531 : :
532 : 25 : bool FloatingPointLiteralSymFPU::isPositive(void) const
533 : : {
534 : 25 : return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, *d_symuf);
535 : : }
536 : :
537 : : /* -------------------------------------------------------------------------- */
538 : :
539 : 86 : std::unique_ptr<FloatingPointLiteral> FloatingPointLiteralSymFPU::convert(
540 : : const FloatingPointSize& target, const RoundingMode& rm) const
541 : : {
542 : : return std::unique_ptr<FloatingPointLiteral>(new FloatingPointLiteralSymFPU(
543 : : target,
544 : 86 : symfpu::convertFloatToFloat<symfpuLiteral::traits>(
545 : 172 : d_fp_size, target, rm, *d_symuf)));
546 : : }
547 : :
548 : 6 : BitVector FloatingPointLiteralSymFPU::convertToSBVTotal(
549 : : BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const
550 : : {
551 : 12 : return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
552 : 12 : d_fp_size, rm, *d_symuf, width, undefinedCase);
553 : : }
554 : :
555 : 8 : BitVector FloatingPointLiteralSymFPU::convertToUBVTotal(
556 : : BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const
557 : : {
558 : 16 : return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
559 : 16 : d_fp_size, rm, *d_symuf, width, undefinedCase);
560 : : }
561 : :
562 : 41 : std::pair<Rational, bool> FloatingPointLiteralSymFPU::convertToRational() const
563 : : {
564 [ + + ][ - + ]: 41 : if (isNaN() || isInfinite())
[ + + ]
565 : : {
566 : 20 : return std::make_pair(Rational(0U, 1U), false);
567 : : }
568 [ + + ]: 31 : if (isZero())
569 : : {
570 : 8 : return std::make_pair(Rational(0U, 1U), true);
571 : : }
572 [ + + ]: 27 : Integer sign(d_symuf->sign ? -1 : 1);
573 : : Integer exp(
574 : 54 : d_symuf->exponent.toSignedInteger()
575 : 27 : - (Integer(d_fp_size.significandWidth()
576 : 27 : - 1))); // -1 as forcibly normalised into the [1,2) range
577 : 27 : Integer significand(d_symuf->significand.toInteger());
578 : 27 : Integer signedSignificand(sign * significand);
579 : :
580 : : // We only have multiplyByPow(uint32_t) so we can't convert all numbers.
581 : : // As we convert Integer -> unsigned int -> uint32_t we need that
582 : : // unsigned int is not smaller than uint32_t
583 : : static_assert(sizeof(unsigned int) >= sizeof(uint32_t),
584 : : "Conversion float -> real could lose data");
585 : : #ifdef CVC5_ASSERTIONS
586 : : // Note that multipling by 2^n requires n bits of space (worst case)
587 : : // so, in effect, these tests limit us to cases where the resultant
588 : : // number requires up to 2^32 bits = 512 megabyte to represent.
589 : 27 : Integer shiftLimit(std::numeric_limits<uint32_t>::max());
590 : : #endif
591 : :
592 [ + + ]: 27 : if (!(exp.strictlyNegative()))
593 : : {
594 [ - + ][ - + ]: 19 : Assert(exp <= shiftLimit);
[ - - ]
595 : 19 : Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
596 : 38 : return std::make_pair(Rational(r), true);
597 : 19 : }
598 : 8 : Integer one(1U);
599 [ - + ][ - + ]: 8 : Assert((-exp) <= shiftLimit);
[ - - ]
600 : 8 : Integer q(one.multiplyByPow2((-exp).toUnsignedInt()));
601 : 8 : Rational r(signedSignificand, q);
602 : 8 : return std::make_pair(r, true);
603 : 27 : }
604 : :
605 : : /* -------------------------------------------------------------------------- */
606 : : } // namespace cvc5::internal
|
