From 7191e58e5561a159c0cd3b81fddbe311ba70a45b Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 19 Nov 2020 14:05:31 -0800
Subject: floatingpoint.h: Split in preparation to cleanly separate symFPU glue
 code. (#5478)

---
 src/util/floatingpoint.cpp | 419 ---------------------------------------------
 1 file changed, 419 deletions(-)

(limited to 'src/util/floatingpoint.cpp')

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
 {
-- 
cgit v1.2.3