diff options
-rw-r--r-- | src/api/cvc4cpp.cpp | 24 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 32 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 38 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 40 | ||||
-rw-r--r-- | src/util/floatingpoint.cpp | 501 | ||||
-rw-r--r-- | src/util/floatingpoint.h | 37 | ||||
-rw-r--r-- | src/util/floatingpoint_literal_symfpu.cpp | 501 | ||||
-rw-r--r-- | src/util/floatingpoint_literal_symfpu.h.in | 201 |
8 files changed, 864 insertions, 510 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index dce190460..f33095a4b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1920,42 +1920,42 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const { CVC4::FloatingPointToFPIEEEBitVector ext = d_node->getConst<FloatingPointToFPIEEEBitVector>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) { CVC4::FloatingPointToFPFloatingPoint ext = d_node->getConst<FloatingPointToFPFloatingPoint>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_REAL) { CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) { CVC4::FloatingPointToFPSignedBitVector ext = d_node->getConst<FloatingPointToFPSignedBitVector>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) { CVC4::FloatingPointToFPUnsignedBitVector ext = d_node->getConst<FloatingPointToFPUnsignedBitVector>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_GENERIC) { CVC4::FloatingPointToFPGeneric ext = d_node->getConst<FloatingPointToFPGeneric>(); - indices = std::make_pair(ext.d_fp_size.exponentWidth(), - ext.d_fp_size.significandWidth()); + indices = std::make_pair(ext.getSize().exponentWidth(), + ext.getSize().significandWidth()); } else if (k == REGEXP_LOOP) { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index e1a4058e8..3e99267cc 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -344,51 +344,59 @@ void Smt2Printer::toStream(std::ostream& out, case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: out << "(_ to_fp " << n.getConst<FloatingPointToFPIEEEBitVector>() - .d_fp_size.exponentWidth() + .getSize() + .exponentWidth() << ' ' << n.getConst<FloatingPointToFPIEEEBitVector>() - .d_fp_size.significandWidth() + .getSize() + .significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: out << "(_ to_fp " << n.getConst<FloatingPointToFPFloatingPoint>() - .d_fp_size.exponentWidth() + .getSize() + .exponentWidth() << ' ' << n.getConst<FloatingPointToFPFloatingPoint>() - .d_fp_size.significandWidth() + .getSize() + .significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_REAL_OP: out << "(_ to_fp " - << n.getConst<FloatingPointToFPReal>().d_fp_size.exponentWidth() + << n.getConst<FloatingPointToFPReal>().getSize().exponentWidth() << ' ' - << n.getConst<FloatingPointToFPReal>().d_fp_size.significandWidth() + << n.getConst<FloatingPointToFPReal>().getSize().significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: out << "(_ to_fp " << n.getConst<FloatingPointToFPSignedBitVector>() - .d_fp_size.exponentWidth() + .getSize() + .exponentWidth() << ' ' << n.getConst<FloatingPointToFPSignedBitVector>() - .d_fp_size.significandWidth() + .getSize() + .significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: out << "(_ to_fp_unsigned " << n.getConst<FloatingPointToFPUnsignedBitVector>() - .d_fp_size.exponentWidth() + .getSize() + .exponentWidth() << ' ' << n.getConst<FloatingPointToFPUnsignedBitVector>() - .d_fp_size.significandWidth() + .getSize() + .significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: out << "(_ to_fp " - << n.getConst<FloatingPointToFPGeneric>().d_fp_size.exponentWidth() + << n.getConst<FloatingPointToFPGeneric>().getSize().exponentWidth() << ' ' - << n.getConst<FloatingPointToFPGeneric>().d_fp_size.significandWidth() + << n.getConst<FloatingPointToFPGeneric>().getSize().significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_UBV_OP: diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index d4d47731d..3e03bbdbe 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -370,7 +370,7 @@ namespace constantFold { FloatingPoint arg1(node[1].getConst<FloatingPoint>()); FloatingPoint arg2(node[2].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2))); } @@ -383,7 +383,7 @@ namespace constantFold { FloatingPoint arg1(node[1].getConst<FloatingPoint>()); FloatingPoint arg2(node[2].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.mult(rm, arg2))); } @@ -397,8 +397,8 @@ namespace constantFold { FloatingPoint arg2(node[2].getConst<FloatingPoint>()); FloatingPoint arg3(node[3].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); - Assert(arg1.d_fp_size == arg3.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); + Assert(arg1.getSize() == arg3.getSize()); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.fma(rm, arg2, arg3))); } @@ -411,7 +411,7 @@ namespace constantFold { FloatingPoint arg1(node[1].getConst<FloatingPoint>()); FloatingPoint arg2(node[2].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.div(rm, arg2))); } @@ -443,7 +443,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst<FloatingPoint>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.rem(arg2))); } @@ -455,7 +455,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst<FloatingPoint>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); FloatingPoint::PartialFloatingPoint res(arg1.min(arg2)); @@ -475,7 +475,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst<FloatingPoint>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); FloatingPoint::PartialFloatingPoint res(arg1.max(arg2)); @@ -495,7 +495,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst<FloatingPoint>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); // Can be called with the third argument non-constant if (node[2].getMetaKind() == kind::metakind::CONSTANT) { @@ -525,7 +525,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst<FloatingPoint>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); // Can be called with the third argument non-constant if (node[2].getMetaKind() == kind::metakind::CONSTANT) { @@ -559,7 +559,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst<FloatingPoint>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2)); @@ -581,7 +581,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst<FloatingPoint>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 <= arg2)); } @@ -594,7 +594,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst<FloatingPoint>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.getSize() == arg2.getSize()); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 < arg2)); } @@ -657,8 +657,8 @@ namespace constantFold { const BitVector &bv = node[0].getConst<BitVector>(); Node lit = NodeManager::currentNM()->mkConst( - FloatingPoint(param.d_fp_size.exponentWidth(), - param.d_fp_size.significandWidth(), + FloatingPoint(param.getSize().exponentWidth(), + param.getSize().significandWidth(), bv)); return RewriteResponse(REWRITE_DONE, lit); @@ -674,7 +674,7 @@ namespace constantFold { return RewriteResponse( REWRITE_DONE, - NodeManager::currentNM()->mkConst(arg1.convert(info.d_fp_size, rm))); + NodeManager::currentNM()->mkConst(arg1.convert(info.getSize(), rm))); } RewriteResponse convertFromRealLiteral (TNode node, bool) { @@ -686,7 +686,7 @@ namespace constantFold { RoundingMode rm(node[0].getConst<RoundingMode>()); Rational arg(node[1].getConst<Rational>()); - FloatingPoint res(param.d_fp_size, rm, arg); + FloatingPoint res(param.getSize(), rm, arg); Node lit = NodeManager::currentNM()->mkConst(res); @@ -702,7 +702,7 @@ namespace constantFold { RoundingMode rm(node[0].getConst<RoundingMode>()); BitVector arg(node[1].getConst<BitVector>()); - FloatingPoint res(param.d_fp_size, rm, arg, true); + FloatingPoint res(param.getSize(), rm, arg, true); Node lit = NodeManager::currentNM()->mkConst(res); @@ -718,7 +718,7 @@ namespace constantFold { RoundingMode rm(node[0].getConst<RoundingMode>()); BitVector arg(node[1].getConst<BitVector>()); - FloatingPoint res(param.d_fp_size, rm, arg, false); + FloatingPoint res(param.getSize(), rm, arg, false); Node lit = NodeManager::currentNM()->mkConst(res); diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 32c718654..ab193d7ba 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -42,18 +42,18 @@ class FloatingPointConstantTypeRule { if (check) { - if (!(validExponentSize(f.d_fp_size.exponentWidth()))) + if (!(validExponentSize(f.getSize().exponentWidth()))) { throw TypeCheckingExceptionPrivate( n, "constant with invalid exponent size"); } - if (!(validSignificandSize(f.d_fp_size.significandWidth()))) + if (!(validSignificandSize(f.getSize().significandWidth()))) { throw TypeCheckingExceptionPrivate( n, "constant with invalid significand size"); } } - return nodeManager->mkFloatingPointType(f.d_fp_size); + return nodeManager->mkFloatingPointType(f.getSize()); } }; @@ -243,7 +243,8 @@ class FloatingPointParametricOpTypeRule { } }; -class FloatingPointToFPIEEEBitVectorTypeRule { +class FloatingPointToFPIEEEBitVectorTypeRule +{ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -264,8 +265,8 @@ class FloatingPointToFPIEEEBitVectorTypeRule { "than bit vector"); } else if (!(operandType.getBitVectorSize() - == info.d_fp_size.exponentWidth() - + info.d_fp_size.significandWidth())) + == info.getSize().exponentWidth() + + info.getSize().significandWidth())) { throw TypeCheckingExceptionPrivate( n, @@ -274,11 +275,12 @@ class FloatingPointToFPIEEEBitVectorTypeRule { } } - return nodeManager->mkFloatingPointType(info.d_fp_size); + return nodeManager->mkFloatingPointType(info.getSize()); } }; -class FloatingPointToFPFloatingPointTypeRule { +class FloatingPointToFPFloatingPointTypeRule +{ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -306,11 +308,12 @@ class FloatingPointToFPFloatingPointTypeRule { } } - return nodeManager->mkFloatingPointType(info.d_fp_size); + return nodeManager->mkFloatingPointType(info.getSize()); } }; -class FloatingPointToFPRealTypeRule { +class FloatingPointToFPRealTypeRule +{ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -338,11 +341,12 @@ class FloatingPointToFPRealTypeRule { } } - return nodeManager->mkFloatingPointType(info.d_fp_size); + return nodeManager->mkFloatingPointType(info.getSize()); } }; -class FloatingPointToFPSignedBitVectorTypeRule { +class FloatingPointToFPSignedBitVectorTypeRule +{ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -370,11 +374,12 @@ class FloatingPointToFPSignedBitVectorTypeRule { } } - return nodeManager->mkFloatingPointType(info.d_fp_size); + return nodeManager->mkFloatingPointType(info.getSize()); } }; -class FloatingPointToFPUnsignedBitVectorTypeRule { +class FloatingPointToFPUnsignedBitVectorTypeRule +{ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -402,11 +407,12 @@ class FloatingPointToFPUnsignedBitVectorTypeRule { } } - return nodeManager->mkFloatingPointType(info.d_fp_size); + return nodeManager->mkFloatingPointType(info.getSize()); } }; -class FloatingPointToFPGenericTypeRule { +class FloatingPointToFPGenericTypeRule +{ public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { @@ -427,7 +433,7 @@ class FloatingPointToFPGenericTypeRule { } } - return nodeManager->mkFloatingPointType(info.d_fp_size); + return nodeManager->mkFloatingPointType(info.getSize()); } }; diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index cebdbbb29..23b8253d8 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -26,49 +26,6 @@ #include "util/floatingpoint_literal_symfpu.h" #include "util/integer.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::CVC4Prop, T> \ - { \ - static const T& iteOp(const ::CVC4::symfpuLiteral::CVC4Prop& 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 - /* -------------------------------------------------------------------------- */ namespace CVC4 { @@ -77,46 +34,23 @@ namespace CVC4 { uint32_t FloatingPoint::getUnpackedExponentWidth(FloatingPointSize& size) { -#ifdef CVC4_USE_SYMFPU - return SymFPUUnpackedFloatLiteral::exponentWidth(size); -#else - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return 2; -#endif + return FloatingPointLiteral::getUnpackedExponentWidth(size); } uint32_t FloatingPoint::getUnpackedSignificandWidth(FloatingPointSize& size) { -#ifdef CVC4_USE_SYMFPU - return SymFPUUnpackedFloatLiteral::significandWidth(size); -#else - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return 2; -#endif + return FloatingPointLiteral::getUnpackedSignificandWidth(size); } FloatingPoint::FloatingPoint(uint32_t d_exp_size, uint32_t d_sig_size, const BitVector& bv) - : d_fp_size(d_exp_size, d_sig_size), -#ifdef CVC4_USE_SYMFPU - d_fpl(new FloatingPointLiteral(symfpu::unpack<symfpuLiteral::traits>( - symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv))) -#else - d_fpl(new FloatingPointLiteral(d_exp_size, d_sig_size, 0.0)) -#endif + : d_fpl(new FloatingPointLiteral(d_exp_size, d_sig_size, bv)) { } FloatingPoint::FloatingPoint(const FloatingPointSize& size, const BitVector& bv) - : d_fp_size(size), -#ifdef CVC4_USE_SYMFPU - d_fpl(new FloatingPointLiteral( - symfpu::unpack<symfpuLiteral::traits>(size, bv))) -#else - d_fpl(new FloatingPointLiteral( - size.exponentWidth(), size.significandWidth(), 0.0)) -#endif + : d_fpl(new FloatingPointLiteral(size, bv)) { } @@ -124,38 +58,13 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, const BitVector& bv, bool signedBV) - : d_fp_size(size) + : d_fpl(new FloatingPointLiteral(size, rm, bv, signedBV)) { -#ifdef CVC4_USE_SYMFPU - if (signedBV) - { - d_fpl.reset(new FloatingPointLiteral( - symfpu::convertSBVToFloat<symfpuLiteral::traits>( - symfpuLiteral::CVC4FPSize(size), - symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4SignedBitVector(bv)))); - } - else - { - d_fpl.reset(new FloatingPointLiteral( - symfpu::convertUBVToFloat<symfpuLiteral::traits>( - symfpuLiteral::CVC4FPSize(size), - symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4UnsignedBitVector(bv)))); - } -#else - d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0)); -#endif } -FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size, - FloatingPointLiteral* fpl) - : d_fp_size(fp_size) -{ - d_fpl.reset(fpl); -} +FloatingPoint::FloatingPoint(FloatingPointLiteral* fpl) { d_fpl.reset(fpl); } -FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size) +FloatingPoint::FloatingPoint(const FloatingPoint& fp) { d_fpl.reset(new FloatingPointLiteral(*fp.d_fpl)); } @@ -163,25 +72,18 @@ FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size) FloatingPoint::FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, const Rational& r) - : d_fp_size(size) { Rational two(2, 1); if (r.isZero()) { -#ifdef CVC4_USE_SYMFPU // In keeping with the SMT-LIB standard - d_fpl.reset(new FloatingPointLiteral( - SymFPUUnpackedFloatLiteral::makeZero(size, false))); -#else - d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0)); -#endif + d_fpl.reset( + new FloatingPointLiteral(FloatingPointLiteral::makeZero(size, false))); } else { -#ifdef CVC4_USE_SYMFPU uint32_t negative = (r.sgn() < 0) ? 1 : 0; -#endif Rational rabs(r.abs()); // Compute the exponent @@ -277,19 +179,14 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, // 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 uint32_t extension = - SymFPUUnpackedFloatLiteral::exponentWidth(exactFormat) - expBits; + FloatingPointLiteral::getUnpackedExponentWidth(exactFormat) - expBits; FloatingPointLiteral exactFloat( - negative, exactExp.signExtend(extension), sig); + exactFormat, negative, exactExp.signExtend(extension), sig); // Then cast... - d_fpl.reset(new FloatingPointLiteral(symfpu::convertFloatToFloat( - exactFormat, size, rm, exactFloat.d_symuf))); -#else - Unreachable() << "no concrete implementation of FloatingPointLiteral"; -#endif + d_fpl.reset(new FloatingPointLiteral(exactFloat.convert(size, rm))); } } @@ -297,37 +194,27 @@ FloatingPoint::~FloatingPoint() { } +const FloatingPointSize& FloatingPoint::getSize() const +{ + return d_fpl->getSize(); +} + FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size) { -#ifdef CVC4_USE_SYMFPU return FloatingPoint( - size, - new FloatingPointLiteral(SymFPUUnpackedFloatLiteral::makeNaN(size))); -#else - return FloatingPoint(2, 2, BitVector(4U, 0U)); -#endif + new FloatingPointLiteral(FloatingPointLiteral::makeNaN(size))); } FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign) { -#ifdef CVC4_USE_SYMFPU - return FloatingPoint(size, - new FloatingPointLiteral( - SymFPUUnpackedFloatLiteral::makeInf(size, sign))); -#else - return FloatingPoint(2, 2, BitVector(4U, 0U)); -#endif + return FloatingPoint( + new FloatingPointLiteral(FloatingPointLiteral::makeInf(size, sign))); } FloatingPoint FloatingPoint::makeZero(const FloatingPointSize& size, bool sign) { -#ifdef CVC4_USE_SYMFPU - return FloatingPoint(size, - new FloatingPointLiteral( - SymFPUUnpackedFloatLiteral::makeZero(size, sign))); -#else - return FloatingPoint(2, 2, BitVector(4U, 0U)); -#endif + return FloatingPoint( + new FloatingPointLiteral(FloatingPointLiteral::makeZero(size, sign))); } FloatingPoint FloatingPoint::makeMinSubnormal(const FloatingPointSize& size, @@ -367,170 +254,75 @@ FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size, return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig)); } -/* Operations implemented using symfpu */ FloatingPoint FloatingPoint::absolute(void) const { -#ifdef CVC4_USE_SYMFPU - return FloatingPoint( - d_fp_size, - new FloatingPointLiteral( - symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->absolute())); } FloatingPoint FloatingPoint::negate(void) const { -#ifdef CVC4_USE_SYMFPU - return FloatingPoint( - d_fp_size, - new FloatingPointLiteral( - symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->negate())); } FloatingPoint FloatingPoint::plus(const RoundingMode& rm, const FloatingPoint& arg) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg.d_fp_size); - return FloatingPoint( - d_fp_size, - new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, true))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->add(rm, *arg.d_fpl))); } FloatingPoint FloatingPoint::sub(const RoundingMode& rm, const FloatingPoint& arg) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg.d_fp_size); - return FloatingPoint( - d_fp_size, - new FloatingPointLiteral(symfpu::add<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, false))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->sub(rm, *arg.d_fpl))); } FloatingPoint FloatingPoint::mult(const RoundingMode& rm, const FloatingPoint& arg) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg.d_fp_size); - return FloatingPoint( - d_fp_size, - new FloatingPointLiteral(symfpu::multiply<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->mult(rm, *arg.d_fpl))); } FloatingPoint FloatingPoint::fma(const RoundingMode& rm, const FloatingPoint& arg1, const FloatingPoint& arg2) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg1.d_fp_size); - Assert(d_fp_size == arg2.d_fp_size); return FloatingPoint( - d_fp_size, - new FloatingPointLiteral( - symfpu::fma<symfpuLiteral::traits>(d_fp_size, - rm, - d_fpl->d_symuf, - arg1.d_fpl->d_symuf, - arg2.d_fpl->d_symuf))); -#else - return *this; -#endif + new FloatingPointLiteral(d_fpl->fma(rm, *arg1.d_fpl, *arg2.d_fpl))); } FloatingPoint FloatingPoint::div(const RoundingMode& rm, const FloatingPoint& arg) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg.d_fp_size); - return FloatingPoint( - d_fp_size, - new FloatingPointLiteral(symfpu::divide<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->div(rm, *arg.d_fpl))); } FloatingPoint FloatingPoint::sqrt(const RoundingMode& rm) const { -#ifdef CVC4_USE_SYMFPU - return FloatingPoint( - d_fp_size, - new FloatingPointLiteral( - symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_fpl->d_symuf))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->sqrt(rm))); } FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const { -#ifdef CVC4_USE_SYMFPU - return FloatingPoint( - d_fp_size, - new FloatingPointLiteral(symfpu::roundToIntegral<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl->d_symuf))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->rti(rm))); } FloatingPoint FloatingPoint::rem(const FloatingPoint& arg) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg.d_fp_size); - return FloatingPoint( - d_fp_size, - new FloatingPointLiteral(symfpu::remainder<symfpuLiteral::traits>( - d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->rem(*arg.d_fpl))); } FloatingPoint FloatingPoint::maxTotal(const FloatingPoint& arg, bool zeroCaseLeft) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg.d_fp_size); return FloatingPoint( - d_fp_size, - new FloatingPointLiteral(symfpu::max<symfpuLiteral::traits>( - d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft))); -#else - return *this; -#endif + new FloatingPointLiteral(d_fpl->maxTotal(*arg.d_fpl, zeroCaseLeft))); } FloatingPoint FloatingPoint::minTotal(const FloatingPoint& arg, bool zeroCaseLeft) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg.d_fp_size); return FloatingPoint( - d_fp_size, - new FloatingPointLiteral(symfpu::min<symfpuLiteral::traits>( - d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft))); -#else - return *this; -#endif + new FloatingPointLiteral(d_fpl->minTotal(*arg.d_fpl, zeroCaseLeft))); } FloatingPoint::PartialFloatingPoint FloatingPoint::max( @@ -549,141 +341,46 @@ FloatingPoint::PartialFloatingPoint FloatingPoint::min( bool FloatingPoint::operator==(const FloatingPoint& fp) const { -#ifdef CVC4_USE_SYMFPU - return ((d_fp_size == fp.d_fp_size) - && symfpu::smtlibEqual<symfpuLiteral::traits>( - d_fp_size, d_fpl->d_symuf, fp.d_fpl->d_symuf)); -#else - return ((d_fp_size == fp.d_fp_size)); -#endif + return *d_fpl == *fp.d_fpl; } -bool FloatingPoint::operator<=(const FloatingPoint& arg) const +bool FloatingPoint::operator<=(const FloatingPoint& fp) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg.d_fp_size); - return symfpu::lessThanOrEqual<symfpuLiteral::traits>( - d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf); -#else - return false; -#endif + return *d_fpl <= *fp.d_fpl; } -bool FloatingPoint::operator<(const FloatingPoint& arg) const +bool FloatingPoint::operator<(const FloatingPoint& fp) const { -#ifdef CVC4_USE_SYMFPU - Assert(d_fp_size == arg.d_fp_size); - return symfpu::lessThan<symfpuLiteral::traits>( - d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf); -#else - return false; -#endif + return *d_fpl < *fp.d_fpl; } -BitVector FloatingPoint::getExponent() const -{ -#ifdef CVC4_USE_SYMFPU - return d_fpl->d_symuf.exponent; -#else - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return BitVector(); -#endif -} +BitVector FloatingPoint::getExponent() const { return d_fpl->getExponent(); } BitVector FloatingPoint::getSignificand() const { -#ifdef CVC4_USE_SYMFPU - return d_fpl->d_symuf.significand; -#else - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return BitVector(); -#endif + return d_fpl->getSignificand(); } -bool FloatingPoint::getSign() const -{ -#ifdef CVC4_USE_SYMFPU - return d_fpl->d_symuf.sign; -#else - Unreachable() << "no concrete implementation of FloatingPointLiteral"; - return false; -#endif -} +bool FloatingPoint::getSign() const { return d_fpl->getSign(); } -bool FloatingPoint::isNormal(void) const -{ -#ifdef CVC4_USE_SYMFPU - return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); -#else - return false; -#endif -} +bool FloatingPoint::isNormal(void) const { return d_fpl->isNormal(); } -bool FloatingPoint::isSubnormal(void) const -{ -#ifdef CVC4_USE_SYMFPU - return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); -#else - return false; -#endif -} +bool FloatingPoint::isSubnormal(void) const { return d_fpl->isSubnormal(); } -bool FloatingPoint::isZero(void) const -{ -#ifdef CVC4_USE_SYMFPU - return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); -#else - return false; -#endif -} +bool FloatingPoint::isZero(void) const { return d_fpl->isZero(); } -bool FloatingPoint::isInfinite(void) const -{ -#ifdef CVC4_USE_SYMFPU - return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); -#else - return false; -#endif -} +bool FloatingPoint::isInfinite(void) const { return d_fpl->isInfinite(); } -bool FloatingPoint::isNaN(void) const -{ -#ifdef CVC4_USE_SYMFPU - return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); -#else - return false; -#endif -} +bool FloatingPoint::isNaN(void) const { return d_fpl->isNaN(); } -bool FloatingPoint::isNegative(void) const -{ -#ifdef CVC4_USE_SYMFPU - return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); -#else - return false; -#endif -} +bool FloatingPoint::isNegative(void) const { return d_fpl->isNegative(); } -bool FloatingPoint::isPositive(void) const -{ -#ifdef CVC4_USE_SYMFPU - return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf); -#else - return false; -#endif -} +bool FloatingPoint::isPositive(void) const { return d_fpl->isPositive(); } FloatingPoint FloatingPoint::convert(const FloatingPointSize& target, const RoundingMode& rm) const { -#ifdef CVC4_USE_SYMFPU - return FloatingPoint(target, - new FloatingPointLiteral( - symfpu::convertFloatToFloat<symfpuLiteral::traits>( - d_fp_size, target, rm, d_fpl->d_symuf))); -#else - return *this; -#endif + return FloatingPoint(new FloatingPointLiteral(d_fpl->convert(target, rm))); } BitVector FloatingPoint::convertToBVTotal(BitVectorSize width, @@ -691,16 +388,11 @@ BitVector FloatingPoint::convertToBVTotal(BitVectorSize width, bool signedBV, BitVector undefinedCase) const { -#ifdef CVC4_USE_SYMFPU - if (signedBV) - return symfpu::convertFloatToSBV<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase); - else - return symfpu::convertFloatToUBV<symfpuLiteral::traits>( - d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase); -#else - return undefinedCase; -#endif + if (signedBV) + { + return d_fpl->convertToSBVTotal(width, rm, undefinedCase); + } + return d_fpl->convertToUBVTotal(width, rm, undefinedCase); } Rational FloatingPoint::convertToRationalTotal(Rational undefinedCase) const @@ -730,59 +422,40 @@ FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const { return PartialRational(Rational(0U, 1U), true); } - else - { -#ifdef CVC4_USE_SYMFPU - Integer sign((d_fpl->d_symuf.getSign()) ? -1 : 1); - Integer exp( - d_fpl->d_symuf.getExponent().toSignedInteger() - - (Integer(d_fp_size.significandWidth() - - 1))); // -1 as forcibly normalised into the [1,2) range - Integer significand(d_fpl->d_symuf.getSignificand().toInteger()); -#else - Integer sign(0); - Integer exp(0); - Integer significand(0); -#endif - Integer signedSignificand(sign * significand); - - // We only have multiplyByPow(uint32_t) so we can't convert all numbers. - // As we convert Integer -> unsigned int -> uint32_t we need that - // unsigned int is not smaller than uint32_t - static_assert(sizeof(unsigned int) >= sizeof(uint32_t), - "Conversion float -> real could loose data"); + Integer sign((d_fpl->getSign()) ? -1 : 1); + Integer exp( + d_fpl->getExponent().toSignedInteger() + - (Integer(d_fpl->getSize().significandWidth() + - 1))); // -1 as forcibly normalised into the [1,2) range + Integer significand(d_fpl->getSignificand().toInteger()); + Integer signedSignificand(sign * significand); + + // We only have multiplyByPow(uint32_t) so we can't convert all numbers. + // As we convert Integer -> unsigned int -> uint32_t we need that + // unsigned int is not smaller than uint32_t + static_assert(sizeof(unsigned int) >= sizeof(uint32_t), + "Conversion float -> real could loose data"); #ifdef CVC4_ASSERTIONS - // Note that multipling by 2^n requires n bits of space (worst case) - // so, in effect, these tests limit us to cases where the resultant - // number requires up to 2^32 bits = 512 megabyte to represent. - Integer shiftLimit(std::numeric_limits<uint32_t>::max()); + // Note that multipling by 2^n requires n bits of space (worst case) + // so, in effect, these tests limit us to cases where the resultant + // number requires up to 2^32 bits = 512 megabyte to represent. + Integer shiftLimit(std::numeric_limits<uint32_t>::max()); #endif - if (!(exp.strictlyNegative())) { - Assert(exp <= shiftLimit); - Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt())); - return PartialRational(Rational(r), true); - } else { - Integer one(1U); - Assert((-exp) <= shiftLimit); - Integer q(one.multiplyByPow2((-exp).toUnsignedInt())); - Rational r(signedSignificand, q); - return PartialRational(r, true); - } + if (!(exp.strictlyNegative())) + { + Assert(exp <= shiftLimit); + Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt())); + return PartialRational(Rational(r), true); } - - Unreachable() << "Convert float literal to real broken."; + Integer one(1U); + Assert((-exp) <= shiftLimit); + Integer q(one.multiplyByPow2((-exp).toUnsignedInt())); + Rational r(signedSignificand, q); + return PartialRational(r, true); } -BitVector FloatingPoint::pack(void) const -{ -#ifdef CVC4_USE_SYMFPU - BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_fpl->d_symuf)); -#else - BitVector bv(4u, 0u); -#endif - return bv; -} +BitVector FloatingPoint::pack(void) const { return d_fpl->pack(); } std::string FloatingPoint::toString(bool printAsIndexed) const { @@ -790,9 +463,9 @@ std::string FloatingPoint::toString(bool printAsIndexed) const // retrive BV value BitVector bv(pack()); uint32_t largestSignificandBit = - d_fp_size.significandWidth() - 2; // -1 for -inclusive, -1 for hidden + getSize().significandWidth() - 2; // -1 for -inclusive, -1 for hidden uint32_t largestExponentBit = - (d_fp_size.exponentWidth() - 1) + (largestSignificandBit + 1); + (getSize().exponentWidth() - 1) + (largestSignificandBit + 1); BitVector v[3]; v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1); v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1); @@ -836,7 +509,7 @@ std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps) std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs) { - return os << "(_ to_fp " << fpcs.d_fp_size.exponentWidth() << " " - << fpcs.d_fp_size.significandWidth() << ")"; + return os << "(_ to_fp " << fpcs.getSize().exponentWidth() << " " + << fpcs.getSize().significandWidth() << ")"; } }/* CVC4 namespace */ diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index 758d51bc5..b6c1bfb53 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -48,28 +48,43 @@ class FloatingPoint /** * Get the number of exponent bits in the unpacked format corresponding to a - * given packed format. These is the unpacked counter-parts of + * given packed format. This is the unpacked counter-part of * FloatingPointSize::exponentWidth(). */ static uint32_t getUnpackedExponentWidth(FloatingPointSize& size); /** * Get the number of exponent bits in the unpacked format corresponding to a - * given packed format. These is the unpacked counter-parts of + * given packed format. This is the unpacked counter-part of * FloatingPointSize::significandWidth(). */ static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size); /** Constructors. */ + + /** Create a FP value from its IEEE bit-vector representation. */ FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv); FloatingPoint(const FloatingPointSize& size, const BitVector& bv); - FloatingPoint(const FloatingPoint& fp); + + /** + * Create a FP value from a signed or unsigned bit-vector value with + * respect to given rounding mode. + */ FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, const BitVector& bv, bool signedBV); + + /** + * Create a FP value from a rational value with respect to given rounding + * mode. + */ FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, const Rational& r); + + /** Copy constructor. */ + FloatingPoint(const FloatingPoint& fp); + /** Destructor. */ ~FloatingPoint(); @@ -117,6 +132,9 @@ class FloatingPoint */ static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign); + /** Return the size of this FP value. */ + const FloatingPointSize& getSize() const; + /** Get the wrapped floating-point value. */ const FloatingPointLiteral* getLiteral(void) const { return d_fpl.get(); } @@ -254,9 +272,6 @@ class FloatingPoint */ PartialRational convertToRational(void) const; - /** The floating-point size of this floating-point value. */ - FloatingPointSize d_fp_size; - private: /** * Constructor. @@ -264,7 +279,7 @@ class FloatingPoint * Note: This constructor takes ownership of 'fpl' and is not intended for * public use. */ - FloatingPoint(const FloatingPointSize& fp_size, FloatingPointLiteral* fpl); + FloatingPoint(FloatingPointLiteral* fpl); /** The floating-point literal of this floating-point value. */ std::unique_ptr<FloatingPointLiteral> d_fpl; @@ -281,7 +296,7 @@ struct FloatingPointHashFunction FloatingPointSizeHashFunction fpshf; BitVectorHashFunction bvhf; - return fpshf(fp.d_fp_size) ^ bvhf(fp.pack()); + return fpshf(fp.getSize()) ^ bvhf(fp.pack()); } }; /* struct FloatingPointHashFunction */ @@ -303,6 +318,10 @@ class FloatingPointConvertSort return d_fp_size == fpcs.d_fp_size; } + /** Return the size of this FP convert sort. */ + FloatingPointSize getSize() const { return d_fp_size; } + + private: /** The floating-point size of this sort. */ FloatingPointSize d_fp_size; }; @@ -314,7 +333,7 @@ struct FloatingPointConvertSortHashFunction inline size_t operator()(const FloatingPointConvertSort& fpcs) const { FloatingPointSizeHashFunction f; - return f(fpcs.d_fp_size) ^ (0x00005300 | (key << 24)); + return f(fpcs.getSize()) ^ (0x00005300 | (key << 24)); } }; /* struct FloatingPointConvertSortHashFunction */ diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index 05a219251..59b14001d 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -15,23 +15,512 @@ #include "base/check.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::CVC4Prop, T> \ + { \ + static const T& iteOp(const ::CVC4::symfpuLiteral::CVC4Prop& 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 +} // namespace symfpu +#endif + +/* -------------------------------------------------------------------------- */ + namespace CVC4 { -#ifndef CVC4_USE_SYMFPU -void FloatingPointLiteral::unfinished(void) const +uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size) +{ +#ifdef CVC4_USE_SYMFPU + return SymFPUUnpackedFloatLiteral::exponentWidth(size); +#else + unimplemented(); + return 2; +#endif +} + +uint32_t FloatingPointLiteral::getUnpackedSignificandWidth( + FloatingPointSize& size) +{ +#ifdef CVC4_USE_SYMFPU + return SymFPUUnpackedFloatLiteral::significandWidth(size); +#else + unimplemented(); + return 2; +#endif +} + +FloatingPointLiteral FloatingPointLiteral::makeNaN( + const FloatingPointSize& size) +{ +#ifdef CVC4_USE_SYMFPU + return FloatingPointLiteral(size, SymFPUUnpackedFloatLiteral::makeNaN(size)); +#else + unimplemented(); + return FloatingPointLiteral(size, BitVector(4u, 0u)); +#endif +} + +FloatingPointLiteral FloatingPointLiteral::makeInf( + const FloatingPointSize& size, bool sign) +{ +#ifdef CVC4_USE_SYMFPU + return FloatingPointLiteral(size, + SymFPUUnpackedFloatLiteral::makeInf(size, sign)); +#else + unimplemented(); + return FloatingPointLiteral(size, BitVector(4u, 0u)); +#endif +} + +FloatingPointLiteral FloatingPointLiteral::makeZero( + const FloatingPointSize& size, bool sign) +{ +#ifdef CVC4_USE_SYMFPU + return FloatingPointLiteral(size, + SymFPUUnpackedFloatLiteral::makeZero(size, sign)); +#else + unimplemented(); + return FloatingPointLiteral(size, BitVector(4u, 0u)); +#endif +} + +FloatingPointLiteral::FloatingPointLiteral(uint32_t d_exp_size, + uint32_t d_sig_size, + const BitVector& bv) + : d_fp_size(d_exp_size, d_sig_size) +#ifdef CVC4_USE_SYMFPU + , + d_symuf(symfpu::unpack<symfpuLiteral::traits>( + symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv)) +#endif +{ +} + +FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, + const BitVector& bv) + : d_fp_size(size) +#ifdef CVC4_USE_SYMFPU + , + d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv)) +#endif +{ +} + +FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, + const RoundingMode& rm, + const BitVector& bv, + bool signedBV) + : d_fp_size(size) +#ifdef CVC4_USE_SYMFPU + , + d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>( + symfpuLiteral::CVC4FPSize(size), + symfpuLiteral::CVC4RM(rm), + symfpuLiteral::CVC4SignedBitVector(bv)) + : symfpu::convertUBVToFloat<symfpuLiteral::traits>( + symfpuLiteral::CVC4FPSize(size), + symfpuLiteral::CVC4RM(rm), + symfpuLiteral::CVC4UnsignedBitVector(bv))) +#endif +{ +} + +BitVector FloatingPointLiteral::pack(void) const { - Unimplemented() << "Floating-point literals not yet implemented."; +#ifdef CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 } -bool FloatingPointLiteral::operator==(const FloatingPointLiteral& other) const +FloatingPointLiteral FloatingPointLiteral::div( + const RoundingMode& rm, const FloatingPointLiteral& arg) const { - unfinished(); +#ifdef CVC4_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( + const RoundingMode& rm, + const FloatingPointLiteral& arg1, + const FloatingPointLiteral& arg2) const +{ +#ifdef CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_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 CVC4_USE_SYMFPU + return d_symuf.exponent; +#else + unimplemented(); + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return BitVector(); +#endif +} + +BitVector FloatingPointLiteral::getSignificand() const +{ +#ifdef CVC4_USE_SYMFPU + return d_symuf.significand; +#else + unimplemented(); + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return BitVector(); +#endif +} + +bool FloatingPointLiteral::getSign() const +{ +#ifdef CVC4_USE_SYMFPU + return d_symuf.sign; +#else + unimplemented(); + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return false; +#endif +} + +bool FloatingPointLiteral::isNormal(void) const +{ +#ifdef CVC4_USE_SYMFPU + return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf); +#else + unimplemented(); + return false; +#endif +} + +bool FloatingPointLiteral::isSubnormal(void) const +{ +#ifdef CVC4_USE_SYMFPU + return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf); +#else + unimplemented(); + return false; +#endif +} + +bool FloatingPointLiteral::isZero(void) const +{ +#ifdef CVC4_USE_SYMFPU + return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf); +#else + unimplemented(); + return false; +#endif +} + +bool FloatingPointLiteral::isInfinite(void) const +{ +#ifdef CVC4_USE_SYMFPU + return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf); +#else + unimplemented(); + return false; +#endif +} + +bool FloatingPointLiteral::isNaN(void) const +{ +#ifdef CVC4_USE_SYMFPU + return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf); +#else + unimplemented(); + return false; +#endif +} + +bool FloatingPointLiteral::isNegative(void) const +{ +#ifdef CVC4_USE_SYMFPU + return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf); +#else + unimplemented(); + return false; +#endif +} + +bool FloatingPointLiteral::isPositive(void) const +{ +#ifdef CVC4_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 CVC4_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 CVC4_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 CVC4_USE_SYMFPU + return symfpu::convertFloatToUBV<symfpuLiteral::traits>( + d_fp_size, rm, d_symuf, width, undefinedCase); +#else + unimplemented(); + return undefinedCase; +#endif +} + +#ifndef CVC4_USE_SYMFPU +void FloatingPointLiteral::unimplemented(void) +{ + Unimplemented() << "no concrete implementation of FloatingPointLiteral"; } size_t FloatingPointLiteral::hash(void) const { - unfinished(); + unimplemented(); return 23; } #endif diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in index 3040dae78..d7e1a2241 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h.in @@ -19,6 +19,7 @@ #define CVC4__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H #include "util/bitvector.h" +#include "util/floatingpoint_size.h" #include "util/roundingmode.h" // clang-format off @@ -32,7 +33,7 @@ namespace CVC4 { class FloatingPointSize; -class FloatingPoint; +class FloatingPointLiteral; /* -------------------------------------------------------------------------- */ @@ -277,23 +278,69 @@ class wrappedBitVector : public BitVector // clang-format off #if @CVC4_USE_SYMFPU@ // clang-format on -using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>; +using SymFPUUnpackedFloatLiteral = + ::symfpu::unpackedFloat<symfpuLiteral::traits>; #endif class FloatingPointLiteral { friend class FloatingPoint; + public: - /** Constructors. */ + /** + * Get the number of exponent bits in the unpacked format corresponding to a + * given packed format. This is the unpacked counter-part of + * FloatingPointSize::exponentWidth(). + */ + static uint32_t getUnpackedExponentWidth(FloatingPointSize& size); + /** + * Get the number of exponent bits in the unpacked format corresponding to a + * given packed format. This is the unpacked counter-part of + * FloatingPointSize::significandWidth(). + */ + static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size); - /** Create an FP literal from a FloatingPoint. */ - FloatingPointLiteral(FloatingPoint& other); + /** + * Create a FP NaN literal of given size. + * size: The FP size (format). + */ + static FloatingPointLiteral makeNaN(const FloatingPointSize& size); + /** + * Create a FP infinity literal of given size. + * size: The FP size (format). + * sign: True for -oo, false otherwise. + */ + static FloatingPointLiteral makeInf(const FloatingPointSize& size, bool sign); + /** + * Create a FP zero literal of given size. + * size: The FP size (format). + * sign: True for -zero, false otherwise. + */ + static FloatingPointLiteral makeZero(const FloatingPointSize& size, + bool sign); // clang-format off -#if @CVC4_USE_SYMFPU@ -// clang-format on +#if !@CVC4_USE_SYMFPU@ + // clang-format on + /** Catch-all for unimplemented functions. */ + static void unimplemented(void); +#endif - /** Create an FP literal from a symFPU unpacked float. */ - FloatingPointLiteral(SymFPUUnpackedFloatLiteral symuf) : d_symuf(symuf){}; + /** Constructors. */ + + /** Create a FP literal from its IEEE bit-vector representation. */ + FloatingPointLiteral(uint32_t d_exp_size, + uint32_t d_sig_size, + const BitVector& bv); + FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv); + + /** + * Create a FP literal from a signed or unsigned bit-vector value with + * respect to given rounding mode. + */ + FloatingPointLiteral(const FloatingPointSize& size, + const RoundingMode& rm, + const BitVector& bv, + bool signedBV); /** * Create a FP literal from unpacked representation. @@ -305,43 +352,155 @@ class FloatingPointLiteral * representation -- for this, the above constructor is to be used while * creating a SymFPUUnpackedFloatLiteral via symfpu::unpack. */ - FloatingPointLiteral(const bool sign, + FloatingPointLiteral(const FloatingPointSize& size, + const bool sign, const BitVector& exp, const BitVector& sig) - : d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig)) + : d_fp_size(size) +// clang-format off +#if @CVC4_USE_SYMFPU@ + // clang-format on + , + d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig)) +#endif { } -#else - FloatingPointLiteral(uint32_t, uint32_t, double) { unfinished(); }; + +// clang-format off +#if @CVC4_USE_SYMFPU@ + // clang-format on + + /** Create a FP literal from a symFPU unpacked float. */ + FloatingPointLiteral(const FloatingPointSize& size, + SymFPUUnpackedFloatLiteral symuf) + : d_fp_size(size), d_symuf(symuf){}; #endif + ~FloatingPointLiteral() {} + /** Return the size of this FP literal. */ + const FloatingPointSize& getSize() const { return d_fp_size; }; + + /** Return the packed (IEEE-754) representation of this literal. */ + BitVector pack(void) const; + + /** Floating-point absolute value literal. */ + FloatingPointLiteral absolute(void) const; + /** Floating-point negation literal. */ + FloatingPointLiteral negate(void) const; + /** Floating-point addition literal. */ + FloatingPointLiteral add(const RoundingMode& rm, + const FloatingPointLiteral& arg) const; + /** Floating-point subtraction literal. */ + FloatingPointLiteral sub(const RoundingMode& rm, + const FloatingPointLiteral& arg) const; + /** Floating-point multiplication literal. */ + FloatingPointLiteral mult(const RoundingMode& rm, + const FloatingPointLiteral& arg) const; + /** Floating-point division literal. */ + FloatingPointLiteral div(const RoundingMode& rm, + const FloatingPointLiteral& arg) const; + /** Floating-point fused multiplication and addition literal. */ + FloatingPointLiteral fma(const RoundingMode& rm, + const FloatingPointLiteral& arg1, + const FloatingPointLiteral& arg2) const; + /** Floating-point square root literal. */ + FloatingPointLiteral sqrt(const RoundingMode& rm) const; + /** Floating-point round to integral literal. */ + FloatingPointLiteral rti(const RoundingMode& rm) const; + /** Floating-point remainder literal. */ + FloatingPointLiteral rem(const FloatingPointLiteral& arg) const; + + /** + * Floating-point max literal (total version). + * zeroCase: true to return the left (rather than the right operand) in case + * of max(-0,+0) or max(+0,-0). + */ + FloatingPointLiteral maxTotal(const FloatingPointLiteral& arg, + bool zeroCaseLeft) const; + /** + * Floating-point min literal (total version). + * zeroCase: true to return the left (rather than the right operand) in case + * of min(-0,+0) or min(+0,-0). + */ + FloatingPointLiteral minTotal(const FloatingPointLiteral& arg, + bool zeroCaseLeft) const; + + /** Equality literal (NOT: fp.eq but =) over floating-point values. */ + bool operator==(const FloatingPointLiteral& fp) const; + /** Floating-point less or equal than literal. */ + bool operator<=(const FloatingPointLiteral& arg) const; + /** Floating-point less than literal. */ + bool operator<(const FloatingPointLiteral& arg) const; + + /** Get the exponent of this floating-point value. */ + BitVector getExponent() const; + /** Get the significand of this floating-point value. */ + BitVector getSignificand() const; + /** True if this value is a negative value. */ + bool getSign() const; + + /** Return true if this literal represents a normal value. */ + bool isNormal(void) const; + /** Return true if this literal represents a subnormal value. */ + bool isSubnormal(void) const; + /** Return true if this literal represents a zero value. */ + bool isZero(void) const; + /** Return true if this literal represents an infinite value. */ + bool isInfinite(void) const; + /** Return true if this literal represents a NaN value. */ + bool isNaN(void) const; + /** Return true if this literal represents a negative value. */ + bool isNegative(void) const; + /** Return true if this literal represents a positive value. */ + bool isPositive(void) const; + + /** + * Convert this floating-point literal to a literal of given size, with + * respect to given rounding mode. + */ + FloatingPointLiteral convert(const FloatingPointSize& target, + const RoundingMode& rm) const; + + /** + * Convert this floating-point literal to a signed bit-vector of given size, + * with respect to given rounding mode (total version). + * Returns given bit-vector 'undefinedCase' in the undefined case. + */ + BitVector convertToSBVTotal(BitVectorSize width, + const RoundingMode& rm, + BitVector undefinedCase) const; + /** + * Convert this floating-point literal to an unsigned bit-vector of given + * size, with respect to given rounding mode (total version). + * Returns given bit-vector 'undefinedCase' in the undefined case. + */ + BitVector convertToUBVTotal(BitVectorSize width, + const RoundingMode& rm, + BitVector undefinedCase) const; // clang-format off #if @CVC4_USE_SYMFPU@ -// clang-format on + // clang-format on /** Return wrapped floating-point literal. */ const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; } #else - /** Catch-all for unimplemented functions. */ - void unfinished(void) const; /** Dummy hash function. */ size_t hash(void) const; - /** Dummy comparison operator overload. */ - bool operator==(const FloatingPointLiteral& other) const; #endif private: + /** The floating-point size of this floating-point literal. */ + FloatingPointSize d_fp_size; // clang-format off #if @CVC4_USE_SYMFPU@ -// clang-format on + // clang-format on /** The actual floating-point value, a SymFPU unpackedFloat. */ SymFPUUnpackedFloatLiteral d_symuf; #endif }; - /* -------------------------------------------------------------------------- */ -} +} // namespace CVC4 #endif |