diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-09-30 14:05:29 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-30 14:05:29 -0700 |
commit | aa65c60968d0b8c0a7cd47adb2e9e1a684c0332a (patch) | |
tree | b70780307f3f1c7310e95e45e937abcdba39ad73 /test/unit/util | |
parent | 2bd861b27f6e340ea5f6739ac57bb6ffa61ffbfc (diff) |
FloatingPoint: Add utility functions for largest and smallest subnormal. (#5166)
Diffstat (limited to 'test/unit/util')
-rw-r--r-- | test/unit/util/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/util/floatingpoint_black.h | 83 |
2 files changed, 84 insertions, 0 deletions
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 5312342a2..c5753e732 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -21,6 +21,7 @@ cvc4_add_unit_test_white(check_white util) cvc4_add_unit_test_black(configuration_black util) cvc4_add_unit_test_black(datatype_black util) cvc4_add_unit_test_black(exception_black util) +cvc4_add_unit_test_black(floatingpoint_black util) cvc4_add_unit_test_black(integer_black util) cvc4_add_unit_test_white(integer_white util) cvc4_add_unit_test_black(output_black util) diff --git a/test/unit/util/floatingpoint_black.h b/test/unit/util/floatingpoint_black.h new file mode 100644 index 000000000..07b87eac3 --- /dev/null +++ b/test/unit/util/floatingpoint_black.h @@ -0,0 +1,83 @@ +/********************* */ +/*! \file floatingpoint_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of CVC4::FloatingPoint. + ** + ** Black box testing of CVC4::FloatingPoint. + **/ +#include <cxxtest/TestSuite.h> + +#include "util/floatingpoint.h" + +using namespace CVC4; + +class FloatingPointBlack : public CxxTest::TestSuite +{ + public: + void testMakeMinSubnormal(); + void testMakeMaxSubnormal(); +}; + +void FloatingPointBlack::testMakeMinSubnormal() +{ + FloatingPointSize size16(5, 11); + FloatingPointSize size32(8, 24); + FloatingPointSize size64(11, 53); + FloatingPointSize size128(15, 113); + + FloatingPoint fp16 = FloatingPoint::makeMinSubnormal(size16, true); + TS_ASSERT(fp16.isSubnormal()); + FloatingPoint mfp16 = FloatingPoint::makeMinSubnormal(size16, false); + TS_ASSERT(mfp16.isSubnormal()); + + FloatingPoint fp32 = FloatingPoint::makeMinSubnormal(size32, true); + TS_ASSERT(fp32.isSubnormal()); + FloatingPoint mfp32 = FloatingPoint::makeMinSubnormal(size32, false); + TS_ASSERT(mfp32.isSubnormal()); + + FloatingPoint fp64 = FloatingPoint::makeMinSubnormal(size64, true); + TS_ASSERT(fp64.isSubnormal()); + FloatingPoint mfp64 = FloatingPoint::makeMinSubnormal(size64, false); + TS_ASSERT(mfp64.isSubnormal()); + + FloatingPoint fp128 = FloatingPoint::makeMinSubnormal(size128, true); + TS_ASSERT(fp128.isSubnormal()); + FloatingPoint mfp128 = FloatingPoint::makeMinSubnormal(size128, false); + TS_ASSERT(mfp128.isSubnormal()); +} + +void FloatingPointBlack::testMakeMaxSubnormal() +{ + FloatingPointSize size16(5, 11); + FloatingPointSize size32(8, 24); + FloatingPointSize size64(11, 53); + FloatingPointSize size128(15, 113); + + FloatingPoint fp16 = FloatingPoint::makeMaxSubnormal(size16, true); + TS_ASSERT(fp16.isSubnormal()); + FloatingPoint mfp16 = FloatingPoint::makeMaxSubnormal(size16, false); + TS_ASSERT(mfp16.isSubnormal()); + + FloatingPoint fp32 = FloatingPoint::makeMaxSubnormal(size32, true); + TS_ASSERT(fp32.isSubnormal()); + FloatingPoint mfp32 = FloatingPoint::makeMaxSubnormal(size32, false); + TS_ASSERT(mfp32.isSubnormal()); + + FloatingPoint fp64 = FloatingPoint::makeMaxSubnormal(size64, true); + TS_ASSERT(fp64.isSubnormal()); + FloatingPoint mfp64 = FloatingPoint::makeMaxSubnormal(size64, false); + TS_ASSERT(mfp64.isSubnormal()); + + FloatingPoint fp128 = FloatingPoint::makeMaxSubnormal(size128, true); + TS_ASSERT(fp128.isSubnormal()); + FloatingPoint mfp128 = FloatingPoint::makeMaxSubnormal(size128, false); + TS_ASSERT(mfp128.isSubnormal()); +} |