From 3a750bb1c4fa455e7faadf7b0f26e28eee342342 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 09:48:54 -0600
Subject: [PATCH] Add utility to access how to print floating point (#8141)

This makes the code for printing a floating point based on its BV components accessible as a utility.

This is required for proper printing of FP constants in LFSC.
---
 src/util/floatingpoint.cpp | 20 ++++++++++++++------
 src/util/floatingpoint.h   |  7 +++++++
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 64ce22f9f..3c8e706c0 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -458,19 +458,27 @@ FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const
 
 BitVector FloatingPoint::pack(void) const { return d_fpl->pack(); }
 
-std::string FloatingPoint::toString(bool printAsIndexed) const
+void FloatingPoint::getIEEEBitvectors(BitVector& sign,
+                                      BitVector& exp,
+                                      BitVector& sig) const
 {
-  std::string str;
-  // retrive BV value
+  // retrieve BV value
   BitVector bv(pack());
   uint32_t largestSignificandBit =
       getSize().significandWidth() - 2;  // -1 for -inclusive, -1 for hidden
   uint32_t largestExponentBit =
       (getSize().exponentWidth() - 1) + (largestSignificandBit + 1);
+  sign = bv.extract(largestExponentBit + 1, largestExponentBit + 1);
+  exp = bv.extract(largestExponentBit, largestSignificandBit + 1);
+  sig = bv.extract(largestSignificandBit, 0);
+}
+
+std::string FloatingPoint::toString(bool printAsIndexed) const
+{
+  std::string str;
+  // retrive BV value
   BitVector v[3];
-  v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1);
-  v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1);
-  v[2] = bv.extract(largestSignificandBit, 0);
+  getIEEEBitvectors(v[0], v[1], v[2]);
   str.append("(fp ");
   for (uint32_t i = 0; i < 3; ++i)
   {
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index fb2c3f29f..def94d62a 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -147,6 +147,13 @@ class FloatingPoint
    */
   std::string toString(bool printAsIndexed = false) const;
 
+  /**
+   * Get the IEEE bit-vector representation of this floating-point value.
+   * Stores the sign bit in `sign`, the exponent in `exp` and the significand
+   * in `sig`.
+   */
+  void getIEEEBitvectors(BitVector& sign, BitVector& exp, BitVector& sig) const;
+
   /** Return the packed (IEEE-754) representation of this floating-point. */
   BitVector pack(void) const;
 
-- 
2.30.2