From 4c2c2de951c52ef48704dbffe7ec5848917f1398 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 1 Oct 2020 11:29:39 -0700
Subject: FloatingPoint: Add utility functions for largest and smallest normal.
 (#5174)

---
 src/util/floatingpoint.cpp  | 19 +++++++++++++++++++
 src/util/floatingpoint.h.in | 14 ++++++++++++++
 2 files changed, 33 insertions(+)

(limited to 'src/util')

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; }
 
-- 
cgit v1.2.3