From: Martin Date: Tue, 19 Sep 2017 00:14:05 +0000 (+0100) Subject: Floating point symfpu support (#1103) X-Git-Tag: cvc5-1.0.0~5632 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=61a846a4998be697867292924454893271eb6496;p=cvc5.git Floating point symfpu support (#1103) - Update the parser to the new constant construction - Fix the problem with parsing +/-zero and remove some dead code - Extend the interface for literal floating-point values. - Add a constructor so that a parameteric operator structure can be created from a type - Add constructors so parametric operator constants can be easily converted - Update SMT2 printing so that it uses the informative output --- diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 92f6b36d8..2aa85fbe3 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2271,17 +2271,25 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } } | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - +INFINITY)); } + { expr = MK_CONST(FloatingPoint::makeInf(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)), + false)); } | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - -INFINITY)); } + { expr = MK_CONST(FloatingPoint::makeInf(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)), + true)); } | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - NAN)); } + { expr = MK_CONST(FloatingPoint::makeNaN(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)))); } + + | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL + { expr = MK_CONST(FloatingPoint::makeZero(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)), + false)); } + | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL + { expr = MK_CONST(FloatingPoint::makeZero(FloatingPointSize(AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb)), + true)); } // NOTE: Theory parametric constants go here ) @@ -2505,26 +2513,6 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind] "bv2nat and int2bv are not part of SMT-LIB, and aren't available " "in SMT-LIB strict compliance mode"); } } - | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - +INFINITY)); } - | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - -INFINITY)); } - | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - NAN)); } - | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - +0.0)); } - | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb), - -0.0)); } | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL { op = MK_CONST(FloatingPointToFPGeneric( AntlrInput::tokenToUnsigned($eb), diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2f2a6ff18..ae65311de 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -202,7 +202,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; } case kind::CONST_FLOATINGPOINT: - out << n.getConst().getLiteral(); + out << n.getConst(); break; case kind::CONST_ROUNDINGMODE: switch (n.getConst()) { diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index 8c446d9d2..fe90279ec 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -36,4 +36,307 @@ void FloatingPointLiteral::unfinished (void) const { Unimplemented("Floating-point literals not yet implemented."); } + FloatingPoint::FloatingPoint (unsigned e, unsigned s, const BitVector &bv) : + fpl(e,s,0.0), + t(e,s) {} + + + static FloatingPointLiteral constructorHelperBitVector (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) { + if (signedBV) { + return FloatingPointLiteral(2,2,0.0); + } else { + return FloatingPointLiteral(2,2,0.0); + } + Unreachable("Constructor helper broken"); + } + + FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) : + fpl(constructorHelperBitVector(ct, rm, bv, signedBV)), + t(ct) {} + + + static FloatingPointLiteral constructorHelperRational (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &ri) { + Rational r(ri); + Rational two(2,1); + + if (r.isZero()) { + return FloatingPointLiteral(2,2,0.0); + } else { + //int negative = (r.sgn() < 0) ? 1 : 0; + r = r.abs(); + + // Compute the exponent + Integer exp(0U); + Integer inc(1U); + Rational working(1,1); + + if (r == working) { + + } else if ( r < working ) { + while (r < working) { + exp -= inc; + working /= two; + } + } else { + while (r >= working) { + exp += inc; + working *= two; + } + exp -= inc; + working /= two; + } + + Assert(working <= r); + Assert(r < working * two); + + // Work out the number of bits required to represent the exponent for a normal number + unsigned expBits = 2; // No point starting with an invalid amount + + Integer doubleInt(2); + if (exp.strictlyPositive()) { + Integer representable(4); // 1 more than exactly representable with expBits + while (representable <= exp) {// hence <= + representable *= doubleInt; + ++expBits; + } + } else if (exp.strictlyNegative()) { + Integer representable(-4); // Exactly representable with expBits + sign + // but -2^n and -(2^n - 1) are both subnormal + while ((representable + doubleInt) > exp) { + representable *= doubleInt; + ++expBits; + } + } + ++expBits; // To allow for sign + + BitVector exactExp(expBits, exp); + + + + // Compute the significand. + unsigned sigBits = ct.significand() + 2; // guard and sticky bits + BitVector sig(sigBits, 0U); + BitVector one(sigBits, 1U); + Rational workingSig(0,1); + for (unsigned i = 0; i < sigBits - 1; ++i) { + Rational mid(workingSig + working); + + if (mid <= r) { + sig = sig | one; + workingSig = mid; + } + + sig = sig.leftShift(one); + working /= two; + } + + // Compute the sticky bit + Rational remainder(r - workingSig); + Assert(Rational(0,1) <= remainder); + + if (!remainder.isZero()) { + sig = sig | one; + } + + // Build an exact float + FloatingPointSize exactFormat(expBits, sigBits); + + // A small subtlety... if the format has expBits the unpacked format + // may have more to allow subnormals to be normalised. + // Thus... + Unreachable("no concrete implementation of FloatingPointLiteral"); + } + Unreachable("Constructor helper broken"); + } + + FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &r) : + fpl(constructorHelperRational(ct, rm, r)), + t(ct) {} + + + FloatingPoint FloatingPoint::makeNaN (const FloatingPointSize &t) { + return FloatingPoint(2, 2, BitVector(4U,0U)); + } + + FloatingPoint FloatingPoint::makeInf (const FloatingPointSize &t, bool sign) { + return FloatingPoint(2, 2, BitVector(4U,0U)); + } + + FloatingPoint FloatingPoint::makeZero (const FloatingPointSize &t, bool sign) { + return FloatingPoint(2, 2, BitVector(4U,0U)); + } + + + /* Operations implemented using symfpu */ + FloatingPoint FloatingPoint::absolute (void) const { + return *this; + } + + FloatingPoint FloatingPoint::negate (void) const { + return *this; + } + + FloatingPoint FloatingPoint::plus (const RoundingMode &rm, const FloatingPoint &arg) const { + Assert(this->t == arg.t); + return *this; + } + + FloatingPoint FloatingPoint::sub (const RoundingMode &rm, const FloatingPoint &arg) const { + Assert(this->t == arg.t); + return *this; + } + + FloatingPoint FloatingPoint::mult (const RoundingMode &rm, const FloatingPoint &arg) const { + Assert(this->t == arg.t); + return *this; + } + + FloatingPoint FloatingPoint::fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const { + Assert(this->t == arg1.t); + Assert(this->t == arg2.t); + return *this; + } + + FloatingPoint FloatingPoint::div (const RoundingMode &rm, const FloatingPoint &arg) const { + Assert(this->t == arg.t); + return *this; + } + + FloatingPoint FloatingPoint::sqrt (const RoundingMode &rm) const { + return *this; + } + + FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const { + return *this; + } + + FloatingPoint FloatingPoint::rem (const FloatingPoint &arg) const { + Assert(this->t == arg.t); + return *this; + } + + FloatingPoint FloatingPoint::maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const { + Assert(this->t == arg.t); + return *this; + } + + FloatingPoint FloatingPoint::minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const { + Assert(this->t == arg.t); + return *this; + } + + FloatingPoint::PartialFloatingPoint FloatingPoint::max (const FloatingPoint &arg) const { + FloatingPoint tmp(maxTotal(arg, true)); + return PartialFloatingPoint(tmp, tmp == maxTotal(arg, false)); + } + + FloatingPoint::PartialFloatingPoint FloatingPoint::min (const FloatingPoint &arg) const { + FloatingPoint tmp(minTotal(arg, true)); + return PartialFloatingPoint(tmp, tmp == minTotal(arg, false)); + } + + bool FloatingPoint::operator ==(const FloatingPoint& fp) const { + return ( (t == fp.t) ); + } + + bool FloatingPoint::operator <= (const FloatingPoint &arg) const { + Assert(this->t == arg.t); + return false; + } + + bool FloatingPoint::operator < (const FloatingPoint &arg) const { + Assert(this->t == arg.t); + return false; + } + + bool FloatingPoint::isNormal (void) const { + return false; + } + + bool FloatingPoint::isSubnormal (void) const { + return false; + } + + bool FloatingPoint::isZero (void) const { + return false; + } + + bool FloatingPoint::isInfinite (void) const { + return false; + } + + bool FloatingPoint::isNaN (void) const { + return false; + } + + bool FloatingPoint::isNegative (void) const { + return false; + } + + bool FloatingPoint::isPositive (void) const { + return false; + } + + FloatingPoint FloatingPoint::convert (const FloatingPointSize &target, const RoundingMode &rm) const { + return *this; + } + + BitVector FloatingPoint::convertToBVTotal (BitVectorSize width, const RoundingMode &rm, bool signedBV, BitVector undefinedCase) const { + if (signedBV) + return undefinedCase; + else + return undefinedCase; + } + + Rational FloatingPoint::convertToRationalTotal (Rational undefinedCase) const { + PartialRational p(convertToRational()); + + return p.second ? p.first : undefinedCase; + } + + FloatingPoint::PartialBitVector FloatingPoint::convertToBV (BitVectorSize width, const RoundingMode &rm, bool signedBV) const { + BitVector tmp(convertToBVTotal (width, rm, signedBV, BitVector(width, 0U))); + BitVector confirm(convertToBVTotal (width, rm, signedBV, BitVector(width, 1U))); + + return PartialBitVector(tmp, tmp == confirm); + } + + FloatingPoint::PartialRational FloatingPoint::convertToRational (void) const { + if (this->isNaN() || this->isInfinite()) { + return PartialRational(Rational(0U, 1U), false); + } + if (this->isZero()) { + return PartialRational(Rational(0U, 1U), true); + + } else { + + Integer sign(0); + Integer exp(0); + Integer significand(0); + Integer signedSignificand(sign * significand); + + // Only have pow(uint32_t) so we should check this. + Assert(this->t.significand() <= 32); + + if (!(exp.strictlyNegative())) { + Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt())); + return PartialRational(Rational(r), true); + } else { + Integer one(1U); + Integer q(one.multiplyByPow2((-exp).toUnsignedInt())); + Rational r(signedSignificand, q); + return PartialRational(r, true); + } + } + + Unreachable("Convert float literal to real broken."); + } + + BitVector FloatingPoint::pack (void) const { + BitVector bv(4u,0u); + return bv; + } + + + }/* CVC4 namespace */ diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index b3be84f13..fa4573123 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -23,6 +23,7 @@ #include #include "util/bitvector.h" +#include "util/rational.h" namespace CVC4 { // Inline these! @@ -127,25 +128,83 @@ namespace CVC4 { public : FloatingPointSize t; - FloatingPoint (unsigned e, unsigned s, double d) : fpl(e,s,d), t(e,s) {} - FloatingPoint (unsigned e, unsigned s, const std::string &bitString) : fpl(e,s,bitString), t(e,s) {} + FloatingPoint (unsigned e, unsigned s, const BitVector &bv); + FloatingPoint (const FloatingPointSize &oldt, const FloatingPointLiteral &oldfpl) : fpl(oldfpl), t(oldt) {} FloatingPoint (const FloatingPoint &fp) : fpl(fp.fpl), t(fp.t) {} + FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV); + FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &r); - bool operator ==(const FloatingPoint& fp) const { - return ( (t == fp.t) && fpl == fp.fpl ); - } + + static FloatingPoint makeNaN (const FloatingPointSize &t); + static FloatingPoint makeInf (const FloatingPointSize &t, bool sign); + static FloatingPoint makeZero (const FloatingPointSize &t, bool sign); const FloatingPointLiteral & getLiteral (void) const { return this->fpl; } + // Gives the corresponding IEEE-754 transfer format + BitVector pack (void) const; + + + FloatingPoint absolute (void) const; + FloatingPoint negate (void) const; + FloatingPoint plus (const RoundingMode &rm, const FloatingPoint &arg) const; + FloatingPoint sub (const RoundingMode &rm, const FloatingPoint &arg) const; + FloatingPoint mult (const RoundingMode &rm, const FloatingPoint &arg) const; + FloatingPoint div (const RoundingMode &rm, const FloatingPoint &arg) const; + FloatingPoint fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const; + FloatingPoint sqrt (const RoundingMode &rm) const; + FloatingPoint rti (const RoundingMode &rm) const; + FloatingPoint rem (const FloatingPoint &arg) const; + + // zeroCase is whether the left or right is returned in the case of min/max(-0,+0) or (+0,-0) + FloatingPoint maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const; + FloatingPoint minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const; + + // These detect when the answer is defined + typedef std::pair PartialFloatingPoint; + + PartialFloatingPoint max (const FloatingPoint &arg) const; + PartialFloatingPoint min (const FloatingPoint &arg) const; + + + bool operator ==(const FloatingPoint& fp) const; + bool operator <= (const FloatingPoint &arg) const; + bool operator < (const FloatingPoint &arg) const; + + bool isNormal (void) const; + bool isSubnormal (void) const; + bool isZero (void) const; + bool isInfinite (void) const; + bool isNaN (void) const; + bool isNegative (void) const; + bool isPositive (void) const; + + FloatingPoint convert (const FloatingPointSize &target, const RoundingMode &rm) const; + + // These require a value to return in the undefined case + BitVector convertToBVTotal (BitVectorSize width, const RoundingMode &rm, + bool signedBV, BitVector undefinedCase) const; + Rational convertToRationalTotal (Rational undefinedCase) const; + + // These detect when the answer is defined + typedef std::pair PartialBitVector; + typedef std::pair PartialRational; + + PartialBitVector convertToBV (BitVectorSize width, const RoundingMode &rm, + bool signedBV) const; + PartialRational convertToRational (void) const; + }; /* class FloatingPoint */ struct CVC4_PUBLIC FloatingPointHashFunction { - inline size_t operator() (const FloatingPoint& fp) const { - FloatingPointSizeHashFunction h; - return h(fp.t) ^ fp.getLiteral().hash(); + size_t operator() (const FloatingPoint& fp) const { + FloatingPointSizeHashFunction fpshf; + BitVectorHashFunction bvhf; + + return fpshf(fp.t) ^ bvhf(fp.pack()); } }; /* struct FloatingPointHashFunction */ @@ -158,6 +217,8 @@ namespace CVC4 { FloatingPointConvertSort (unsigned _e, unsigned _s) : t(_e,_s) {} + FloatingPointConvertSort (const FloatingPointSize &fps) + : t(fps) {} bool operator ==(const FloatingPointConvertSort& fpcs) const { return t == fpcs.t; @@ -171,22 +232,39 @@ namespace CVC4 { */ class CVC4_PUBLIC FloatingPointToFPIEEEBitVector : public FloatingPointConvertSort { - public : FloatingPointToFPIEEEBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + public : + FloatingPointToFPIEEEBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + FloatingPointToFPIEEEBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} }; + class CVC4_PUBLIC FloatingPointToFPFloatingPoint : public FloatingPointConvertSort { - public : FloatingPointToFPFloatingPoint (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + public : + FloatingPointToFPFloatingPoint (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + FloatingPointToFPFloatingPoint (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} }; + class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort { - public : FloatingPointToFPReal (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + public : + FloatingPointToFPReal (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + FloatingPointToFPReal (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} }; + class CVC4_PUBLIC FloatingPointToFPSignedBitVector : public FloatingPointConvertSort { - public : FloatingPointToFPSignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + public : + FloatingPointToFPSignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + FloatingPointToFPSignedBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} }; + class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort { - public : FloatingPointToFPUnsignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + public : + FloatingPointToFPUnsignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + FloatingPointToFPUnsignedBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} }; + class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort { - public : FloatingPointToFPGeneric (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + public : + FloatingPointToFPGeneric (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} + FloatingPointToFPGeneric (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} }; @@ -215,14 +293,26 @@ namespace CVC4 { FloatingPointToBV (unsigned s) : bvs(s) {} + FloatingPointToBV (const FloatingPointToBV &old) : bvs(old.bvs) {} + FloatingPointToBV (const BitVectorSize &old) : bvs(old) {} operator unsigned () const { return bvs; } }; class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV { public : FloatingPointToUBV (unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToUBV (const FloatingPointToBV &old) : FloatingPointToBV(old) {} }; class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV { public : FloatingPointToSBV (unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToSBV (const FloatingPointToBV &old) : FloatingPointToBV(old) {} + }; + class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV { + public : FloatingPointToUBVTotal (unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToUBVTotal (const FloatingPointToBV &old) : FloatingPointToBV(old) {} + }; + class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV { + public : FloatingPointToSBVTotal (unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToSBVTotal (const FloatingPointToBV &old) : FloatingPointToBV(old) {} }; @@ -235,16 +325,28 @@ namespace CVC4 { }; /* struct FloatingPointToBVHashFunction */ - + // It is not possible to pack a number without a size to pack to, + // thus it is difficult to implement this in a sensible way. Use + // FloatingPoint instead... + /* inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) CVC4_PUBLIC; inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) { - fp.unfinished(); - return os; + return os << "FloatingPointLiteral"; } + */ inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC; inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) { - return os << fp.getLiteral(); + 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 FloatingPointSize& fps) CVC4_PUBLIC;