From: Aina Niemetz Date: Tue, 2 Mar 2021 00:07:25 +0000 (-0800) Subject: google test: util: Migrate floatingpoint_black. (#6021) X-Git-Tag: cvc5-1.0.0~2174 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=822ae21e0b26e9a98b3a5585dbcd2694bbbce685;p=cvc5.git google test: util: Migrate floatingpoint_black. (#6021) --- diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index fb76f49e2..046f4c93e 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -22,7 +22,7 @@ cvc4_add_unit_test_black(configuration_black util) cvc4_add_unit_test_black(datatype_black util) cvc4_add_unit_test_black(exception_black util) if(CVC4_USE_SYMFPU) -cvc4_add_cxx_unit_test_black(floatingpoint_black util) +cvc4_add_unit_test_black(floatingpoint_black util) endif() cvc4_add_unit_test_black(integer_black util) cvc4_add_unit_test_white(integer_white util) diff --git a/test/unit/util/floatingpoint_black.cpp b/test/unit/util/floatingpoint_black.cpp new file mode 100644 index 000000000..f60fe4a8b --- /dev/null +++ b/test/unit/util/floatingpoint_black.cpp @@ -0,0 +1,139 @@ +/********************* */ +/*! \file floatingpoint_black.cpp + ** \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 "test.h" +#include "util/floatingpoint.h" + +namespace CVC4 { +namespace test { + +class TestUtilBlackFloatingPoint : public TestInternal +{ +}; + +TEST_F(TestUtilBlackFloatingPoint, makeMinSubnormal) +{ + FloatingPointSize size16(5, 11); + FloatingPointSize size32(8, 24); + FloatingPointSize size64(11, 53); + FloatingPointSize size128(15, 113); + + FloatingPoint fp16 = FloatingPoint::makeMinSubnormal(size16, true); + ASSERT_TRUE(fp16.isSubnormal()); + FloatingPoint mfp16 = FloatingPoint::makeMinSubnormal(size16, false); + ASSERT_TRUE(mfp16.isSubnormal()); + + FloatingPoint fp32 = FloatingPoint::makeMinSubnormal(size32, true); + ASSERT_TRUE(fp32.isSubnormal()); + FloatingPoint mfp32 = FloatingPoint::makeMinSubnormal(size32, false); + ASSERT_TRUE(mfp32.isSubnormal()); + + FloatingPoint fp64 = FloatingPoint::makeMinSubnormal(size64, true); + ASSERT_TRUE(fp64.isSubnormal()); + FloatingPoint mfp64 = FloatingPoint::makeMinSubnormal(size64, false); + ASSERT_TRUE(mfp64.isSubnormal()); + + FloatingPoint fp128 = FloatingPoint::makeMinSubnormal(size128, true); + ASSERT_TRUE(fp128.isSubnormal()); + FloatingPoint mfp128 = FloatingPoint::makeMinSubnormal(size128, false); + ASSERT_TRUE(mfp128.isSubnormal()); +} + +TEST_F(TestUtilBlackFloatingPoint, makeMaxSubnormal) +{ + FloatingPointSize size16(5, 11); + FloatingPointSize size32(8, 24); + FloatingPointSize size64(11, 53); + FloatingPointSize size128(15, 113); + + FloatingPoint fp16 = FloatingPoint::makeMaxSubnormal(size16, true); + ASSERT_TRUE(fp16.isSubnormal()); + FloatingPoint mfp16 = FloatingPoint::makeMaxSubnormal(size16, false); + ASSERT_TRUE(mfp16.isSubnormal()); + + FloatingPoint fp32 = FloatingPoint::makeMaxSubnormal(size32, true); + ASSERT_TRUE(fp32.isSubnormal()); + FloatingPoint mfp32 = FloatingPoint::makeMaxSubnormal(size32, false); + ASSERT_TRUE(mfp32.isSubnormal()); + + FloatingPoint fp64 = FloatingPoint::makeMaxSubnormal(size64, true); + ASSERT_TRUE(fp64.isSubnormal()); + FloatingPoint mfp64 = FloatingPoint::makeMaxSubnormal(size64, false); + ASSERT_TRUE(mfp64.isSubnormal()); + + FloatingPoint fp128 = FloatingPoint::makeMaxSubnormal(size128, true); + ASSERT_TRUE(fp128.isSubnormal()); + FloatingPoint mfp128 = FloatingPoint::makeMaxSubnormal(size128, false); + ASSERT_TRUE(mfp128.isSubnormal()); +} + +TEST_F(TestUtilBlackFloatingPoint, makeMinNormal) +{ + FloatingPointSize size16(5, 11); + FloatingPointSize size32(8, 24); + FloatingPointSize size64(11, 53); + FloatingPointSize size128(15, 113); + + FloatingPoint fp16 = FloatingPoint::makeMinNormal(size16, true); + ASSERT_TRUE(fp16.isNormal()); + FloatingPoint mfp16 = FloatingPoint::makeMinNormal(size16, false); + ASSERT_TRUE(mfp16.isNormal()); + + FloatingPoint fp32 = FloatingPoint::makeMinNormal(size32, true); + ASSERT_TRUE(fp32.isNormal()); + FloatingPoint mfp32 = FloatingPoint::makeMinNormal(size32, false); + ASSERT_TRUE(mfp32.isNormal()); + + FloatingPoint fp64 = FloatingPoint::makeMinNormal(size64, true); + ASSERT_TRUE(fp64.isNormal()); + FloatingPoint mfp64 = FloatingPoint::makeMinNormal(size64, false); + ASSERT_TRUE(mfp64.isNormal()); + + FloatingPoint fp128 = FloatingPoint::makeMinNormal(size128, true); + ASSERT_TRUE(fp128.isNormal()); + FloatingPoint mfp128 = FloatingPoint::makeMinNormal(size128, false); + ASSERT_TRUE(mfp128.isNormal()); +} + +TEST_F(TestUtilBlackFloatingPoint, makeMaxNormal) +{ + FloatingPointSize size16(5, 11); + FloatingPointSize size32(8, 24); + FloatingPointSize size64(11, 53); + FloatingPointSize size128(15, 113); + + FloatingPoint fp16 = FloatingPoint::makeMaxNormal(size16, true); + ASSERT_TRUE(fp16.isNormal()); + FloatingPoint mfp16 = FloatingPoint::makeMaxNormal(size16, false); + ASSERT_TRUE(mfp16.isNormal()); + + FloatingPoint fp32 = FloatingPoint::makeMaxNormal(size32, true); + ASSERT_TRUE(fp32.isNormal()); + FloatingPoint mfp32 = FloatingPoint::makeMaxNormal(size32, false); + ASSERT_TRUE(mfp32.isNormal()); + + FloatingPoint fp64 = FloatingPoint::makeMaxNormal(size64, true); + ASSERT_TRUE(fp64.isNormal()); + FloatingPoint mfp64 = FloatingPoint::makeMaxNormal(size64, false); + ASSERT_TRUE(mfp64.isNormal()); + + FloatingPoint fp128 = FloatingPoint::makeMaxNormal(size128, true); + ASSERT_TRUE(fp128.isNormal()); + FloatingPoint mfp128 = FloatingPoint::makeMaxNormal(size128, false); + ASSERT_TRUE(mfp128.isNormal()); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/util/floatingpoint_black.h b/test/unit/util/floatingpoint_black.h deleted file mode 100644 index 4517bcafc..000000000 --- a/test/unit/util/floatingpoint_black.h +++ /dev/null @@ -1,141 +0,0 @@ -/********************* */ -/*! \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 - -#include "util/floatingpoint.h" - -using namespace CVC4; - -class FloatingPointBlack : public CxxTest::TestSuite -{ - public: - void testMakeMinSubnormal(); - void testMakeMaxSubnormal(); - void testMakeMinNormal(); - void testMakeMaxNormal(); -}; - -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()); -} - -void FloatingPointBlack::testMakeMinNormal() -{ - FloatingPointSize size16(5, 11); - FloatingPointSize size32(8, 24); - FloatingPointSize size64(11, 53); - FloatingPointSize size128(15, 113); - - FloatingPoint fp16 = FloatingPoint::makeMinNormal(size16, true); - TS_ASSERT(fp16.isNormal()); - FloatingPoint mfp16 = FloatingPoint::makeMinNormal(size16, false); - TS_ASSERT(mfp16.isNormal()); - - FloatingPoint fp32 = FloatingPoint::makeMinNormal(size32, true); - TS_ASSERT(fp32.isNormal()); - FloatingPoint mfp32 = FloatingPoint::makeMinNormal(size32, false); - TS_ASSERT(mfp32.isNormal()); - - FloatingPoint fp64 = FloatingPoint::makeMinNormal(size64, true); - TS_ASSERT(fp64.isNormal()); - FloatingPoint mfp64 = FloatingPoint::makeMinNormal(size64, false); - TS_ASSERT(mfp64.isNormal()); - - FloatingPoint fp128 = FloatingPoint::makeMinNormal(size128, true); - TS_ASSERT(fp128.isNormal()); - FloatingPoint mfp128 = FloatingPoint::makeMinNormal(size128, false); - TS_ASSERT(mfp128.isNormal()); -} - -void FloatingPointBlack::testMakeMaxNormal() -{ - FloatingPointSize size16(5, 11); - FloatingPointSize size32(8, 24); - FloatingPointSize size64(11, 53); - FloatingPointSize size128(15, 113); - - FloatingPoint fp16 = FloatingPoint::makeMaxNormal(size16, true); - TS_ASSERT(fp16.isNormal()); - FloatingPoint mfp16 = FloatingPoint::makeMaxNormal(size16, false); - TS_ASSERT(mfp16.isNormal()); - - FloatingPoint fp32 = FloatingPoint::makeMaxNormal(size32, true); - TS_ASSERT(fp32.isNormal()); - FloatingPoint mfp32 = FloatingPoint::makeMaxNormal(size32, false); - TS_ASSERT(mfp32.isNormal()); - - FloatingPoint fp64 = FloatingPoint::makeMaxNormal(size64, true); - TS_ASSERT(fp64.isNormal()); - FloatingPoint mfp64 = FloatingPoint::makeMaxNormal(size64, false); - TS_ASSERT(mfp64.isNormal()); - - FloatingPoint fp128 = FloatingPoint::makeMaxNormal(size128, true); - TS_ASSERT(fp128.isNormal()); - FloatingPoint mfp128 = FloatingPoint::makeMaxNormal(size128, false); - TS_ASSERT(mfp128.isNormal()); -}