diff options
Diffstat (limited to 'src/util/floatingpoint.cpp')
| -rw-r--r-- | src/util/floatingpoint.cpp | 442 |
1 files changed, 269 insertions, 173 deletions
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index ae6197791..4e4b076f0 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -17,12 +17,15 @@ **/ #include "util/floatingpoint.h" -#include "base/check.h" -#include "util/integer.h" #include <math.h> + #include <limits> +#include "base/check.h" +#include "util/integer.h" +#include "util/symfpu_literal.h" + #ifdef CVC4_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" @@ -40,6 +43,8 @@ #include "symfpu/utils/properties.h" #endif +/* -------------------------------------------------------------------------- */ + #ifdef CVC4_USE_SYMFPU namespace symfpu { @@ -64,24 +69,41 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv); } #endif +/* -------------------------------------------------------------------------- */ + namespace CVC4 { -#ifndef CVC4_USE_SYMFPU -void FloatingPointLiteral::unfinished(void) const +/* -------------------------------------------------------------------------- */ + +uint32_t FloatingPoint::getUnpackedExponentWidth(FloatingPointSize& size) { - Unimplemented() << "Floating-point literals not yet implemented."; +#ifdef CVC4_USE_SYMFPU + return SymFPUUnpackedFloatLiteral::exponentWidth(size); +#else + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return 2; +#endif } + +uint32_t FloatingPoint::getUnpackedSignificandWidth(FloatingPointSize& size) +{ +#ifdef CVC4_USE_SYMFPU + return SymFPUUnpackedFloatLiteral::significandWidth(size); +#else + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return 2; #endif +} FloatingPoint::FloatingPoint(uint32_t d_exp_size, uint32_t d_sig_size, const BitVector& bv) : d_fp_size(d_exp_size, d_sig_size), #ifdef CVC4_USE_SYMFPU - d_fpl(symfpu::unpack<symfpuLiteral::traits>( - symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv)) + d_fpl(new FloatingPointLiteral(symfpu::unpack<symfpuLiteral::traits>( + symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv))) #else - d_fpl(d_exp_size, d_sig_size, 0.0) + d_fpl(new FloatingPointLiteral(d_exp_size, d_sig_size, 0.0)) #endif { } @@ -89,23 +111,25 @@ FloatingPoint::FloatingPoint(uint32_t d_exp_size, FloatingPoint::FloatingPoint(const FloatingPointSize& size, const BitVector& bv) : d_fp_size(size), #ifdef CVC4_USE_SYMFPU - d_fpl(symfpu::unpack<symfpuLiteral::traits>(size, bv)) + d_fpl(new FloatingPointLiteral( + symfpu::unpack<symfpuLiteral::traits>(size, bv))) #else - d_fpl(size.exponentWidth(), size.significandWidth(), 0.0) + d_fpl(new FloatingPointLiteral( + size.exponentWidth(), size.significandWidth(), 0.0)) #endif { } -static FloatingPointLiteral constructorHelperBitVector( - const FloatingPointSize& size, - const RoundingMode& rm, - const BitVector& bv, - bool signedBV) +FloatingPoint::FloatingPoint(const FloatingPointSize& size, + const RoundingMode& rm, + const BitVector& bv, + bool signedBV) + : d_fp_size(size) { #ifdef CVC4_USE_SYMFPU if (signedBV) { - return FloatingPointLiteral( + d_fpl = new FloatingPointLiteral( symfpu::convertSBVToFloat<symfpuLiteral::traits>( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), @@ -113,154 +137,174 @@ static FloatingPointLiteral constructorHelperBitVector( } else { - return FloatingPointLiteral( + d_fpl = new FloatingPointLiteral( symfpu::convertUBVToFloat<symfpuLiteral::traits>( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), symfpuLiteral::CVC4UnsignedBitVector(bv))); } #else - return FloatingPointLiteral(2, 2, 0.0); + d_fpl = new FloatingPointLiteral(2, 2, 0.0); #endif - Unreachable() << "Constructor helper broken"; } -FloatingPoint::FloatingPoint(const FloatingPointSize& size, - const RoundingMode& rm, - const BitVector& bv, - bool signedBV) - : d_fp_size(size), d_fpl(constructorHelperBitVector(size, rm, bv, signedBV)) +FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size, + const FloatingPointLiteral* fpl) + : d_fp_size(fp_size) +{ + d_fpl = new FloatingPointLiteral(*fpl); +} + +FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size) { + d_fpl = new FloatingPointLiteral(*fp.d_fpl); } -static FloatingPointLiteral constructorHelperRational( - const FloatingPointSize& size, const RoundingMode& rm, const Rational& ri) +FloatingPoint::FloatingPoint(const FloatingPointSize& size, + const RoundingMode& rm, + const Rational& r) + : d_fp_size(size) { - Rational r(ri); Rational two(2, 1); if (r.isZero()) { #ifdef CVC4_USE_SYMFPU - return FloatingPointLiteral::makeZero( - size, false); // In keeping with the SMT-LIB standard + // In keeping with the SMT-LIB standard + d_fpl = new FloatingPointLiteral( + SymFPUUnpackedFloatLiteral::makeZero(size, false)); #else - return FloatingPointLiteral(2,2,0.0); + d_fpl = new FloatingPointLiteral(2, 2, 0.0); #endif - } else { + } + else + { #ifdef CVC4_USE_SYMFPU - uint32_t negative = (r.sgn() < 0) ? 1 : 0; + uint32_t negative = (r.sgn() < 0) ? 1 : 0; #endif - r = r.abs(); - - // Compute the exponent - Integer exp(0U); - Integer inc(1U); - Rational working(1,1); + Rational rabs(r.abs()); - if (r == working) { + // Compute the exponent + Integer exp(0U); + Integer inc(1U); + Rational working(1, 1); - } else if ( r < working ) { - while (r < working) { - exp -= inc; - working /= two; - } - } else { - while (r >= working) { - exp += inc; - working *= two; - } - exp -= inc; - working /= two; + if (rabs != working) + { + if (rabs < working) + { + while (rabs < working) + { + 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 - uint32_t 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; - } + else + { + while (rabs >= working) + { + exp += inc; + working *= two; + } + exp -= inc; + working /= two; } - ++expBits; // To allow for sign + } + + Assert(working <= rabs); + Assert(rabs < working * two); - BitVector exactExp(expBits, exp); + // Work out the number of bits required to represent the exponent for a + // normal number + uint32_t expBits = 2; // No point starting with an invalid amount - // Compute the significand. - uint32_t sigBits = size.significandWidth() + 2; // guard and sticky bits - BitVector sig(sigBits, 0U); - BitVector one(sigBits, 1U); - Rational workingSig(0,1); - for (uint32_t i = 0; i < sigBits - 1; ++i) + Integer doubleInt(2); + if (exp.strictlyPositive()) + { + // 1 more than exactly representable with expBits + Integer representable(4); + 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) { - Rational mid(workingSig + working); + representable *= doubleInt; + ++expBits; + } + } + ++expBits; // To allow for sign - if (mid <= r) { - sig = sig | one; - workingSig = mid; - } + BitVector exactExp(expBits, exp); - sig = sig.leftShift(one); - working /= two; + // Compute the significand. + uint32_t sigBits = size.significandWidth() + 2; // guard and sticky bits + BitVector sig(sigBits, 0U); + BitVector one(sigBits, 1U); + Rational workingSig(0, 1); + for (uint32_t i = 0; i < sigBits - 1; ++i) + { + Rational mid(workingSig + working); + + if (mid <= rabs) + { + sig = sig | one; + workingSig = mid; } - // Compute the sticky bit - Rational remainder(r - workingSig); - Assert(Rational(0, 1) <= remainder); + sig = sig.leftShift(one); + working /= two; + } - if (!remainder.isZero()) { - sig = sig | one; - } + // Compute the sticky bit + Rational remainder(rabs - workingSig); + Assert(Rational(0, 1) <= remainder); + + if (!remainder.isZero()) + { + sig = sig | one; + } - // Build an exact float - FloatingPointSize exactFormat(expBits, sigBits); + // 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... + // A small subtlety... if the format has expBits the unpacked format + // may have more to allow subnormals to be normalised. + // Thus... #ifdef CVC4_USE_SYMFPU - uint32_t extension = - FloatingPointLiteral::exponentWidth(exactFormat) - expBits; + uint32_t extension = + SymFPUUnpackedFloatLiteral::exponentWidth(exactFormat) - expBits; - FloatingPointLiteral exactFloat( - negative, exactExp.signExtend(extension), sig); + FloatingPointLiteral exactFloat( + negative, exactExp.signExtend(extension), sig); - // Then cast... - FloatingPointLiteral rounded( - symfpu::convertFloatToFloat(exactFormat, size, rm, exactFloat)); - return rounded; + // Then cast... + d_fpl = new FloatingPointLiteral( + symfpu::convertFloatToFloat(exactFormat, size, rm, exactFloat.d_symuf)); #else - Unreachable() << "no concrete implementation of FloatingPointLiteral"; + Unreachable() << "no concrete implementation of FloatingPointLiteral"; #endif - } - Unreachable() << "Constructor helper broken"; + } } -FloatingPoint::FloatingPoint(const FloatingPointSize& size, - const RoundingMode& rm, - const Rational& r) - : d_fp_size(size), d_fpl(constructorHelperRational(size, rm, r)) +FloatingPoint::~FloatingPoint() { + delete d_fpl; + d_fpl = nullptr; } FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size) { #ifdef CVC4_USE_SYMFPU return FloatingPoint( - size, symfpu::unpackedFloat<symfpuLiteral::traits>::makeNaN(size)); + size, + new FloatingPointLiteral(SymFPUUnpackedFloatLiteral::makeNaN(size))); #else return FloatingPoint(2, 2, BitVector(4U, 0U)); #endif @@ -269,8 +313,9 @@ FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size) FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign) { #ifdef CVC4_USE_SYMFPU - return FloatingPoint( - size, symfpu::unpackedFloat<symfpuLiteral::traits>::makeInf(size, sign)); + return FloatingPoint(size, + new FloatingPointLiteral( + SymFPUUnpackedFloatLiteral::makeInf(size, sign))); #else return FloatingPoint(2, 2, BitVector(4U, 0U)); #endif @@ -279,8 +324,9 @@ FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign) FloatingPoint FloatingPoint::makeZero(const FloatingPointSize& size, bool sign) { #ifdef CVC4_USE_SYMFPU - return FloatingPoint( - size, symfpu::unpackedFloat<symfpuLiteral::traits>::makeZero(size, sign)); + return FloatingPoint(size, + new FloatingPointLiteral( + SymFPUUnpackedFloatLiteral::makeZero(size, sign))); #else return FloatingPoint(2, 2, BitVector(4U, 0U)); #endif @@ -328,7 +374,9 @@ FloatingPoint FloatingPoint::absolute(void) const { #ifdef CVC4_USE_SYMFPU return FloatingPoint( - d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_fpl)); + d_fp_size, + new FloatingPointLiteral( + symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf))); #else return *this; #endif @@ -337,8 +385,10 @@ FloatingPoint FloatingPoint::absolute(void) const FloatingPoint FloatingPoint::negate(void) const { #ifdef CVC4_USE_SYMFPU - return FloatingPoint(d_fp_size, - symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_fpl)); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral( + symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf))); #else return *this; #endif @@ -348,10 +398,11 @@ FloatingPoint FloatingPoint::plus(const RoundingMode& rm, const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::add<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl, arg.d_fpl, true)); + Assert(d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>( + d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, true))); #else return *this; #endif @@ -361,10 +412,11 @@ FloatingPoint FloatingPoint::sub(const RoundingMode& rm, const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::add<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl, arg.d_fpl, false)); + Assert(d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>( + d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, false))); #else return *this; #endif @@ -374,10 +426,11 @@ FloatingPoint FloatingPoint::mult(const RoundingMode& rm, const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); + Assert(d_fp_size == arg.d_fp_size); return FloatingPoint( d_fp_size, - symfpu::multiply<symfpuLiteral::traits>(d_fp_size, rm, d_fpl, arg.d_fpl)); + new FloatingPointLiteral(symfpu::multiply<symfpuLiteral::traits>( + d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf))); #else return *this; #endif @@ -388,11 +441,16 @@ FloatingPoint FloatingPoint::fma(const RoundingMode& rm, const FloatingPoint& arg2) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg1.d_fp_size); - Assert(this->d_fp_size == arg2.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::fma<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl, arg1.d_fpl, arg2.d_fpl)); + Assert(d_fp_size == arg1.d_fp_size); + Assert(d_fp_size == arg2.d_fp_size); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral( + symfpu::fma<symfpuLiteral::traits>(d_fp_size, + rm, + d_fpl->d_symuf, + arg1.d_fpl->d_symuf, + arg2.d_fpl->d_symuf))); #else return *this; #endif @@ -402,10 +460,11 @@ FloatingPoint FloatingPoint::div(const RoundingMode& rm, const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); + Assert(d_fp_size == arg.d_fp_size); return FloatingPoint( d_fp_size, - symfpu::divide<symfpuLiteral::traits>(d_fp_size, rm, d_fpl, arg.d_fpl)); + new FloatingPointLiteral(symfpu::divide<symfpuLiteral::traits>( + d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf))); #else return *this; #endif @@ -415,7 +474,9 @@ FloatingPoint FloatingPoint::sqrt(const RoundingMode& rm) const { #ifdef CVC4_USE_SYMFPU return FloatingPoint( - d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_fpl)); + d_fp_size, + new FloatingPointLiteral( + symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_fpl->d_symuf))); #else return *this; #endif @@ -426,7 +487,8 @@ FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const #ifdef CVC4_USE_SYMFPU return FloatingPoint( d_fp_size, - symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_fpl)); + new FloatingPointLiteral(symfpu::roundToIntegral<symfpuLiteral::traits>( + d_fp_size, rm, d_fpl->d_symuf))); #else return *this; #endif @@ -435,10 +497,11 @@ FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const FloatingPoint FloatingPoint::rem(const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); + Assert(d_fp_size == arg.d_fp_size); return FloatingPoint( d_fp_size, - symfpu::remainder<symfpuLiteral::traits>(d_fp_size, d_fpl, arg.d_fpl)); + new FloatingPointLiteral(symfpu::remainder<symfpuLiteral::traits>( + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf))); #else return *this; #endif @@ -448,10 +511,11 @@ FloatingPoint FloatingPoint::maxTotal(const FloatingPoint& arg, bool zeroCaseLeft) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::max<symfpuLiteral::traits>( - d_fp_size, d_fpl, arg.d_fpl, zeroCaseLeft)); + Assert(d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral(symfpu::max<symfpuLiteral::traits>( + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft))); #else return *this; #endif @@ -461,10 +525,11 @@ FloatingPoint FloatingPoint::minTotal(const FloatingPoint& arg, bool zeroCaseLeft) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::min<symfpuLiteral::traits>( - d_fp_size, d_fpl, arg.d_fpl, zeroCaseLeft)); + Assert(d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral(symfpu::min<symfpuLiteral::traits>( + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft))); #else return *this; #endif @@ -489,7 +554,7 @@ bool FloatingPoint::operator==(const FloatingPoint& fp) const #ifdef CVC4_USE_SYMFPU return ((d_fp_size == fp.d_fp_size) && symfpu::smtlibEqual<symfpuLiteral::traits>( - d_fp_size, d_fpl, fp.d_fpl)); + d_fp_size, d_fpl->d_symuf, fp.d_fpl->d_symuf)); #else return ((d_fp_size == fp.d_fp_size)); #endif @@ -498,9 +563,9 @@ bool FloatingPoint::operator==(const FloatingPoint& fp) const bool FloatingPoint::operator<=(const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); + Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThanOrEqual<symfpuLiteral::traits>( - d_fp_size, d_fpl, arg.d_fpl); + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf); #else return false; #endif @@ -509,9 +574,40 @@ bool FloatingPoint::operator<=(const FloatingPoint& arg) const bool FloatingPoint::operator<(const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return symfpu::lessThan<symfpuLiteral::traits>(d_fp_size, d_fpl, arg.d_fpl); + Assert(d_fp_size == arg.d_fp_size); + return symfpu::lessThan<symfpuLiteral::traits>( + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf); +#else + return false; +#endif +} + +BitVector FloatingPoint::getExponent() const +{ +#ifdef CVC4_USE_SYMFPU + return d_fpl->d_symuf.exponent; +#else + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return BitVector(); +#endif +} + +BitVector FloatingPoint::getSignificand() const +{ +#ifdef CVC4_USE_SYMFPU + return d_fpl->d_symuf.significand; +#else + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return BitVector(); +#endif +} + +bool FloatingPoint::getSign() const +{ +#ifdef CVC4_USE_SYMFPU + return d_fpl->d_symuf.sign; #else + Unreachable() << "no concrete implementation of FloatingPointLiteral"; return false; #endif } @@ -519,7 +615,7 @@ bool FloatingPoint::operator<(const FloatingPoint& arg) const bool FloatingPoint::isNormal(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_fpl); + return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -528,7 +624,7 @@ bool FloatingPoint::isNormal(void) const bool FloatingPoint::isSubnormal(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_fpl); + return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -537,7 +633,7 @@ bool FloatingPoint::isSubnormal(void) const bool FloatingPoint::isZero(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_fpl); + return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -546,7 +642,7 @@ bool FloatingPoint::isZero(void) const bool FloatingPoint::isInfinite(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_fpl); + return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -555,7 +651,7 @@ bool FloatingPoint::isInfinite(void) const bool FloatingPoint::isNaN(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_fpl); + return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -564,7 +660,7 @@ bool FloatingPoint::isNaN(void) const bool FloatingPoint::isNegative(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_fpl); + return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -573,7 +669,7 @@ bool FloatingPoint::isNegative(void) const bool FloatingPoint::isPositive(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_fpl); + return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -584,8 +680,9 @@ FloatingPoint FloatingPoint::convert(const FloatingPointSize& target, { #ifdef CVC4_USE_SYMFPU return FloatingPoint(target, - symfpu::convertFloatToFloat<symfpuLiteral::traits>( - d_fp_size, target, rm, d_fpl)); + new FloatingPointLiteral( + symfpu::convertFloatToFloat<symfpuLiteral::traits>( + d_fp_size, target, rm, d_fpl->d_symuf))); #else return *this; #endif @@ -599,10 +696,10 @@ BitVector FloatingPoint::convertToBVTotal(BitVectorSize width, #ifdef CVC4_USE_SYMFPU if (signedBV) return symfpu::convertFloatToSBV<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl, width, undefinedCase); + d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase); else return symfpu::convertFloatToUBV<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl, width, undefinedCase); + d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase); #else return undefinedCase; #endif @@ -627,23 +724,23 @@ FloatingPoint::PartialBitVector FloatingPoint::convertToBV( FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const { - if (this->isNaN() || this->isInfinite()) + if (isNaN() || isInfinite()) { return PartialRational(Rational(0U, 1U), false); } - if (this->isZero()) + if (isZero()) { return PartialRational(Rational(0U, 1U), true); } else { #ifdef CVC4_USE_SYMFPU - Integer sign((this->d_fpl.getSign()) ? -1 : 1); + Integer sign((d_fpl->d_symuf.getSign()) ? -1 : 1); Integer exp( - this->d_fpl.getExponent().toSignedInteger() + d_fpl->d_symuf.getExponent().toSignedInteger() - (Integer(d_fp_size.significandWidth() - 1))); // -1 as forcibly normalised into the [1,2) range - Integer significand(this->d_fpl.getSignificand().toInteger()); + Integer significand(d_fpl->d_symuf.getSignificand().toInteger()); #else Integer sign(0); Integer exp(0); @@ -682,8 +779,7 @@ FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const BitVector FloatingPoint::pack(void) const { #ifdef CVC4_USE_SYMFPU - BitVector bv( - symfpu::pack<symfpuLiteral::traits>(this->d_fp_size, this->d_fpl)); + BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf)); #else BitVector bv(4u, 0u); #endif |