1 files changed, 13 insertions, 13 deletions
diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in
index bac0fbd59..d38cae5fa 100644
--- a/src/util/floatingpoint.h.in
+++ b/src/util/floatingpoint.h.in
@@ -2,10 +2,10 @@
 /*! \file floatingpoint.h.in
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Martin Brain, Tim King
+ **   Martin Brain, Haniel Barbosa, Tim King
  ** Copyright (c) 2013  University of Oxford
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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;