FloatingPoint: Add utility functions for largest and smallest subnormal. (#5166)

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());
+}