diff options
Diffstat (limited to 'src/util/floatingpoint_literal_symfpu.cpp')
| -rw-r--r-- | src/util/floatingpoint_literal_symfpu.cpp | 185 |
1 files changed, 0 insertions, 185 deletions
diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index c2c3fe77b..dc3dce6b9 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -16,7 +16,6 @@ #include "base/check.h" -#ifdef CVC5_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" #include "symfpu/core/compare.h" @@ -31,11 +30,9 @@ #include "symfpu/core/sqrt.h" #include "symfpu/utils/numberOfRoundingModes.h" #include "symfpu/utils/properties.h" -#endif /* -------------------------------------------------------------------------- */ -#ifdef CVC5_USE_SYMFPU namespace symfpu { #define CVC5_LIT_ITE_DFN(T) \ @@ -57,7 +54,6 @@ CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::ubv); #undef CVC5_LIT_ITE_DFN } // namespace symfpu -#endif /* -------------------------------------------------------------------------- */ @@ -65,44 +61,30 @@ namespace cvc5 { uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size) { -#ifdef CVC5_USE_SYMFPU return SymFPUUnpackedFloatLiteral::exponentWidth(size); -#else - unimplemented(); - return 2; -#endif } uint32_t FloatingPointLiteral::getUnpackedSignificandWidth( FloatingPointSize& size) { -#ifdef CVC5_USE_SYMFPU return SymFPUUnpackedFloatLiteral::significandWidth(size); -#else - unimplemented(); - return 2; -#endif } FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size, uint32_t sig_size, const BitVector& bv) : d_fp_size(exp_size, sig_size) -#ifdef CVC5_USE_SYMFPU , d_symuf(symfpu::unpack<symfpuLiteral::traits>( symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv)) -#endif { } FloatingPointLiteral::FloatingPointLiteral( const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size)) -#endif { Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN); } @@ -112,12 +94,10 @@ FloatingPointLiteral::FloatingPointLiteral( FloatingPointLiteral::SpecialConstKind kind, bool sign) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF ? SymFPUUnpackedFloatLiteral::makeInf(size, sign) : SymFPUUnpackedFloatLiteral::makeZero(size, sign)) -#endif { Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF || kind == FloatingPointLiteral::SpecialConstKind::FPZERO); @@ -126,10 +106,8 @@ FloatingPointLiteral::FloatingPointLiteral( FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv)) -#endif { } @@ -138,7 +116,6 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv, bool signedBV) : d_fp_size(size) -#ifdef CVC5_USE_SYMFPU , d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>( symfpuLiteral::Cvc5FPSize(size), @@ -148,97 +125,61 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, symfpuLiteral::Cvc5FPSize(size), symfpuLiteral::Cvc5RM(rm), symfpuLiteral::Cvc5UnsignedBitVector(bv))) -#endif { } BitVector FloatingPointLiteral::pack(void) const { -#ifdef CVC5_USE_SYMFPU BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf)); -#else - unimplemented(); - BitVector bv(4u, 0u); -#endif return bv; } FloatingPointLiteral FloatingPointLiteral::absolute(void) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::negate(void) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::add( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::add<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf, true)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::sub( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::add<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf, false)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::mult( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::multiply<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::div( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::divide<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::fma( @@ -246,276 +187,150 @@ FloatingPointLiteral FloatingPointLiteral::fma( const FloatingPointLiteral& arg1, const FloatingPointLiteral& arg2) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg1.d_fp_size); Assert(d_fp_size == arg2.d_fp_size); return FloatingPointLiteral( d_fp_size, symfpu::fma<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::rem( const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::remainder<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::maxTotal( const FloatingPointLiteral& arg, bool zeroCaseLeft) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral( d_fp_size, symfpu::max<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft)); -#else - unimplemented(); - return *this; -#endif } FloatingPointLiteral FloatingPointLiteral::minTotal( const FloatingPointLiteral& arg, bool zeroCaseLeft) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral( d_fp_size, symfpu::min<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft)); -#else - unimplemented(); - return *this; -#endif } bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const { -#ifdef CVC5_USE_SYMFPU return ((d_fp_size == fp.d_fp_size) && symfpu::smtlibEqual<symfpuLiteral::traits>( d_fp_size, d_symuf, fp.d_symuf)); -#else - unimplemented(); - return ((d_fp_size == fp.d_fp_size)); -#endif } bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThanOrEqual<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const { -#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThan<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf); -#else - unimplemented(); - return false; -#endif } BitVector FloatingPointLiteral::getExponent() const { -#ifdef CVC5_USE_SYMFPU return d_symuf.exponent; -#else - unimplemented(); - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return BitVector(); -#endif } BitVector FloatingPointLiteral::getSignificand() const { -#ifdef CVC5_USE_SYMFPU return d_symuf.significand; -#else - unimplemented(); - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return BitVector(); -#endif } bool FloatingPointLiteral::getSign() const { -#ifdef CVC5_USE_SYMFPU return d_symuf.sign; -#else - unimplemented(); - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return false; -#endif } bool FloatingPointLiteral::isNormal(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isSubnormal(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isZero(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isInfinite(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isNaN(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isNegative(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } bool FloatingPointLiteral::isPositive(void) const { -#ifdef CVC5_USE_SYMFPU return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf); -#else - unimplemented(); - return false; -#endif } FloatingPointLiteral FloatingPointLiteral::convert( const FloatingPointSize& target, const RoundingMode& rm) const { -#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( target, symfpu::convertFloatToFloat<symfpuLiteral::traits>( d_fp_size, target, rm, d_symuf)); -#else - unimplemented(); - return *this; -#endif } BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const { -#ifdef CVC5_USE_SYMFPU return symfpu::convertFloatToSBV<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, width, undefinedCase); -#else - unimplemented(); - return undefinedCase; -#endif } BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const { -#ifdef CVC5_USE_SYMFPU return symfpu::convertFloatToUBV<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, width, undefinedCase); -#else - unimplemented(); - return undefinedCase; -#endif } -#ifndef CVC5_USE_SYMFPU -void FloatingPointLiteral::unimplemented(void) -{ - Unimplemented() << "no concrete implementation of FloatingPointLiteral"; -} - -size_t FloatingPointLiteral::hash(void) const -{ - unimplemented(); - return 23; -} -#endif - } // namespace cvc5 |