diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-06-05 09:54:51 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-05 09:54:51 -0300 |
commit | 80b0795702e71d54ed7c17ba809eebde628eb516 (patch) | |
tree | d9950f742d4763b520185d4f27aa666d67509429 /src/util/floatingpoint.h.in | |
parent | 60746dc3ac7806475b5b6dab03123df024bf613e (diff) |
Printing FP values as binary or indexed BVs according to option (#4554)
Diffstat (limited to 'src/util/floatingpoint.h.in')
-rw-r--r-- | src/util/floatingpoint.h.in | 22 |
1 files changed, 11 insertions, 11 deletions
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; |