FloatingPoint: Add utility functions for largest and smallest normal. (#5174)

2 files changed, 33 insertions, 0 deletions

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 7693d37cb..c84779be0 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -695,6 +695,25 @@ FloatingPoint FloatingPoint::makeMaxSubnormal(const FloatingPointSize& size,
   return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
 }
 
+FloatingPoint FloatingPoint::makeMinNormal(const FloatingPointSize& size,
+                                           bool sign)
+{
+  BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
+  BitVector bvexp = BitVector::mkOne(size.packedExponentWidth());
+  BitVector bvsig = BitVector::mkZero(size.packedSignificandWidth());
+  return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
+}
+
+FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size,
+                                           bool sign)
+{
+  BitVector bvsign = sign ? BitVector::mkOne(1) : BitVector::mkZero(1);
+  BitVector bvexp =
+      BitVector::mkOnes(size.packedExponentWidth()).setBit(0, false);
+  BitVector bvsig = BitVector::mkOnes(size.packedSignificandWidth());
+  return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig));
+}
+
   /* Operations implemented using symfpu */
   FloatingPoint FloatingPoint::absolute (void) const {
 #ifdef CVC4_USE_SYMFPU
diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in
index 637f01104..9e78c20c0 100644
--- a/src/util/floatingpoint.h.in
+++ b/src/util/floatingpoint.h.in
@@ -368,6 +368,20 @@ namespace CVC4 {
      */
     static FloatingPoint makeMaxSubnormal(const FloatingPointSize& size,
                                           bool sign);
+    /**
+     * Create the smallest normal FP value of given size.
+     * t:    The FP size (format).
+     * sign: True for positive sign, false otherwise.
+     */
+    static FloatingPoint makeMinNormal(const FloatingPointSize& size,
+                                       bool sign);
+    /**
+     * Create the largest normal FP value of given size.
+     * t:    The FP size (format).
+     * sign: True for positive sign, false otherwise.
+     */
+    static FloatingPoint makeMaxNormal(const FloatingPointSize& size,
+                                          bool sign);
 
     const FloatingPointLiteral& getLiteral(void) const { return this->fpl; }