**/
#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"
#include "symfpu/utils/properties.h"
#endif
+/* -------------------------------------------------------------------------- */
+
#ifdef CVC4_USE_SYMFPU
namespace symfpu {
}
#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
{
}
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),
}
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
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
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
{
#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
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
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
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
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
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
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
{
#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
#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
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
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
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
#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
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
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
}
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
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
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
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
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
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
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
{
#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
#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
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);
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
projects / cvc5.git / commitdiff