diff options
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/floatingpoint.cpp | 646 | ||||
| -rw-r--r-- | src/util/floatingpoint.h | 198 |
2 files changed, 822 insertions, 22 deletions
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index fe90279ec..74e6189ed 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -15,8 +15,55 @@ **/ #include "util/floatingpoint.h" - #include "base/cvc4_assert.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 { @@ -32,22 +79,428 @@ FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s); } -void FloatingPointLiteral::unfinished (void) const { - Unimplemented("Floating-point literals not yet implemented."); +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); } - FloatingPoint::FloatingPoint (unsigned e, unsigned s, const BitVector &bv) : - fpl(e,s,0.0), - t(e,s) {} +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())); +} - 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"); +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) + { + 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); + + 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 + { + 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 traits::precondition(const prop &p) +{ + Assert(p); + return; +} +void traits::postcondition(const prop &p) +{ + Assert(p); + return; +} +void traits::invariant(const prop &p) +{ + Assert(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) : @@ -60,9 +513,16 @@ void FloatingPointLiteral::unfinished (void) const { 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 { - //int negative = (r.sgn() < 0) ? 1 : 0; +#ifdef CVC4_USE_SYMFPU + int negative = (r.sgn() < 0) ? 1 : 0; +#endif r = r.abs(); // Compute the exponent @@ -114,7 +574,7 @@ void FloatingPointLiteral::unfinished (void) const { // Compute the significand. - unsigned sigBits = ct.significand() + 2; // guard and sticky bits + unsigned sigBits = ct.significandWidth() + 2; // guard and sticky bits BitVector sig(sigBits, 0U); BitVector one(sigBits, 1U); Rational workingSig(0,1); @@ -144,7 +604,20 @@ void FloatingPointLiteral::unfinished (void) const { // 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"); } @@ -155,74 +628,146 @@ void FloatingPointLiteral::unfinished (void) const { 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 { @@ -236,56 +781,109 @@ void FloatingPointLiteral::unfinished (void) const { } 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 undefinedCase; + return symfpu::convertFloatToSBV<symfpuLiteral::traits>( + t, rm, fpl, width, undefinedCase); else - return undefinedCase; + return symfpu::convertFloatToUBV<symfpuLiteral::traits>( + t, rm, fpl, width, undefinedCase); +#else + return undefinedCase; +#endif } Rational FloatingPoint::convertToRationalTotal (Rational undefinedCase) const { @@ -309,10 +907,18 @@ void FloatingPointLiteral::unfinished (void) const { 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. @@ -333,7 +939,11 @@ void FloatingPointLiteral::unfinished (void) const { } 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; } diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index fa4573123..95bec903e 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -20,11 +20,15 @@ #ifndef __CVC4__FLOATINGPOINT_H #define __CVC4__FLOATINGPOINT_H -#include <fenv.h> - #include "util/bitvector.h" #include "util/rational.h" +#include <fenv.h> + +#ifdef CVC4_USE_SYMFPU +#include "symfpu/core/unpackedFloat.h" +#endif + namespace CVC4 { // Inline these! inline bool CVC4_PUBLIC validExponentSize (unsigned e) { return e >= 2; } @@ -62,6 +66,22 @@ namespace CVC4 { return (e == fps.e) && (s == fps.s); } + // Implement the interface that symfpu uses for floating-point formats. + inline unsigned exponentWidth(void) const { return this->exponent(); } + inline unsigned significandWidth(void) const { return this->significand(); } + inline unsigned packedWidth(void) const + { + return this->exponentWidth() + this->significandWidth(); + } + inline unsigned packedExponentWidth(void) const + { + return this->exponentWidth(); + } + inline unsigned packedSignificandWidth(void) const + { + return this->significandWidth() - 1; + } + }; /* class FloatingPointSize */ struct CVC4_PUBLIC FloatingPointSizeHashFunction { @@ -95,11 +115,181 @@ namespace CVC4 { } }; /* struct RoundingModeHashFunction */ + /** + * This is a symfpu literal "back-end". It allows the library to be used as + * an arbitrary precision floating-point implementation. This is effectively + * the glue between symfpu's notion of "signed bit-vector" and CVC4's + * BitVector. + */ + namespace symfpuLiteral { + // Forward declaration of wrapper so that traits can be defined early and so + // used in the implementation of wrappedBitVector. + template <bool T> + class wrappedBitVector; + + // This is the template parameter for symfpu's templates. + class traits + { + public: + // The six key types that symfpu uses. + typedef unsigned bwt; + typedef bool prop; + typedef ::CVC4::RoundingMode rm; + typedef ::CVC4::FloatingPointSize fpt; + typedef wrappedBitVector<true> sbv; + typedef wrappedBitVector<false> ubv; + + // Give concrete instances of each rounding mode, mainly for comparisons. + static rm RNE(void); + static rm RNA(void); + static rm RTP(void); + static rm RTN(void); + static rm RTZ(void); + + // The sympfu properties. + static void precondition(const prop &p); + static void postcondition(const prop &p); + static void invariant(const prop &p); + }; + + // Use the same type names as symfpu. + typedef traits::bwt bwt; + typedef traits::prop prop; + typedef traits::rm rm; + typedef traits::fpt fpt; + typedef traits::ubv ubv; + typedef traits::sbv sbv; + + // Type function for mapping between types + template <bool T> + struct signedToLiteralType; + + template <> + struct signedToLiteralType<true> + { + typedef int literalType; + }; + template <> + struct signedToLiteralType<false> + { + typedef unsigned int literalType; + }; + + // This is an additional interface for CVC4::BitVector. + // The template parameter distinguishes signed and unsigned bit-vectors, a + // distinction symfpu uses. + template <bool isSigned> + class wrappedBitVector : public BitVector + { + protected: + typedef typename signedToLiteralType<isSigned>::literalType literalType; + + friend wrappedBitVector<!isSigned>; // To allow conversion between the + // types +#ifdef CVC4_USE_SYMFPU + friend ::symfpu::ite<prop, wrappedBitVector<isSigned> >; // For ITE +#endif + + public: + wrappedBitVector(const bwt w, const unsigned v) : BitVector(w, v) {} + wrappedBitVector(const prop &p) : BitVector(1, p ? 1U : 0U) {} + wrappedBitVector(const wrappedBitVector<isSigned> &old) : BitVector(old) {} + wrappedBitVector(const BitVector &old) : BitVector(old) {} + bwt getWidth(void) const { return getSize(); } + /*** Constant creation and test ***/ + + static wrappedBitVector<isSigned> one(const bwt &w); + static wrappedBitVector<isSigned> zero(const bwt &w); + static wrappedBitVector<isSigned> allOnes(const bwt &w); + + prop isAllOnes() const; + prop isAllZeros() const; + + static wrappedBitVector<isSigned> maxValue(const bwt &w); + static wrappedBitVector<isSigned> minValue(const bwt &w); + + /*** Operators ***/ + wrappedBitVector<isSigned> operator<<( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator>>( + const wrappedBitVector<isSigned> &op) const; + + /* Inherited but ... + * *sigh* if we use the inherited version then it will return a + * CVC4::BitVector which can be converted back to a + * wrappedBitVector<isSigned> but isn't done automatically when working + * out types for templates instantiation. ITE is a particular + * problem as expressions and constants no longer derive the + * same type. There aren't any good solutions in C++, we could + * use CRTP but Liana wouldn't appreciate that, so the following + * pointless wrapping functions are needed. + */ + wrappedBitVector<isSigned> operator|( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator&( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator+( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator-( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator*( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator/( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator%( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> operator-(void) const; + wrappedBitVector<isSigned> operator~(void)const; + + wrappedBitVector<isSigned> increment() const; + wrappedBitVector<isSigned> decrement() const; + wrappedBitVector<isSigned> signExtendRightShift( + const wrappedBitVector<isSigned> &op) const; + + /*** Modular opertaions ***/ + // No overflow checking so these are the same as other operations + wrappedBitVector<isSigned> modularLeftShift( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> modularRightShift( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> modularIncrement() const; + wrappedBitVector<isSigned> modularDecrement() const; + wrappedBitVector<isSigned> modularAdd( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> modularNegate() const; + + /*** Comparisons ***/ + // Inherited ... ish ... + prop operator==(const wrappedBitVector<isSigned> &op) const; + prop operator<=(const wrappedBitVector<isSigned> &op) const; + prop operator>=(const wrappedBitVector<isSigned> &op) const; + prop operator<(const wrappedBitVector<isSigned> &op) const; + prop operator>(const wrappedBitVector<isSigned> &op) const; + + /*** Type conversion ***/ + wrappedBitVector<true> toSigned(void) const; + wrappedBitVector<false> toUnsigned(void) const; + + /*** Bit hacks ***/ + wrappedBitVector<isSigned> extend(bwt extension) const; + wrappedBitVector<isSigned> contract(bwt reduction) const; + wrappedBitVector<isSigned> resize(bwt newSize) const; + wrappedBitVector<isSigned> matchWidth( + const wrappedBitVector<isSigned> &op) const; + wrappedBitVector<isSigned> append( + const wrappedBitVector<isSigned> &op) const; + + // Inclusive of end points, thus if the same, extracts just one bit + wrappedBitVector<isSigned> extract(bwt upper, bwt lower) const; + }; + } /** * A concrete floating point number */ - +#ifdef CVC4_USE_SYMFPU + typedef ::symfpu::unpackedFloat<symfpuLiteral::traits> FloatingPointLiteral; +#else class CVC4_PUBLIC FloatingPointLiteral { public : // This intentional left unfinished as the choice of literal @@ -109,7 +299,6 @@ namespace CVC4 { FloatingPointLiteral(unsigned, unsigned, double) { unfinished(); } FloatingPointLiteral(unsigned, unsigned, const std::string &) { unfinished(); } FloatingPointLiteral(const FloatingPointLiteral &) { unfinished(); } - bool operator == (const FloatingPointLiteral &op) const { unfinished(); return false; @@ -120,6 +309,7 @@ namespace CVC4 { return 23; } }; +#endif class CVC4_PUBLIC FloatingPoint { protected : |