From: Aina Niemetz Date: Fri, 20 Nov 2020 22:30:57 +0000 (-0800) Subject: FloatingPoint: Separate out symFPU glue code. (#5492) X-Git-Tag: cvc5-1.0.0~2568 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fedb3256b37511943c4a843327d36da31480be69;p=cvc5.git FloatingPoint: Separate out symFPU glue code. (#5492) This works towards having the symFPU headers only included where it's absolutely needed (only in the .cpp files, not in any other headers). Note: src/util/floatingpoint.h.in will be converted to a regular .h file in the next step to simplify reviewing. --- diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 0d088fe41..f7c58af7b 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -13,11 +13,13 @@ **/ #include "theory/fp/fp_converter.h" -#include "theory/theory.h" -// theory.h Only needed for the leaf test #include +#include "theory/theory.h" // theory.h Only needed for the leaf test +#include "util/floatingpoint.h" +#include "util/symfpu_literal.h" + #ifdef CVC4_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" @@ -919,9 +921,11 @@ Node FpConverter::convert(TNode node) if (current.getKind() == kind::CONST_FLOATINGPOINT) { /******** Constants ********/ - d_fpMap.insert(current, - symfpu::unpackedFloat( - current.getConst().getLiteral())); + d_fpMap.insert( + current, + symfpu::unpackedFloat(current.getConst() + .getLiteral() + ->getSymUF())); } else { @@ -1711,43 +1715,23 @@ Node FpConverter::getValue(Valuation &val, TNode var) #ifdef CVC4_USE_SYMFPU TypeNode t(var.getType()); + Assert(t.isRoundingMode() || t.isFloatingPoint()) + << "Asking for the value of a type that is not managed by the " + "floating-point theory"; + if (t.isRoundingMode()) { rmMap::const_iterator i(d_rmMap.find(var)); - if (i == d_rmMap.end()) - { - Unreachable() << "Asking for the value of an unregistered expression"; - } - else - { - Node value = rmToNode((*i).second); - return value; - } + Assert(i != d_rmMap.end()) + << "Asking for the value of an unregistered expression"; + return rmToNode((*i).second); } - else if (t.isFloatingPoint()) - { - fpMap::const_iterator i(d_fpMap.find(var)); - - if (i == d_fpMap.end()) - { - Unreachable() << "Asking for the value of an unregistered expression"; - } - else - { - Node value = ufToNode(fpt(t), (*i).second); - return value; - } - } - else - { - Unreachable() - << "Asking for the value of a type that is not managed by the " - "floating-point theory"; - } - - Unreachable() << "Unable to find value"; + fpMap::const_iterator i(d_fpMap.find(var)); + Assert(i != d_fpMap.end()) + << "Asking for the value of an unregistered expression"; + return ufToNode(fpt(t), (*i).second); #else Unimplemented() << "Conversion is dependent on SymFPU"; #endif diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index fd4434832..59e65c9e1 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -29,7 +29,7 @@ #include "expr/type.h" #include "theory/valuation.h" #include "util/bitvector.h" -#include "util/floatingpoint.h" +#include "util/floatingpoint_size.h" #include "util/hash.h" #ifdef CVC4_USE_SYMFPU diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 49b4e85c5..b56fa259c 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -887,18 +887,10 @@ namespace constantFold { switch (k) { #ifdef CVC4_USE_SYMFPU - case kind::FLOATINGPOINT_COMPONENT_NAN: - result = arg0.getLiteral().nan; - break; - case kind::FLOATINGPOINT_COMPONENT_INF: - result = arg0.getLiteral().inf; - break; - case kind::FLOATINGPOINT_COMPONENT_ZERO: - result = arg0.getLiteral().zero; - break; - case kind::FLOATINGPOINT_COMPONENT_SIGN: - result = arg0.getLiteral().sign; - break; + case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break; + case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break; + case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break; + case kind::FLOATINGPOINT_COMPONENT_SIGN: result = arg0.getSign(); break; #endif default: Unreachable() << "Unknown kind used in componentFlag"; break; } @@ -919,11 +911,11 @@ namespace constantFold { return RewriteResponse( REWRITE_DONE, #ifdef CVC4_USE_SYMFPU - NodeManager::currentNM()->mkConst((BitVector)arg0.getLiteral().exponent) + NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent()) #else node #endif - ); + ); } RewriteResponse componentSignificand(TNode node, bool) @@ -932,14 +924,14 @@ namespace constantFold { FloatingPoint arg0(node[0].getConst()); - return RewriteResponse(REWRITE_DONE, + return RewriteResponse( + REWRITE_DONE, #ifdef CVC4_USE_SYMFPU - NodeManager::currentNM()->mkConst( - (BitVector)arg0.getLiteral().significand) + NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand()) #else - node + node #endif - ); + ); } RewriteResponse roundingModeBitBlast(TNode node, bool) diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 4d4f3c660..d632e80c8 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -19,6 +19,7 @@ // This is only needed for checking that components are only applied to leaves. #include "theory/theory.h" +#include "util/roundingmode.h" #ifndef CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H #define CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H @@ -693,12 +694,10 @@ class FloatingPointComponentExponent * Here we use types from floatingpoint.h which are the literal * back-end but it should't make a difference. */ FloatingPointSize fps = operandType.getConst(); - symfpuLiteral::CVC4FPSize format(fps); // The symfpu interface to type info - unsigned bw = FloatingPointLiteral::exponentWidth(format); + unsigned bw = FloatingPoint::getUnpackedExponentWidth(fps); #else unsigned bw = 2; #endif - return nodeManager->mkBitVectorType(bw); } }; @@ -736,12 +735,10 @@ class FloatingPointComponentSignificand #ifdef CVC4_USE_SYMFPU /* As before we need to use some of sympfu. */ FloatingPointSize fps = operandType.getConst(); - symfpuLiteral::CVC4FPSize format(fps); - unsigned bw = FloatingPointLiteral::significandWidth(format); + unsigned bw = FloatingPoint::getUnpackedSignificandWidth(fps); #else unsigned bw = 1; #endif - return nodeManager->mkBitVectorType(bw); } }; @@ -771,12 +768,7 @@ class RoundingModeBitBlast } } -#ifdef CVC4_USE_SYMFPU - /* Uses sympfu for the macro. */ - return nodeManager->mkBitVectorType(SYMFPU_NUMBER_OF_ROUNDING_MODES); -#else - return nodeManager->mkBitVectorType(5); -#endif + return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES); } }; diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index ae6197791..4e4b076f0 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -17,12 +17,15 @@ **/ #include "util/floatingpoint.h" -#include "base/check.h" -#include "util/integer.h" #include + #include +#include "base/check.h" +#include "util/integer.h" +#include "util/symfpu_literal.h" + #ifdef CVC4_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" @@ -40,6 +43,8 @@ #include "symfpu/utils/properties.h" #endif +/* -------------------------------------------------------------------------- */ + #ifdef CVC4_USE_SYMFPU namespace symfpu { @@ -64,24 +69,41 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv); } #endif +/* -------------------------------------------------------------------------- */ + namespace CVC4 { -#ifndef CVC4_USE_SYMFPU -void FloatingPointLiteral::unfinished(void) const +/* -------------------------------------------------------------------------- */ + +uint32_t FloatingPoint::getUnpackedExponentWidth(FloatingPointSize& size) { - Unimplemented() << "Floating-point literals not yet implemented."; +#ifdef CVC4_USE_SYMFPU + return SymFPUUnpackedFloatLiteral::exponentWidth(size); +#else + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return 2; +#endif } + +uint32_t FloatingPoint::getUnpackedSignificandWidth(FloatingPointSize& size) +{ +#ifdef CVC4_USE_SYMFPU + return SymFPUUnpackedFloatLiteral::significandWidth(size); +#else + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return 2; #endif +} 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(symfpu::unpack( - symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv)) + d_fpl(new FloatingPointLiteral(symfpu::unpack( + symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv))) #else - d_fpl(d_exp_size, d_sig_size, 0.0) + d_fpl(new FloatingPointLiteral(d_exp_size, d_sig_size, 0.0)) #endif { } @@ -89,23 +111,25 @@ FloatingPoint::FloatingPoint(uint32_t d_exp_size, FloatingPoint::FloatingPoint(const FloatingPointSize& size, const BitVector& bv) : d_fp_size(size), #ifdef CVC4_USE_SYMFPU - d_fpl(symfpu::unpack(size, bv)) + d_fpl(new FloatingPointLiteral( + symfpu::unpack(size, bv))) #else - d_fpl(size.exponentWidth(), size.significandWidth(), 0.0) + d_fpl(new FloatingPointLiteral( + size.exponentWidth(), size.significandWidth(), 0.0)) #endif { } -static FloatingPointLiteral constructorHelperBitVector( - const FloatingPointSize& size, - const RoundingMode& rm, - const BitVector& bv, - bool signedBV) +FloatingPoint::FloatingPoint(const FloatingPointSize& size, + const RoundingMode& rm, + const BitVector& bv, + bool signedBV) + : d_fp_size(size) { #ifdef CVC4_USE_SYMFPU if (signedBV) { - return FloatingPointLiteral( + d_fpl = new FloatingPointLiteral( symfpu::convertSBVToFloat( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), @@ -113,154 +137,174 @@ static FloatingPointLiteral constructorHelperBitVector( } else { - return FloatingPointLiteral( + d_fpl = new FloatingPointLiteral( symfpu::convertUBVToFloat( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), symfpuLiteral::CVC4UnsignedBitVector(bv))); } #else - return FloatingPointLiteral(2, 2, 0.0); + d_fpl = new FloatingPointLiteral(2, 2, 0.0); #endif - Unreachable() << "Constructor helper broken"; } -FloatingPoint::FloatingPoint(const FloatingPointSize& size, - const RoundingMode& rm, - const BitVector& bv, - bool signedBV) - : d_fp_size(size), d_fpl(constructorHelperBitVector(size, rm, bv, signedBV)) +FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size, + const FloatingPointLiteral* fpl) + : d_fp_size(fp_size) +{ + d_fpl = new FloatingPointLiteral(*fpl); +} + +FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size) { + d_fpl = new FloatingPointLiteral(*fp.d_fpl); } -static FloatingPointLiteral constructorHelperRational( - const FloatingPointSize& size, const RoundingMode& rm, const Rational& ri) +FloatingPoint::FloatingPoint(const FloatingPointSize& size, + const RoundingMode& rm, + const Rational& r) + : d_fp_size(size) { - Rational r(ri); Rational two(2, 1); if (r.isZero()) { #ifdef CVC4_USE_SYMFPU - return FloatingPointLiteral::makeZero( - size, false); // In keeping with the SMT-LIB standard + // In keeping with the SMT-LIB standard + d_fpl = new FloatingPointLiteral( + SymFPUUnpackedFloatLiteral::makeZero(size, false)); #else - return FloatingPointLiteral(2,2,0.0); + d_fpl = new FloatingPointLiteral(2, 2, 0.0); #endif - } else { + } + else + { #ifdef CVC4_USE_SYMFPU - uint32_t negative = (r.sgn() < 0) ? 1 : 0; + uint32_t negative = (r.sgn() < 0) ? 1 : 0; #endif - r = r.abs(); - - // Compute the exponent - Integer exp(0U); - Integer inc(1U); - Rational working(1,1); + Rational rabs(r.abs()); - if (r == working) { + // Compute the exponent + Integer exp(0U); + Integer inc(1U); + Rational working(1, 1); - } else if ( r < working ) { - while (r < working) { - exp -= inc; - working /= two; - } - } else { - while (r >= working) { - exp += inc; - working *= two; - } - exp -= inc; - working /= two; + if (rabs != working) + { + if (rabs < working) + { + while (rabs < working) + { + exp -= inc; + working /= two; + } } - - Assert(working <= r); - Assert(r < working * two); - - // Work out the number of bits required to represent the exponent for a normal number - uint32_t expBits = 2; // No point starting with an invalid amount - - Integer doubleInt(2); - if (exp.strictlyPositive()) { - Integer representable(4); // 1 more than exactly representable with expBits - while (representable <= exp) {// hence <= - representable *= doubleInt; - ++expBits; - } - } else if (exp.strictlyNegative()) { - Integer representable(-4); // Exactly representable with expBits + sign - // but -2^n and -(2^n - 1) are both subnormal - while ((representable + doubleInt) > exp) { - representable *= doubleInt; - ++expBits; - } + else + { + while (rabs >= working) + { + exp += inc; + working *= two; + } + exp -= inc; + working /= two; } - ++expBits; // To allow for sign + } + + Assert(working <= rabs); + Assert(rabs < working * two); - BitVector exactExp(expBits, exp); + // Work out the number of bits required to represent the exponent for a + // normal number + uint32_t expBits = 2; // No point starting with an invalid amount - // Compute the significand. - uint32_t sigBits = size.significandWidth() + 2; // guard and sticky bits - BitVector sig(sigBits, 0U); - BitVector one(sigBits, 1U); - Rational workingSig(0,1); - for (uint32_t i = 0; i < sigBits - 1; ++i) + Integer doubleInt(2); + if (exp.strictlyPositive()) + { + // 1 more than exactly representable with expBits + Integer representable(4); + while (representable <= exp) + { // hence <= + representable *= doubleInt; + ++expBits; + } + } + else if (exp.strictlyNegative()) + { + Integer representable(-4); // Exactly representable with expBits + sign + // but -2^n and -(2^n - 1) are both subnormal + while ((representable + doubleInt) > exp) { - Rational mid(workingSig + working); + representable *= doubleInt; + ++expBits; + } + } + ++expBits; // To allow for sign - if (mid <= r) { - sig = sig | one; - workingSig = mid; - } + BitVector exactExp(expBits, exp); - sig = sig.leftShift(one); - working /= two; + // Compute the significand. + uint32_t sigBits = size.significandWidth() + 2; // guard and sticky bits + BitVector sig(sigBits, 0U); + BitVector one(sigBits, 1U); + Rational workingSig(0, 1); + for (uint32_t i = 0; i < sigBits - 1; ++i) + { + Rational mid(workingSig + working); + + if (mid <= rabs) + { + sig = sig | one; + workingSig = mid; } - // Compute the sticky bit - Rational remainder(r - workingSig); - Assert(Rational(0, 1) <= remainder); + sig = sig.leftShift(one); + working /= two; + } - if (!remainder.isZero()) { - sig = sig | one; - } + // Compute the sticky bit + Rational remainder(rabs - workingSig); + Assert(Rational(0, 1) <= remainder); + + if (!remainder.isZero()) + { + sig = sig | one; + } - // Build an exact float - FloatingPointSize exactFormat(expBits, sigBits); + // Build an exact float + FloatingPointSize exactFormat(expBits, sigBits); - // A small subtlety... if the format has expBits the unpacked format - // may have more to allow subnormals to be normalised. - // Thus... + // 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 = - FloatingPointLiteral::exponentWidth(exactFormat) - expBits; + uint32_t extension = + SymFPUUnpackedFloatLiteral::exponentWidth(exactFormat) - expBits; - FloatingPointLiteral exactFloat( - negative, exactExp.signExtend(extension), sig); + FloatingPointLiteral exactFloat( + negative, exactExp.signExtend(extension), sig); - // Then cast... - FloatingPointLiteral rounded( - symfpu::convertFloatToFloat(exactFormat, size, rm, exactFloat)); - return rounded; + // Then cast... + d_fpl = new FloatingPointLiteral( + symfpu::convertFloatToFloat(exactFormat, size, rm, exactFloat.d_symuf)); #else - Unreachable() << "no concrete implementation of FloatingPointLiteral"; + Unreachable() << "no concrete implementation of FloatingPointLiteral"; #endif - } - Unreachable() << "Constructor helper broken"; + } } -FloatingPoint::FloatingPoint(const FloatingPointSize& size, - const RoundingMode& rm, - const Rational& r) - : d_fp_size(size), d_fpl(constructorHelperRational(size, rm, r)) +FloatingPoint::~FloatingPoint() { + delete d_fpl; + d_fpl = nullptr; } FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size) { #ifdef CVC4_USE_SYMFPU return FloatingPoint( - size, symfpu::unpackedFloat::makeNaN(size)); + size, + new FloatingPointLiteral(SymFPUUnpackedFloatLiteral::makeNaN(size))); #else return FloatingPoint(2, 2, BitVector(4U, 0U)); #endif @@ -269,8 +313,9 @@ FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size) FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign) { #ifdef CVC4_USE_SYMFPU - return FloatingPoint( - size, symfpu::unpackedFloat::makeInf(size, sign)); + return FloatingPoint(size, + new FloatingPointLiteral( + SymFPUUnpackedFloatLiteral::makeInf(size, sign))); #else return FloatingPoint(2, 2, BitVector(4U, 0U)); #endif @@ -279,8 +324,9 @@ FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign) FloatingPoint FloatingPoint::makeZero(const FloatingPointSize& size, bool sign) { #ifdef CVC4_USE_SYMFPU - return FloatingPoint( - size, symfpu::unpackedFloat::makeZero(size, sign)); + return FloatingPoint(size, + new FloatingPointLiteral( + SymFPUUnpackedFloatLiteral::makeZero(size, sign))); #else return FloatingPoint(2, 2, BitVector(4U, 0U)); #endif @@ -328,7 +374,9 @@ FloatingPoint FloatingPoint::absolute(void) const { #ifdef CVC4_USE_SYMFPU return FloatingPoint( - d_fp_size, symfpu::absolute(d_fp_size, d_fpl)); + d_fp_size, + new FloatingPointLiteral( + symfpu::absolute(d_fp_size, d_fpl->d_symuf))); #else return *this; #endif @@ -337,8 +385,10 @@ FloatingPoint FloatingPoint::absolute(void) const FloatingPoint FloatingPoint::negate(void) const { #ifdef CVC4_USE_SYMFPU - return FloatingPoint(d_fp_size, - symfpu::negate(d_fp_size, d_fpl)); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral( + symfpu::negate(d_fp_size, d_fpl->d_symuf))); #else return *this; #endif @@ -348,10 +398,11 @@ FloatingPoint FloatingPoint::plus(const RoundingMode& rm, const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::add( - d_fp_size, rm, d_fpl, arg.d_fpl, true)); + Assert(d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral(symfpu::add( + d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, true))); #else return *this; #endif @@ -361,10 +412,11 @@ FloatingPoint FloatingPoint::sub(const RoundingMode& rm, const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::add( - d_fp_size, rm, d_fpl, arg.d_fpl, false)); + Assert(d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral(symfpu::add( + d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf, false))); #else return *this; #endif @@ -374,10 +426,11 @@ FloatingPoint FloatingPoint::mult(const RoundingMode& rm, const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); + Assert(d_fp_size == arg.d_fp_size); return FloatingPoint( d_fp_size, - symfpu::multiply(d_fp_size, rm, d_fpl, arg.d_fpl)); + new FloatingPointLiteral(symfpu::multiply( + d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf))); #else return *this; #endif @@ -388,11 +441,16 @@ FloatingPoint FloatingPoint::fma(const RoundingMode& rm, const FloatingPoint& arg2) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg1.d_fp_size); - Assert(this->d_fp_size == arg2.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::fma( - d_fp_size, rm, d_fpl, arg1.d_fpl, arg2.d_fpl)); + 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(d_fp_size, + rm, + d_fpl->d_symuf, + arg1.d_fpl->d_symuf, + arg2.d_fpl->d_symuf))); #else return *this; #endif @@ -402,10 +460,11 @@ FloatingPoint FloatingPoint::div(const RoundingMode& rm, const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); + Assert(d_fp_size == arg.d_fp_size); return FloatingPoint( d_fp_size, - symfpu::divide(d_fp_size, rm, d_fpl, arg.d_fpl)); + new FloatingPointLiteral(symfpu::divide( + d_fp_size, rm, d_fpl->d_symuf, arg.d_fpl->d_symuf))); #else return *this; #endif @@ -415,7 +474,9 @@ FloatingPoint FloatingPoint::sqrt(const RoundingMode& rm) const { #ifdef CVC4_USE_SYMFPU return FloatingPoint( - d_fp_size, symfpu::sqrt(d_fp_size, rm, d_fpl)); + d_fp_size, + new FloatingPointLiteral( + symfpu::sqrt(d_fp_size, rm, d_fpl->d_symuf))); #else return *this; #endif @@ -426,7 +487,8 @@ FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const #ifdef CVC4_USE_SYMFPU return FloatingPoint( d_fp_size, - symfpu::roundToIntegral(d_fp_size, rm, d_fpl)); + new FloatingPointLiteral(symfpu::roundToIntegral( + d_fp_size, rm, d_fpl->d_symuf))); #else return *this; #endif @@ -435,10 +497,11 @@ FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const FloatingPoint FloatingPoint::rem(const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); + Assert(d_fp_size == arg.d_fp_size); return FloatingPoint( d_fp_size, - symfpu::remainder(d_fp_size, d_fpl, arg.d_fpl)); + new FloatingPointLiteral(symfpu::remainder( + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf))); #else return *this; #endif @@ -448,10 +511,11 @@ FloatingPoint FloatingPoint::maxTotal(const FloatingPoint& arg, bool zeroCaseLeft) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::max( - d_fp_size, d_fpl, arg.d_fpl, zeroCaseLeft)); + Assert(d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral(symfpu::max( + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft))); #else return *this; #endif @@ -461,10 +525,11 @@ FloatingPoint FloatingPoint::minTotal(const FloatingPoint& arg, bool zeroCaseLeft) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return FloatingPoint(d_fp_size, - symfpu::min( - d_fp_size, d_fpl, arg.d_fpl, zeroCaseLeft)); + Assert(d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + new FloatingPointLiteral(symfpu::min( + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf, zeroCaseLeft))); #else return *this; #endif @@ -489,7 +554,7 @@ bool FloatingPoint::operator==(const FloatingPoint& fp) const #ifdef CVC4_USE_SYMFPU return ((d_fp_size == fp.d_fp_size) && symfpu::smtlibEqual( - d_fp_size, d_fpl, fp.d_fpl)); + d_fp_size, d_fpl->d_symuf, fp.d_fpl->d_symuf)); #else return ((d_fp_size == fp.d_fp_size)); #endif @@ -498,9 +563,9 @@ bool FloatingPoint::operator==(const FloatingPoint& fp) const bool FloatingPoint::operator<=(const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); + Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThanOrEqual( - d_fp_size, d_fpl, arg.d_fpl); + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf); #else return false; #endif @@ -509,9 +574,40 @@ bool FloatingPoint::operator<=(const FloatingPoint& arg) const bool FloatingPoint::operator<(const FloatingPoint& arg) const { #ifdef CVC4_USE_SYMFPU - Assert(this->d_fp_size == arg.d_fp_size); - return symfpu::lessThan(d_fp_size, d_fpl, arg.d_fpl); + Assert(d_fp_size == arg.d_fp_size); + return symfpu::lessThan( + d_fp_size, d_fpl->d_symuf, arg.d_fpl->d_symuf); +#else + return false; +#endif +} + +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::getSignificand() const +{ +#ifdef CVC4_USE_SYMFPU + return d_fpl->d_symuf.significand; +#else + Unreachable() << "no concrete implementation of FloatingPointLiteral"; + return BitVector(); +#endif +} + +bool FloatingPoint::getSign() const +{ +#ifdef CVC4_USE_SYMFPU + return d_fpl->d_symuf.sign; #else + Unreachable() << "no concrete implementation of FloatingPointLiteral"; return false; #endif } @@ -519,7 +615,7 @@ bool FloatingPoint::operator<(const FloatingPoint& arg) const bool FloatingPoint::isNormal(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isNormal(d_fp_size, d_fpl); + return symfpu::isNormal(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -528,7 +624,7 @@ bool FloatingPoint::isNormal(void) const bool FloatingPoint::isSubnormal(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isSubnormal(d_fp_size, d_fpl); + return symfpu::isSubnormal(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -537,7 +633,7 @@ bool FloatingPoint::isSubnormal(void) const bool FloatingPoint::isZero(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isZero(d_fp_size, d_fpl); + return symfpu::isZero(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -546,7 +642,7 @@ bool FloatingPoint::isZero(void) const bool FloatingPoint::isInfinite(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isInfinite(d_fp_size, d_fpl); + return symfpu::isInfinite(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -555,7 +651,7 @@ bool FloatingPoint::isInfinite(void) const bool FloatingPoint::isNaN(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isNaN(d_fp_size, d_fpl); + return symfpu::isNaN(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -564,7 +660,7 @@ bool FloatingPoint::isNaN(void) const bool FloatingPoint::isNegative(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isNegative(d_fp_size, d_fpl); + return symfpu::isNegative(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -573,7 +669,7 @@ bool FloatingPoint::isNegative(void) const bool FloatingPoint::isPositive(void) const { #ifdef CVC4_USE_SYMFPU - return symfpu::isPositive(d_fp_size, d_fpl); + return symfpu::isPositive(d_fp_size, d_fpl->d_symuf); #else return false; #endif @@ -584,8 +680,9 @@ FloatingPoint FloatingPoint::convert(const FloatingPointSize& target, { #ifdef CVC4_USE_SYMFPU return FloatingPoint(target, - symfpu::convertFloatToFloat( - d_fp_size, target, rm, d_fpl)); + new FloatingPointLiteral( + symfpu::convertFloatToFloat( + d_fp_size, target, rm, d_fpl->d_symuf))); #else return *this; #endif @@ -599,10 +696,10 @@ BitVector FloatingPoint::convertToBVTotal(BitVectorSize width, #ifdef CVC4_USE_SYMFPU if (signedBV) return symfpu::convertFloatToSBV( - d_fp_size, rm, d_fpl, width, undefinedCase); + d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase); else return symfpu::convertFloatToUBV( - d_fp_size, rm, d_fpl, width, undefinedCase); + d_fp_size, rm, d_fpl->d_symuf, width, undefinedCase); #else return undefinedCase; #endif @@ -627,23 +724,23 @@ FloatingPoint::PartialBitVector FloatingPoint::convertToBV( FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const { - if (this->isNaN() || this->isInfinite()) + if (isNaN() || isInfinite()) { return PartialRational(Rational(0U, 1U), false); } - if (this->isZero()) + if (isZero()) { return PartialRational(Rational(0U, 1U), true); } else { #ifdef CVC4_USE_SYMFPU - Integer sign((this->d_fpl.getSign()) ? -1 : 1); + Integer sign((d_fpl->d_symuf.getSign()) ? -1 : 1); Integer exp( - this->d_fpl.getExponent().toSignedInteger() + d_fpl->d_symuf.getExponent().toSignedInteger() - (Integer(d_fp_size.significandWidth() - 1))); // -1 as forcibly normalised into the [1,2) range - Integer significand(this->d_fpl.getSignificand().toInteger()); + Integer significand(d_fpl->d_symuf.getSignificand().toInteger()); #else Integer sign(0); Integer exp(0); @@ -682,8 +779,7 @@ FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const BitVector FloatingPoint::pack(void) const { #ifdef CVC4_USE_SYMFPU - BitVector bv( - symfpu::pack(this->d_fp_size, this->d_fpl)); + BitVector bv(symfpu::pack(d_fp_size, d_fpl->d_symuf)); #else BitVector bv(4u, 0u); #endif diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in index bcf792c56..04279d8e5 100644 --- a/src/util/floatingpoint.h.in +++ b/src/util/floatingpoint.h.in @@ -24,13 +24,6 @@ #include "util/floatingpoint_size.h" #include "util/rational.h" #include "util/roundingmode.h" -#include "util/symfpu_literal.h" - -// clang-format off -#if @CVC4_USE_SYMFPU@ -// clang-format on -#include -#endif /* @CVC4_USE_SYMFPU@ */ /* -------------------------------------------------------------------------- */ @@ -38,37 +31,7 @@ namespace CVC4 { /* -------------------------------------------------------------------------- */ -/** - * A concrete floating point value. - */ -// clang-format off -#if @CVC4_USE_SYMFPU@ -// clang-format on -using FloatingPointLiteral = ::symfpu::unpackedFloat; -#else -class CVC4_PUBLIC FloatingPointLiteral -{ - public: - // This intentional left unfinished as the choice of literal - // representation is solver specific. - void unfinished(void) const; - - FloatingPointLiteral(uint32_t, uint32_t, double) { unfinished(); } - FloatingPointLiteral(uint32_t, uint32_t, const std::string&) { unfinished(); } - FloatingPointLiteral(const FloatingPointLiteral&) { unfinished(); } - bool operator==(const FloatingPointLiteral& op) const - { - unfinished(); - return false; - } - - size_t hash(void) const - { - unfinished(); - return 23; - } -}; -#endif /* @CVC4_USE_SYMFPU@ */ +class FloatingPointLiteral; class CVC4_PUBLIC FloatingPoint { @@ -81,20 +44,25 @@ class CVC4_PUBLIC FloatingPoint using PartialBitVector = std::pair; using PartialRational = std::pair; + /** + * Get the number of exponent bits in the unpacked format corresponding to a + * given packed format. These is the unpacked counter-parts 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 + * FloatingPointSize::significandWidth(). + */ + static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size); + /** Constructors. */ FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv); FloatingPoint(const FloatingPointSize& size, const BitVector& bv); - FloatingPoint(const FloatingPointSize& fp_size, - const FloatingPointLiteral& fpl) - : d_fp_size(fp_size), d_fpl(fpl) - { - } - - FloatingPoint(const FloatingPoint& fp) - : d_fp_size(fp.d_fp_size), d_fpl(fp.d_fpl) - { - } + const FloatingPointLiteral* fpl); + FloatingPoint(const FloatingPoint& fp); FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, const BitVector& bv, @@ -102,6 +70,8 @@ class CVC4_PUBLIC FloatingPoint FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, const Rational& r); + /** Destructor. */ + ~FloatingPoint(); /** * Create a FP NaN value of given size. @@ -148,7 +118,7 @@ class CVC4_PUBLIC FloatingPoint static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign); /** Get the wrapped floating-point value. */ - const FloatingPointLiteral& getLiteral(void) const { return this->d_fpl; } + const FloatingPointLiteral* getLiteral(void) const { return d_fpl; } /** * Return a string representation of this floating-point. @@ -220,6 +190,13 @@ class CVC4_PUBLIC FloatingPoint /** Floating-point less than. */ bool operator<(const FloatingPoint& 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 floating-point represents a normal value. */ bool isNormal(void) const; /** Return true if this floating-point represents a subnormal value. */ @@ -280,9 +257,9 @@ class CVC4_PUBLIC FloatingPoint /** The floating-point size of this floating-point value. */ FloatingPointSize d_fp_size; - protected: + private: /** The floating-point literal of this floating-point value. */ - FloatingPointLiteral d_fpl; + FloatingPointLiteral* d_fpl; }; /* class FloatingPoint */ diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h index 181755a60..245654a53 100644 --- a/src/util/roundingmode.h +++ b/src/util/roundingmode.h @@ -10,9 +10,6 @@ ** directory for licensing information.\endverbatim ** ** \brief The definition of rounding mode values. - ** - ** [[ Add lengthier description here ]] - ** \todo document this file **/ #include "cvc4_public.h" @@ -23,6 +20,8 @@ namespace CVC4 { +#define CVC4_NUM_ROUNDING_MODES 5 + /** * A concrete instance of the rounding mode sort */ diff --git a/src/util/symfpu_literal.cpp b/src/util/symfpu_literal.cpp index a547daccd..46d3cbe40 100644 --- a/src/util/symfpu_literal.cpp +++ b/src/util/symfpu_literal.cpp @@ -17,6 +17,25 @@ namespace CVC4 { +#ifndef CVC4_USE_SYMFPU +void FloatingPointLiteral::unfinished(void) const +{ + Unimplemented() << "Floating-point literals not yet implemented."; +} + +bool FloatingPointLiteral::operator==(const FloatingPointLiteral& other) const +{ + unfinished(); + return false; +} + +size_t FloatingPointLiteral::hash(void) const +{ + unfinished(); + return 23; +} +#endif + namespace symfpuLiteral { // To simplify the property macros diff --git a/src/util/symfpu_literal.h.in b/src/util/symfpu_literal.h.in index e0cd95d52..e477bb0c1 100644 --- a/src/util/symfpu_literal.h.in +++ b/src/util/symfpu_literal.h.in @@ -10,6 +10,8 @@ ** directory for licensing information.\endverbatim ** ** \brief SymFPU glue code for floating-point values. + ** + ** !!! This header is not to be included in any other headers !!! **/ #include "cvc4_public.h" @@ -25,9 +27,14 @@ #include #endif /* @CVC4_USE_SYMFPU@ */ +/* -------------------------------------------------------------------------- */ + namespace CVC4 { class FloatingPointSize; +class FloatingPoint; + +/* -------------------------------------------------------------------------- */ /** * This is a symfpu literal "back-end". It allows the library to be used as @@ -37,6 +44,8 @@ class FloatingPointSize; */ namespace symfpuLiteral { +/* -------------------------------------------------------------------------- */ + /** * Forward declaration of wrapper so that traits can be defined early and so * used in the implementation of wrappedBitVector. @@ -253,7 +262,66 @@ class wrappedBitVector : public BitVector wrappedBitVector extract(CVC4BitWidth upper, CVC4BitWidth lower) const; }; + +/* -------------------------------------------------------------------------- */ + } // namespace symfpuLiteral + +/* -------------------------------------------------------------------------- */ + +// clang-format off +#if @CVC4_USE_SYMFPU@ +// clang-format on +using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat; +#endif + +class FloatingPointLiteral +{ + friend class FloatingPoint; + public: + /** Constructors. */ + FloatingPointLiteral(FloatingPoint& other); +// clang-format off +#if @CVC4_USE_SYMFPU@ +// clang-format on + FloatingPointLiteral(SymFPUUnpackedFloatLiteral symuf) : d_symuf(symuf){}; + FloatingPointLiteral(const bool sign, + const BitVector& exp, + const BitVector& sig) + : d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig)) + { + } +#else + FloatingPointLiteral(uint32_t, uint32_t, double) { unfinished(); }; +#endif + ~FloatingPointLiteral() {} + +// clang-format off +#if @CVC4_USE_SYMFPU@ +// 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: +// clang-format off +#if @CVC4_USE_SYMFPU@ +// clang-format on + /** The actual floating-point value, a SymFPU unpackedFloat. */ + SymFPUUnpackedFloatLiteral d_symuf; +#endif +}; + + +/* -------------------------------------------------------------------------- */ + } #endif