From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 15:48:54 +0000 (-0600)
Subject: Add utility to access how to print floating point (#8141)
X-Git-Tag: cvc5-1.0.0~347
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3a750bb1c4fa455e7faadf7b0f26e28eee342342;p=cvc5.git

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 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;