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 : : * Black box testing of cvc5::FloatingPoint.
11 : : *
12 : : * Cross-checks the MPFR and SymFPU floating-point literal backends.
13 : : * Ported from Bitwuzla's FP unit tests, see
14 : : * https://github.com/bitwuzla/bitwuzla/tree/main/test/unit/fp
15 : : * (Copyright (C) 2022 by the Bitwuzla authors, MIT license).
16 : : */
17 : :
18 : : #include "base/check.h"
19 : : #include "test.h"
20 : : #include "util/floatingpoint.h"
21 : : #ifdef CVC5_USE_MPFR
22 : : #include "util/floatingpoint_literal_mpfr.h"
23 : : #endif
24 : : #include "util/floatingpoint_literal_symfpu.h"
25 : : #include "util/random.h"
26 : :
27 : : namespace cvc5::internal {
28 : : namespace test {
29 : :
30 : : /* -------------------------------------------------------------------------- */
31 : :
32 : : class TestUtilBlackFloatingPoint : public TestInternal
33 : : {
34 : : protected:
35 : : // With CVC5_SLOW_TESTS, these complement the exhaustive Float16 testing
36 : : // below and we can afford a large number of them. Without it, they run on
37 : : // every CI and nightly build, where the cross-checks are otherwise by far
38 : : // the slowest unit test, so we use lower counts.
39 : : #ifdef CVC5_SLOW_TESTS
40 : : /** Default number of random tests when not exhaustively testing. */
41 : : static constexpr uint32_t N_TESTS = 1000;
42 : : /** Number of tests fp.rem (significantly slower than other operators). */
43 : : static constexpr uint32_t N_TESTS_REM = 500;
44 : : #else
45 : : /** Default number of random tests when not exhaustively testing. */
46 : : static constexpr uint32_t N_TESTS = 100;
47 : : /** Number of tests fp.rem (significantly slower than other operators). */
48 : : static constexpr uint32_t N_TESTS_REM = 50;
49 : : #endif
50 : : /** Min/max bit-vector width used in convertToBV cross-checks. */
51 : : static constexpr uint32_t MIN_SIZE_TO_BV = 4;
52 : : static constexpr uint32_t MAX_SIZE_TO_BV = 64;
53 : :
54 : 32 : TestUtilBlackFloatingPoint()
55 : 96 : : d_rng(Random::getRandom()),
56 : 32 : d_fp16(5, 11),
57 : 32 : d_fp32(8, 24),
58 : 32 : d_fp64(11, 53),
59 : 32 : d_fp128(15, 113),
60 : 32 : d_all_formats({d_fp16, d_fp32, d_fp64, d_fp128}),
61 : 32 : d_formats_32_128({d_fp32, d_fp64, d_fp128}),
62 : : // If slow tests are enabled (CVC5_SLOW_TESTS), we exhaustively test
63 : : // for Float16, and randomly for other formats. Else, we test randomly
64 : : // for all formats, for N_TESTS each.
65 : : #ifdef CVC5_SLOW_TESTS
66 : : d_test_formats(d_formats_32_128)
67 : : #else
68 : 64 : d_test_formats(d_all_formats)
69 : : #endif
70 : : {
71 : 32 : }
72 : :
73 : 32 : void SetUp() override
74 : : {
75 : 32 : TestInternal::SetUp();
76 : 64 : d_all_rms = {RoundingMode::ROUND_NEAREST_TIES_TO_EVEN,
77 : : RoundingMode::ROUND_NEAREST_TIES_TO_AWAY,
78 : : RoundingMode::ROUND_TOWARD_POSITIVE,
79 : : RoundingMode::ROUND_TOWARD_NEGATIVE,
80 : 32 : RoundingMode::ROUND_TOWARD_ZERO};
81 : 32 : }
82 : :
83 : : /** @return A random boolean. */
84 : 0 : bool pickBool() { return d_rng.pick<uint32_t>(0, 1) != 0; }
85 : :
86 : : /** @return A random rounding mode. */
87 : 2400 : RoundingMode pickRm()
88 : : {
89 : 2400 : return d_all_rms[d_rng.pick<size_t>() % d_all_rms.size()];
90 : : }
91 : :
92 : : /** @return A random floating-point format. */
93 : 300 : FloatingPointSize pickFormat()
94 : : {
95 : 300 : return d_all_formats[d_rng.pick<size_t>() % d_all_formats.size()];
96 : : }
97 : :
98 : : /**
99 : : * Test `fun` exhaustively for all Float16 values.
100 : : * Does nothing unless compiled with CVC5_SLOW_TESTS.
101 : : */
102 : 16 : void testForFloat16(
103 : : [[maybe_unused]] std::function<void(const BitVector&, const BitVector&)>
104 : : fun)
105 : : {
106 : : #ifdef CVC5_SLOW_TESTS
107 : : uint32_t expSize = 5;
108 : : uint32_t sigBits = 10; // significand width minus hidden bit
109 : : for (uint32_t i = 0; i < (1u << expSize); ++i)
110 : : {
111 : : BitVector bvexp(expSize, i);
112 : : for (uint32_t j = 0; j < (1u << sigBits); ++j)
113 : : {
114 : : BitVector bvsig(sigBits, j);
115 : : fun(bvexp, bvsig);
116 : : }
117 : : }
118 : : #endif
119 : 16 : }
120 : :
121 : : /** Test `fun` for given formats. */
122 : 21 : void testForFormats(
123 : : const std::vector<FloatingPointSize>& formats,
124 : : uint32_t nTests,
125 : : std::function<void(const FloatingPointSize&, const BitVector&)> fun)
126 : : {
127 [ + + ]: 105 : for (const auto& f : formats)
128 : : {
129 : 84 : uint32_t bvSize = f.exponentWidth() + f.significandWidth();
130 [ + + ]: 8084 : for (uint32_t i = 0; i < nTests; ++i)
131 : : {
132 : 8000 : BitVector bv = BitVector::mkRandom(bvSize);
133 : 8000 : fun(f, bv);
134 : 8000 : }
135 : : }
136 : 21 : }
137 : :
138 : : /**
139 : : * Check the nextUp/nextDown round trips for the value with packed
140 : : * representation bv: nextDown(nextUp(fp)) and nextUp(nextDown(fp)) are fp
141 : : * again (up to the sign of zero, since the two zeros compare equal),
142 : : * unless the first step reaches an infinity. Does nothing for NaN and the
143 : : * infinities.
144 : : */
145 : 400 : void checkNextUpDownRoundTrip(const FloatingPointSize& fmt,
146 : : const BitVector& bv)
147 : : {
148 : 400 : FloatingPoint fp(fmt, bv);
149 [ + + ][ - + ]: 400 : if (fp.isNaN() || fp.isInfinite())
[ + + ]
150 : : {
151 : 6 : return;
152 : : }
153 : :
154 : 394 : FloatingPoint up = FloatingPoint::nextUp(fp);
155 [ - + ][ + - ]: 394 : ASSERT_FALSE(up.isNaN());
156 [ - + ]: 394 : if (up.isInfinite())
157 : : {
158 : 0 : ASSERT_TRUE(up.isPositive());
159 : : }
160 : : else
161 : : {
162 : 394 : FloatingPoint back = FloatingPoint::nextDown(up);
163 [ - + ]: 394 : if (fp.isZero())
164 : : {
165 : 0 : ASSERT_TRUE(back.isZero());
166 : : }
167 : : else
168 : : {
169 [ - + ][ + - ]: 788 : ASSERT_EQ(back.pack(), bv);
170 : : }
171 [ + - ]: 394 : }
172 : :
173 : 394 : FloatingPoint down = FloatingPoint::nextDown(fp);
174 [ - + ][ + - ]: 394 : ASSERT_FALSE(down.isNaN());
175 [ - + ]: 394 : if (down.isInfinite())
176 : : {
177 : 0 : ASSERT_TRUE(down.isNegative());
178 : : }
179 : : else
180 : : {
181 : 394 : FloatingPoint back = FloatingPoint::nextUp(down);
182 [ - + ]: 394 : if (fp.isZero())
183 : : {
184 : 0 : ASSERT_TRUE(back.isZero());
185 : : }
186 : : else
187 : : {
188 [ - + ][ + - ]: 788 : ASSERT_EQ(back.pack(), bv);
189 : : }
190 [ + - ]: 394 : }
191 [ + - ][ + + ]: 400 : }
192 : :
193 : : Random& d_rng;
194 : :
195 : : FloatingPointSize d_fp16;
196 : : FloatingPointSize d_fp32;
197 : : FloatingPointSize d_fp64;
198 : : FloatingPointSize d_fp128;
199 : :
200 : : std::vector<FloatingPointSize> d_all_formats;
201 : : std::vector<FloatingPointSize> d_formats_32_128;
202 : : std::vector<RoundingMode> d_all_rms;
203 : : const std::vector<FloatingPointSize>& d_test_formats;
204 : : };
205 : :
206 : : /* -------------------------------------------------------------------------- */
207 : :
208 : 4 : TEST_F(TestUtilBlackFloatingPoint, move)
209 : : {
210 : 1 : BitVector bv1 = BitVector::mkRandom(d_fp16.packedWidth());
211 : 1 : BitVector bv2 = BitVector::mkRandom(d_fp128.packedWidth());
212 : 1 : FloatingPoint fp1(d_fp16, bv1);
213 : 1 : FloatingPoint fp2(d_fp128, bv2);
214 : :
215 : 1 : fp1 = std::move(fp2);
216 [ - + ][ + - ]: 2 : ASSERT_EQ(fp1.pack(), bv2);
217 [ - + ][ + - ]: 1 : ASSERT_EQ(fp1.getSize(), d_fp128);
218 : :
219 : 1 : auto fp3 = std::move(fp1);
220 [ - + ][ + - ]: 2 : ASSERT_EQ(fp3.pack(), bv2);
221 [ - + ][ + - ]: 1 : ASSERT_EQ(fp3.getSize(), d_fp128);
222 : :
223 : 1 : FloatingPoint fp4(std::move(fp3));
224 [ - + ][ + - ]: 2 : ASSERT_EQ(fp4.pack(), bv2);
225 [ - + ][ + - ]: 1 : ASSERT_EQ(fp4.getSize(), d_fp128);
226 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
227 : :
228 : 4 : TEST_F(TestUtilBlackFloatingPoint, makeMinSubnormal)
229 : : {
230 [ + + ]: 5 : for (const auto& size : d_all_formats)
231 : : {
232 : 4 : FloatingPoint fp = FloatingPoint::makeMinSubnormal(size, true);
233 [ - + ][ + - ]: 4 : ASSERT_TRUE(fp.isSubnormal());
234 : 4 : FloatingPoint mfp = FloatingPoint::makeMinSubnormal(size, false);
235 [ - + ][ + - ]: 4 : ASSERT_TRUE(mfp.isSubnormal());
236 [ + - ]: 4 : }
237 : : }
238 : :
239 : 4 : TEST_F(TestUtilBlackFloatingPoint, makeMaxSubnormal)
240 : : {
241 [ + + ]: 5 : for (const auto& size : d_all_formats)
242 : : {
243 : 4 : FloatingPoint fp = FloatingPoint::makeMaxSubnormal(size, true);
244 [ - + ][ + - ]: 4 : ASSERT_TRUE(fp.isSubnormal());
245 : 4 : FloatingPoint mfp = FloatingPoint::makeMaxSubnormal(size, false);
246 [ - + ][ + - ]: 4 : ASSERT_TRUE(mfp.isSubnormal());
247 [ + - ]: 4 : }
248 : : }
249 : :
250 : 4 : TEST_F(TestUtilBlackFloatingPoint, makeMinNormal)
251 : : {
252 [ + + ]: 5 : for (const auto& size : d_all_formats)
253 : : {
254 : 4 : FloatingPoint fp = FloatingPoint::makeMinNormal(size, true);
255 [ - + ][ + - ]: 4 : ASSERT_TRUE(fp.isNormal());
256 : 4 : FloatingPoint mfp = FloatingPoint::makeMinNormal(size, false);
257 [ - + ][ + - ]: 4 : ASSERT_TRUE(mfp.isNormal());
258 [ + - ]: 4 : }
259 : : }
260 : :
261 : 4 : TEST_F(TestUtilBlackFloatingPoint, makeMaxNormal)
262 : : {
263 [ + + ]: 5 : for (const auto& size : d_all_formats)
264 : : {
265 : 4 : FloatingPoint fp = FloatingPoint::makeMaxNormal(size, true);
266 [ - + ][ + - ]: 4 : ASSERT_TRUE(fp.isNormal());
267 : 4 : FloatingPoint mfp = FloatingPoint::makeMaxNormal(size, false);
268 [ - + ][ + - ]: 4 : ASSERT_TRUE(mfp.isNormal());
269 [ + - ]: 4 : }
270 : : }
271 : :
272 : 4 : TEST_F(TestUtilBlackFloatingPoint, fromSbv1)
273 : : {
274 : 1 : BitVector bv0(1, 0u);
275 : 1 : BitVector bv1(1, 1u);
276 [ + + ]: 5 : for (const auto& bv : {bv0, bv1})
277 : : {
278 [ + + ]: 6 : for (bool sign : {true, false})
279 : : {
280 : 0 : FloatingPoint fp(FloatingPointSize(5, 11),
281 : 0 : RoundingMode::ROUND_NEAREST_TIES_TO_AWAY,
282 : : bv,
283 : 4 : sign);
284 : 4 : }
285 [ + + ][ - - ]: 3 : }
286 : 1 : }
287 : :
288 : 4 : TEST_F(TestUtilBlackFloatingPoint, nextUpNextDownSpecial)
289 : : {
290 [ + + ]: 5 : for (const auto& size : d_all_formats)
291 : : {
292 : 4 : FloatingPoint nan = FloatingPoint::makeNaN(size);
293 : 4 : FloatingPoint pinf = FloatingPoint::makeInf(size, false);
294 : 4 : FloatingPoint ninf = FloatingPoint::makeInf(size, true);
295 : 4 : FloatingPoint pzero = FloatingPoint::makeZero(size, false);
296 : 4 : FloatingPoint nzero = FloatingPoint::makeZero(size, true);
297 : 4 : FloatingPoint minSub = FloatingPoint::makeMinSubnormal(size, false);
298 : 4 : FloatingPoint nminSub = FloatingPoint::makeMinSubnormal(size, true);
299 : 4 : FloatingPoint maxSub = FloatingPoint::makeMaxSubnormal(size, false);
300 : 4 : FloatingPoint nmaxSub = FloatingPoint::makeMaxSubnormal(size, true);
301 : 4 : FloatingPoint minNorm = FloatingPoint::makeMinNormal(size, false);
302 : 4 : FloatingPoint nminNorm = FloatingPoint::makeMinNormal(size, true);
303 : 4 : FloatingPoint maxNorm = FloatingPoint::makeMaxNormal(size, false);
304 : 4 : FloatingPoint nmaxNorm = FloatingPoint::makeMaxNormal(size, true);
305 : :
306 : : // nextUp(NaN) and nextDown(NaN) are NaN
307 [ - + ][ + - ]: 4 : ASSERT_TRUE(FloatingPoint::nextUp(nan).isNaN());
308 [ - + ][ + - ]: 4 : ASSERT_TRUE(FloatingPoint::nextDown(nan).isNaN());
309 : : // the infinities are the extremes of the order, stepping away from them
310 : : // reaches the largest finite value of the respective sign
311 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextUp(pinf).pack(), pinf.pack());
312 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextUp(ninf).pack(), nmaxNorm.pack());
313 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextDown(ninf).pack(), ninf.pack());
314 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextDown(pinf).pack(), maxNorm.pack());
315 : : // nextUp of the zero class is the smallest positive subnormal, its
316 : : // nextDown the negative subnormal of smallest magnitude
317 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextUp(pzero).pack(), minSub.pack());
318 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextUp(nzero).pack(), minSub.pack());
319 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextDown(pzero).pack(), nminSub.pack());
320 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextDown(nzero).pack(), nminSub.pack());
321 : : // when the result is the zero class, its sign is the sign of the argument
322 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextUp(nminSub).pack(), nzero.pack());
323 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextDown(minSub).pack(), pzero.pack());
324 : : // crossing the subnormal/normal boundary
325 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextUp(maxSub).pack(), minNorm.pack());
326 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextDown(minNorm).pack(), maxSub.pack());
327 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextUp(nminNorm).pack(), nmaxSub.pack());
328 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextDown(nmaxSub).pack(), nminNorm.pack());
329 : : // stepping beyond the largest normals reaches the infinities
330 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextUp(maxNorm).pack(), pinf.pack());
331 [ - + ][ + - ]: 8 : ASSERT_EQ(FloatingPoint::nextDown(nmaxNorm).pack(), ninf.pack());
332 [ + - ][ + - ]: 4 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
333 : : }
334 : :
335 : 4 : TEST_F(TestUtilBlackFloatingPoint, nextUpNextDownRoundTrip)
336 : : {
337 : : // Round trips through nextUp/nextDown. Exhaustive for Float16 if
338 : : // CVC5_SLOW_TESTS is enabled, else only a random subset is tested for
339 : : // Float16 (as with the other formats). The exhaustive run additionally
340 : : // establishes adjacency in the value order: if nextUp skipped over a
341 : : // value b, the round trip starting at b would not return to b.
342 : 0 : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
343 [ - - ]: 0 : for (bool sign : {false, true})
344 : : {
345 [ - - ]: 0 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
346 : 0 : checkNextUpDownRoundTrip(d_fp16, bvsign.concat(bvexp).concat(bvsig));
347 : 0 : }
348 : 1 : };
349 : 1 : testForFloat16(fun16);
350 : 1 : testForFormats(d_test_formats,
351 : : N_TESTS,
352 : 400 : [this](const FloatingPointSize& fmt, const BitVector& bv) {
353 : 400 : checkNextUpDownRoundTrip(fmt, bv);
354 : 400 : });
355 : 1 : }
356 : :
357 : 4 : TEST_F(TestUtilBlackFloatingPoint, nextUpNextDownOrder)
358 : : {
359 : : // nextUp and nextDown are strictly above resp. below in the value order
360 : : // (checked on the exact rationals the values denote), for random values of
361 : : // all formats.
362 : 1 : Rational zero(0);
363 : 1 : testForFormats(d_all_formats,
364 : : N_TESTS,
365 : 400 : [&](const FloatingPointSize& fmt, const BitVector& bv) {
366 : 400 : FloatingPoint fp(fmt, bv);
367 [ + + ][ - + ]: 400 : if (fp.isNaN() || fp.isInfinite())
[ + + ]
368 : : {
369 : 2 : return;
370 : : }
371 : 398 : Rational rfp = fp.convertToRationalTotal(zero);
372 : 398 : FloatingPoint up = FloatingPoint::nextUp(fp);
373 [ + - ]: 398 : if (!up.isInfinite())
374 : : {
375 [ - + ][ + - ]: 398 : ASSERT_TRUE(rfp < up.convertToRationalTotal(zero));
376 : : }
377 : 398 : FloatingPoint down = FloatingPoint::nextDown(fp);
378 [ + - ]: 398 : if (!down.isInfinite())
379 : : {
380 [ - + ][ + - ]: 398 : ASSERT_TRUE(down.convertToRationalTotal(zero) < rfp);
381 : : }
382 [ + - ][ + - ]: 400 : });
[ + + ]
383 : 1 : }
384 : :
385 : : /* -------------------------------------------------------------------------- */
386 : : /* Crosscheck MPFR and SymFPU back ends. */
387 : : /* -------------------------------------------------------------------------- */
388 : :
389 : : #ifdef CVC5_USE_MPFR
390 : : namespace {
391 : : /** @return An FP literal with MPFR as the back end. */
392 : 12800 : FloatingPointLiteralMPFR fpMPFR(const FloatingPointSize& fmt,
393 : : const BitVector& bv)
394 : : {
395 : 12800 : return FloatingPointLiteralMPFR(fmt, bv);
396 : : }
397 : :
398 : : /** @return An FP literal with SymFPU as the back end. */
399 : 12800 : FloatingPointLiteralSymFPU fpSymFPU(const FloatingPointSize& fmt,
400 : : const BitVector& bv)
401 : : {
402 : 12800 : return FloatingPointLiteralSymFPU(fmt, bv);
403 : : }
404 : : } // namespace
405 : :
406 : 4 : TEST_F(TestUtilBlackFloatingPoint, pack)
407 : : {
408 : : // Exhaustive for Float16 if CVC5_SLOW_TESTS is enabled, else only a random
409 : : // subset is tested for Float16 (as with the other formats).
410 : 0 : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
411 [ - - ]: 0 : for (bool sign : {false, true})
412 : : {
413 [ - - ]: 0 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
414 : 0 : BitVector bv = bvsign.concat(bvexp).concat(bvsig);
415 : :
416 : 0 : auto mpfr = fpMPFR(d_fp16, bv);
417 : 0 : auto sym = fpSymFPU(d_fp16, bv);
418 : :
419 : 0 : BitVector packedMpfr = mpfr.pack();
420 : 0 : BitVector packedSym = sym.pack();
421 : :
422 : : // Both backends must produce the same packed representation.
423 [ - - ]: 0 : ASSERT_EQ(packedMpfr, packedSym)
424 [ - - ]: 0 : << "pack mismatch for bv=" << bv.toString();
425 [ - - ][ - - ]: 0 : }
[ - - ][ - - ]
[ - - ][ - - ]
426 : 1 : };
427 : 1 : testForFloat16(fun16);
428 : 1 : testForFormats(d_test_formats,
429 : : N_TESTS,
430 : 400 : [](const FloatingPointSize& fmt, const BitVector& bv) {
431 : 400 : auto mpfr = fpMPFR(fmt, bv);
432 : 400 : auto sym = fpSymFPU(fmt, bv);
433 [ - + ][ + - ]: 800 : ASSERT_EQ(mpfr.pack(), sym.pack());
434 [ + - ][ + - ]: 400 : });
435 : 1 : }
436 : :
437 : 4 : TEST_F(TestUtilBlackFloatingPoint, classification)
438 : : {
439 : 1 : BitVector ezero = BitVector::mkZero(5);
440 : 1 : BitVector eones = BitVector::mkOnes(5);
441 : 1 : BitVector szero = BitVector::mkZero(10);
442 : 0 : auto fun16 = [&, this](const BitVector& bvexp, const BitVector& bvsig) {
443 [ - - ]: 0 : for (bool sign : {false, true})
444 : : {
445 [ - - ]: 0 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
446 : 0 : BitVector bv = bvsign.concat(bvexp).concat(bvsig);
447 : :
448 : 0 : auto mpfr = fpMPFR(d_fp16, bv);
449 : 0 : auto sym = fpSymFPU(d_fp16, bv);
450 : :
451 : 0 : ASSERT_EQ(mpfr.isNormal(), sym.isNormal());
452 : 0 : ASSERT_EQ(mpfr.isSubnormal(), sym.isSubnormal());
453 : 0 : ASSERT_EQ(mpfr.isZero(), sym.isZero());
454 : 0 : ASSERT_EQ(mpfr.isInfinite(), sym.isInfinite());
455 : 0 : ASSERT_EQ(mpfr.isNaN(), sym.isNaN());
456 : 0 : ASSERT_EQ(mpfr.isNegative(), sym.isNegative());
457 : 0 : ASSERT_EQ(mpfr.isPositive(), sym.isPositive());
458 : 0 : ASSERT_EQ(mpfr.getSign(), sym.getSign());
459 : :
460 [ - - ]: 0 : if (bvexp != ezero)
461 : : {
462 [ - - ]: 0 : if (bvexp != eones)
463 : : {
464 : 0 : ASSERT_TRUE(mpfr.isNormal());
465 : 0 : ASSERT_FALSE(mpfr.isSubnormal());
466 : 0 : ASSERT_FALSE(mpfr.isInfinite());
467 : 0 : ASSERT_FALSE(mpfr.isNaN());
468 : 0 : ASSERT_FALSE(mpfr.isZero());
469 : : }
470 : : else
471 : : {
472 [ - - ]: 0 : if (bvsig == szero)
473 : : {
474 : 0 : ASSERT_TRUE(mpfr.isInfinite());
475 : 0 : ASSERT_FALSE(mpfr.isNormal());
476 : 0 : ASSERT_FALSE(mpfr.isSubnormal());
477 : 0 : ASSERT_FALSE(mpfr.isNaN());
478 : 0 : ASSERT_FALSE(mpfr.isZero());
479 : : }
480 : : else
481 : : {
482 : 0 : ASSERT_TRUE(mpfr.isNaN());
483 : 0 : ASSERT_FALSE(mpfr.isNormal());
484 : 0 : ASSERT_FALSE(mpfr.isSubnormal());
485 : 0 : ASSERT_FALSE(mpfr.isInfinite());
486 : 0 : ASSERT_FALSE(mpfr.isZero());
487 : : }
488 : : }
489 : : }
490 : : else
491 : : {
492 [ - - ]: 0 : if (bvsig == szero)
493 : : {
494 : 0 : ASSERT_TRUE(mpfr.isZero());
495 : 0 : ASSERT_FALSE(mpfr.isNormal());
496 : 0 : ASSERT_FALSE(mpfr.isSubnormal());
497 : 0 : ASSERT_FALSE(mpfr.isInfinite());
498 : 0 : ASSERT_FALSE(mpfr.isNaN());
499 : : }
500 : : else
501 : : {
502 : 0 : ASSERT_TRUE(mpfr.isSubnormal());
503 : 0 : ASSERT_FALSE(mpfr.isNormal());
504 : 0 : ASSERT_FALSE(mpfr.isInfinite());
505 : 0 : ASSERT_FALSE(mpfr.isNaN());
506 : 0 : ASSERT_FALSE(mpfr.isZero());
507 : : }
508 : : }
509 [ - - ][ - - ]: 0 : }
[ - - ][ - - ]
510 : 1 : };
511 : 1 : testForFloat16(fun16);
512 : 1 : testForFormats(d_test_formats,
513 : : N_TESTS,
514 : 400 : [](const FloatingPointSize& fmt, const BitVector& bv1) {
515 : 400 : auto mpfr = fpMPFR(fmt, bv1);
516 : 400 : auto sym = fpSymFPU(fmt, bv1);
517 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr.isNormal(), sym.isNormal());
518 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr.isSubnormal(), sym.isSubnormal());
519 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr.isZero(), sym.isZero());
520 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr.isNaN(), sym.isNaN());
521 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr.isInfinite(), sym.isInfinite());
522 [ + - ][ + - ]: 400 : });
523 : 1 : }
524 : :
525 : 4 : TEST_F(TestUtilBlackFloatingPoint, components)
526 : : {
527 : 0 : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
528 [ - - ]: 0 : for (bool sign : {false, true})
529 : : {
530 [ - - ]: 0 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
531 : 0 : BitVector bv = bvsign.concat(bvexp).concat(bvsig);
532 : :
533 : 0 : auto mpfr = fpMPFR(d_fp16, bv);
534 : 0 : auto sym = fpSymFPU(d_fp16, bv);
535 : :
536 : 0 : ASSERT_EQ(mpfr.getUnpackedExponent(), sym.getUnpackedExponent());
537 : 0 : ASSERT_EQ(mpfr.getUnpackedSignificand(), sym.getUnpackedSignificand());
538 [ - - ][ - - ]: 0 : }
[ - - ][ - - ]
539 : 1 : };
540 : 1 : testForFloat16(fun16);
541 : 1 : testForFormats(
542 : : d_test_formats,
543 : : N_TESTS,
544 : 400 : [](const FloatingPointSize& fmt, const BitVector& bv) {
545 : 400 : auto mpfr = fpMPFR(fmt, bv);
546 : 400 : auto sym = fpSymFPU(fmt, bv);
547 [ - + ][ + - ]: 800 : ASSERT_EQ(mpfr.getUnpackedExponent(), sym.getUnpackedExponent());
548 [ - + ][ + - ]: 800 : ASSERT_EQ(mpfr.getUnpackedSignificand(), sym.getUnpackedSignificand());
549 [ + - ][ + - ]: 400 : });
550 : 1 : }
551 : :
552 : 4 : TEST_F(TestUtilBlackFloatingPoint, specialConstants)
553 : : {
554 [ + + ]: 5 : for (const auto& size : d_all_formats)
555 : : {
556 : : using SCKind = FloatingPointLiteral::SpecialConstKind;
557 : : // NaN
558 : : {
559 : 4 : auto mpfr = FloatingPointLiteralMPFR(size, SCKind::FPNAN);
560 : 4 : auto sym = FloatingPointLiteralSymFPU(size, SCKind::FPNAN);
561 [ - + ][ + - ]: 8 : ASSERT_EQ(mpfr.pack(), sym.pack());
562 [ - + ][ + - ]: 4 : ASSERT_TRUE(mpfr.isNaN());
563 [ - + ][ + - ]: 4 : ASSERT_FALSE(mpfr.isInfinite());
564 [ - + ][ + - ]: 4 : ASSERT_FALSE(mpfr.isNormal());
565 [ - + ][ + - ]: 4 : ASSERT_FALSE(mpfr.isSubnormal());
566 [ - + ][ + - ]: 4 : ASSERT_FALSE(mpfr.isZero());
567 [ + - ][ + - ]: 4 : }
568 [ + + ]: 12 : for (bool sign : {false, true})
569 : : {
570 : : // +inf, -inf
571 : : {
572 : 8 : auto mpfr = FloatingPointLiteralMPFR(size, SCKind::FPINF, sign);
573 : 8 : auto sym = FloatingPointLiteralSymFPU(size, SCKind::FPINF, sign);
574 [ - + ][ + - ]: 16 : ASSERT_EQ(mpfr.pack(), sym.pack());
575 [ - + ][ + - ]: 8 : ASSERT_TRUE(mpfr.isInfinite());
576 [ - + ][ + - ]: 8 : ASSERT_FALSE(mpfr.isNaN());
577 [ - + ][ + - ]: 8 : ASSERT_FALSE(mpfr.isNormal());
578 [ - + ][ + - ]: 8 : ASSERT_FALSE(mpfr.isSubnormal());
579 [ - + ][ + - ]: 8 : ASSERT_FALSE(mpfr.isZero());
580 [ + - ][ + - ]: 8 : }
581 : : // +zero, -zero
582 : : {
583 : 8 : auto mpfr = FloatingPointLiteralMPFR(size, SCKind::FPZERO, sign);
584 : 8 : auto sym = FloatingPointLiteralSymFPU(size, SCKind::FPZERO, sign);
585 [ - + ][ + - ]: 16 : ASSERT_EQ(mpfr.pack(), sym.pack());
586 [ - + ][ + - ]: 8 : ASSERT_TRUE(mpfr.isZero());
587 [ - + ][ + - ]: 8 : ASSERT_FALSE(mpfr.isInfinite());
588 [ - + ][ + - ]: 8 : ASSERT_FALSE(mpfr.isNaN());
589 [ - + ][ + - ]: 8 : ASSERT_FALSE(mpfr.isNormal());
590 [ - + ][ + - ]: 8 : ASSERT_FALSE(mpfr.isSubnormal());
591 [ + - ][ + - ]: 8 : }
592 : : }
593 : : }
594 : : }
595 : :
596 : 4 : TEST_F(TestUtilBlackFloatingPoint, fromUbvSbv)
597 : : {
598 : : #ifdef CVC5_SLOW_TESTS
599 : : // Test exhaustively for Float16.
600 : : for (uint64_t bw = 2; bw <= 16; ++bw)
601 : : {
602 : : for (uint64_t i = 0; i < (1ul << bw); ++i)
603 : : {
604 : : BitVector bv = BitVector(bw, i);
605 : : for (RoundingMode rm : d_all_rms)
606 : : {
607 : : for (bool sign : {false, true})
608 : : {
609 : : FloatingPointLiteralMPFR mpfr(d_fp16, rm, bv, sign);
610 : : FloatingPointLiteralSymFPU symfpu(d_fp16, rm, bv, sign);
611 : : ASSERT_EQ(mpfr.pack(), symfpu.pack());
612 : : }
613 : : }
614 : : }
615 : : }
616 : : #endif
617 : : // Test randomly for all formats if CVC5_SLOW_TESTS is not defined, else
618 : : // only for larger formats since we already tested Float16 exhaustively.
619 [ + + ]: 5 : for (const auto& f : d_test_formats)
620 : : {
621 [ + + ]: 68 : for (uint64_t bw = 1; bw <= 16; ++bw)
622 : : {
623 [ + + ]: 704 : for (uint64_t i = 0; i < 10; ++i)
624 : : {
625 : 640 : auto bv = BitVector::mkRandom(bw);
626 [ + + ]: 3840 : for (RoundingMode rm : d_all_rms)
627 : : {
628 [ + + ]: 9600 : for (auto sign : {false, true})
629 : : {
630 : 6400 : FloatingPointLiteralMPFR mpfr(f, rm, bv, sign);
631 : 6400 : FloatingPointLiteralSymFPU symfpu(f, rm, bv, sign);
632 [ - + ][ + - ]: 12800 : ASSERT_EQ(mpfr.pack(), symfpu.pack());
633 [ + - ][ + - ]: 6400 : }
634 : : }
635 [ + - ]: 640 : }
636 : : }
637 : : }
638 : : }
639 : :
640 : : /* -------------------------------------------------------------------------- */
641 : : /* Unary operators without FM: fp.abs, fp.neg */
642 : : /* -------------------------------------------------------------------------- */
643 : :
644 : : #define TEST_UNARY_OP(NAME, METHOD) \
645 : : TEST_F(TestUtilBlackFloatingPoint, NAME) \
646 : : { \
647 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) { \
648 : : for (bool sign : {false, true}) \
649 : : { \
650 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1); \
651 : : BitVector bv = bvsign.concat(bvexp).concat(bvsig); \
652 : : auto mpfr = fpMPFR(d_fp16, bv); \
653 : : auto sym = fpSymFPU(d_fp16, bv); \
654 : : ASSERT_EQ(mpfr.METHOD()->pack(), sym.METHOD()->pack()); \
655 : : } \
656 : : }; \
657 : : testForFloat16(fun16); \
658 : : testForFormats(d_test_formats, \
659 : : N_TESTS, \
660 : : [](const FloatingPointSize& fmt, const BitVector& bv) { \
661 : : auto mpfr = fpMPFR(fmt, bv); \
662 : : auto sym = fpSymFPU(fmt, bv); \
663 : : ASSERT_EQ(mpfr.METHOD()->pack(), sym.METHOD()->pack()); \
664 : : }); \
665 : : }
666 : :
667 [ - + ][ + - ]: 1204 : TEST_UNARY_OP(absolute, absolute)
[ + - ][ + - ]
668 [ - + ][ + - ]: 1204 : TEST_UNARY_OP(negate, negate)
[ + - ][ + - ]
669 : :
670 : : #undef TEST_UNARY_OP
671 : :
672 : : /* -------------------------------------------------------------------------- */
673 : : /* Unary operators with RM: fp.sqrt, fp.rti */
674 : : /* -------------------------------------------------------------------------- */
675 : :
676 : : #define TEST_UNARY_RM_OP(NAME, METHOD) \
677 : : TEST_F(TestUtilBlackFloatingPoint, NAME) \
678 : : { \
679 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) { \
680 : : for (bool sign : {false, true}) \
681 : : { \
682 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1); \
683 : : BitVector bv = bvsign.concat(bvexp).concat(bvsig); \
684 : : auto mpfr = fpMPFR(d_fp16, bv); \
685 : : auto sym = fpSymFPU(d_fp16, bv); \
686 : : for (auto rm : d_all_rms) \
687 : : { \
688 : : ASSERT_EQ(mpfr.METHOD(rm)->pack(), sym.METHOD(rm)->pack()); \
689 : : } \
690 : : } \
691 : : }; \
692 : : testForFloat16(fun16); \
693 : : testForFormats(d_test_formats, \
694 : : N_TESTS, \
695 : : [this](const FloatingPointSize& fmt, const BitVector& bv) { \
696 : : auto mpfr = fpMPFR(fmt, bv); \
697 : : auto sym = fpSymFPU(fmt, bv); \
698 : : for (auto rm : d_all_rms) \
699 : : { \
700 : : ASSERT_EQ(mpfr.METHOD(rm)->pack(), \
701 : : sym.METHOD(rm)->pack()); \
702 : : } \
703 : : }); \
704 : : }
705 : :
706 [ - + ][ + - ]: 4404 : TEST_UNARY_RM_OP(fpSqrt, sqrt)
[ + + ][ + - ]
[ + - ]
707 [ - + ][ + - ]: 4404 : TEST_UNARY_RM_OP(fpRti, rti)
[ + + ][ + - ]
[ + - ]
708 : :
709 : : #undef TEST_UNARY_RM_OP
710 : :
711 : : /* -------------------------------------------------------------------------- */
712 : : /* Binary operator without RM: fp.rem */
713 : : /* -------------------------------------------------------------------------- */
714 : :
715 : 4 : TEST_F(TestUtilBlackFloatingPoint, fpRem)
716 : : {
717 : : // Exhaustive for Float16 (one operand exhaustive, other random) if
718 : : // CVC5_SLOW_TESTS is not enabled, else only a random subset is tested for
719 : : // Float16 (as with the other formats).
720 : 0 : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
721 : 0 : bool sign = pickBool();
722 [ - - ]: 0 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
723 : 0 : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig);
724 : 0 : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth());
725 : :
726 : 0 : auto mpfr1 = fpMPFR(d_fp16, bv1);
727 : 0 : auto mpfr2 = fpMPFR(d_fp16, bv2);
728 : 0 : auto sym1 = fpSymFPU(d_fp16, bv1);
729 : 0 : auto sym2 = fpSymFPU(d_fp16, bv2);
730 : :
731 : 0 : ASSERT_EQ(mpfr1.rem(mpfr2)->pack(), sym1.rem(sym2)->pack());
732 [ - - ][ - - ]: 1 : };
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ]
733 : 1 : testForFloat16(fun16);
734 : 1 : testForFormats(d_test_formats,
735 : : N_TESTS_REM,
736 : 200 : [](const FloatingPointSize& fmt, const BitVector& bv1) {
737 : 200 : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
738 : 200 : auto mpfr1 = fpMPFR(fmt, bv1);
739 : 200 : auto mpfr2 = fpMPFR(fmt, bv2);
740 : 200 : auto sym1 = fpSymFPU(fmt, bv1);
741 : 200 : auto sym2 = fpSymFPU(fmt, bv2);
742 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr1.rem(mpfr2)->pack(), sym1.rem(sym2)->pack());
743 [ + - ][ + - ]: 200 : });
[ + - ][ + - ]
[ + - ]
744 : 1 : }
745 : :
746 : : /* -------------------------------------------------------------------------- */
747 : : /* Binary operators with RM: fp.add, fp.sub, fp.mult, fp.div */
748 : : /* -------------------------------------------------------------------------- */
749 : :
750 : : #define TEST_BINARY_RM_OP(NAME, METHOD) \
751 : : TEST_F(TestUtilBlackFloatingPoint, NAME) \
752 : : { \
753 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) { \
754 : : bool sign = pickBool(); \
755 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1); \
756 : : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig); \
757 : : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth()); \
758 : : auto mpfr1 = fpMPFR(d_fp16, bv1); \
759 : : auto mpfr2 = fpMPFR(d_fp16, bv2); \
760 : : auto sym1 = fpSymFPU(d_fp16, bv1); \
761 : : auto sym2 = fpSymFPU(d_fp16, bv2); \
762 : : for (auto rm : d_all_rms) \
763 : : { \
764 : : ASSERT_EQ(mpfr1.METHOD(rm, mpfr2)->pack(), \
765 : : sym1.METHOD(rm, sym2)->pack()); \
766 : : } \
767 : : }; \
768 : : testForFloat16(fun16); \
769 : : testForFormats( \
770 : : d_test_formats, \
771 : : N_TESTS, \
772 : : [this](const FloatingPointSize& fmt, const BitVector& bv1) { \
773 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth()); \
774 : : auto mpfr1 = fpMPFR(fmt, bv1); \
775 : : auto mpfr2 = fpMPFR(fmt, bv2); \
776 : : auto sym1 = fpSymFPU(fmt, bv1); \
777 : : auto sym2 = fpSymFPU(fmt, bv2); \
778 : : for (auto rm : d_all_rms) \
779 : : { \
780 : : ASSERT_EQ(mpfr1.METHOD(rm, mpfr2)->pack(), \
781 : : sym1.METHOD(rm, sym2)->pack()); \
782 : : } \
783 : : }); \
784 : : }
785 : :
786 [ - + ][ + - ]: 4404 : TEST_BINARY_RM_OP(fpAdd, add)
[ + + ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
787 [ - + ][ + - ]: 4404 : TEST_BINARY_RM_OP(fpSub, sub)
[ + + ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
788 [ - + ][ + - ]: 4404 : TEST_BINARY_RM_OP(fpMult, mult)
[ + + ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
789 [ - + ][ + - ]: 4404 : TEST_BINARY_RM_OP(fpDiv, div)
[ + + ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
790 : :
791 : : #undef TEST_BINARY_RM_OP
792 : :
793 : : /* -------------------------------------------------------------------------- */
794 : : /* Ternary operator with RM: fp.fma */
795 : : /* -------------------------------------------------------------------------- */
796 : :
797 : 4 : TEST_F(TestUtilBlackFloatingPoint, fpFma)
798 : : {
799 : 0 : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
800 : 0 : bool sign = pickBool();
801 [ - - ]: 0 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
802 : 0 : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig);
803 : 0 : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth());
804 : 0 : BitVector bv3 = BitVector::mkRandom(d_fp16.packedWidth());
805 : :
806 : 0 : auto mpfr1 = fpMPFR(d_fp16, bv1);
807 : 0 : auto mpfr2 = fpMPFR(d_fp16, bv2);
808 : 0 : auto mpfr3 = fpMPFR(d_fp16, bv3);
809 : 0 : auto sym1 = fpSymFPU(d_fp16, bv1);
810 : 0 : auto sym2 = fpSymFPU(d_fp16, bv2);
811 : 0 : auto sym3 = fpSymFPU(d_fp16, bv3);
812 : :
813 [ - - ]: 0 : for (auto rm : d_all_rms)
814 : : {
815 [ - - ]: 0 : ASSERT_EQ(mpfr1.fma(rm, mpfr2, mpfr3)->pack(),
816 [ - - ]: 0 : sym1.fma(rm, sym2, sym3)->pack());
817 : : }
818 [ - - ][ - - ]: 1 : };
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ][ - - ]
819 : 1 : testForFloat16(fun16);
820 : 1 : testForFormats(d_test_formats,
821 : : N_TESTS,
822 : 800 : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
823 : 400 : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
824 : 400 : BitVector bv3 = BitVector::mkRandom(fmt.packedWidth());
825 : 400 : auto mpfr1 = fpMPFR(fmt, bv1);
826 : 400 : auto mpfr2 = fpMPFR(fmt, bv2);
827 : 400 : auto mpfr3 = fpMPFR(fmt, bv3);
828 : 400 : auto sym1 = fpSymFPU(fmt, bv1);
829 : 400 : auto sym2 = fpSymFPU(fmt, bv2);
830 : 400 : auto sym3 = fpSymFPU(fmt, bv3);
831 [ + + ]: 2400 : for (auto rm : d_all_rms)
832 : : {
833 [ - + ]: 4000 : ASSERT_EQ(mpfr1.fma(rm, mpfr2, mpfr3)->pack(),
834 [ + - ]: 2000 : sym1.fma(rm, sym2, sym3)->pack());
835 : : }
836 [ + - ][ + - ]: 400 : });
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
837 : 1 : }
838 : :
839 : : /* -------------------------------------------------------------------------- */
840 : : /* Min/Max */
841 : : /* -------------------------------------------------------------------------- */
842 : :
843 : 4 : TEST_F(TestUtilBlackFloatingPoint, fpMinMax)
844 : : {
845 : 0 : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
846 : 0 : bool sign = pickBool();
847 [ - - ]: 0 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
848 : 0 : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig);
849 : 0 : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth());
850 : :
851 : 0 : auto mpfr1 = fpMPFR(d_fp16, bv1);
852 : 0 : auto mpfr2 = fpMPFR(d_fp16, bv2);
853 : 0 : auto sym1 = fpSymFPU(d_fp16, bv1);
854 : 0 : auto sym2 = fpSymFPU(d_fp16, bv2);
855 : :
856 [ - - ]: 0 : for (bool zeroCaseLeft : {false, true})
857 : : {
858 [ - - ]: 0 : ASSERT_EQ(mpfr1.maxTotal(mpfr2, zeroCaseLeft)->pack(),
859 [ - - ]: 0 : sym1.maxTotal(sym2, zeroCaseLeft)->pack());
860 [ - - ]: 0 : ASSERT_EQ(mpfr1.minTotal(mpfr2, zeroCaseLeft)->pack(),
861 [ - - ]: 0 : sym1.minTotal(sym2, zeroCaseLeft)->pack());
862 : : }
863 [ - - ][ - - ]: 1 : };
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ]
864 : 1 : testForFloat16(fun16);
865 : 1 : testForFormats(d_test_formats,
866 : : N_TESTS,
867 : 400 : [](const FloatingPointSize& fmt, const BitVector& bv1) {
868 : 400 : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
869 : 400 : auto mpfr1 = fpMPFR(fmt, bv1);
870 : 400 : auto mpfr2 = fpMPFR(fmt, bv2);
871 : 400 : auto sym1 = fpSymFPU(fmt, bv1);
872 : 400 : auto sym2 = fpSymFPU(fmt, bv2);
873 [ + + ]: 1200 : for (bool zeroCaseLeft : {false, true})
874 : : {
875 [ - + ]: 1600 : ASSERT_EQ(mpfr1.maxTotal(mpfr2, zeroCaseLeft)->pack(),
876 [ + - ]: 800 : sym1.maxTotal(sym2, zeroCaseLeft)->pack());
877 [ - + ]: 1600 : ASSERT_EQ(mpfr1.minTotal(mpfr2, zeroCaseLeft)->pack(),
878 [ + - ]: 800 : sym1.minTotal(sym2, zeroCaseLeft)->pack());
879 : : }
880 [ + - ][ + - ]: 400 : });
[ + - ][ + - ]
[ + - ]
881 : 1 : }
882 : :
883 : : /* -------------------------------------------------------------------------- */
884 : : /* Comparisons: ==, <=, < */
885 : : /* -------------------------------------------------------------------------- */
886 : :
887 : 4 : TEST_F(TestUtilBlackFloatingPoint, comparisons)
888 : : {
889 : 0 : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
890 : 0 : bool sign = pickBool();
891 [ - - ]: 0 : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
892 : 0 : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig);
893 : 0 : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth());
894 : :
895 : 0 : auto mpfr1 = fpMPFR(d_fp16, bv1);
896 : 0 : auto mpfr2 = fpMPFR(d_fp16, bv2);
897 : 0 : auto sym1 = fpSymFPU(d_fp16, bv1);
898 : 0 : auto sym2 = fpSymFPU(d_fp16, bv2);
899 : :
900 : 0 : ASSERT_EQ(mpfr1 == mpfr2, sym1 == sym2);
901 : 0 : ASSERT_EQ(mpfr1 <= mpfr2, sym1 <= sym2);
902 : 0 : ASSERT_EQ(mpfr1 < mpfr2, sym1 < sym2);
903 : :
904 : : // Self-comparison
905 : 0 : ASSERT_EQ(mpfr1 == mpfr1, sym1 == sym1);
906 : 0 : ASSERT_EQ(mpfr1 <= mpfr1, sym1 <= sym1);
907 : 0 : ASSERT_EQ(mpfr1 < mpfr1, sym1 < sym1);
908 [ - - ][ - - ]: 1 : };
[ - - ][ - - ]
[ - - ][ - - ]
[ - - ]
909 : 1 : testForFloat16(fun16);
910 : 1 : testForFormats(d_test_formats,
911 : : N_TESTS,
912 : 400 : [](const FloatingPointSize& fmt, const BitVector& bv1) {
913 : 400 : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
914 : 400 : auto mpfr1 = fpMPFR(fmt, bv1);
915 : 400 : auto mpfr2 = fpMPFR(fmt, bv2);
916 : 400 : auto sym1 = fpSymFPU(fmt, bv1);
917 : 400 : auto sym2 = fpSymFPU(fmt, bv2);
918 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr1 == mpfr2, sym1 == sym2);
919 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr1 <= mpfr2, sym1 <= sym2);
920 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr1 < mpfr2, sym1 < sym2);
921 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr1 == mpfr1, sym1 == sym1);
922 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr1 <= mpfr1, sym1 <= sym1);
923 [ - + ][ + - ]: 400 : ASSERT_EQ(mpfr1 < mpfr1, sym1 < sym1);
924 [ + - ][ + - ]: 400 : });
[ + - ][ + - ]
[ + - ]
925 : 1 : }
926 : :
927 : : /* -------------------------------------------------------------------------- */
928 : : /* Convert (FP to FP) */
929 : : /* -------------------------------------------------------------------------- */
930 : :
931 : 4 : TEST_F(TestUtilBlackFloatingPoint, fpConvert)
932 : : {
933 [ + + ]: 101 : for (uint32_t i = 0; i < N_TESTS; ++i)
934 : : {
935 : 100 : FloatingPointSize srcFmt = pickFormat();
936 : 100 : FloatingPointSize dstFmt = pickFormat();
937 : 100 : BitVector bv = BitVector::mkRandom(srcFmt.packedWidth());
938 : 100 : RoundingMode rm = pickRm();
939 : :
940 : 100 : auto mpfr = fpMPFR(srcFmt, bv);
941 : 100 : auto sym = fpSymFPU(srcFmt, bv);
942 : :
943 [ - + ]: 200 : ASSERT_EQ(mpfr.convert(dstFmt, rm)->pack(),
944 [ + - ]: 100 : sym.convert(dstFmt, rm)->pack());
945 [ + - ][ + - ]: 100 : }
[ + - ]
946 : : }
947 : :
948 : : /* -------------------------------------------------------------------------- */
949 : : /* Convert to BV (signed / unsigned) */
950 : : /* -------------------------------------------------------------------------- */
951 : :
952 : 4 : TEST_F(TestUtilBlackFloatingPoint, convertToBV)
953 : : {
954 [ + + ]: 101 : for (uint32_t i = 0; i < N_TESTS; ++i)
955 : : {
956 : 100 : FloatingPointSize fmt = pickFormat();
957 : 100 : BitVector bv = BitVector::mkRandom(fmt.packedWidth());
958 : 100 : RoundingMode rm = pickRm();
959 : 100 : uint32_t width = d_rng.pick<uint32_t>(MIN_SIZE_TO_BV, MAX_SIZE_TO_BV);
960 : 100 : BitVector undef = BitVector::mkRandom(width);
961 : :
962 : 100 : auto mpfr = fpMPFR(fmt, bv);
963 : 100 : auto sym = fpSymFPU(fmt, bv);
964 : :
965 : : // SymFPU to_sbv has an issue for a corner case, see #12734 that may
966 : : // get triggered in this test, thus it is temporarily disabled.
967 : : // ASSERT_EQ(mpfr.convertToSBVTotal(width, rm, undef),
968 : : // sym.convertToSBVTotal(width, rm, undef));
969 [ - + ]: 200 : ASSERT_EQ(mpfr.convertToUBVTotal(width, rm, undef),
970 [ + - ]: 100 : sym.convertToUBVTotal(width, rm, undef));
971 [ + - ][ + - ]: 100 : }
[ + - ][ + - ]
972 : : }
973 : :
974 : : /* -------------------------------------------------------------------------- */
975 : : /* Chained operations */
976 : : /* -------------------------------------------------------------------------- */
977 : :
978 : 4 : TEST_F(TestUtilBlackFloatingPoint, chainedAddMul)
979 : : {
980 : 1 : testForFormats(d_all_formats,
981 : : N_TESTS,
982 : 1200 : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
983 : 400 : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
984 : 400 : BitVector bv3 = BitVector::mkRandom(fmt.packedWidth());
985 : :
986 : 400 : auto mpfr1 = fpMPFR(fmt, bv1);
987 : 400 : auto mpfr2 = fpMPFR(fmt, bv2);
988 : 400 : auto mpfr3 = fpMPFR(fmt, bv3);
989 : 400 : auto sym1 = fpSymFPU(fmt, bv1);
990 : 400 : auto sym2 = fpSymFPU(fmt, bv2);
991 : 400 : auto sym3 = fpSymFPU(fmt, bv3);
992 : :
993 : 400 : RoundingMode rm1 = pickRm();
994 : 400 : RoundingMode rm2 = pickRm();
995 : :
996 : : // (a + b) * c
997 [ - + ]: 800 : ASSERT_EQ(mpfr1.add(rm1, mpfr2)->mult(rm2, mpfr3)->pack(),
998 [ + - ]: 400 : sym1.add(rm1, sym2)->mult(rm2, sym3)->pack());
999 [ + - ][ + - ]: 400 : });
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
1000 : 1 : }
1001 : :
1002 : 4 : TEST_F(TestUtilBlackFloatingPoint, chainedAbsAdd)
1003 : : {
1004 : 1 : testForFormats(d_all_formats,
1005 : : N_TESTS,
1006 : 800 : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
1007 : 400 : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
1008 : :
1009 : 400 : auto mpfr1 = fpMPFR(fmt, bv1);
1010 : 400 : auto mpfr2 = fpMPFR(fmt, bv2);
1011 : 400 : auto sym1 = fpSymFPU(fmt, bv1);
1012 : 400 : auto sym2 = fpSymFPU(fmt, bv2);
1013 : :
1014 : 400 : RoundingMode rm = pickRm();
1015 : :
1016 : : // abs(a + b)
1017 [ - + ]: 800 : ASSERT_EQ(mpfr1.add(rm, mpfr2)->absolute()->pack(),
1018 [ + - ]: 400 : sym1.add(rm, sym2)->absolute()->pack());
1019 : : // neg(a + b)
1020 [ - + ]: 800 : ASSERT_EQ(mpfr1.add(rm, mpfr2)->negate()->pack(),
1021 [ + - ]: 400 : sym1.add(rm, sym2)->negate()->pack());
1022 [ + - ][ + - ]: 400 : });
[ + - ][ + - ]
[ + - ]
1023 : 1 : }
1024 : :
1025 : 4 : TEST_F(TestUtilBlackFloatingPoint, chainedSqrtAdd)
1026 : : {
1027 : 1 : testForFormats(d_all_formats,
1028 : : N_TESTS,
1029 : 1200 : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
1030 : 400 : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
1031 : :
1032 : 400 : auto mpfr1 = fpMPFR(fmt, bv1);
1033 : 400 : auto mpfr2 = fpMPFR(fmt, bv2);
1034 : 400 : auto sym1 = fpSymFPU(fmt, bv1);
1035 : 400 : auto sym2 = fpSymFPU(fmt, bv2);
1036 : :
1037 : 400 : RoundingMode rm1 = pickRm();
1038 : 400 : RoundingMode rm2 = pickRm();
1039 : :
1040 : : // sqrt(a + b)
1041 [ - + ]: 800 : ASSERT_EQ(mpfr1.add(rm2, mpfr2)->sqrt(rm1)->pack(),
1042 [ + - ]: 400 : sym1.add(rm2, sym2)->sqrt(rm1)->pack());
1043 : : // rti(a + b)
1044 [ - + ]: 800 : ASSERT_EQ(mpfr1.add(rm2, mpfr2)->rti(rm1)->pack(),
1045 [ + - ]: 400 : sym1.add(rm2, sym2)->rti(rm1)->pack());
1046 [ + - ][ + - ]: 400 : });
[ + - ][ + - ]
[ + - ]
1047 : 1 : }
1048 : :
1049 : 4 : TEST_F(TestUtilBlackFloatingPoint, chainedRemAdd)
1050 : : {
1051 : 1 : testForFormats(d_all_formats,
1052 : : N_TESTS_REM,
1053 : 400 : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
1054 : 200 : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
1055 : 200 : BitVector bv3 = BitVector::mkRandom(fmt.packedWidth());
1056 : :
1057 : 200 : auto mpfr1 = fpMPFR(fmt, bv1);
1058 : 200 : auto mpfr2 = fpMPFR(fmt, bv2);
1059 : 200 : auto mpfr3 = fpMPFR(fmt, bv3);
1060 : 200 : auto sym1 = fpSymFPU(fmt, bv1);
1061 : 200 : auto sym2 = fpSymFPU(fmt, bv2);
1062 : 200 : auto sym3 = fpSymFPU(fmt, bv3);
1063 : :
1064 : 200 : RoundingMode rm = pickRm();
1065 : :
1066 : : // (a + b) rem c
1067 [ - + ]: 400 : ASSERT_EQ(mpfr1.add(rm, mpfr2)->rem(mpfr3)->pack(),
1068 [ + - ]: 200 : sym1.add(rm, sym2)->rem(sym3)->pack());
1069 : : // (a rem b) + c
1070 [ - + ]: 400 : ASSERT_EQ(mpfr1.rem(mpfr2)->add(rm, mpfr3)->pack(),
1071 [ + - ]: 200 : sym1.rem(sym2)->add(rm, sym3)->pack());
1072 [ + - ][ + - ]: 200 : });
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
1073 : 1 : }
1074 : : #else
1075 : : TEST_F(TestUtilBlackFloatingPoint, crosscheckDisabled)
1076 : : {
1077 : : GTEST_SKIP() << "MPFR-vs-SymFPU cross-checks require -DUSE_MPFR=ON";
1078 : : }
1079 : : #endif
1080 : :
1081 : : } // namespace test
1082 : : } // namespace cvc5::internal
|
