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 : : /** Default number of random tests when not exhaustively testing. */
36 : : static constexpr uint32_t N_TESTS = 1000;
37 : : /** Number of tests fp.rem (significantly slower than other operators). */
38 : : static constexpr uint32_t N_TESTS_REM = 100;
39 : : /** Min/max bit-vector width used in convertToBV cross-checks. */
40 : : static constexpr uint32_t MIN_SIZE_TO_BV = 4;
41 : : static constexpr uint32_t MAX_SIZE_TO_BV = 64;
42 : :
43 : 7 : TestUtilBlackFloatingPoint()
44 : 21 : : d_rng(Random::getRandom()),
45 : 7 : d_fp16(5, 11),
46 : 7 : d_fp32(8, 24),
47 : 7 : d_fp64(11, 53),
48 : 14 : d_fp128(15, 113)
49 : : {
50 : 7 : }
51 : :
52 : 7 : void SetUp() override
53 : : {
54 : 7 : TestInternal::SetUp();
55 : 7 : d_all_formats = {d_fp16, d_fp32, d_fp64, d_fp128};
56 : 7 : d_formats_32_128 = {d_fp32, d_fp64, d_fp128};
57 : 14 : d_all_rms = {RoundingMode::ROUND_NEAREST_TIES_TO_EVEN,
58 : : RoundingMode::ROUND_NEAREST_TIES_TO_AWAY,
59 : : RoundingMode::ROUND_TOWARD_POSITIVE,
60 : : RoundingMode::ROUND_TOWARD_NEGATIVE,
61 : 7 : RoundingMode::ROUND_TOWARD_ZERO};
62 : 7 : }
63 : :
64 : : /** @return A random boolean. */
65 : : bool pickBool() { return d_rng.pick<uint32_t>(0, 1) != 0; }
66 : :
67 : : /** @return A random rounding mode. */
68 : : RoundingMode pickRm()
69 : : {
70 : : return d_all_rms[d_rng.pick<size_t>() % d_all_rms.size()];
71 : : }
72 : :
73 : : /** @return A random floating-point format. */
74 : : FloatingPointSize pickFormat()
75 : : {
76 : : return d_all_formats[d_rng.pick<size_t>() % d_all_formats.size()];
77 : : }
78 : :
79 : : /** Test `fun` exhaustively for all Float16 values. */
80 : : void testForFloat16(
81 : : std::function<void(const BitVector&, const BitVector&)> fun)
82 : : {
83 : : uint32_t expSize = 5;
84 : : uint32_t sigBits = 10; // significand width minus hidden bit
85 : : for (uint32_t i = 0; i < (1u << expSize); ++i)
86 : : {
87 : : BitVector bvexp(expSize, i);
88 : : for (uint32_t j = 0; j < (1u << sigBits); ++j)
89 : : {
90 : : BitVector bvsig(sigBits, j);
91 : : fun(bvexp, bvsig);
92 : : }
93 : : }
94 : : }
95 : :
96 : : /** Test `fun` for given formats. */
97 : : void testForFormats(
98 : : const std::vector<FloatingPointSize>& formats,
99 : : uint32_t nTests,
100 : : std::function<void(const FloatingPointSize&, const BitVector&)> fun)
101 : : {
102 : : for (const auto& f : formats)
103 : : {
104 : : uint32_t bvSize = f.exponentWidth() + f.significandWidth();
105 : : for (uint32_t i = 0; i < nTests; ++i)
106 : : {
107 : : BitVector bv = BitVector::mkRandom(bvSize);
108 : : fun(f, bv);
109 : : }
110 : : }
111 : : }
112 : :
113 : : Random& d_rng;
114 : :
115 : : FloatingPointSize d_fp16;
116 : : FloatingPointSize d_fp32;
117 : : FloatingPointSize d_fp64;
118 : : FloatingPointSize d_fp128;
119 : :
120 : : std::vector<FloatingPointSize> d_all_formats;
121 : : std::vector<FloatingPointSize> d_formats_32_128;
122 : : std::vector<RoundingMode> d_all_rms;
123 : : };
124 : :
125 : : /* -------------------------------------------------------------------------- */
126 : :
127 : 4 : TEST_F(TestUtilBlackFloatingPoint, move)
128 : : {
129 : 1 : BitVector bv1 = BitVector::mkRandom(d_fp16.packedWidth());
130 : 1 : BitVector bv2 = BitVector::mkRandom(d_fp128.packedWidth());
131 : 1 : FloatingPoint fp1(d_fp16, bv1);
132 : 1 : FloatingPoint fp2(d_fp128, bv2);
133 : :
134 : 1 : fp1 = std::move(fp2);
135 [ - + ][ + - ]: 2 : ASSERT_EQ(fp1.pack(), bv2);
136 [ - + ][ + - ]: 1 : ASSERT_EQ(fp1.getSize(), d_fp128);
137 : :
138 : 1 : auto fp3 = std::move(fp1);
139 [ - + ][ + - ]: 2 : ASSERT_EQ(fp3.pack(), bv2);
140 [ - + ][ + - ]: 1 : ASSERT_EQ(fp3.getSize(), d_fp128);
141 : :
142 : 1 : FloatingPoint fp4(std::move(fp3));
143 [ - + ][ + - ]: 2 : ASSERT_EQ(fp4.pack(), bv2);
144 [ - + ][ + - ]: 1 : ASSERT_EQ(fp4.getSize(), d_fp128);
145 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
146 : :
147 : 4 : TEST_F(TestUtilBlackFloatingPoint, makeMinSubnormal)
148 : : {
149 [ + + ]: 5 : for (const auto& size : d_all_formats)
150 : : {
151 : 4 : FloatingPoint fp = FloatingPoint::makeMinSubnormal(size, true);
152 [ - + ][ + - ]: 4 : ASSERT_TRUE(fp.isSubnormal());
153 : 4 : FloatingPoint mfp = FloatingPoint::makeMinSubnormal(size, false);
154 [ - + ][ + - ]: 4 : ASSERT_TRUE(mfp.isSubnormal());
155 [ + - ]: 4 : }
156 : : }
157 : :
158 : 4 : TEST_F(TestUtilBlackFloatingPoint, makeMaxSubnormal)
159 : : {
160 [ + + ]: 5 : for (const auto& size : d_all_formats)
161 : : {
162 : 4 : FloatingPoint fp = FloatingPoint::makeMaxSubnormal(size, true);
163 [ - + ][ + - ]: 4 : ASSERT_TRUE(fp.isSubnormal());
164 : 4 : FloatingPoint mfp = FloatingPoint::makeMaxSubnormal(size, false);
165 [ - + ][ + - ]: 4 : ASSERT_TRUE(mfp.isSubnormal());
166 [ + - ]: 4 : }
167 : : }
168 : :
169 : 4 : TEST_F(TestUtilBlackFloatingPoint, makeMinNormal)
170 : : {
171 [ + + ]: 5 : for (const auto& size : d_all_formats)
172 : : {
173 : 4 : FloatingPoint fp = FloatingPoint::makeMinNormal(size, true);
174 [ - + ][ + - ]: 4 : ASSERT_TRUE(fp.isNormal());
175 : 4 : FloatingPoint mfp = FloatingPoint::makeMinNormal(size, false);
176 [ - + ][ + - ]: 4 : ASSERT_TRUE(mfp.isNormal());
177 [ + - ]: 4 : }
178 : : }
179 : :
180 : 4 : TEST_F(TestUtilBlackFloatingPoint, makeMaxNormal)
181 : : {
182 [ + + ]: 5 : for (const auto& size : d_all_formats)
183 : : {
184 : 4 : FloatingPoint fp = FloatingPoint::makeMaxNormal(size, true);
185 [ - + ][ + - ]: 4 : ASSERT_TRUE(fp.isNormal());
186 : 4 : FloatingPoint mfp = FloatingPoint::makeMaxNormal(size, false);
187 [ - + ][ + - ]: 4 : ASSERT_TRUE(mfp.isNormal());
188 [ + - ]: 4 : }
189 : : }
190 : :
191 : 4 : TEST_F(TestUtilBlackFloatingPoint, fromSbv1)
192 : : {
193 : 1 : BitVector bv0(1, 0u);
194 : 1 : BitVector bv1(1, 1u);
195 [ + + ]: 5 : for (const auto& bv : {bv0, bv1})
196 : : {
197 [ + + ]: 6 : for (bool sign : {true, false})
198 : : {
199 : 0 : FloatingPoint fp(FloatingPointSize(5, 11),
200 : 0 : RoundingMode::ROUND_NEAREST_TIES_TO_AWAY,
201 : : bv,
202 : 4 : sign);
203 : 4 : }
204 [ + + ][ - - ]: 3 : }
205 : 1 : }
206 : :
207 : : /* -------------------------------------------------------------------------- */
208 : : /* Crosscheck MPFR and SymFPU back ends. */
209 : : /* -------------------------------------------------------------------------- */
210 : :
211 : : #ifdef CVC5_USE_MPFR
212 : : namespace {
213 : : /** @return An FP literal with MPFR as the back end. */
214 : : FloatingPointLiteralMPFR fpMPFR(const FloatingPointSize& fmt,
215 : : const BitVector& bv)
216 : : {
217 : : return FloatingPointLiteralMPFR(fmt, bv);
218 : : }
219 : :
220 : : /** @return An FP literal with SymFPU as the back end. */
221 : : FloatingPointLiteralSymFPU fpSymFPU(const FloatingPointSize& fmt,
222 : : const BitVector& bv)
223 : : {
224 : : return FloatingPointLiteralSymFPU(fmt, bv);
225 : : }
226 : : } // namespace
227 : :
228 : : TEST_F(TestUtilBlackFloatingPoint, pack)
229 : : {
230 : : // Exhaustive for Float16
231 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
232 : : for (bool sign : {false, true})
233 : : {
234 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
235 : : BitVector bv = bvsign.concat(bvexp).concat(bvsig);
236 : :
237 : : auto mpfr = fpMPFR(d_fp16, bv);
238 : : auto sym = fpSymFPU(d_fp16, bv);
239 : :
240 : : BitVector packedMpfr = mpfr.pack();
241 : : BitVector packedSym = sym.pack();
242 : :
243 : : // Both backends must produce the same packed representation.
244 : : ASSERT_EQ(packedMpfr, packedSym)
245 : : << "pack mismatch for bv=" << bv.toString();
246 : : }
247 : : };
248 : : testForFloat16(fun16);
249 : :
250 : : // Random for larger formats
251 : : testForFormats(d_formats_32_128,
252 : : N_TESTS,
253 : : [](const FloatingPointSize& fmt, const BitVector& bv) {
254 : : auto mpfr = fpMPFR(fmt, bv);
255 : : auto sym = fpSymFPU(fmt, bv);
256 : : ASSERT_EQ(mpfr.pack(), sym.pack());
257 : : });
258 : : }
259 : :
260 : : TEST_F(TestUtilBlackFloatingPoint, classification)
261 : : {
262 : : BitVector ezero = BitVector::mkZero(5);
263 : : BitVector eones = BitVector::mkOnes(5);
264 : : BitVector szero = BitVector::mkZero(10);
265 : : auto fun16 = [&, this](const BitVector& bvexp, const BitVector& bvsig) {
266 : : for (bool sign : {false, true})
267 : : {
268 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
269 : : BitVector bv = bvsign.concat(bvexp).concat(bvsig);
270 : :
271 : : auto mpfr = fpMPFR(d_fp16, bv);
272 : : auto sym = fpSymFPU(d_fp16, bv);
273 : :
274 : : ASSERT_EQ(mpfr.isNormal(), sym.isNormal());
275 : : ASSERT_EQ(mpfr.isSubnormal(), sym.isSubnormal());
276 : : ASSERT_EQ(mpfr.isZero(), sym.isZero());
277 : : ASSERT_EQ(mpfr.isInfinite(), sym.isInfinite());
278 : : ASSERT_EQ(mpfr.isNaN(), sym.isNaN());
279 : : ASSERT_EQ(mpfr.isNegative(), sym.isNegative());
280 : : ASSERT_EQ(mpfr.isPositive(), sym.isPositive());
281 : : ASSERT_EQ(mpfr.getSign(), sym.getSign());
282 : :
283 : : if (bvexp != ezero)
284 : : {
285 : : if (bvexp != eones)
286 : : {
287 : : ASSERT_TRUE(mpfr.isNormal());
288 : : ASSERT_FALSE(mpfr.isSubnormal());
289 : : ASSERT_FALSE(mpfr.isInfinite());
290 : : ASSERT_FALSE(mpfr.isNaN());
291 : : ASSERT_FALSE(mpfr.isZero());
292 : : }
293 : : else
294 : : {
295 : : if (bvsig == szero)
296 : : {
297 : : ASSERT_TRUE(mpfr.isInfinite());
298 : : ASSERT_FALSE(mpfr.isNormal());
299 : : ASSERT_FALSE(mpfr.isSubnormal());
300 : : ASSERT_FALSE(mpfr.isNaN());
301 : : ASSERT_FALSE(mpfr.isZero());
302 : : }
303 : : else
304 : : {
305 : : ASSERT_TRUE(mpfr.isNaN());
306 : : ASSERT_FALSE(mpfr.isNormal());
307 : : ASSERT_FALSE(mpfr.isSubnormal());
308 : : ASSERT_FALSE(mpfr.isInfinite());
309 : : ASSERT_FALSE(mpfr.isZero());
310 : : }
311 : : }
312 : : }
313 : : else
314 : : {
315 : : if (bvsig == szero)
316 : : {
317 : : ASSERT_TRUE(mpfr.isZero());
318 : : ASSERT_FALSE(mpfr.isNormal());
319 : : ASSERT_FALSE(mpfr.isSubnormal());
320 : : ASSERT_FALSE(mpfr.isInfinite());
321 : : ASSERT_FALSE(mpfr.isNaN());
322 : : }
323 : : else
324 : : {
325 : : ASSERT_TRUE(mpfr.isSubnormal());
326 : : ASSERT_FALSE(mpfr.isNormal());
327 : : ASSERT_FALSE(mpfr.isInfinite());
328 : : ASSERT_FALSE(mpfr.isNaN());
329 : : ASSERT_FALSE(mpfr.isZero());
330 : : }
331 : : }
332 : : }
333 : : };
334 : : testForFloat16(fun16);
335 : : testForFormats(d_formats_32_128,
336 : : N_TESTS,
337 : : [](const FloatingPointSize& fmt, const BitVector& bv1) {
338 : : auto mpfr = fpMPFR(fmt, bv1);
339 : : auto sym = fpSymFPU(fmt, bv1);
340 : : ASSERT_EQ(mpfr.isNormal(), sym.isNormal());
341 : : ASSERT_EQ(mpfr.isSubnormal(), sym.isSubnormal());
342 : : ASSERT_EQ(mpfr.isZero(), sym.isZero());
343 : : ASSERT_EQ(mpfr.isNaN(), sym.isNaN());
344 : : ASSERT_EQ(mpfr.isInfinite(), sym.isInfinite());
345 : : });
346 : : }
347 : :
348 : : TEST_F(TestUtilBlackFloatingPoint, components)
349 : : {
350 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
351 : : for (bool sign : {false, true})
352 : : {
353 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
354 : : BitVector bv = bvsign.concat(bvexp).concat(bvsig);
355 : :
356 : : auto mpfr = fpMPFR(d_fp16, bv);
357 : : auto sym = fpSymFPU(d_fp16, bv);
358 : :
359 : : ASSERT_EQ(mpfr.getUnpackedExponent(), sym.getUnpackedExponent());
360 : : ASSERT_EQ(mpfr.getUnpackedSignificand(), sym.getUnpackedSignificand());
361 : : }
362 : : };
363 : : testForFloat16(fun16);
364 : : testForFormats(
365 : : d_formats_32_128,
366 : : N_TESTS,
367 : : [](const FloatingPointSize& fmt, const BitVector& bv) {
368 : : auto mpfr = fpMPFR(fmt, bv);
369 : : auto sym = fpSymFPU(fmt, bv);
370 : : ASSERT_EQ(mpfr.getUnpackedExponent(), sym.getUnpackedExponent());
371 : : ASSERT_EQ(mpfr.getUnpackedSignificand(), sym.getUnpackedSignificand());
372 : : });
373 : : }
374 : :
375 : : TEST_F(TestUtilBlackFloatingPoint, specialConstants)
376 : : {
377 : : for (const auto& size : d_all_formats)
378 : : {
379 : : using SCKind = FloatingPointLiteral::SpecialConstKind;
380 : : // NaN
381 : : {
382 : : auto mpfr = FloatingPointLiteralMPFR(size, SCKind::FPNAN);
383 : : auto sym = FloatingPointLiteralSymFPU(size, SCKind::FPNAN);
384 : : ASSERT_EQ(mpfr.pack(), sym.pack());
385 : : ASSERT_TRUE(mpfr.isNaN());
386 : : ASSERT_FALSE(mpfr.isInfinite());
387 : : ASSERT_FALSE(mpfr.isNormal());
388 : : ASSERT_FALSE(mpfr.isSubnormal());
389 : : ASSERT_FALSE(mpfr.isZero());
390 : : }
391 : : for (bool sign : {false, true})
392 : : {
393 : : // +inf, -inf
394 : : {
395 : : auto mpfr = FloatingPointLiteralMPFR(size, SCKind::FPINF, sign);
396 : : auto sym = FloatingPointLiteralSymFPU(size, SCKind::FPINF, sign);
397 : : ASSERT_EQ(mpfr.pack(), sym.pack());
398 : : ASSERT_TRUE(mpfr.isInfinite());
399 : : ASSERT_FALSE(mpfr.isNaN());
400 : : ASSERT_FALSE(mpfr.isNormal());
401 : : ASSERT_FALSE(mpfr.isSubnormal());
402 : : ASSERT_FALSE(mpfr.isZero());
403 : : }
404 : : // +zero, -zero
405 : : {
406 : : auto mpfr = FloatingPointLiteralMPFR(size, SCKind::FPZERO, sign);
407 : : auto sym = FloatingPointLiteralSymFPU(size, SCKind::FPZERO, sign);
408 : : ASSERT_EQ(mpfr.pack(), sym.pack());
409 : : ASSERT_TRUE(mpfr.isZero());
410 : : ASSERT_FALSE(mpfr.isInfinite());
411 : : ASSERT_FALSE(mpfr.isNaN());
412 : : ASSERT_FALSE(mpfr.isNormal());
413 : : ASSERT_FALSE(mpfr.isSubnormal());
414 : : }
415 : : }
416 : : }
417 : : }
418 : :
419 : : TEST_F(TestUtilBlackFloatingPoint, fromUbvSbv)
420 : : {
421 : : // Exhaustive for Float16
422 : : for (uint64_t bw = 2; bw <= 16; ++bw)
423 : : {
424 : : for (uint64_t i = 0; i < (1ul << bw); ++i)
425 : : {
426 : : BitVector bv = BitVector(bw, i);
427 : : for (RoundingMode rm : d_all_rms)
428 : : {
429 : : for (bool sign : {false, true})
430 : : {
431 : : FloatingPointLiteralMPFR mpfr(d_fp16, rm, bv, sign);
432 : : FloatingPointLiteralSymFPU symfpu(d_fp16, rm, bv, sign);
433 : : ASSERT_EQ(mpfr.pack(), symfpu.pack());
434 : : }
435 : : }
436 : : }
437 : : }
438 : : for (const auto& f : d_all_formats)
439 : : {
440 : : for (uint64_t bw = 1; bw <= 16; ++bw)
441 : : {
442 : : for (uint64_t i = 0; i < 10; ++i)
443 : : {
444 : : auto bv = BitVector::mkRandom(bw);
445 : : for (RoundingMode rm : d_all_rms)
446 : : {
447 : : for (auto sign : {false, true})
448 : : {
449 : : FloatingPointLiteralMPFR mpfr(f, rm, bv, sign);
450 : : FloatingPointLiteralSymFPU symfpu(f, rm, bv, sign);
451 : : ASSERT_EQ(mpfr.pack(), symfpu.pack());
452 : : }
453 : : }
454 : : }
455 : : }
456 : : }
457 : : }
458 : :
459 : : /* -------------------------------------------------------------------------- */
460 : : /* Unary operators without FM: fp.abs, fp.neg */
461 : : /* -------------------------------------------------------------------------- */
462 : :
463 : : #define TEST_UNARY_OP(NAME, METHOD) \
464 : : TEST_F(TestUtilBlackFloatingPoint, NAME) \
465 : : { \
466 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) { \
467 : : for (bool sign : {false, true}) \
468 : : { \
469 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1); \
470 : : BitVector bv = bvsign.concat(bvexp).concat(bvsig); \
471 : : auto mpfr = fpMPFR(d_fp16, bv); \
472 : : auto sym = fpSymFPU(d_fp16, bv); \
473 : : ASSERT_EQ(mpfr.METHOD()->pack(), sym.METHOD()->pack()); \
474 : : } \
475 : : }; \
476 : : testForFloat16(fun16); \
477 : : testForFormats(d_formats_32_128, \
478 : : N_TESTS, \
479 : : [](const FloatingPointSize& fmt, const BitVector& bv) { \
480 : : auto mpfr = fpMPFR(fmt, bv); \
481 : : auto sym = fpSymFPU(fmt, bv); \
482 : : ASSERT_EQ(mpfr.METHOD()->pack(), sym.METHOD()->pack()); \
483 : : }); \
484 : : }
485 : :
486 : : TEST_UNARY_OP(absolute, absolute)
487 : : TEST_UNARY_OP(negate, negate)
488 : :
489 : : #undef TEST_UNARY_OP
490 : :
491 : : /* -------------------------------------------------------------------------- */
492 : : /* Unary operators with RM: fp.sqrt, fp.rti */
493 : : /* -------------------------------------------------------------------------- */
494 : :
495 : : #define TEST_UNARY_RM_OP(NAME, METHOD) \
496 : : TEST_F(TestUtilBlackFloatingPoint, NAME) \
497 : : { \
498 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) { \
499 : : for (bool sign : {false, true}) \
500 : : { \
501 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1); \
502 : : BitVector bv = bvsign.concat(bvexp).concat(bvsig); \
503 : : auto mpfr = fpMPFR(d_fp16, bv); \
504 : : auto sym = fpSymFPU(d_fp16, bv); \
505 : : for (auto rm : d_all_rms) \
506 : : { \
507 : : ASSERT_EQ(mpfr.METHOD(rm)->pack(), sym.METHOD(rm)->pack()); \
508 : : } \
509 : : } \
510 : : }; \
511 : : testForFloat16(fun16); \
512 : : testForFormats(d_formats_32_128, \
513 : : N_TESTS, \
514 : : [this](const FloatingPointSize& fmt, const BitVector& bv) { \
515 : : auto mpfr = fpMPFR(fmt, bv); \
516 : : auto sym = fpSymFPU(fmt, bv); \
517 : : for (auto rm : d_all_rms) \
518 : : { \
519 : : ASSERT_EQ(mpfr.METHOD(rm)->pack(), \
520 : : sym.METHOD(rm)->pack()); \
521 : : } \
522 : : }); \
523 : : }
524 : :
525 : : TEST_UNARY_RM_OP(fpSqrt, sqrt)
526 : : TEST_UNARY_RM_OP(fpRti, rti)
527 : :
528 : : #undef TEST_UNARY_RM_OP
529 : :
530 : : /* -------------------------------------------------------------------------- */
531 : : /* Binary operator without RM: fp.rem */
532 : : /* -------------------------------------------------------------------------- */
533 : :
534 : : TEST_F(TestUtilBlackFloatingPoint, fpRem)
535 : : {
536 : : // Exhaustive for Float16 (one operand exhaustive, other random)
537 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
538 : : bool sign = pickBool();
539 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
540 : : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig);
541 : : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth());
542 : :
543 : : auto mpfr1 = fpMPFR(d_fp16, bv1);
544 : : auto mpfr2 = fpMPFR(d_fp16, bv2);
545 : : auto sym1 = fpSymFPU(d_fp16, bv1);
546 : : auto sym2 = fpSymFPU(d_fp16, bv2);
547 : :
548 : : ASSERT_EQ(mpfr1.rem(mpfr2)->pack(), sym1.rem(sym2)->pack());
549 : : };
550 : : testForFloat16(fun16);
551 : :
552 : : testForFormats(d_formats_32_128,
553 : : N_TESTS,
554 : : [](const FloatingPointSize& fmt, const BitVector& bv1) {
555 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
556 : : auto mpfr1 = fpMPFR(fmt, bv1);
557 : : auto mpfr2 = fpMPFR(fmt, bv2);
558 : : auto sym1 = fpSymFPU(fmt, bv1);
559 : : auto sym2 = fpSymFPU(fmt, bv2);
560 : : ASSERT_EQ(mpfr1.rem(mpfr2)->pack(), sym1.rem(sym2)->pack());
561 : : });
562 : : }
563 : :
564 : : /* -------------------------------------------------------------------------- */
565 : : /* Binary operators with RM: fp.add, fp.sub, fp.mult, fp.div */
566 : : /* -------------------------------------------------------------------------- */
567 : :
568 : : #define TEST_BINARY_RM_OP(NAME, METHOD) \
569 : : TEST_F(TestUtilBlackFloatingPoint, NAME) \
570 : : { \
571 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) { \
572 : : bool sign = pickBool(); \
573 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1); \
574 : : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig); \
575 : : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth()); \
576 : : auto mpfr1 = fpMPFR(d_fp16, bv1); \
577 : : auto mpfr2 = fpMPFR(d_fp16, bv2); \
578 : : auto sym1 = fpSymFPU(d_fp16, bv1); \
579 : : auto sym2 = fpSymFPU(d_fp16, bv2); \
580 : : for (auto rm : d_all_rms) \
581 : : { \
582 : : ASSERT_EQ(mpfr1.METHOD(rm, mpfr2)->pack(), \
583 : : sym1.METHOD(rm, sym2)->pack()); \
584 : : } \
585 : : }; \
586 : : testForFloat16(fun16); \
587 : : testForFormats( \
588 : : d_formats_32_128, \
589 : : N_TESTS, \
590 : : [this](const FloatingPointSize& fmt, const BitVector& bv1) { \
591 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth()); \
592 : : auto mpfr1 = fpMPFR(fmt, bv1); \
593 : : auto mpfr2 = fpMPFR(fmt, bv2); \
594 : : auto sym1 = fpSymFPU(fmt, bv1); \
595 : : auto sym2 = fpSymFPU(fmt, bv2); \
596 : : for (auto rm : d_all_rms) \
597 : : { \
598 : : ASSERT_EQ(mpfr1.METHOD(rm, mpfr2)->pack(), \
599 : : sym1.METHOD(rm, sym2)->pack()); \
600 : : } \
601 : : }); \
602 : : }
603 : :
604 : : TEST_BINARY_RM_OP(fpAdd, add)
605 : : TEST_BINARY_RM_OP(fpSub, sub)
606 : : TEST_BINARY_RM_OP(fpMult, mult)
607 : : TEST_BINARY_RM_OP(fpDiv, div)
608 : :
609 : : #undef TEST_BINARY_RM_OP
610 : :
611 : : /* -------------------------------------------------------------------------- */
612 : : /* Ternary operator with RM: fp.fma */
613 : : /* -------------------------------------------------------------------------- */
614 : :
615 : : TEST_F(TestUtilBlackFloatingPoint, fpFma)
616 : : {
617 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
618 : : bool sign = pickBool();
619 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
620 : : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig);
621 : : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth());
622 : : BitVector bv3 = BitVector::mkRandom(d_fp16.packedWidth());
623 : :
624 : : auto mpfr1 = fpMPFR(d_fp16, bv1);
625 : : auto mpfr2 = fpMPFR(d_fp16, bv2);
626 : : auto mpfr3 = fpMPFR(d_fp16, bv3);
627 : : auto sym1 = fpSymFPU(d_fp16, bv1);
628 : : auto sym2 = fpSymFPU(d_fp16, bv2);
629 : : auto sym3 = fpSymFPU(d_fp16, bv3);
630 : :
631 : : for (auto rm : d_all_rms)
632 : : {
633 : : ASSERT_EQ(mpfr1.fma(rm, mpfr2, mpfr3)->pack(),
634 : : sym1.fma(rm, sym2, sym3)->pack());
635 : : }
636 : : };
637 : : testForFloat16(fun16);
638 : :
639 : : testForFormats(d_formats_32_128,
640 : : N_TESTS,
641 : : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
642 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
643 : : BitVector bv3 = BitVector::mkRandom(fmt.packedWidth());
644 : : auto mpfr1 = fpMPFR(fmt, bv1);
645 : : auto mpfr2 = fpMPFR(fmt, bv2);
646 : : auto mpfr3 = fpMPFR(fmt, bv3);
647 : : auto sym1 = fpSymFPU(fmt, bv1);
648 : : auto sym2 = fpSymFPU(fmt, bv2);
649 : : auto sym3 = fpSymFPU(fmt, bv3);
650 : : for (auto rm : d_all_rms)
651 : : {
652 : : ASSERT_EQ(mpfr1.fma(rm, mpfr2, mpfr3)->pack(),
653 : : sym1.fma(rm, sym2, sym3)->pack());
654 : : }
655 : : });
656 : : }
657 : :
658 : : /* -------------------------------------------------------------------------- */
659 : : /* Min/Max */
660 : : /* -------------------------------------------------------------------------- */
661 : :
662 : : TEST_F(TestUtilBlackFloatingPoint, fpMinMax)
663 : : {
664 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
665 : : bool sign = pickBool();
666 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
667 : : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig);
668 : : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth());
669 : :
670 : : auto mpfr1 = fpMPFR(d_fp16, bv1);
671 : : auto mpfr2 = fpMPFR(d_fp16, bv2);
672 : : auto sym1 = fpSymFPU(d_fp16, bv1);
673 : : auto sym2 = fpSymFPU(d_fp16, bv2);
674 : :
675 : : for (bool zeroCaseLeft : {false, true})
676 : : {
677 : : ASSERT_EQ(mpfr1.maxTotal(mpfr2, zeroCaseLeft)->pack(),
678 : : sym1.maxTotal(sym2, zeroCaseLeft)->pack());
679 : : ASSERT_EQ(mpfr1.minTotal(mpfr2, zeroCaseLeft)->pack(),
680 : : sym1.minTotal(sym2, zeroCaseLeft)->pack());
681 : : }
682 : : };
683 : : testForFloat16(fun16);
684 : : testForFormats(d_formats_32_128,
685 : : N_TESTS,
686 : : [](const FloatingPointSize& fmt, const BitVector& bv1) {
687 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
688 : : auto mpfr1 = fpMPFR(fmt, bv1);
689 : : auto mpfr2 = fpMPFR(fmt, bv2);
690 : : auto sym1 = fpSymFPU(fmt, bv1);
691 : : auto sym2 = fpSymFPU(fmt, bv2);
692 : : for (bool zeroCaseLeft : {false, true})
693 : : {
694 : : ASSERT_EQ(mpfr1.maxTotal(mpfr2, zeroCaseLeft)->pack(),
695 : : sym1.maxTotal(sym2, zeroCaseLeft)->pack());
696 : : ASSERT_EQ(mpfr1.minTotal(mpfr2, zeroCaseLeft)->pack(),
697 : : sym1.minTotal(sym2, zeroCaseLeft)->pack());
698 : : }
699 : : });
700 : : }
701 : :
702 : : /* -------------------------------------------------------------------------- */
703 : : /* Comparisons: ==, <=, < */
704 : : /* -------------------------------------------------------------------------- */
705 : :
706 : : TEST_F(TestUtilBlackFloatingPoint, comparisons)
707 : : {
708 : : auto fun16 = [this](const BitVector& bvexp, const BitVector& bvsig) {
709 : : bool sign = pickBool();
710 : : BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
711 : : BitVector bv1 = bvsign.concat(bvexp).concat(bvsig);
712 : : BitVector bv2 = BitVector::mkRandom(d_fp16.packedWidth());
713 : :
714 : : auto mpfr1 = fpMPFR(d_fp16, bv1);
715 : : auto mpfr2 = fpMPFR(d_fp16, bv2);
716 : : auto sym1 = fpSymFPU(d_fp16, bv1);
717 : : auto sym2 = fpSymFPU(d_fp16, bv2);
718 : :
719 : : ASSERT_EQ(mpfr1 == mpfr2, sym1 == sym2);
720 : : ASSERT_EQ(mpfr1 <= mpfr2, sym1 <= sym2);
721 : : ASSERT_EQ(mpfr1 < mpfr2, sym1 < sym2);
722 : :
723 : : // Self-comparison
724 : : ASSERT_EQ(mpfr1 == mpfr1, sym1 == sym1);
725 : : ASSERT_EQ(mpfr1 <= mpfr1, sym1 <= sym1);
726 : : ASSERT_EQ(mpfr1 < mpfr1, sym1 < sym1);
727 : : };
728 : : testForFloat16(fun16);
729 : : testForFormats(d_formats_32_128,
730 : : N_TESTS,
731 : : [](const FloatingPointSize& fmt, const BitVector& bv1) {
732 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
733 : : auto mpfr1 = fpMPFR(fmt, bv1);
734 : : auto mpfr2 = fpMPFR(fmt, bv2);
735 : : auto sym1 = fpSymFPU(fmt, bv1);
736 : : auto sym2 = fpSymFPU(fmt, bv2);
737 : : ASSERT_EQ(mpfr1 == mpfr2, sym1 == sym2);
738 : : ASSERT_EQ(mpfr1 <= mpfr2, sym1 <= sym2);
739 : : ASSERT_EQ(mpfr1 < mpfr2, sym1 < sym2);
740 : : ASSERT_EQ(mpfr1 == mpfr1, sym1 == sym1);
741 : : ASSERT_EQ(mpfr1 <= mpfr1, sym1 <= sym1);
742 : : ASSERT_EQ(mpfr1 < mpfr1, sym1 < sym1);
743 : : });
744 : : }
745 : :
746 : : /* -------------------------------------------------------------------------- */
747 : : /* Convert (FP to FP) */
748 : : /* -------------------------------------------------------------------------- */
749 : :
750 : : TEST_F(TestUtilBlackFloatingPoint, fpConvert)
751 : : {
752 : : for (uint32_t i = 0; i < N_TESTS; ++i)
753 : : {
754 : : FloatingPointSize srcFmt = pickFormat();
755 : : FloatingPointSize dstFmt = pickFormat();
756 : : BitVector bv = BitVector::mkRandom(srcFmt.packedWidth());
757 : : RoundingMode rm = pickRm();
758 : :
759 : : auto mpfr = fpMPFR(srcFmt, bv);
760 : : auto sym = fpSymFPU(srcFmt, bv);
761 : :
762 : : ASSERT_EQ(mpfr.convert(dstFmt, rm)->pack(),
763 : : sym.convert(dstFmt, rm)->pack());
764 : : }
765 : : }
766 : :
767 : : /* -------------------------------------------------------------------------- */
768 : : /* Convert to BV (signed / unsigned) */
769 : : /* -------------------------------------------------------------------------- */
770 : :
771 : : TEST_F(TestUtilBlackFloatingPoint, convertToBV)
772 : : {
773 : : for (uint32_t i = 0; i < N_TESTS; ++i)
774 : : {
775 : : FloatingPointSize fmt = pickFormat();
776 : : BitVector bv = BitVector::mkRandom(fmt.packedWidth());
777 : : RoundingMode rm = pickRm();
778 : : uint32_t width = d_rng.pick<uint32_t>(MIN_SIZE_TO_BV, MAX_SIZE_TO_BV);
779 : : BitVector undef = BitVector::mkRandom(width);
780 : :
781 : : auto mpfr = fpMPFR(fmt, bv);
782 : : auto sym = fpSymFPU(fmt, bv);
783 : :
784 : : ASSERT_EQ(mpfr.convertToSBVTotal(width, rm, undef),
785 : : sym.convertToSBVTotal(width, rm, undef));
786 : : ASSERT_EQ(mpfr.convertToUBVTotal(width, rm, undef),
787 : : sym.convertToUBVTotal(width, rm, undef));
788 : : }
789 : : }
790 : :
791 : : /* -------------------------------------------------------------------------- */
792 : : /* Chained operations */
793 : : /* -------------------------------------------------------------------------- */
794 : :
795 : : TEST_F(TestUtilBlackFloatingPoint, chainedAddMul)
796 : : {
797 : : testForFormats(d_all_formats,
798 : : N_TESTS,
799 : : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
800 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
801 : : BitVector bv3 = BitVector::mkRandom(fmt.packedWidth());
802 : :
803 : : auto mpfr1 = fpMPFR(fmt, bv1);
804 : : auto mpfr2 = fpMPFR(fmt, bv2);
805 : : auto mpfr3 = fpMPFR(fmt, bv3);
806 : : auto sym1 = fpSymFPU(fmt, bv1);
807 : : auto sym2 = fpSymFPU(fmt, bv2);
808 : : auto sym3 = fpSymFPU(fmt, bv3);
809 : :
810 : : RoundingMode rm1 = pickRm();
811 : : RoundingMode rm2 = pickRm();
812 : :
813 : : // (a + b) * c
814 : : ASSERT_EQ(mpfr1.add(rm1, mpfr2)->mult(rm2, mpfr3)->pack(),
815 : : sym1.add(rm1, sym2)->mult(rm2, sym3)->pack());
816 : : });
817 : : }
818 : :
819 : : TEST_F(TestUtilBlackFloatingPoint, chainedAbsAdd)
820 : : {
821 : : testForFormats(d_all_formats,
822 : : N_TESTS,
823 : : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
824 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
825 : :
826 : : auto mpfr1 = fpMPFR(fmt, bv1);
827 : : auto mpfr2 = fpMPFR(fmt, bv2);
828 : : auto sym1 = fpSymFPU(fmt, bv1);
829 : : auto sym2 = fpSymFPU(fmt, bv2);
830 : :
831 : : RoundingMode rm = pickRm();
832 : :
833 : : // abs(a + b)
834 : : ASSERT_EQ(mpfr1.add(rm, mpfr2)->absolute()->pack(),
835 : : sym1.add(rm, sym2)->absolute()->pack());
836 : : // neg(a + b)
837 : : ASSERT_EQ(mpfr1.add(rm, mpfr2)->negate()->pack(),
838 : : sym1.add(rm, sym2)->negate()->pack());
839 : : });
840 : : }
841 : :
842 : : TEST_F(TestUtilBlackFloatingPoint, chainedSqrtAdd)
843 : : {
844 : : testForFormats(d_all_formats,
845 : : N_TESTS,
846 : : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
847 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
848 : :
849 : : auto mpfr1 = fpMPFR(fmt, bv1);
850 : : auto mpfr2 = fpMPFR(fmt, bv2);
851 : : auto sym1 = fpSymFPU(fmt, bv1);
852 : : auto sym2 = fpSymFPU(fmt, bv2);
853 : :
854 : : RoundingMode rm1 = pickRm();
855 : : RoundingMode rm2 = pickRm();
856 : :
857 : : // sqrt(a + b)
858 : : ASSERT_EQ(mpfr1.add(rm2, mpfr2)->sqrt(rm1)->pack(),
859 : : sym1.add(rm2, sym2)->sqrt(rm1)->pack());
860 : : // rti(a + b)
861 : : ASSERT_EQ(mpfr1.add(rm2, mpfr2)->rti(rm1)->pack(),
862 : : sym1.add(rm2, sym2)->rti(rm1)->pack());
863 : : });
864 : : }
865 : :
866 : : TEST_F(TestUtilBlackFloatingPoint, chainedRemAdd)
867 : : {
868 : : testForFormats(d_all_formats,
869 : : N_TESTS_REM,
870 : : [this](const FloatingPointSize& fmt, const BitVector& bv1) {
871 : : BitVector bv2 = BitVector::mkRandom(fmt.packedWidth());
872 : : BitVector bv3 = BitVector::mkRandom(fmt.packedWidth());
873 : :
874 : : auto mpfr1 = fpMPFR(fmt, bv1);
875 : : auto mpfr2 = fpMPFR(fmt, bv2);
876 : : auto mpfr3 = fpMPFR(fmt, bv3);
877 : : auto sym1 = fpSymFPU(fmt, bv1);
878 : : auto sym2 = fpSymFPU(fmt, bv2);
879 : : auto sym3 = fpSymFPU(fmt, bv3);
880 : :
881 : : RoundingMode rm = pickRm();
882 : :
883 : : // (a + b) rem c
884 : : ASSERT_EQ(mpfr1.add(rm, mpfr2)->rem(mpfr3)->pack(),
885 : : sym1.add(rm, sym2)->rem(sym3)->pack());
886 : : // (a rem b) + c
887 : : ASSERT_EQ(mpfr1.rem(mpfr2)->add(rm, mpfr3)->pack(),
888 : : sym1.rem(sym2)->add(rm, sym3)->pack());
889 : : });
890 : : }
891 : : #else
892 : 4 : TEST_F(TestUtilBlackFloatingPoint, crosscheckDisabled)
893 : : {
894 : 1 : GTEST_SKIP() << "MPFR-vs-SymFPU cross-checks require -DUSE_MPFR=ON";
895 : : }
896 : : #endif
897 : :
898 : : } // namespace test
899 : : } // namespace cvc5::internal
|
