/********************* */
/*! \file floatingpoint.cpp
** \verbatim
- ** Original author: Martin Brain
- ** Major contributors:
- ** Minor contributors (to current version):
- ** This file is part of the CVC4 project.
+ ** Top contributors (to current version):
+ ** Martin Brain, Martin Brain, Tim King
** Copyright (c) 2013 University of Oxford
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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
**
** \brief [[ Implementations of the utility functions for working with floating point theories. ]]
**
**/
-#include "util/cvc4_assert.h"
#include "util/floatingpoint.h"
+#include "base/check.h"
+#include "util/integer.h"
+
+#include <math.h>
+
+#ifdef CVC4_USE_SYMFPU
+#include "symfpu/core/add.h"
+#include "symfpu/core/classify.h"
+#include "symfpu/core/compare.h"
+#include "symfpu/core/convert.h"
+#include "symfpu/core/divide.h"
+#include "symfpu/core/fma.h"
+#include "symfpu/core/ite.h"
+#include "symfpu/core/multiply.h"
+#include "symfpu/core/packing.h"
+#include "symfpu/core/remainder.h"
+#include "symfpu/core/sign.h"
+#include "symfpu/core/sqrt.h"
+#include "symfpu/utils/numberOfRoundingModes.h"
+#include "symfpu/utils/properties.h"
+#endif
+
+#ifdef CVC4_USE_SYMFPU
+namespace symfpu {
+
+#define CVC4_LIT_ITE_DFN(T) \
+ template <> \
+ struct ite<::CVC4::symfpuLiteral::prop, T> \
+ { \
+ static const T &iteOp(const ::CVC4::symfpuLiteral::prop &cond, \
+ const T &l, \
+ const T &r) \
+ { \
+ return cond ? l : r; \
+ } \
+ }
+
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
+
+#undef CVC4_LIT_ITE_DFN
+}
+#endif
+
+#ifndef CVC4_USE_SYMFPU
+#define PRECONDITION(X) Assert((X))
+#endif
namespace CVC4 {
- FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
+FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
+{
+ PrettyCheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
+ PrettyCheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
+}
+
+FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
+{
+ PrettyCheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
+ PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
+}
+
+namespace symfpuLiteral {
+
+// To simplify the property macros
+typedef traits t;
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(const bwt &w)
+{
+ return wrappedBitVector<isSigned>(w, 1);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(const bwt &w)
+{
+ return wrappedBitVector<isSigned>(w, 0);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(const bwt &w)
+{
+ return ~wrappedBitVector<isSigned>::zero(w);
+}
+
+template <bool isSigned>
+prop wrappedBitVector<isSigned>::isAllOnes() const
+{
+ return (*this == wrappedBitVector<isSigned>::allOnes(this->getWidth()));
+}
+template <bool isSigned>
+prop wrappedBitVector<isSigned>::isAllZeros() const
+{
+ return (*this == wrappedBitVector<isSigned>::zero(this->getWidth()));
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(const bwt &w)
+{
+ if (isSigned)
+ {
+ BitVector base(w - 1, 0U);
+ return wrappedBitVector<true>((~base).zeroExtend(1));
+ }
+ else
+ {
+ return wrappedBitVector<false>::allOnes(w);
+ }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(const bwt &w)
+{
+ if (isSigned)
+ {
+ BitVector base(w, 1U);
+ BitVector shiftAmount(w, w - 1);
+ BitVector result(base.leftShift(shiftAmount));
+ return wrappedBitVector<true>(result);
+ }
+ else
+ {
+ return wrappedBitVector<false>::zero(w);
+ }
+}
+
+/*** Operators ***/
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::leftShift(op);
+}
+
+template <>
+wrappedBitVector<true> wrappedBitVector<true>::operator>>(
+ const wrappedBitVector<true> &op) const
+{
+ return this->BitVector::arithRightShift(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator>>(
+ const wrappedBitVector<false> &op) const
+{
+ return this->BitVector::logicalRightShift(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator|(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator&(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator+(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator-(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator*(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator/(
+ const wrappedBitVector<false> &op) const
+{
+ return this->BitVector::unsignedDivTotal(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator%(
+ const wrappedBitVector<false> &op) const
+{
+ return this->BitVector::unsignedRemTotal(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
+{
+ return this->BitVector::operator-();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void)const
+{
+ return this->BitVector::operator~();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
+{
+ return *this + wrappedBitVector<isSigned>::one(this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
+{
+ return *this - wrappedBitVector<isSigned>::one(this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::arithRightShift(BitVector(this->getWidth(), op));
+}
+
+/*** Modular opertaions ***/
+// No overflow checking so these are the same as other operations
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return *this << op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return *this >> op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const
+{
+ return this->increment();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
+{
+ return this->decrement();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return *this + op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
+{
+ return -(*this);
+}
+
+/*** Comparisons ***/
+
+template <bool isSigned>
+prop wrappedBitVector<isSigned>::operator==(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::operator==(op);
+}
+
+template <>
+prop wrappedBitVector<true>::operator<=(const wrappedBitVector<true> &op) const
+{
+ return this->signedLessThanEq(op);
+}
+
+template <>
+prop wrappedBitVector<true>::operator>=(const wrappedBitVector<true> &op) const
+{
+ return !(this->signedLessThan(op));
+}
+
+template <>
+prop wrappedBitVector<true>::operator<(const wrappedBitVector<true> &op) const
+{
+ return this->signedLessThan(op);
+}
+
+template <>
+prop wrappedBitVector<true>::operator>(const wrappedBitVector<true> &op) const
+{
+ return !(this->signedLessThanEq(op));
+}
+
+template <>
+prop wrappedBitVector<false>::operator<=(
+ const wrappedBitVector<false> &op) const
+{
+ return this->unsignedLessThanEq(op);
+}
+
+template <>
+prop wrappedBitVector<false>::operator>=(
+ const wrappedBitVector<false> &op) const
+{
+ return !(this->unsignedLessThan(op));
+}
+
+template <>
+prop wrappedBitVector<false>::operator<(const wrappedBitVector<false> &op) const
+{
+ return this->unsignedLessThan(op);
+}
+
+template <>
+prop wrappedBitVector<false>::operator>(const wrappedBitVector<false> &op) const
+{
+ return !(this->unsignedLessThanEq(op));
+}
+
+/*** Type conversion ***/
+// CVC4 nodes make no distinction between signed and unsigned, thus ...
+template <bool isSigned>
+wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const
+{
+ return wrappedBitVector<true>(*this);
+}
+
+template <bool isSigned>
+wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
+{
+ return wrappedBitVector<false>(*this);
+}
+
+/*** Bit hacks ***/
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
+ bwt extension) const
+{
+ if (isSigned)
{
- CheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
- CheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
+ return this->BitVector::signExtend(extension);
}
+ else
+ {
+ return this->BitVector::zeroExtend(extension);
+ }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
+ bwt reduction) const
+{
+ PRECONDITION(this->getWidth() > reduction);
- FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
+ return this->extract((this->getWidth() - 1) - reduction, 0);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(bwt newSize) const
+{
+ bwt width = this->getWidth();
+
+ if (newSize > width)
+ {
+ return this->extend(newSize - width);
+ }
+ else if (newSize < width)
+ {
+ return this->contract(width - newSize);
+ }
+ else
{
- CheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
- CheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
+ return *this;
}
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
+ const wrappedBitVector<isSigned> &op) const
+{
+ PRECONDITION(this->getWidth() <= op.getWidth());
+ return this->extend(op.getWidth() - this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
+ const wrappedBitVector<isSigned> &op) const
+{
+ return this->BitVector::concat(op);
+}
+
+// Inclusive of end points, thus if the same, extracts just one bit
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(bwt upper,
+ bwt lower) const
+{
+ PRECONDITION(upper >= lower);
+ return this->BitVector::extract(upper, lower);
+}
+
+// Explicit instantiation
+template class wrappedBitVector<true>;
+template class wrappedBitVector<false>;
+
+rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; };
+rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; };
+rm traits::RTP(void) { return ::CVC4::roundTowardPositive; };
+rm traits::RTN(void) { return ::CVC4::roundTowardNegative; };
+rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
+// This is a literal back-end so props are actually bools
+// so these can be handled in the same way as the internal assertions above
- void FloatingPointLiteral::unfinished (void) const {
- Unimplemented("Floating-point literals not yet implemented.");
+void traits::precondition(const prop &p)
+{
+ AlwaysAssert(p);
+ return;
+}
+void traits::postcondition(const prop &p)
+{
+ AlwaysAssert(p);
+ return;
+}
+void traits::invariant(const prop &p)
+{
+ AlwaysAssert(p);
+ return;
+}
+}
+
+#ifndef CVC4_USE_SYMFPU
+void FloatingPointLiteral::unfinished(void) const
+{
+ Unimplemented() << "Floating-point literals not yet implemented.";
+}
+#endif
+
+FloatingPoint::FloatingPoint(unsigned e, unsigned s, const BitVector &bv)
+ :
+#ifdef CVC4_USE_SYMFPU
+ fpl(symfpu::unpack<symfpuLiteral::traits>(symfpuLiteral::fpt(e, s), bv)),
+#else
+ fpl(e, s, 0.0),
+#endif
+ t(e, s)
+{
+}
+
+static FloatingPointLiteral constructorHelperBitVector(
+ const FloatingPointSize &ct,
+ const RoundingMode &rm,
+ const BitVector &bv,
+ bool signedBV)
+{
+#ifdef CVC4_USE_SYMFPU
+ if (signedBV)
+ {
+ return FloatingPointLiteral(
+ symfpu::convertSBVToFloat<symfpuLiteral::traits>(
+ symfpuLiteral::fpt(ct),
+ symfpuLiteral::rm(rm),
+ symfpuLiteral::sbv(bv)));
+ }
+ else
+ {
+ return FloatingPointLiteral(
+ symfpu::convertUBVToFloat<symfpuLiteral::traits>(
+ symfpuLiteral::fpt(ct),
+ symfpuLiteral::rm(rm),
+ symfpuLiteral::ubv(bv)));
+ }
+#else
+ return FloatingPointLiteral(2, 2, 0.0);
+#endif
+ 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) {}
-}/* CVC4 namespace */
+
+ static FloatingPointLiteral constructorHelperRational (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &ri) {
+ Rational r(ri);
+ Rational two(2,1);
+
+ if (r.isZero()) {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPointLiteral::makeZero(
+ ct, false); // In keeping with the SMT-LIB standard
+#else
+ return FloatingPointLiteral(2,2,0.0);
+#endif
+ } else {
+#ifdef CVC4_USE_SYMFPU
+ int negative = (r.sgn() < 0) ? 1 : 0;
+#endif
+ 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.significandWidth() + 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...
+#ifdef CVC4_USE_SYMFPU
+ unsigned extension =
+ FloatingPointLiteral::exponentWidth(exactFormat) - expBits;
+
+ FloatingPointLiteral exactFloat(
+ negative, exactExp.signExtend(extension), sig);
+
+ // Then cast...
+ FloatingPointLiteral rounded(
+ symfpu::convertFloatToFloat(exactFormat, ct, rm, exactFloat));
+ return rounded;
+#else
+ Unreachable() << "no concrete implementation of FloatingPointLiteral";
+#endif
+ }
+ 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) {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeNaN(t));
+#else
+ return FloatingPoint(2, 2, BitVector(4U,0U));
+#endif
+ }
+
+ FloatingPoint FloatingPoint::makeInf (const FloatingPointSize &t, bool sign) {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeInf(t, sign));
+#else
+ return FloatingPoint(2, 2, BitVector(4U,0U));
+#endif
+ }
+
+ FloatingPoint FloatingPoint::makeZero (const FloatingPointSize &t, bool sign) {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeZero(t, sign));
+#else
+ return FloatingPoint(2, 2, BitVector(4U,0U));
+#endif
+ }
+
+
+ /* Operations implemented using symfpu */
+ FloatingPoint FloatingPoint::absolute (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(t, symfpu::absolute<symfpuLiteral::traits>(t, fpl));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::negate (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(t, symfpu::negate<symfpuLiteral::traits>(t, fpl));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::plus (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, true));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::sub (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, false));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::mult (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::multiply<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg1.t);
+ Assert(this->t == arg2.t);
+ return FloatingPoint(
+ t, symfpu::fma<symfpuLiteral::traits>(t, rm, fpl, arg1.fpl, arg2.fpl));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::div (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::divide<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::sqrt (const RoundingMode &rm) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(t, symfpu::sqrt<symfpuLiteral::traits>(t, rm, fpl));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ t, symfpu::roundToIntegral<symfpuLiteral::traits>(t, rm, fpl));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::rem (const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::remainder<symfpuLiteral::traits>(t, fpl, arg.fpl));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::max<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
+#else
+ return *this;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg.t);
+ return FloatingPoint(
+ t, symfpu::min<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
+#else
+ return *this;
+#endif
+ }
+
+ 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 {
+#ifdef CVC4_USE_SYMFPU
+ return ((t == fp.t)
+ && symfpu::smtlibEqual<symfpuLiteral::traits>(t, fpl, fp.fpl));
+#else
+ return ( (t == fp.t) );
+#endif
+ }
+
+ bool FloatingPoint::operator <= (const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg.t);
+ return symfpu::lessThanOrEqual<symfpuLiteral::traits>(t, fpl, arg.fpl);
+#else
+ return false;
+#endif
+ }
+
+ bool FloatingPoint::operator < (const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
+ Assert(this->t == arg.t);
+ return symfpu::lessThan<symfpuLiteral::traits>(t, fpl, arg.fpl);
+#else
+ return false;
+#endif
+ }
+
+ bool FloatingPoint::isNormal (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isNormal<symfpuLiteral::traits>(t, fpl);
+#else
+ return false;
+#endif
+ }
+
+ bool FloatingPoint::isSubnormal (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isSubnormal<symfpuLiteral::traits>(t, fpl);
+#else
+ return false;
+#endif
+ }
+
+ bool FloatingPoint::isZero (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isZero<symfpuLiteral::traits>(t, fpl);
+#else
+ return false;
+#endif
+ }
+
+ bool FloatingPoint::isInfinite (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isInfinite<symfpuLiteral::traits>(t, fpl);
+#else
+ return false;
+#endif
+ }
+
+ bool FloatingPoint::isNaN (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isNaN<symfpuLiteral::traits>(t, fpl);
+#else
+ return false;
+#endif
+ }
+
+ bool FloatingPoint::isNegative (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isNegative<symfpuLiteral::traits>(t, fpl);
+#else
+ return false;
+#endif
+ }
+
+ bool FloatingPoint::isPositive (void) const {
+#ifdef CVC4_USE_SYMFPU
+ return symfpu::isPositive<symfpuLiteral::traits>(t, fpl);
+#else
+ return false;
+#endif
+ }
+
+ FloatingPoint FloatingPoint::convert (const FloatingPointSize &target, const RoundingMode &rm) const {
+#ifdef CVC4_USE_SYMFPU
+ return FloatingPoint(
+ target,
+ symfpu::convertFloatToFloat<symfpuLiteral::traits>(t, target, rm, fpl));
+#else
+ return *this;
+#endif
+ }
+
+ BitVector FloatingPoint::convertToBVTotal (BitVectorSize width, const RoundingMode &rm, bool signedBV, BitVector undefinedCase) const {
+#ifdef CVC4_USE_SYMFPU
+ if (signedBV)
+ return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
+ t, rm, fpl, width, undefinedCase);
+ else
+ return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
+ t, rm, fpl, width, undefinedCase);
+#else
+ return undefinedCase;
+#endif
+ }
+
+ 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 {
+#ifdef CVC4_USE_SYMFPU
+ Integer sign((this->fpl.getSign()) ? -1 : 1);
+ Integer exp(
+ this->fpl.getExponent().toSignedInteger()
+ - (Integer(t.significand()
+ - 1))); // -1 as forcibly normalised into the [1,2) range
+ Integer significand(this->fpl.getSignificand().toInteger());
+#else
+ Integer sign(0);
+ Integer exp(0);
+ Integer significand(0);
+#endif
+ 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 {
+#ifdef CVC4_USE_SYMFPU
+ BitVector bv(symfpu::pack<symfpuLiteral::traits>(this->t, this->fpl));
+#else
+ BitVector bv(4u,0u);
+#endif
+ return bv;
+ }
+
+
+
+}/* CVC4 namespace */
projects / cvc5.git / blobdiff