Printing FP values as binary or indexed BVs according to option (#4554)

2 files changed, 47 insertions, 12 deletions

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index f5545f73c..2c2816515 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -959,6 +959,41 @@ static FloatingPointLiteral constructorHelperBitVector(
     return bv;
   }
 
-
+std::string FloatingPoint::toString(bool printAsIndexed) const
+{
+  std::string str;
+  // retrive BV value
+  BitVector bv(pack());
+  unsigned largestSignificandBit =
+      t.significand() - 2;  // -1 for -inclusive, -1 for hidden
+  unsigned largestExponentBit =
+      (t.exponent() - 1) + (largestSignificandBit + 1);
+  BitVector v[3];
+  v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1);
+  v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1);
+  v[2] = bv.extract(largestSignificandBit, 0);
+  str.append("(fp ");
+  for (unsigned i = 0; i < 3; ++i)
+  {
+    if (printAsIndexed)
+    {
+      str.append("(_ bv");
+      str.append(v[i].getValue().toString());
+      str.append(" ");
+      str.append(std::to_string(v[i].getSize()));
+      str.append(")");
+    }
+    else
+    {
+      str.append("#b");
+      str.append(v[i].toString());
+    }
+    if (i < 2)
+    {
+      str.append(" ");
+    }
+  }
+  return str;
+}
 
 }/* CVC4 namespace */
diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in
index bac0fbd59..11aa660f5 100644
--- a/src/util/floatingpoint.h.in
+++ b/src/util/floatingpoint.h.in
@@ -333,6 +333,13 @@ namespace CVC4 {
       return this->fpl;
     }
 
+    /* Return string representation.
+     *
+     * If printAsIndexed is true then it prints
+     * the bit-vector components of the FP value as indexed symbols, otherwise
+     * in binary notation. */
+    std::string toString(bool printAsIndexed = false) const;
+
     // Gives the corresponding IEEE-754 transfer format
     BitVector pack (void) const;
 
@@ -526,17 +533,10 @@ namespace CVC4 {
   */
 
   inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC;
-  inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) {
-    BitVector bv(fp.pack());
-
-    unsigned largestSignificandBit = fp.t.significand() - 2; // -1 for -inclusive, -1 for hidden
-    unsigned largestExponentBit = (fp.t.exponent() - 1) + (largestSignificandBit + 1);
-
-    return os
-      << "(fp #b" << bv.extract(largestExponentBit + 1, largestExponentBit + 1)
-      << " #b" << bv.extract(largestExponentBit, largestSignificandBit + 1)
-      << " #b" << bv.extract(largestSignificandBit, 0)
-      << ")";
+  inline std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp)
+  {
+    // print in binary notation
+    return os << fp.toString();
   }
 
   inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) CVC4_PUBLIC;