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.

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 64ce22f9f7260ccbb500aa7fb1e28ee5449bae5f..3c8e706c0e2c7f1d398dc9bbf266d809900b5085 100644 (file)
--- 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 fb2c3f29f2079d52d19b0a16c98b225713421c13..def94d62a2776f735c5cb63062124d78b887d745 100644 (file)
--- 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;