diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-11-19 14:05:31 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-19 14:05:31 -0800 |
commit | 7191e58e5561a159c0cd3b81fddbe311ba70a45b (patch) | |
tree | d270db3e145e40d25135dfaafb90589750fa4215 /src/util/floatingpoint.cpp | |
parent | 6d6428a609d76e62cec5ff0ce2bad36e8afe2601 (diff) |
floatingpoint.h: Split in preparation to cleanly separate symFPU glue code. (#5478)
Diffstat (limited to 'src/util/floatingpoint.cpp')
-rw-r--r-- | src/util/floatingpoint.cpp | 419 |
1 files changed, 0 insertions, 419 deletions
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index cfb0120fb..ae6197791 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -64,427 +64,8 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv); } #endif -#ifndef CVC4_USE_SYMFPU -#define PRECONDITION(X) Assert((X)) -#endif - namespace CVC4 { -FloatingPointSize::FloatingPointSize(uint32_t exp_size, uint32_t sig_size) - : d_exp_size(exp_size), d_sig_size(sig_size) -{ - PrettyCheckArgument(validExponentSize(exp_size), - exp_size, - "Invalid exponent size : %d", - exp_size); - PrettyCheckArgument(validSignificandSize(sig_size), - sig_size, - "Invalid significand size : %d", - sig_size); -} - -FloatingPointSize::FloatingPointSize(const FloatingPointSize& old) - : d_exp_size(old.d_exp_size), d_sig_size(old.d_sig_size) -{ - PrettyCheckArgument(validExponentSize(d_exp_size), - d_exp_size, - "Invalid exponent size : %d", - d_exp_size); - PrettyCheckArgument(validSignificandSize(d_sig_size), - d_sig_size, - "Invalid significand size : %d", - d_sig_size); -} - -namespace symfpuLiteral { - -// To simplify the property macros -typedef traits t; - -template <bool isSigned> -wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one( - const CVC4BitWidth& w) -{ - return wrappedBitVector<isSigned>(w, 1); -} - -template <bool isSigned> -wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero( - const CVC4BitWidth& w) -{ - return wrappedBitVector<isSigned>(w, 0); -} - -template <bool isSigned> -wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes( - const CVC4BitWidth& w) -{ - return ~wrappedBitVector<isSigned>::zero(w); -} - -template <bool isSigned> -CVC4Prop wrappedBitVector<isSigned>::isAllOnes() const -{ - return (*this == wrappedBitVector<isSigned>::allOnes(this->getWidth())); -} -template <bool isSigned> -CVC4Prop wrappedBitVector<isSigned>::isAllZeros() const -{ - return (*this == wrappedBitVector<isSigned>::zero(this->getWidth())); -} - -template <bool isSigned> -wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue( - const CVC4BitWidth& 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 CVC4BitWidth& 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> -CVC4Prop wrappedBitVector<isSigned>::operator==( - const wrappedBitVector<isSigned>& op) const -{ - return this->BitVector::operator==(op); -} - -template <> -CVC4Prop wrappedBitVector<true>::operator<=( - const wrappedBitVector<true>& op) const -{ - return this->signedLessThanEq(op); -} - -template <> -CVC4Prop wrappedBitVector<true>::operator>=( - const wrappedBitVector<true>& op) const -{ - return !(this->signedLessThan(op)); -} - -template <> -CVC4Prop wrappedBitVector<true>::operator<( - const wrappedBitVector<true>& op) const -{ - return this->signedLessThan(op); -} - -template <> -CVC4Prop wrappedBitVector<true>::operator>( - const wrappedBitVector<true>& op) const -{ - return !(this->signedLessThanEq(op)); -} - -template <> -CVC4Prop wrappedBitVector<false>::operator<=( - const wrappedBitVector<false>& op) const -{ - return this->unsignedLessThanEq(op); -} - -template <> -CVC4Prop wrappedBitVector<false>::operator>=( - const wrappedBitVector<false>& op) const -{ - return !(this->unsignedLessThan(op)); -} - -template <> -CVC4Prop wrappedBitVector<false>::operator<( - const wrappedBitVector<false>& op) const -{ - return this->unsignedLessThan(op); -} - -template <> -CVC4Prop 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( - CVC4BitWidth extension) const -{ - if (isSigned) - { - return this->BitVector::signExtend(extension); - } - else - { - return this->BitVector::zeroExtend(extension); - } -} - -template <bool isSigned> -wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract( - CVC4BitWidth reduction) const -{ - PRECONDITION(this->getWidth() > reduction); - - return this->extract((this->getWidth() - 1) - reduction, 0); -} - -template <bool isSigned> -wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize( - CVC4BitWidth newSize) const -{ - CVC4BitWidth 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( - CVC4BitWidth upper, CVC4BitWidth lower) const -{ - PRECONDITION(upper >= lower); - return this->BitVector::extract(upper, lower); -} - -// Explicit instantiation -template class wrappedBitVector<true>; -template class wrappedBitVector<false>; - -traits::rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; }; -traits::rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; }; -traits::rm traits::RTP(void) { return ::CVC4::roundTowardPositive; }; -traits::rm traits::RTN(void) { return ::CVC4::roundTowardNegative; }; -traits::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 traits::prop& p) -{ - Assert(p); - return; -} -void traits::postcondition(const traits::prop& p) -{ - Assert(p); - return; -} -void traits::invariant(const traits::prop& p) -{ - Assert(p); - return; -} -} - #ifndef CVC4_USE_SYMFPU void FloatingPointLiteral::unfinished(void) const { |