From: Aina Niemetz Date: Wed, 18 Nov 2020 00:45:39 +0000 (-0800) Subject: FloatingPoint: Clean up and document header, format. (#5453) X-Git-Tag: cvc5-1.0.0~2591 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4bdba195950858dc1b2b9afa80d216dc58c66b68;p=cvc5.git FloatingPoint: Clean up and document header, format. (#5453) This cleans up the src/util/floatingpoint.h.in header to conform to the code style guidelines of CVC4. This further attempts to fully document the header. The main changes (except for added documentation) are renames of member variables, getting rid of the redundant functions FloatingPointSize::exponent() and FloatingPointSize::significand(), and a more explicit naming of CVC4 wrapper types vs symFPU trait types. Else, it's mainly reordering and formatting. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 24902b888..a7cc8e17f 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1433,10 +1433,10 @@ uint32_t Op::getIndices() const case INT_TO_BITVECTOR: i = d_node->getConst().d_size; break; case IAND: i = d_node->getConst().d_size; break; case FLOATINGPOINT_TO_UBV: - i = d_node->getConst().bvs.d_size; + i = d_node->getConst().d_bv_size.d_size; break; case FLOATINGPOINT_TO_SBV: - i = d_node->getConst().bvs.d_size; + i = d_node->getConst().d_bv_size.d_size; break; case TUPLE_UPDATE: i = d_node->getConst().getIndex(); break; case REGEXP_REPEAT: @@ -1469,36 +1469,42 @@ std::pair Op::getIndices() const { CVC4::FloatingPointToFPIEEEBitVector ext = d_node->getConst(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) { CVC4::FloatingPointToFPFloatingPoint ext = d_node->getConst(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_REAL) { CVC4::FloatingPointToFPReal ext = d_node->getConst(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) { CVC4::FloatingPointToFPSignedBitVector ext = d_node->getConst(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) { CVC4::FloatingPointToFPUnsignedBitVector ext = d_node->getConst(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_GENERIC) { CVC4::FloatingPointToFPGeneric ext = d_node->getConst(); - indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + indices = std::make_pair(ext.d_fp_size.exponentWidth(), + ext.d_fp_size.significandWidth()); } else if (k == REGEXP_LOOP) { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 90c1daf24..895e05093 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -1073,10 +1073,9 @@ inline bool TypeNode::isTester() const { /** Is this a floating-point type of with exp exponent bits and sig significand bits */ inline bool TypeNode::isFloatingPoint(unsigned exp, unsigned sig) const { - return - ( getKind() == kind::FLOATINGPOINT_TYPE && - getConst().exponent() == exp && - getConst().significand() == sig ); + return (getKind() == kind::FLOATINGPOINT_TYPE + && getConst().exponentWidth() == exp + && getConst().significandWidth() == sig); } /** Is this a bit-vector type of size size */ @@ -1088,13 +1087,13 @@ inline bool TypeNode::isBitVector(unsigned size) const { /** Get the exponent size of this floating-point type */ inline unsigned TypeNode::getFloatingPointExponentSize() const { Assert(isFloatingPoint()); - return getConst().exponent(); + return getConst().exponentWidth(); } /** Get the significand size of this floating-point type */ inline unsigned TypeNode::getFloatingPointSignificandSize() const { Assert(isFloatingPoint()); - return getConst().significand(); + return getConst().significandWidth(); } /** Get the size of this bit-vector type */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d44842633..6628576dd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -183,9 +183,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const break; case kind::FLOATINGPOINT_TYPE: out << "(_ FloatingPoint " - << n.getConst().exponent() << " " - << n.getConst().significand() - << ")"; + << n.getConst().exponentWidth() << " " + << n.getConst().significandWidth() << ")"; break; case kind::CONST_BITVECTOR: { @@ -353,53 +352,69 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: out << "(_ to_fp " - << n.getConst().t.exponent() << ' ' - << n.getConst().t.significand() + << n.getConst() + .d_fp_size.exponentWidth() + << ' ' + << n.getConst() + .d_fp_size.significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: out << "(_ to_fp " - << n.getConst().t.exponent() << ' ' - << n.getConst().t.significand() + << n.getConst() + .d_fp_size.exponentWidth() + << ' ' + << n.getConst() + .d_fp_size.significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_REAL_OP: - out << "(_ to_fp " << n.getConst().t.exponent() - << ' ' << n.getConst().t.significand() << ")"; + out << "(_ to_fp " + << n.getConst().d_fp_size.exponentWidth() + << ' ' + << n.getConst().d_fp_size.significandWidth() + << ")"; break; case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: out << "(_ to_fp " - << n.getConst().t.exponent() << ' ' - << n.getConst().t.significand() + << n.getConst() + .d_fp_size.exponentWidth() + << ' ' + << n.getConst() + .d_fp_size.significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: out << "(_ to_fp_unsigned " - << n.getConst().t.exponent() + << n.getConst() + .d_fp_size.exponentWidth() << ' ' - << n.getConst().t.significand() + << n.getConst() + .d_fp_size.significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: - out << "(_ to_fp " << n.getConst().t.exponent() - << ' ' << n.getConst().t.significand() + out << "(_ to_fp " + << n.getConst().d_fp_size.exponentWidth() + << ' ' + << n.getConst().d_fp_size.significandWidth() << ")"; break; case kind::FLOATINGPOINT_TO_UBV_OP: - out << "(_ fp.to_ubv " << n.getConst().bvs.d_size - << ")"; + out << "(_ fp.to_ubv " + << n.getConst().d_bv_size.d_size << ")"; break; case kind::FLOATINGPOINT_TO_SBV_OP: - out << "(_ fp.to_sbv " << n.getConst().bvs.d_size - << ")"; + out << "(_ fp.to_sbv " + << n.getConst().d_bv_size.d_size << ")"; break; case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: out << "(_ fp.to_ubv_total " - << n.getConst().bvs.d_size << ")"; + << n.getConst().d_bv_size.d_size << ")"; break; case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: out << "(_ fp.to_sbv_total " - << n.getConst().bvs.d_size << ")"; + << n.getConst().d_bv_size.d_size << ")"; break; case kind::REGEXP_REPEAT_OP: out << "(_ re.^ " << n.getConst().d_repeatAmount << ")"; diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 47a4af43e..0d088fe41 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -1578,7 +1578,7 @@ Node FpConverter::convert(TNode node) symfpu::convertFloatToUBV(fpt(childType), (*mode).second, (*arg1).second, - info.bvs, + info.d_bv_size, ubv(current[2]))); i = d_ubvMap.find(current); } @@ -1620,7 +1620,7 @@ Node FpConverter::convert(TNode node) symfpu::convertFloatToSBV(fpt(childType), (*mode).second, (*arg1).second, - info.bvs, + info.d_bv_size, sbv(current[2]))); i = d_sbvMap.find(current); diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 120f71b6d..49b4e85c5 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -369,7 +369,7 @@ namespace constantFold { FloatingPoint arg1(node[1].getConst()); FloatingPoint arg2(node[2].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2))); } @@ -382,7 +382,7 @@ namespace constantFold { FloatingPoint arg1(node[1].getConst()); FloatingPoint arg2(node[2].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.mult(rm, arg2))); } @@ -396,8 +396,8 @@ namespace constantFold { FloatingPoint arg2(node[2].getConst()); FloatingPoint arg3(node[3].getConst()); - Assert(arg1.t == arg2.t); - Assert(arg1.t == arg3.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); + Assert(arg1.d_fp_size == arg3.d_fp_size); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.fma(rm, arg2, arg3))); } @@ -410,7 +410,7 @@ namespace constantFold { FloatingPoint arg1(node[1].getConst()); FloatingPoint arg2(node[2].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.div(rm, arg2))); } @@ -442,7 +442,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst()); FloatingPoint arg2(node[1].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.rem(arg2))); } @@ -454,7 +454,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst()); FloatingPoint arg2(node[1].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); FloatingPoint::PartialFloatingPoint res(arg1.min(arg2)); @@ -474,7 +474,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst()); FloatingPoint arg2(node[1].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); FloatingPoint::PartialFloatingPoint res(arg1.max(arg2)); @@ -494,7 +494,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst()); FloatingPoint arg2(node[1].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); // Can be called with the third argument non-constant if (node[2].getMetaKind() == kind::metakind::CONSTANT) { @@ -524,7 +524,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst()); FloatingPoint arg2(node[1].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); // Can be called with the third argument non-constant if (node[2].getMetaKind() == kind::metakind::CONSTANT) { @@ -558,7 +558,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst()); FloatingPoint arg2(node[1].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2)); @@ -580,7 +580,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst()); FloatingPoint arg2(node[1].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 <= arg2)); } @@ -593,7 +593,7 @@ namespace constantFold { FloatingPoint arg1(node[0].getConst()); FloatingPoint arg2(node[1].getConst()); - Assert(arg1.t == arg2.t); + Assert(arg1.d_fp_size == arg2.d_fp_size); return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 < arg2)); } @@ -654,12 +654,12 @@ namespace constantFold { TNode op = node.getOperator(); const FloatingPointToFPIEEEBitVector ¶m = op.getConst(); const BitVector &bv = node[0].getConst(); - - Node lit = - NodeManager::currentNM()->mkConst(FloatingPoint(param.t.exponent(), - param.t.significand(), - bv)); - + + Node lit = NodeManager::currentNM()->mkConst( + FloatingPoint(param.d_fp_size.exponentWidth(), + param.d_fp_size.significandWidth(), + bv)); + return RewriteResponse(REWRITE_DONE, lit); } @@ -671,7 +671,9 @@ namespace constantFold { FloatingPoint arg1(node[1].getConst()); FloatingPointToFPFloatingPoint info = node.getOperator().getConst(); - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.convert(info.t,rm))); + return RewriteResponse( + REWRITE_DONE, + NodeManager::currentNM()->mkConst(arg1.convert(info.d_fp_size, rm))); } RewriteResponse convertFromRealLiteral (TNode node, bool) { @@ -683,8 +685,8 @@ namespace constantFold { RoundingMode rm(node[0].getConst()); Rational arg(node[1].getConst()); - FloatingPoint res(param.t, rm, arg); - + FloatingPoint res(param.d_fp_size, rm, arg); + Node lit = NodeManager::currentNM()->mkConst(res); return RewriteResponse(REWRITE_DONE, lit); @@ -699,8 +701,8 @@ namespace constantFold { RoundingMode rm(node[0].getConst()); BitVector arg(node[1].getConst()); - FloatingPoint res(param.t, rm, arg, true); - + FloatingPoint res(param.d_fp_size, rm, arg, true); + Node lit = NodeManager::currentNM()->mkConst(res); return RewriteResponse(REWRITE_DONE, lit); @@ -715,8 +717,8 @@ namespace constantFold { RoundingMode rm(node[0].getConst()); BitVector arg(node[1].getConst()); - FloatingPoint res(param.t, rm, arg, false); - + FloatingPoint res(param.d_fp_size, rm, arg, false); + Node lit = NodeManager::currentNM()->mkConst(res); return RewriteResponse(REWRITE_DONE, lit); @@ -731,7 +733,8 @@ namespace constantFold { RoundingMode rm(node[0].getConst()); FloatingPoint arg(node[1].getConst()); - FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, false)); + FloatingPoint::PartialBitVector res( + arg.convertToBV(param.d_bv_size, rm, false)); if (res.second) { Node lit = NodeManager::currentNM()->mkConst(res.first); @@ -751,7 +754,8 @@ namespace constantFold { RoundingMode rm(node[0].getConst()); FloatingPoint arg(node[1].getConst()); - FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, true)); + FloatingPoint::PartialBitVector res( + arg.convertToBV(param.d_bv_size, rm, true)); if (res.second) { Node lit = NodeManager::currentNM()->mkConst(res.first); @@ -791,12 +795,14 @@ namespace constantFold { if (node[2].getMetaKind() == kind::metakind::CONSTANT) { BitVector partialValue(node[2].getConst()); - BitVector folded(arg.convertToBVTotal(param.bvs, rm, false, partialValue)); + BitVector folded( + arg.convertToBVTotal(param.d_bv_size, rm, false, partialValue)); Node lit = NodeManager::currentNM()->mkConst(folded); return RewriteResponse(REWRITE_DONE, lit); } else { - FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, false)); + FloatingPoint::PartialBitVector res( + arg.convertToBV(param.d_bv_size, rm, false)); if (res.second) { Node lit = NodeManager::currentNM()->mkConst(res.first); @@ -821,13 +827,14 @@ namespace constantFold { if (node[2].getMetaKind() == kind::metakind::CONSTANT) { BitVector partialValue(node[2].getConst()); - BitVector folded(arg.convertToBVTotal(param.bvs, rm, true, partialValue)); + BitVector folded( + arg.convertToBVTotal(param.d_bv_size, rm, true, partialValue)); Node lit = NodeManager::currentNM()->mkConst(folded); return RewriteResponse(REWRITE_DONE, lit); } else { - - FloatingPoint::PartialBitVector res(arg.convertToBV(param.bvs, rm, true)); + FloatingPoint::PartialBitVector res( + arg.convertToBV(param.d_bv_size, rm, true)); if (res.second) { Node lit = NodeManager::currentNM()->mkConst(res.first); diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index bff909a39..4d4f3c660 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -39,17 +39,20 @@ class FloatingPointConstantTypeRule { const FloatingPoint& f = n.getConst(); - if (check) { - if (!(validExponentSize(f.t.exponent()))) { + if (check) + { + if (!(validExponentSize(f.d_fp_size.exponentWidth()))) + { throw TypeCheckingExceptionPrivate( n, "constant with invalid exponent size"); } - if (!(validSignificandSize(f.t.significand()))) { + if (!(validSignificandSize(f.d_fp_size.significandWidth()))) + { throw TypeCheckingExceptionPrivate( n, "constant with invalid significand size"); } } - return nodeManager->mkFloatingPointType(f.t); + return nodeManager->mkFloatingPointType(f.d_fp_size); } }; @@ -252,13 +255,17 @@ class FloatingPointToFPIEEEBitVectorTypeRule { if (check) { TypeNode operandType = n[0].getType(check); - if (!(operandType.isBitVector())) { + if (!(operandType.isBitVector())) + { throw TypeCheckingExceptionPrivate(n, "conversion to floating-point from " "bit vector used with sort other " "than bit vector"); - } else if (!(operandType.getBitVectorSize() == - info.t.exponent() + info.t.significand())) { + } + else if (!(operandType.getBitVectorSize() + == info.d_fp_size.exponentWidth() + + info.d_fp_size.significandWidth())) + { throw TypeCheckingExceptionPrivate( n, "conversion to floating-point from bit vector used with bit vector " @@ -266,7 +273,7 @@ class FloatingPointToFPIEEEBitVectorTypeRule { } } - return nodeManager->mkFloatingPointType(info.t); + return nodeManager->mkFloatingPointType(info.d_fp_size); } }; @@ -298,7 +305,7 @@ class FloatingPointToFPFloatingPointTypeRule { } } - return nodeManager->mkFloatingPointType(info.t); + return nodeManager->mkFloatingPointType(info.d_fp_size); } }; @@ -330,7 +337,7 @@ class FloatingPointToFPRealTypeRule { } } - return nodeManager->mkFloatingPointType(info.t); + return nodeManager->mkFloatingPointType(info.d_fp_size); } }; @@ -362,7 +369,7 @@ class FloatingPointToFPSignedBitVectorTypeRule { } } - return nodeManager->mkFloatingPointType(info.t); + return nodeManager->mkFloatingPointType(info.d_fp_size); } }; @@ -394,7 +401,7 @@ class FloatingPointToFPUnsignedBitVectorTypeRule { } } - return nodeManager->mkFloatingPointType(info.t); + return nodeManager->mkFloatingPointType(info.d_fp_size); } }; @@ -419,7 +426,7 @@ class FloatingPointToFPGenericTypeRule { } } - return nodeManager->mkFloatingPointType(info.t); + return nodeManager->mkFloatingPointType(info.d_fp_size); } }; @@ -450,7 +457,7 @@ class FloatingPointToUBVTypeRule { } } - return nodeManager->mkBitVectorType(info.bvs); + return nodeManager->mkBitVectorType(info.d_bv_size); } }; @@ -481,7 +488,7 @@ class FloatingPointToSBVTypeRule { } } - return nodeManager->mkBitVectorType(info.bvs); + return nodeManager->mkBitVectorType(info.d_bv_size); } }; @@ -522,7 +529,7 @@ class FloatingPointToUBVTotalTypeRule { } } - return nodeManager->mkBitVectorType(info.bvs); + return nodeManager->mkBitVectorType(info.d_bv_size); } }; @@ -563,7 +570,7 @@ class FloatingPointToSBVTotalTypeRule { } } - return nodeManager->mkBitVectorType(info.bvs); + return nodeManager->mkBitVectorType(info.d_bv_size); } }; @@ -686,7 +693,7 @@ 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::fpt format(fps); // The symfpu interface to type info + symfpuLiteral::CVC4FPSize format(fps); // The symfpu interface to type info unsigned bw = FloatingPointLiteral::exponentWidth(format); #else unsigned bw = 2; @@ -729,7 +736,7 @@ class FloatingPointComponentSignificand #ifdef CVC4_USE_SYMFPU /* As before we need to use some of sympfu. */ FloatingPointSize fps = operandType.getConst(); - symfpuLiteral::fpt format(fps); + symfpuLiteral::CVC4FPSize format(fps); unsigned bw = FloatingPointLiteral::significandWidth(format); #else unsigned bw = 1; @@ -791,8 +798,8 @@ public: * = 5 + ((2^e)-1)*2^s */ - Integer significandValues = Integer(2).pow(fps.significand()); - Integer exponentValues = Integer(2).pow(fps.exponent()); + Integer significandValues = Integer(2).pow(fps.significandWidth()); + Integer exponentValues = Integer(2).pow(fps.exponentWidth()); exponentValues -= Integer(1); return Integer(5) + exponentValues * significandValues; diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index c84779be0..6e8f8369a 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -43,16 +43,16 @@ #ifdef CVC4_USE_SYMFPU namespace symfpu { -#define CVC4_LIT_ITE_DFN(T) \ - template <> \ - struct ite<::CVC4::symfpuLiteral::prop, T> \ - { \ - static const T &iteOp(const ::CVC4::symfpuLiteral::prop &cond, \ - const T &l, \ - const T &r) \ - { \ - return cond ? l : r; \ - } \ +#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); @@ -70,16 +70,30 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv); namespace CVC4 { -FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s) +FloatingPointSize::FloatingPointSize(unsigned exp_size, unsigned sig_size) + : d_exp_size(exp_size), d_sig_size(sig_size) { - PrettyCheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e); - PrettyCheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s); + PrettyCheckArgument(validExponentSize(exp_size), + exp_size, + "Invalid exponent size : %d", + exp_size); + PrettyCheckArgument(validSignificandSize(sig_size), + sig_size, + "Invalid significand size : %d", + sig_size); } -FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s) +FloatingPointSize::FloatingPointSize(const FloatingPointSize& old) + : d_exp_size(old.d_exp_size), d_sig_size(old.d_sig_size) { - PrettyCheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e); - PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s); + PrettyCheckArgument(validExponentSize(d_exp_size), + d_exp_size, + "Invalid exponent size : %d", + d_exp_size); + PrettyCheckArgument(validSignificandSize(d_sig_size), + d_sig_size, + "Invalid significand size : %d", + d_sig_size); } namespace symfpuLiteral { @@ -88,36 +102,40 @@ namespace symfpuLiteral { typedef traits t; template -wrappedBitVector wrappedBitVector::one(const bwt &w) +wrappedBitVector wrappedBitVector::one( + const CVC4BitWidth& w) { return wrappedBitVector(w, 1); } template -wrappedBitVector wrappedBitVector::zero(const bwt &w) +wrappedBitVector wrappedBitVector::zero( + const CVC4BitWidth& w) { return wrappedBitVector(w, 0); } template -wrappedBitVector wrappedBitVector::allOnes(const bwt &w) +wrappedBitVector wrappedBitVector::allOnes( + const CVC4BitWidth& w) { return ~wrappedBitVector::zero(w); } template -prop wrappedBitVector::isAllOnes() const +CVC4Prop wrappedBitVector::isAllOnes() const { return (*this == wrappedBitVector::allOnes(this->getWidth())); } template -prop wrappedBitVector::isAllZeros() const +CVC4Prop wrappedBitVector::isAllZeros() const { return (*this == wrappedBitVector::zero(this->getWidth())); } template -wrappedBitVector wrappedBitVector::maxValue(const bwt &w) +wrappedBitVector wrappedBitVector::maxValue( + const CVC4BitWidth& w) { if (isSigned) { @@ -131,7 +149,8 @@ wrappedBitVector wrappedBitVector::maxValue(const bwt &w) } template -wrappedBitVector wrappedBitVector::minValue(const bwt &w) +wrappedBitVector wrappedBitVector::minValue( + const CVC4BitWidth& w) { if (isSigned) { @@ -292,58 +311,64 @@ wrappedBitVector wrappedBitVector::modularNegate() const /*** Comparisons ***/ template -prop wrappedBitVector::operator==( - const wrappedBitVector &op) const +CVC4Prop wrappedBitVector::operator==( + const wrappedBitVector& op) const { return this->BitVector::operator==(op); } template <> -prop wrappedBitVector::operator<=(const wrappedBitVector &op) const +CVC4Prop wrappedBitVector::operator<=( + const wrappedBitVector& op) const { return this->signedLessThanEq(op); } template <> -prop wrappedBitVector::operator>=(const wrappedBitVector &op) const +CVC4Prop wrappedBitVector::operator>=( + const wrappedBitVector& op) const { return !(this->signedLessThan(op)); } template <> -prop wrappedBitVector::operator<(const wrappedBitVector &op) const +CVC4Prop wrappedBitVector::operator<( + const wrappedBitVector& op) const { return this->signedLessThan(op); } template <> -prop wrappedBitVector::operator>(const wrappedBitVector &op) const +CVC4Prop wrappedBitVector::operator>( + const wrappedBitVector& op) const { return !(this->signedLessThanEq(op)); } template <> -prop wrappedBitVector::operator<=( - const wrappedBitVector &op) const +CVC4Prop wrappedBitVector::operator<=( + const wrappedBitVector& op) const { return this->unsignedLessThanEq(op); } template <> -prop wrappedBitVector::operator>=( - const wrappedBitVector &op) const +CVC4Prop wrappedBitVector::operator>=( + const wrappedBitVector& op) const { return !(this->unsignedLessThan(op)); } template <> -prop wrappedBitVector::operator<(const wrappedBitVector &op) const +CVC4Prop wrappedBitVector::operator<( + const wrappedBitVector& op) const { return this->unsignedLessThan(op); } template <> -prop wrappedBitVector::operator>(const wrappedBitVector &op) const +CVC4Prop wrappedBitVector::operator>( + const wrappedBitVector& op) const { return !(this->unsignedLessThanEq(op)); } @@ -366,7 +391,7 @@ wrappedBitVector wrappedBitVector::toUnsigned(void) const template wrappedBitVector wrappedBitVector::extend( - bwt extension) const + CVC4BitWidth extension) const { if (isSigned) { @@ -380,7 +405,7 @@ wrappedBitVector wrappedBitVector::extend( template wrappedBitVector wrappedBitVector::contract( - bwt reduction) const + CVC4BitWidth reduction) const { PRECONDITION(this->getWidth() > reduction); @@ -388,9 +413,10 @@ wrappedBitVector wrappedBitVector::contract( } template -wrappedBitVector wrappedBitVector::resize(bwt newSize) const +wrappedBitVector wrappedBitVector::resize( + CVC4BitWidth newSize) const { - bwt width = this->getWidth(); + CVC4BitWidth width = this->getWidth(); if (newSize > width) { @@ -423,8 +449,8 @@ wrappedBitVector wrappedBitVector::append( // Inclusive of end points, thus if the same, extracts just one bit template -wrappedBitVector wrappedBitVector::extract(bwt upper, - bwt lower) const +wrappedBitVector wrappedBitVector::extract( + CVC4BitWidth upper, CVC4BitWidth lower) const { PRECONDITION(upper >= lower); return this->BitVector::extract(upper, lower); @@ -434,25 +460,25 @@ wrappedBitVector wrappedBitVector::extract(bwt upper, template class wrappedBitVector; template class wrappedBitVector; -rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; }; -rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; }; -rm traits::RTP(void) { return ::CVC4::roundTowardPositive; }; -rm traits::RTN(void) { return ::CVC4::roundTowardNegative; }; -rm traits::RTZ(void) { return ::CVC4::roundTowardZero; }; +traits::rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; }; +traits::rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; }; +traits::rm traits::RTP(void) { return ::CVC4::roundTowardPositive; }; +traits::rm traits::RTN(void) { return ::CVC4::roundTowardNegative; }; +traits::rm traits::RTZ(void) { return ::CVC4::roundTowardZero; }; // This is a literal back-end so props are actually bools // so these can be handled in the same way as the internal assertions above -void traits::precondition(const prop &p) +void traits::precondition(const traits::prop& p) { Assert(p); return; } -void traits::postcondition(const prop &p) +void traits::postcondition(const traits::prop& p) { Assert(p); return; } -void traits::invariant(const prop &p) +void traits::invariant(const traits::prop& p) { Assert(p); return; @@ -466,25 +492,26 @@ void FloatingPointLiteral::unfinished(void) const } #endif -FloatingPoint::FloatingPoint(unsigned e, unsigned s, const BitVector &bv) - : +FloatingPoint::FloatingPoint(unsigned d_exp_size, + unsigned d_sig_size, + const BitVector& bv) + : d_fp_size(d_exp_size, d_sig_size), #ifdef CVC4_USE_SYMFPU - fpl(symfpu::unpack(symfpuLiteral::fpt(e, s), bv)), + d_fpl(symfpu::unpack( + symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv)) #else - fpl(e, s, 0.0), + d_fpl(d_exp_size, d_sig_size, 0.0) #endif - t(e, s) { } FloatingPoint::FloatingPoint(const FloatingPointSize& size, const BitVector& bv) - : + : d_fp_size(size), #ifdef CVC4_USE_SYMFPU - fpl(symfpu::unpack(size, bv)), + d_fpl(symfpu::unpack(size, bv)) #else - fpl(size.exponent(), size.significand(), 0.0), + d_fpl(size.exponentWidth(), size.significandWidth(), 0.0) #endif - t(size) { } @@ -499,17 +526,17 @@ static FloatingPointLiteral constructorHelperBitVector( { return FloatingPointLiteral( symfpu::convertSBVToFloat( - symfpuLiteral::fpt(size), - symfpuLiteral::rm(rm), - symfpuLiteral::sbv(bv))); + symfpuLiteral::CVC4FPSize(size), + symfpuLiteral::CVC4RM(rm), + symfpuLiteral::CVC4SignedBitVector(bv))); } else { return FloatingPointLiteral( symfpu::convertUBVToFloat( - symfpuLiteral::fpt(size), - symfpuLiteral::rm(rm), - symfpuLiteral::ubv(bv))); + symfpuLiteral::CVC4FPSize(size), + symfpuLiteral::CVC4RM(rm), + symfpuLiteral::CVC4UnsignedBitVector(bv))); } #else return FloatingPointLiteral(2, 2, 0.0); @@ -521,7 +548,7 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, const BitVector& bv, bool signedBV) - : fpl(constructorHelperBitVector(size, rm, bv, signedBV)), t(size) + : d_fp_size(size), d_fpl(constructorHelperBitVector(size, rm, bv, signedBV)) { } @@ -643,7 +670,7 @@ static FloatingPointLiteral constructorHelperRational( FloatingPoint::FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, const Rational& r) - : fpl(constructorHelperRational(size, rm, r)), t(size) + : d_fp_size(size), d_fpl(constructorHelperRational(size, rm, r)) { } @@ -714,265 +741,327 @@ FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size, return FloatingPoint(size, bvsign.concat(bvexp).concat(bvsig)); } - /* Operations implemented using symfpu */ - FloatingPoint FloatingPoint::absolute (void) const { +/* Operations implemented using symfpu */ +FloatingPoint FloatingPoint::absolute(void) const +{ #ifdef CVC4_USE_SYMFPU - return FloatingPoint(t, symfpu::absolute(t, fpl)); + return FloatingPoint( + d_fp_size, symfpu::absolute(d_fp_size, d_fpl)); #else - return *this; + return *this; #endif - } - - FloatingPoint FloatingPoint::negate (void) const { +} + +FloatingPoint FloatingPoint::negate(void) const +{ #ifdef CVC4_USE_SYMFPU - return FloatingPoint(t, symfpu::negate(t, fpl)); + return FloatingPoint(d_fp_size, + symfpu::negate(d_fp_size, d_fpl)); #else - return *this; + return *this; #endif - } - - FloatingPoint FloatingPoint::plus (const RoundingMode &rm, const FloatingPoint &arg) const { +} + +FloatingPoint FloatingPoint::plus(const RoundingMode& rm, + const FloatingPoint& arg) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg.t); - return FloatingPoint( - t, symfpu::add(t, rm, fpl, arg.fpl, true)); + 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)); #else - return *this; + return *this; #endif - } +} - FloatingPoint FloatingPoint::sub (const RoundingMode &rm, const FloatingPoint &arg) const { +FloatingPoint FloatingPoint::sub(const RoundingMode& rm, + const FloatingPoint& arg) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg.t); - return FloatingPoint( - t, symfpu::add(t, rm, fpl, arg.fpl, false)); + 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)); #else - return *this; + return *this; #endif - } +} - FloatingPoint FloatingPoint::mult (const RoundingMode &rm, const FloatingPoint &arg) const { +FloatingPoint FloatingPoint::mult(const RoundingMode& rm, + const FloatingPoint& arg) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg.t); - return FloatingPoint( - t, symfpu::multiply(t, rm, fpl, arg.fpl)); + Assert(this->d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + symfpu::multiply(d_fp_size, rm, d_fpl, arg.d_fpl)); #else - return *this; + return *this; #endif - } +} - FloatingPoint FloatingPoint::fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const { +FloatingPoint FloatingPoint::fma(const RoundingMode& rm, + const FloatingPoint& arg1, + const FloatingPoint& arg2) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg1.t); - Assert(this->t == arg2.t); - return FloatingPoint( - t, symfpu::fma(t, rm, fpl, arg1.fpl, arg2.fpl)); + 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)); #else - return *this; + return *this; #endif - } +} - FloatingPoint FloatingPoint::div (const RoundingMode &rm, const FloatingPoint &arg) const { +FloatingPoint FloatingPoint::div(const RoundingMode& rm, + const FloatingPoint& arg) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg.t); - return FloatingPoint( - t, symfpu::divide(t, rm, fpl, arg.fpl)); + Assert(this->d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + symfpu::divide(d_fp_size, rm, d_fpl, arg.d_fpl)); #else - return *this; + return *this; #endif - } +} - FloatingPoint FloatingPoint::sqrt (const RoundingMode &rm) const { +FloatingPoint FloatingPoint::sqrt(const RoundingMode& rm) const +{ #ifdef CVC4_USE_SYMFPU - return FloatingPoint(t, symfpu::sqrt(t, rm, fpl)); + return FloatingPoint( + d_fp_size, symfpu::sqrt(d_fp_size, rm, d_fpl)); #else - return *this; + return *this; #endif - } +} - FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const { +FloatingPoint FloatingPoint::rti(const RoundingMode& rm) const +{ #ifdef CVC4_USE_SYMFPU - return FloatingPoint( - t, symfpu::roundToIntegral(t, rm, fpl)); + return FloatingPoint( + d_fp_size, + symfpu::roundToIntegral(d_fp_size, rm, d_fpl)); #else - return *this; + return *this; #endif - } +} - FloatingPoint FloatingPoint::rem (const FloatingPoint &arg) const { +FloatingPoint FloatingPoint::rem(const FloatingPoint& arg) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg.t); - return FloatingPoint( - t, symfpu::remainder(t, fpl, arg.fpl)); + Assert(this->d_fp_size == arg.d_fp_size); + return FloatingPoint( + d_fp_size, + symfpu::remainder(d_fp_size, d_fpl, arg.d_fpl)); #else - return *this; + return *this; #endif - } +} - FloatingPoint FloatingPoint::maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const { +FloatingPoint FloatingPoint::maxTotal(const FloatingPoint& arg, + bool zeroCaseLeft) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg.t); - return FloatingPoint( - t, symfpu::max(t, fpl, arg.fpl, zeroCaseLeft)); + 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)); #else - return *this; + return *this; #endif - } - - FloatingPoint FloatingPoint::minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const { +} + +FloatingPoint FloatingPoint::minTotal(const FloatingPoint& arg, + bool zeroCaseLeft) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg.t); - return FloatingPoint( - t, symfpu::min(t, fpl, arg.fpl, zeroCaseLeft)); + 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)); #else - return *this; + return *this; #endif - } +} - FloatingPoint::PartialFloatingPoint FloatingPoint::max (const FloatingPoint &arg) const { - FloatingPoint tmp(maxTotal(arg, true)); - return PartialFloatingPoint(tmp, tmp == maxTotal(arg, false)); - } +FloatingPoint::PartialFloatingPoint FloatingPoint::max( + const FloatingPoint& arg) const +{ + FloatingPoint tmp(maxTotal(arg, true)); + return PartialFloatingPoint(tmp, tmp == maxTotal(arg, false)); +} - FloatingPoint::PartialFloatingPoint FloatingPoint::min (const FloatingPoint &arg) const { - FloatingPoint tmp(minTotal(arg, true)); - return PartialFloatingPoint(tmp, tmp == minTotal(arg, false)); - } +FloatingPoint::PartialFloatingPoint FloatingPoint::min( + const FloatingPoint& arg) const +{ + FloatingPoint tmp(minTotal(arg, true)); + return PartialFloatingPoint(tmp, tmp == minTotal(arg, false)); +} - bool FloatingPoint::operator ==(const FloatingPoint& fp) const { +bool FloatingPoint::operator==(const FloatingPoint& fp) const +{ #ifdef CVC4_USE_SYMFPU - return ((t == fp.t) - && symfpu::smtlibEqual(t, fpl, fp.fpl)); + return ((d_fp_size == fp.d_fp_size) + && symfpu::smtlibEqual( + d_fp_size, d_fpl, fp.d_fpl)); #else - return ( (t == fp.t) ); + return ((d_fp_size == fp.d_fp_size)); #endif - } +} - bool FloatingPoint::operator <= (const FloatingPoint &arg) const { +bool FloatingPoint::operator<=(const FloatingPoint& arg) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg.t); - return symfpu::lessThanOrEqual(t, fpl, arg.fpl); + Assert(this->d_fp_size == arg.d_fp_size); + return symfpu::lessThanOrEqual( + d_fp_size, d_fpl, arg.d_fpl); #else - return false; + return false; #endif - } +} - bool FloatingPoint::operator < (const FloatingPoint &arg) const { +bool FloatingPoint::operator<(const FloatingPoint& arg) const +{ #ifdef CVC4_USE_SYMFPU - Assert(this->t == arg.t); - return symfpu::lessThan(t, fpl, arg.fpl); + Assert(this->d_fp_size == arg.d_fp_size); + return symfpu::lessThan(d_fp_size, d_fpl, arg.d_fpl); #else - return false; + return false; #endif - } +} - bool FloatingPoint::isNormal (void) const { +bool FloatingPoint::isNormal(void) const +{ #ifdef CVC4_USE_SYMFPU - return symfpu::isNormal(t, fpl); + return symfpu::isNormal(d_fp_size, d_fpl); #else - return false; + return false; #endif - } +} - bool FloatingPoint::isSubnormal (void) const { +bool FloatingPoint::isSubnormal(void) const +{ #ifdef CVC4_USE_SYMFPU - return symfpu::isSubnormal(t, fpl); + return symfpu::isSubnormal(d_fp_size, d_fpl); #else - return false; + return false; #endif - } +} - bool FloatingPoint::isZero (void) const { +bool FloatingPoint::isZero(void) const +{ #ifdef CVC4_USE_SYMFPU - return symfpu::isZero(t, fpl); + return symfpu::isZero(d_fp_size, d_fpl); #else - return false; + return false; #endif - } +} - bool FloatingPoint::isInfinite (void) const { +bool FloatingPoint::isInfinite(void) const +{ #ifdef CVC4_USE_SYMFPU - return symfpu::isInfinite(t, fpl); + return symfpu::isInfinite(d_fp_size, d_fpl); #else - return false; + return false; #endif - } +} - bool FloatingPoint::isNaN (void) const { +bool FloatingPoint::isNaN(void) const +{ #ifdef CVC4_USE_SYMFPU - return symfpu::isNaN(t, fpl); + return symfpu::isNaN(d_fp_size, d_fpl); #else - return false; + return false; #endif - } +} - bool FloatingPoint::isNegative (void) const { +bool FloatingPoint::isNegative(void) const +{ #ifdef CVC4_USE_SYMFPU - return symfpu::isNegative(t, fpl); + return symfpu::isNegative(d_fp_size, d_fpl); #else - return false; + return false; #endif - } +} - bool FloatingPoint::isPositive (void) const { +bool FloatingPoint::isPositive(void) const +{ #ifdef CVC4_USE_SYMFPU - return symfpu::isPositive(t, fpl); + return symfpu::isPositive(d_fp_size, d_fpl); #else - return false; + return false; #endif - } +} - FloatingPoint FloatingPoint::convert (const FloatingPointSize &target, const RoundingMode &rm) const { +FloatingPoint FloatingPoint::convert(const FloatingPointSize& target, + const RoundingMode& rm) const +{ #ifdef CVC4_USE_SYMFPU - return FloatingPoint( - target, - symfpu::convertFloatToFloat(t, target, rm, fpl)); + return FloatingPoint(target, + symfpu::convertFloatToFloat( + d_fp_size, target, rm, d_fpl)); #else - return *this; + return *this; #endif - } - - BitVector FloatingPoint::convertToBVTotal (BitVectorSize width, const RoundingMode &rm, bool signedBV, BitVector undefinedCase) const { +} + +BitVector FloatingPoint::convertToBVTotal(BitVectorSize width, + const RoundingMode& rm, + bool signedBV, + BitVector undefinedCase) const +{ #ifdef CVC4_USE_SYMFPU if (signedBV) return symfpu::convertFloatToSBV( - t, rm, fpl, width, undefinedCase); + d_fp_size, rm, d_fpl, width, undefinedCase); else return symfpu::convertFloatToUBV( - t, rm, fpl, width, undefinedCase); + d_fp_size, rm, d_fpl, width, undefinedCase); #else - return undefinedCase; + return undefinedCase; #endif - } +} - Rational FloatingPoint::convertToRationalTotal (Rational undefinedCase) const { - PartialRational p(convertToRational()); +Rational FloatingPoint::convertToRationalTotal(Rational undefinedCase) const +{ + PartialRational p(convertToRational()); - return p.second ? p.first : undefinedCase; - } + return p.second ? p.first : undefinedCase; +} - FloatingPoint::PartialBitVector FloatingPoint::convertToBV (BitVectorSize width, const RoundingMode &rm, bool signedBV) const { - BitVector tmp(convertToBVTotal (width, rm, signedBV, BitVector(width, 0U))); - BitVector confirm(convertToBVTotal (width, rm, signedBV, BitVector(width, 1U))); +FloatingPoint::PartialBitVector FloatingPoint::convertToBV( + BitVectorSize width, const RoundingMode& rm, bool signedBV) const +{ + BitVector tmp(convertToBVTotal(width, rm, signedBV, BitVector(width, 0U))); + BitVector confirm( + convertToBVTotal(width, rm, signedBV, BitVector(width, 1U))); - return PartialBitVector(tmp, tmp == confirm); - } + return PartialBitVector(tmp, tmp == confirm); +} - FloatingPoint::PartialRational FloatingPoint::convertToRational (void) const { - if (this->isNaN() || this->isInfinite()) { - return PartialRational(Rational(0U, 1U), false); - } - if (this->isZero()) { - return PartialRational(Rational(0U, 1U), true); - - } else { +FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const +{ + if (this->isNaN() || this->isInfinite()) + { + return PartialRational(Rational(0U, 1U), false); + } + if (this->isZero()) + { + return PartialRational(Rational(0U, 1U), true); + } + else + { #ifdef CVC4_USE_SYMFPU - Integer sign((this->fpl.getSign()) ? -1 : 1); - Integer exp( - this->fpl.getExponent().toSignedInteger() - - (Integer(t.significand() - - 1))); // -1 as forcibly normalised into the [1,2) range - Integer significand(this->fpl.getSignificand().toInteger()); + Integer sign((this->d_fpl.getSign()) ? -1 : 1); + Integer exp( + this->d_fpl.getExponent().toSignedInteger() + - (Integer(d_fp_size.significandWidth() + - 1))); // -1 as forcibly normalised into the [1,2) range + Integer significand(this->d_fpl.getSignificand().toInteger()); #else Integer sign(0); Integer exp(0); @@ -1003,19 +1092,21 @@ FloatingPoint FloatingPoint::makeMaxNormal(const FloatingPointSize& size, Rational r(signedSignificand, q); return PartialRational(r, true); } - } + } Unreachable() << "Convert float literal to real broken."; - } +} - BitVector FloatingPoint::pack (void) const { +BitVector FloatingPoint::pack(void) const +{ #ifdef CVC4_USE_SYMFPU - BitVector bv(symfpu::pack(this->t, this->fpl)); + BitVector bv( + symfpu::pack(this->d_fp_size, this->d_fpl)); #else - BitVector bv(4u,0u); + BitVector bv(4u, 0u); #endif - return bv; - } + return bv; +} std::string FloatingPoint::toString(bool printAsIndexed) const { @@ -1023,9 +1114,9 @@ std::string FloatingPoint::toString(bool printAsIndexed) const // retrive BV value BitVector bv(pack()); unsigned largestSignificandBit = - t.significand() - 2; // -1 for -inclusive, -1 for hidden + d_fp_size.significandWidth() - 2; // -1 for -inclusive, -1 for hidden unsigned largestExponentBit = - (t.exponent() - 1) + (largestSignificandBit + 1); + (d_fp_size.exponentWidth() - 1) + (largestSignificandBit + 1); BitVector v[3]; v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1); v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1); @@ -1055,4 +1146,21 @@ std::string FloatingPoint::toString(bool printAsIndexed) const return str; } +std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp) +{ + // print in binary notation + return os << fp.toString(); +} + +std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps) +{ + return os << "(_ FloatingPoint " << fps.exponentWidth() << " " + << fps.significandWidth() << ")"; +} + +std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs) +{ + return os << "(_ to_fp " << fpcs.d_fp_size.exponentWidth() << " " + << fpcs.d_fp_size.significandWidth() << ")"; +} }/* CVC4 namespace */ diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in index 9e78c20c0..0d62e9c3e 100644 --- a/src/util/floatingpoint.h.in +++ b/src/util/floatingpoint.h.in @@ -20,587 +20,846 @@ #ifndef CVC4__FLOATINGPOINT_H #define CVC4__FLOATINGPOINT_H +#include + #include "util/bitvector.h" #include "util/rational.h" -#include - +// clang-format off #if @CVC4_USE_SYMFPU@ +// clang-format on #include #endif /* @CVC4_USE_SYMFPU@ */ namespace CVC4 { - // Inline these! - inline bool CVC4_PUBLIC validExponentSize (unsigned e) { return e >= 2; } - inline bool CVC4_PUBLIC validSignificandSize (unsigned s) { return s >= 2; } - - /** - * Floating point sorts are parameterised by two non-zero constants - * giving the width (in bits) of the exponent and significand - * (including the hidden bit). - */ - class CVC4_PUBLIC FloatingPointSize { - /* - Class invariants: - * VALIDEXPONENTSIZE(e) - * VALIDSIGNIFCANDSIZE(s) - */ - - private : - unsigned e; - unsigned s; - - public : - FloatingPointSize (unsigned _e, unsigned _s); - FloatingPointSize (const FloatingPointSize &old); - - inline unsigned exponent (void) const { - return this->e; - } - - inline unsigned significand (void) const { - return this->s; - } - - bool operator ==(const FloatingPointSize& fps) const { - return (e == fps.e) && (s == fps.s); - } - - // Implement the interface that symfpu uses for floating-point formats. - inline unsigned exponentWidth(void) const { return this->exponent(); } - inline unsigned significandWidth(void) const { return this->significand(); } - inline unsigned packedWidth(void) const - { - return this->exponentWidth() + this->significandWidth(); - } - inline unsigned packedExponentWidth(void) const - { - return this->exponentWidth(); - } - inline unsigned packedSignificandWidth(void) const - { - return this->significandWidth() - 1; - } - - }; /* class FloatingPointSize */ - - struct CVC4_PUBLIC FloatingPointSizeHashFunction { - static inline size_t ROLL(size_t X, size_t N) { - return (((X) << (N)) | ((X) >> (8*sizeof((X)) - (N)) )); - } - - inline size_t operator() (const FloatingPointSize& t) const { - return size_t(ROLL(t.exponent(), 4*sizeof(unsigned)) | - t.significand()); - } - }; /* struct FloatingPointSizeHashFunction */ +// Inline these! +inline bool CVC4_PUBLIC validExponentSize(unsigned e) { return e >= 2; } +inline bool CVC4_PUBLIC validSignificandSize(unsigned s) { return s >= 2; } + +/* -------------------------------------------------------------------------- */ + +/** + * Floating point sorts are parameterised by two constants > 1 giving the + * width (in bits) of the exponent and significand (including the hidden bit). + * So, IEEE-754 single precision, a.k.a. float, is described as 8 24. + */ +class CVC4_PUBLIC FloatingPointSize +{ + public: + /** Constructors. */ + FloatingPointSize(unsigned exp_size, unsigned sig_size); + FloatingPointSize(const FloatingPointSize& old); + + /** Operator overload for equality comparison. */ + bool operator==(const FloatingPointSize& fps) const + { + return (d_exp_size == fps.d_exp_size) && (d_sig_size == fps.d_sig_size); + } + /** Implement the interface that symfpu uses for floating-point formats. */ + /** Get the exponent bit-width of this floating-point format. */ + inline unsigned exponentWidth(void) const { return this->d_exp_size; } + /** Get the significand bit-width of this floating-point format. */ + inline unsigned significandWidth(void) const { return this->d_sig_size; } /** - * A concrete instance of the rounding mode sort + * Get the bit-width of the packed representation of this floating-point + * format (= exponent + significand bit-width, convenience wrapper). */ - enum CVC4_PUBLIC RoundingMode { - roundNearestTiesToEven = FE_TONEAREST, - roundTowardPositive = FE_UPWARD, - roundTowardNegative = FE_DOWNWARD, - roundTowardZero = FE_TOWARDZERO, - // Initializes this to the diagonalization of the 4 other values. - roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) | - ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8)) - }; /* enum RoundingMode */ - - struct CVC4_PUBLIC RoundingModeHashFunction { - inline size_t operator() (const RoundingMode& rm) const { - return size_t(rm); - } - }; /* struct RoundingModeHashFunction */ - + inline unsigned packedWidth(void) const + { + return this->exponentWidth() + this->significandWidth(); + } /** - * This is a symfpu literal "back-end". It allows the library to be used as - * an arbitrary precision floating-point implementation. This is effectively - * the glue between symfpu's notion of "signed bit-vector" and CVC4's - * BitVector. + * Get the exponent bit-width of the packed representation of this + * floating-point format (= exponent bit-width). */ - namespace symfpuLiteral { - // Forward declaration of wrapper so that traits can be defined early and so - // used in the implementation of wrappedBitVector. - template - class wrappedBitVector; - - // This is the template parameter for symfpu's templates. - class traits + inline unsigned packedExponentWidth(void) const { - public: - // The six key types that symfpu uses. - using bwt = uint32_t; - using prop = bool; - using rm = ::CVC4::RoundingMode; - using fpt = ::CVC4::FloatingPointSize; - using sbv = wrappedBitVector; - using ubv = wrappedBitVector; - - // Give concrete instances of each rounding mode, mainly for comparisons. - static rm RNE(void); - static rm RNA(void); - static rm RTP(void); - static rm RTN(void); - static rm RTZ(void); - - // The sympfu properties. - static void precondition(const prop &p); - static void postcondition(const prop &p); - static void invariant(const prop &p); - }; - - // Use the same type names as symfpu. - using bwt = traits::bwt; - using prop = traits::prop; - using rm = traits::rm; - using fpt = traits::fpt; - using ubv = traits::ubv; - using sbv = traits::sbv; - - // Type function for mapping between types - template - struct signedToLiteralType; - - template <> - struct signedToLiteralType - { - using literalType = int32_t; - }; - template <> - struct signedToLiteralType + return this->exponentWidth(); + } + /** + * Get the significand bit-width of the packed representation of this + * floating-point format (= significand bit-width - 1). + */ + inline unsigned packedSignificandWidth(void) const { - using literalType = uint32_t; - }; - - // This is an additional interface for CVC4::BitVector. - // The template parameter distinguishes signed and unsigned bit-vectors, a - // distinction symfpu uses. - template - class wrappedBitVector : public BitVector + return this->significandWidth() - 1; + } + + private: + /** Exponent bit-width. */ + unsigned d_exp_size; + /** Significand bit-width. */ + unsigned d_sig_size; + +}; /* class FloatingPointSize */ + +/** + * Hash function for floating point formats. + */ +struct CVC4_PUBLIC FloatingPointSizeHashFunction +{ + static inline size_t ROLL(size_t X, size_t N) { - protected: - using literalType = typename signedToLiteralType::literalType; + return (((X) << (N)) | ((X) >> (8 * sizeof((X)) - (N)))); + } - friend wrappedBitVector; // To allow conversion between the - // types + inline size_t operator()(const FloatingPointSize& t) const + { + return size_t(ROLL(t.exponentWidth(), 4 * sizeof(unsigned)) + | t.significandWidth()); + } +}; /* struct FloatingPointSizeHashFunction */ + +/* -------------------------------------------------------------------------- */ + +/** + * A concrete instance of the rounding mode sort + */ +enum CVC4_PUBLIC RoundingMode +{ + roundNearestTiesToEven = FE_TONEAREST, + roundTowardPositive = FE_UPWARD, + roundTowardNegative = FE_DOWNWARD, + roundTowardZero = FE_TOWARDZERO, + // Initializes this to the diagonalization of the 4 other values. + roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) + | ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8)) +}; /* enum RoundingMode */ + +/** + * Hash function for rounding mode values. + */ +struct CVC4_PUBLIC RoundingModeHashFunction +{ + inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); } +}; /* struct RoundingModeHashFunction */ + +/* -------------------------------------------------------------------------- */ + +/** + * This is a symfpu literal "back-end". It allows the library to be used as + * an arbitrary precision floating-point implementation. This is effectively + * the glue between symfpu's notion of "signed bit-vector" and CVC4's + * BitVector. + */ +namespace symfpuLiteral { + +/** + * Forward declaration of wrapper so that traits can be defined early and so + * used in the implementation of wrappedBitVector. + */ +template +class wrappedBitVector; + +using CVC4BitWidth = uint32_t; +using CVC4Prop = bool; +using CVC4RM = ::CVC4::RoundingMode; +using CVC4FPSize = ::CVC4::FloatingPointSize; +using CVC4UnsignedBitVector = wrappedBitVector; +using CVC4SignedBitVector = wrappedBitVector; + +/** + * This is the template parameter for symfpu's templates. + */ +class traits +{ + public: + /** The six key types that symfpu uses. */ + using bwt = CVC4BitWidth; // bit-width type + using prop = CVC4Prop; // boolean type + using rm = CVC4RM; // rounding-mode type + using fpt = CVC4FPSize; // floating-point format type + using ubv = CVC4UnsignedBitVector; // unsigned bit-vector type + using sbv = CVC4SignedBitVector; // signed bit-vector type + + /** Give concrete instances of each rounding mode, mainly for comparisons. */ + static rm RNE(void); + static rm RNA(void); + static rm RTP(void); + static rm RTN(void); + static rm RTZ(void); + + /** The sympfu properties. */ + static void precondition(const prop& p); + static void postcondition(const prop& p); + static void invariant(const prop& p); +}; + +/** + * Type function for mapping between types. + */ +template +struct signedToLiteralType; + +template <> +struct signedToLiteralType +{ + using literalType = int32_t; +}; +template <> +struct signedToLiteralType +{ + using literalType = uint32_t; +}; + +/** + * This extends the interface for CVC4::BitVector for compatibility with symFPU. + * The template parameter distinguishes signed and unsigned bit-vectors, a + * distinction symfpu uses. + */ +template +class wrappedBitVector : public BitVector +{ + protected: + using literalType = typename signedToLiteralType::literalType; + friend wrappedBitVector; // To allow conversion between types + +// clang-format off #if @CVC4_USE_SYMFPU@ - friend ::symfpu::ite >; // For ITE + // clang-format on + friend ::symfpu::ite >; // For ITE #endif /* @CVC4_USE_SYMFPU@ */ - public: - wrappedBitVector(const bwt w, const unsigned v) : BitVector(w, v) {} - wrappedBitVector(const prop &p) : BitVector(1, p ? 1U : 0U) {} - wrappedBitVector(const wrappedBitVector &old) : BitVector(old) {} - wrappedBitVector(const BitVector &old) : BitVector(old) {} - bwt getWidth(void) const { return getSize(); } - /*** Constant creation and test ***/ - - static wrappedBitVector one(const bwt &w); - static wrappedBitVector zero(const bwt &w); - static wrappedBitVector allOnes(const bwt &w); - - prop isAllOnes() const; - prop isAllZeros() const; - - static wrappedBitVector maxValue(const bwt &w); - static wrappedBitVector minValue(const bwt &w); - - /*** Operators ***/ - wrappedBitVector operator<<( - const wrappedBitVector &op) const; - wrappedBitVector operator>>( - const wrappedBitVector &op) const; - - /* Inherited but ... - * *sigh* if we use the inherited version then it will return a - * CVC4::BitVector which can be converted back to a - * wrappedBitVector but isn't done automatically when working - * out types for templates instantiation. ITE is a particular - * problem as expressions and constants no longer derive the - * same type. There aren't any good solutions in C++, we could - * use CRTP but Liana wouldn't appreciate that, so the following - * pointless wrapping functions are needed. - */ - wrappedBitVector operator|( - const wrappedBitVector &op) const; - wrappedBitVector operator&( - const wrappedBitVector &op) const; - wrappedBitVector operator+( - const wrappedBitVector &op) const; - wrappedBitVector operator-( - const wrappedBitVector &op) const; - wrappedBitVector operator*( - const wrappedBitVector &op) const; - wrappedBitVector operator/( - const wrappedBitVector &op) const; - wrappedBitVector operator%( - const wrappedBitVector &op) const; - wrappedBitVector operator-(void) const; - wrappedBitVector operator~(void)const; - - wrappedBitVector increment() const; - wrappedBitVector decrement() const; - wrappedBitVector signExtendRightShift( - const wrappedBitVector &op) const; - - /*** Modular opertaions ***/ - // No overflow checking so these are the same as other operations - wrappedBitVector modularLeftShift( - const wrappedBitVector &op) const; - wrappedBitVector modularRightShift( - const wrappedBitVector &op) const; - wrappedBitVector modularIncrement() const; - wrappedBitVector modularDecrement() const; - wrappedBitVector modularAdd( - const wrappedBitVector &op) const; - wrappedBitVector modularNegate() const; - - /*** Comparisons ***/ - // Inherited ... ish ... - prop operator==(const wrappedBitVector &op) const; - prop operator<=(const wrappedBitVector &op) const; - prop operator>=(const wrappedBitVector &op) const; - prop operator<(const wrappedBitVector &op) const; - prop operator>(const wrappedBitVector &op) const; - - /*** Type conversion ***/ - wrappedBitVector toSigned(void) const; - wrappedBitVector toUnsigned(void) const; - - /*** Bit hacks ***/ - wrappedBitVector extend(bwt extension) const; - wrappedBitVector contract(bwt reduction) const; - wrappedBitVector resize(bwt newSize) const; - wrappedBitVector matchWidth( - const wrappedBitVector &op) const; - wrappedBitVector append( - const wrappedBitVector &op) const; - - // Inclusive of end points, thus if the same, extracts just one bit - wrappedBitVector extract(bwt upper, bwt lower) const; - }; - } + public: + /** Constructors. */ + wrappedBitVector(const CVC4BitWidth w, const unsigned v) : BitVector(w, v) {} + wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {} + wrappedBitVector(const wrappedBitVector& old) : BitVector(old) {} + wrappedBitVector(const BitVector& old) : BitVector(old) {} + + /** Get the bit-width of this wrapped bit-vector. */ + CVC4BitWidth getWidth(void) const { return getSize(); } + + /** Create a zero value of given bit-width 'w'. */ + static wrappedBitVector one(const CVC4BitWidth& w); + /** Create a one value of given bit-width 'w'. */ + static wrappedBitVector zero(const CVC4BitWidth& w); + /** Create a ones value (all bits 1) of given bit-width 'w'. */ + static wrappedBitVector allOnes(const CVC4BitWidth& w); + /** Create a maximum signed/unsigned value of given bit-width 'w'. */ + static wrappedBitVector maxValue(const CVC4BitWidth& w); + /** Create a minimum signed/unsigned value of given bit-width 'w'. */ + static wrappedBitVector minValue(const CVC4BitWidth& w); + + /** Return true if this a bit-vector representing a ones value. */ + CVC4Prop isAllOnes() const; + /** Return true if this a bit-vector representing a zero value. */ + CVC4Prop isAllZeros() const; + + /** Left shift. */ + wrappedBitVector operator<<( + const wrappedBitVector& op) const; + /** Logical (unsigned) and arithmetic (signed) right shift. */ + wrappedBitVector operator>>( + const wrappedBitVector& op) const; + + /** + * Inherited but ... + * *sigh* if we use the inherited version then it will return a + * CVC4::BitVector which can be converted back to a + * wrappedBitVector but isn't done automatically when working + * out types for templates instantiation. ITE is a particular + * problem as expressions and constants no longer derive the + * same type. There aren't any good solutions in C++, we could + * use CRTP but Liana wouldn't appreciate that, so the following + * pointless wrapping functions are needed. + */ + + /** Bit-wise or. */ + wrappedBitVector operator|( + const wrappedBitVector& op) const; + /** Bit-wise and. */ + wrappedBitVector operator&( + const wrappedBitVector& op) const; + /** Bit-vector addition. */ + wrappedBitVector operator+( + const wrappedBitVector& op) const; + /** Bit-vector subtraction. */ + wrappedBitVector operator-( + const wrappedBitVector& op) const; + /** Bit-vector multiplication. */ + wrappedBitVector operator*( + const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned division. */ + wrappedBitVector operator/( + const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned remainder. */ + wrappedBitVector operator%( + const wrappedBitVector& op) const; + /** Bit-vector negation. */ + wrappedBitVector operator-(void) const; + /** Bit-wise not. */ + wrappedBitVector operator~(void) const; + + /** Bit-vector increment. */ + wrappedBitVector increment() const; + /** Bit-vector decrement. */ + wrappedBitVector decrement() const; + /** + * Bit-vector logical/arithmetic right shift where 'op' extended to the + * bit-width of this wrapped bit-vector. + */ + wrappedBitVector signExtendRightShift( + const wrappedBitVector& op) const; /** - * A concrete floating point number + * Modular operations. + * Note: No overflow checking so these are the same as other operations. */ + wrappedBitVector modularLeftShift( + const wrappedBitVector& op) const; + wrappedBitVector modularRightShift( + const wrappedBitVector& op) const; + wrappedBitVector modularIncrement() const; + wrappedBitVector modularDecrement() const; + wrappedBitVector modularAdd( + const wrappedBitVector& op) const; + wrappedBitVector modularNegate() const; + + /** Bit-vector equality. */ + CVC4Prop operator==(const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned less or equal than. */ + CVC4Prop operator<=(const wrappedBitVector& op) const; + /** Bit-vector sign/unsigned greater or equal than. */ + CVC4Prop operator>=(const wrappedBitVector& op) const; + /** Bit-vector signed/unsigned less than. */ + CVC4Prop operator<(const wrappedBitVector& op) const; + /** Bit-vector sign/unsigned greater or equal than. */ + CVC4Prop operator>(const wrappedBitVector& op) const; + + /** Convert this bit-vector to a signed bit-vector. */ + wrappedBitVector toSigned(void) const; + /** Convert this bit-vector to an unsigned bit-vector. */ + wrappedBitVector toUnsigned(void) const; + + /** Bit-vector signed/unsigned (zero) extension. */ + wrappedBitVector extend(CVC4BitWidth extension) const; + /** + * Create a "contracted" bit-vector by cutting off the 'reduction' number of + * most significant bits, i.e., by extracting the (bit-width - reduction) + * least significant bits. + */ + wrappedBitVector contract(CVC4BitWidth reduction) const; + /** + * Create a "resized" bit-vector of given size bei either extending (if new + * size is larger) or contracting (if it is smaller) this wrapped bit-vector. + */ + wrappedBitVector resize(CVC4BitWidth newSize) const; + /** + * Create an extension of this bit-vector that matches the bit-width of the + * given bit-vector. + * Note: The size of the given bit-vector may not be larger than the size of + * this bit-vector. + */ + wrappedBitVector matchWidth( + const wrappedBitVector& op) const; + /** Bit-vector concatenation. */ + wrappedBitVector append(const wrappedBitVector& op) const; + + /** Inclusive of end points, thus if the same, extracts just one bit. */ + wrappedBitVector extract(CVC4BitWidth upper, + CVC4BitWidth lower) const; +}; +} // namespace symfpuLiteral + +/** + * A concrete floating point value. + */ +// clang-format off #if @CVC4_USE_SYMFPU@ - using FloatingPointLiteral = ::symfpu::unpackedFloat; +// 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(unsigned, unsigned, double) { unfinished(); } - FloatingPointLiteral(unsigned, unsigned, 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 CVC4_PUBLIC FloatingPointLiteral +{ + public: + // This intentional left unfinished as the choice of literal + // representation is solver specific. + void unfinished(void) const; + + FloatingPointLiteral(unsigned, unsigned, double) { unfinished(); } + FloatingPointLiteral(unsigned, unsigned, const std::string&) { unfinished(); } + FloatingPointLiteral(const FloatingPointLiteral&) { unfinished(); } + bool operator==(const FloatingPointLiteral& op) const + { + unfinished(); + return false; + } - class CVC4_PUBLIC FloatingPoint { - protected : - FloatingPointLiteral fpl; - - public : - FloatingPointSize t; - - /** Constructors. */ - FloatingPoint(unsigned e, unsigned s, const BitVector& bv); - FloatingPoint(const FloatingPointSize& size, const BitVector& bv); - - FloatingPoint(const FloatingPointSize& oldt, - const FloatingPointLiteral& oldfpl) - : fpl(oldfpl), t(oldt) - { - } - - FloatingPoint(const FloatingPoint& fp) : fpl(fp.fpl), t(fp.t) {} - FloatingPoint(const FloatingPointSize& size, - const RoundingMode& rm, - const BitVector& bv, - bool signedBV); - FloatingPoint(const FloatingPointSize& size, - const RoundingMode& rm, - const Rational& r); - - /** - * Create a FP NaN value of given size. - * t: The FP size (format). - */ - static FloatingPoint makeNaN (const FloatingPointSize &size); - /** - * Create a FP infinity value of given size. - * t: The FP size (format). - * sign: True for +oo, false otherwise. - */ - static FloatingPoint makeInf(const FloatingPointSize& size, bool sign); - /** - * Create a FP zero value of given size. - * t: The FP size (format). - * sign: True for +zero, false otherwise. - */ - static FloatingPoint makeZero(const FloatingPointSize& size, bool sign); - /** - * Create the smallest subnormal FP value of given size. - * t: The FP size (format). - * sign: True for positive sign, false otherwise. - */ - static FloatingPoint makeMinSubnormal(const FloatingPointSize& size, - bool sign); - /** - * Create the largest subnormal FP value of given size. - * t: The FP size (format). - * sign: True for positive sign, false otherwise. - */ - static FloatingPoint makeMaxSubnormal(const FloatingPointSize& size, - bool sign); - /** - * Create the smallest normal FP value of given size. - * t: The FP size (format). - * sign: True for positive sign, false otherwise. - */ - static FloatingPoint makeMinNormal(const FloatingPointSize& size, - bool sign); - /** - * Create the largest normal FP value of given size. - * t: The FP size (format). - * sign: True for positive sign, false otherwise. - */ - static FloatingPoint makeMaxNormal(const FloatingPointSize& size, - bool sign); - - const FloatingPointLiteral& getLiteral(void) const { return this->fpl; } - - /* Return string representation. - * - * If printAsIndexed is true then it prints - * the bit-vector components of the FP value as indexed symbols, otherwise - * in binary notation. */ - std::string toString(bool printAsIndexed = false) const; - - // Gives the corresponding IEEE-754 transfer format - BitVector pack (void) const; - - - FloatingPoint absolute (void) const; - FloatingPoint negate (void) const; - FloatingPoint plus (const RoundingMode &rm, const FloatingPoint &arg) const; - FloatingPoint sub (const RoundingMode &rm, const FloatingPoint &arg) const; - FloatingPoint mult (const RoundingMode &rm, const FloatingPoint &arg) const; - FloatingPoint div (const RoundingMode &rm, const FloatingPoint &arg) const; - FloatingPoint fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const; - FloatingPoint sqrt (const RoundingMode &rm) const; - FloatingPoint rti (const RoundingMode &rm) const; - FloatingPoint rem (const FloatingPoint &arg) const; - - // zeroCase is whether the left or right is returned in the case of min/max(-0,+0) or (+0,-0) - FloatingPoint maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const; - FloatingPoint minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const; - - // These detect when the answer is defined - typedef std::pair PartialFloatingPoint; - - PartialFloatingPoint max (const FloatingPoint &arg) const; - PartialFloatingPoint min (const FloatingPoint &arg) const; - - - bool operator ==(const FloatingPoint& fp) const; - bool operator <= (const FloatingPoint &arg) const; - bool operator < (const FloatingPoint &arg) const; - - bool isNormal (void) const; - bool isSubnormal (void) const; - bool isZero (void) const; - bool isInfinite (void) const; - bool isNaN (void) const; - bool isNegative (void) const; - bool isPositive (void) const; - - FloatingPoint convert (const FloatingPointSize &target, const RoundingMode &rm) const; - - // These require a value to return in the undefined case - BitVector convertToBVTotal (BitVectorSize width, const RoundingMode &rm, - bool signedBV, BitVector undefinedCase) const; - Rational convertToRationalTotal (Rational undefinedCase) const; - - // These detect when the answer is defined - typedef std::pair PartialBitVector; - typedef std::pair PartialRational; - - PartialBitVector convertToBV (BitVectorSize width, const RoundingMode &rm, - bool signedBV) const; - PartialRational convertToRational (void) const; - - }; /* class FloatingPoint */ - - - struct CVC4_PUBLIC FloatingPointHashFunction { - size_t operator() (const FloatingPoint& fp) const { - FloatingPointSizeHashFunction fpshf; - BitVectorHashFunction bvhf; - - return fpshf(fp.t) ^ bvhf(fp.pack()); - } - }; /* struct FloatingPointHashFunction */ + size_t hash(void) const + { + unfinished(); + return 23; + } +}; +#endif /* @CVC4_USE_SYMFPU@ */ +class CVC4_PUBLIC FloatingPoint +{ + public: /** - * The parameter type for the conversions to floating point. + * Wrappers to represent results of non-total functions (e.g., min/max). + * The Boolean flag is true if the result is defined, and false otherwise. */ - class CVC4_PUBLIC FloatingPointConvertSort { - public : - FloatingPointSize t; + using PartialFloatingPoint = std::pair; + using PartialBitVector = std::pair; + using PartialRational = std::pair; - FloatingPointConvertSort (unsigned _e, unsigned _s) - : t(_e,_s) {} - FloatingPointConvertSort (const FloatingPointSize &fps) - : t(fps) {} + /** Constructors. */ + FloatingPoint(unsigned e, unsigned s, const BitVector& bv); + FloatingPoint(const FloatingPointSize& size, const BitVector& bv); - bool operator ==(const FloatingPointConvertSort& fpcs) const { - return t == fpcs.t; - } + 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) + { + } + FloatingPoint(const FloatingPointSize& size, + const RoundingMode& rm, + const BitVector& bv, + bool signedBV); + FloatingPoint(const FloatingPointSize& size, + const RoundingMode& rm, + const Rational& r); /** - * As different conversions are different parameterised kinds, there - * is a need for different (C++) types for each one. + * Create a FP NaN value of given size. + * size: The FP size (format). */ + static FloatingPoint makeNaN(const FloatingPointSize& size); + /** + * Create a FP infinity value of given size. + * size: The FP size (format). + * sign: True for -oo, false otherwise. + */ + static FloatingPoint makeInf(const FloatingPointSize& size, bool sign); + /** + * Create a FP zero value of given size. + * size: The FP size (format). + * sign: True for -zero, false otherwise. + */ + static FloatingPoint makeZero(const FloatingPointSize& size, bool sign); + /** + * Create the smallest subnormal FP value of given size. + * size: The FP size (format). + * sign: True for negative sign, false otherwise. + */ + static FloatingPoint makeMinSubnormal(const FloatingPointSize& size, + bool sign); + /** + * Create the largest subnormal FP value of given size. + * size: The FP size (format). + * sign: True for negative sign, false otherwise. + */ + static FloatingPoint makeMaxSubnormal(const FloatingPointSize& size, + bool sign); + /** + * Create the smallest normal FP value of given size. + * size: The FP size (format). + * sign: True for negative sign, false otherwise. + */ + static FloatingPoint makeMinNormal(const FloatingPointSize& size, bool sign); + /** + * Create the largest normal FP value of given size. + * size: The FP size (format). + * sign: True for negative sign, false otherwise. + */ + static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign); - class CVC4_PUBLIC FloatingPointToFPIEEEBitVector : public FloatingPointConvertSort { - public : - FloatingPointToFPIEEEBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} - FloatingPointToFPIEEEBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} - }; - - class CVC4_PUBLIC FloatingPointToFPFloatingPoint : public FloatingPointConvertSort { - public : - FloatingPointToFPFloatingPoint (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} - FloatingPointToFPFloatingPoint (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} - }; - - class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort { - public : - FloatingPointToFPReal (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} - FloatingPointToFPReal (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} - }; - - class CVC4_PUBLIC FloatingPointToFPSignedBitVector : public FloatingPointConvertSort { - public : - FloatingPointToFPSignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} - FloatingPointToFPSignedBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} - }; + /** Get the wrapped floating-point value. */ + const FloatingPointLiteral& getLiteral(void) const { return this->d_fpl; } - class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort { - public : - FloatingPointToFPUnsignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} - FloatingPointToFPUnsignedBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} - }; + /** + * Return a string representation of this floating-point. + * + * If printAsIndexed is true then it prints the bit-vector components of the + * FP value as indexed symbols, otherwise in binary notation. + */ + std::string toString(bool printAsIndexed = false) const; + + /** Return the packed (IEEE-754) representation of this floating-point. */ + BitVector pack(void) const; + + /** Floating-point absolute value. */ + FloatingPoint absolute(void) const; + /** Floating-point negation. */ + FloatingPoint negate(void) const; + /** Floating-point addition. */ + FloatingPoint plus(const RoundingMode& rm, const FloatingPoint& arg) const; + /** Floating-point subtraction. */ + FloatingPoint sub(const RoundingMode& rm, const FloatingPoint& arg) const; + /** Floating-point multiplication. */ + FloatingPoint mult(const RoundingMode& rm, const FloatingPoint& arg) const; + /** Floating-point division. */ + FloatingPoint div(const RoundingMode& rm, const FloatingPoint& arg) const; + /** Floating-point fused multiplication and addition. */ + FloatingPoint fma(const RoundingMode& rm, + const FloatingPoint& arg1, + const FloatingPoint& arg2) const; + /** Floating-point square root. */ + FloatingPoint sqrt(const RoundingMode& rm) const; + /** Floating-point round to integral. */ + FloatingPoint rti(const RoundingMode& rm) const; + /** Floating-point remainder. */ + FloatingPoint rem(const FloatingPoint& arg) const; - class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort { - public : - FloatingPointToFPGeneric (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {} - FloatingPointToFPGeneric (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {} - }; + /** + * Floating-point max (total version). + * zeroCase: true to return the left (rather than the right operand) in case + * of max(-0,+0) or max(+0,-0). + */ + FloatingPoint maxTotal(const FloatingPoint& arg, bool zeroCaseLeft) const; + /** + * Floating-point min (total version). + * zeroCase: true to return the left (rather than the right operand) in case + * of min(-0,+0) or min(+0,-0). + */ + FloatingPoint minTotal(const FloatingPoint& arg, bool zeroCaseLeft) const; + /** + * Floating-point max. + * + * Returns a partial floating-point, which is a pair of FloatingPoint and + * bool. The boolean flag is true if the result is defined, and false if it + * is undefined. + */ + PartialFloatingPoint max(const FloatingPoint& arg) const; + /** Floating-point min. + * + * Returns a partial floating-point, which is a pair of FloatingPoint and + * bool. The boolean flag is true if the result is defined, and false if it + * is undefined. + */ + PartialFloatingPoint min(const FloatingPoint& arg) const; + + /** Equality (NOT: fp.eq but =) over floating-point values. */ + bool operator==(const FloatingPoint& fp) const; + /** Floating-point less or equal than. */ + bool operator<=(const FloatingPoint& arg) const; + /** Floating-point less than. */ + bool operator<(const FloatingPoint& arg) 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. */ + bool isSubnormal(void) const; + /** Return true if this floating-point represents a zero value. */ + bool isZero(void) const; + /** Return true if this floating-point represents an infinite value. */ + bool isInfinite(void) const; + /** Return true if this floating-point represents a NaN value. */ + bool isNaN(void) const; + /** Return true if this floating-point represents a negative value. */ + bool isNegative(void) const; + /** Return true if this floating-point represents a positive value. */ + bool isPositive(void) const; + /** + * Convert this floating-point to a floating-point of given size, with + * respect to given rounding mode. + */ + FloatingPoint convert(const FloatingPointSize& target, + const RoundingMode& rm) const; - template - struct CVC4_PUBLIC FloatingPointConvertSortHashFunction { - inline size_t operator() (const FloatingPointConvertSort& fpcs) const { - FloatingPointSizeHashFunction f; - return f(fpcs.t) ^ (0x00005300 | (key << 24)); - } - }; /* struct FloatingPointConvertSortHashFunction */ + /** + * Convert this floating-point to a bit-vector of given size, with + * respect to given rounding mode (total version). + * Returns given bit-vector 'undefinedCase' in the undefined case. + */ + BitVector convertToBVTotal(BitVectorSize width, + const RoundingMode& rm, + bool signedBV, + BitVector undefinedCase) const; + /** + * Convert this floating-point to a rational, with respect to given rounding + * mode (total version). + * Returns given rational 'undefinedCase' in the undefined case. + */ + Rational convertToRationalTotal(Rational undefinedCase) const; + /** + * Convert this floating-point to a bit-vector of given size. + * + * Returns a partial bit-vector, which is a pair of BitVector and bool. + * The boolean flag is true if the result is defined, and false if it + * is undefined. + */ + PartialBitVector convertToBV(BitVectorSize width, + const RoundingMode& rm, + bool signedBV) const; + /** + * Convert this floating-point to a Rational. + * + * Returns a partial Rational, which is a pair of Rational and bool. + * The boolean flag is true if the result is defined, and false if it + * is undefined. + */ + PartialRational convertToRational(void) const; + /** The floating-point size of this floating-point value. */ + FloatingPointSize d_fp_size; + protected: + /** The floating-point literal of this floating-point value. */ + FloatingPointLiteral d_fpl; +}; /* class FloatingPoint */ +/** + * Hash function for floating-point values. + */ +struct CVC4_PUBLIC FloatingPointHashFunction +{ + size_t operator()(const FloatingPoint& fp) const + { + FloatingPointSizeHashFunction fpshf; + BitVectorHashFunction bvhf; + return fpshf(fp.d_fp_size) ^ bvhf(fp.pack()); + } +}; /* struct FloatingPointHashFunction */ + +/* -------------------------------------------------------------------------- */ + +/** + * The parameter type for the conversions to floating point. + */ +class CVC4_PUBLIC FloatingPointConvertSort +{ + public: + /** Constructors. */ + FloatingPointConvertSort(unsigned _e, unsigned _s) : d_fp_size(_e, _s) {} + FloatingPointConvertSort(const FloatingPointSize& fps) : d_fp_size(fps) {} + + /** Operator overload for comparison of conversion sorts. */ + bool operator==(const FloatingPointConvertSort& fpcs) const + { + return d_fp_size == fpcs.d_fp_size; + } + /** The floating-point size of this sort. */ + FloatingPointSize d_fp_size; +}; - /** - * The parameter type for the conversion to bit vector. - */ - class CVC4_PUBLIC FloatingPointToBV { - public : - BitVectorSize bvs; - - FloatingPointToBV (unsigned s) - : bvs(s) {} - FloatingPointToBV (const FloatingPointToBV &old) : bvs(old.bvs) {} - FloatingPointToBV (const BitVectorSize &old) : bvs(old) {} - operator unsigned () const { return bvs; } - }; - - class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV { - public : FloatingPointToUBV (unsigned _s) : FloatingPointToBV(_s) {} - FloatingPointToUBV (const FloatingPointToBV &old) : FloatingPointToBV(old) {} - }; - class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV { - public : FloatingPointToSBV (unsigned _s) : FloatingPointToBV(_s) {} - FloatingPointToSBV (const FloatingPointToBV &old) : FloatingPointToBV(old) {} - }; - class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV { - public : FloatingPointToUBVTotal (unsigned _s) : FloatingPointToBV(_s) {} - FloatingPointToUBVTotal (const FloatingPointToBV &old) : FloatingPointToBV(old) {} - }; - class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV { - public : FloatingPointToSBVTotal (unsigned _s) : FloatingPointToBV(_s) {} - FloatingPointToSBVTotal (const FloatingPointToBV &old) : FloatingPointToBV(old) {} - }; - - - template - struct CVC4_PUBLIC FloatingPointToBVHashFunction { - inline size_t operator() (const FloatingPointToBV& fptbv) const { - UnsignedHashFunction< ::CVC4::BitVectorSize > f; - return (key ^ 0x46504256) ^ f(fptbv.bvs); - } - }; /* struct FloatingPointToBVHashFunction */ - - - // It is not possible to pack a number without a size to pack to, - // thus it is difficult to implement this in a sensible way. Use - // FloatingPoint instead... - /* - inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) CVC4_PUBLIC; - inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) { - return os << "FloatingPointLiteral"; +/** Hash function for conversion sorts. */ +template +struct CVC4_PUBLIC FloatingPointConvertSortHashFunction +{ + inline size_t operator()(const FloatingPointConvertSort& fpcs) const + { + FloatingPointSizeHashFunction f; + return f(fpcs.d_fp_size) ^ (0x00005300 | (key << 24)); } - */ - - inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC; - inline std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp) +}; /* struct FloatingPointConvertSortHashFunction */ + +/** + * As different conversions are different parameterised kinds, there + * is a need for different (C++) types for each one. + */ + +/** + * Conversion from floating-point to IEEE bit-vector (first bit represents the + * sign, the following exponent width bits the exponent, and the remaining bits + * the significand). + */ +class CVC4_PUBLIC FloatingPointToFPIEEEBitVector + : public FloatingPointConvertSort +{ + public: + /** Constructors. */ + FloatingPointToFPIEEEBitVector(unsigned _e, unsigned _s) + : FloatingPointConvertSort(_e, _s) { - // print in binary notation - return os << fp.toString(); } - - inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) CVC4_PUBLIC; - inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) { - return os << "(_ FloatingPoint " << fps.exponent() << " " << fps.significand() << ")"; + FloatingPointToFPIEEEBitVector(const FloatingPointConvertSort& old) + : FloatingPointConvertSort(old) + { } - - inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) CVC4_PUBLIC; - inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) { - return os << "(_ to_fp " << fpcs.t.exponent() << " " << fpcs.t.significand() << ")"; +}; + +/** + * Conversion from floating-point to another floating-point (of possibly + * different size). + */ +class CVC4_PUBLIC FloatingPointToFPFloatingPoint + : public FloatingPointConvertSort +{ + public: + /** Constructors. */ + FloatingPointToFPFloatingPoint(unsigned _e, unsigned _s) + : FloatingPointConvertSort(_e, _s) + { + } + FloatingPointToFPFloatingPoint(const FloatingPointConvertSort& old) + : FloatingPointConvertSort(old) + { + } +}; + +/** + * Conversion from floating-point to Real. + */ +class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort +{ + public: + /** Constructors. */ + FloatingPointToFPReal(unsigned _e, unsigned _s) + : FloatingPointConvertSort(_e, _s) + { + } + FloatingPointToFPReal(const FloatingPointConvertSort& old) + : FloatingPointConvertSort(old) + { + } +}; + +/** + * Conversion from floating-point to signed bit-vector value. + */ +class CVC4_PUBLIC FloatingPointToFPSignedBitVector + : public FloatingPointConvertSort +{ + public: + /** Constructors. */ + FloatingPointToFPSignedBitVector(unsigned _e, unsigned _s) + : FloatingPointConvertSort(_e, _s) + { + } + FloatingPointToFPSignedBitVector(const FloatingPointConvertSort& old) + : FloatingPointConvertSort(old) + { + } +}; + +/** + * Conversion from floating-point to unsigned bit-vector value. + */ +class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector + : public FloatingPointConvertSort +{ + public: + /** Constructors. */ + FloatingPointToFPUnsignedBitVector(unsigned _e, unsigned _s) + : FloatingPointConvertSort(_e, _s) + { + } + FloatingPointToFPUnsignedBitVector(const FloatingPointConvertSort& old) + : FloatingPointConvertSort(old) + { + } +}; + +class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort +{ + public: + /** Constructors. */ + FloatingPointToFPGeneric(unsigned _e, unsigned _s) + : FloatingPointConvertSort(_e, _s) + { + } + FloatingPointToFPGeneric(const FloatingPointConvertSort& old) + : FloatingPointConvertSort(old) + { + } +}; + +/** + * Base type for floating-point to bit-vector conversion. + */ +class CVC4_PUBLIC FloatingPointToBV +{ + public: + /** Constructors. */ + FloatingPointToBV(unsigned s) : d_bv_size(s) {} + FloatingPointToBV(const FloatingPointToBV& old) : d_bv_size(old.d_bv_size) {} + FloatingPointToBV(const BitVectorSize& old) : d_bv_size(old) {} + + /** Return the bit-width of the bit-vector to convert to. */ + operator unsigned() const { return d_bv_size; } + + /** The bit-width of the bit-vector to converto to. */ + BitVectorSize d_bv_size; +}; + +/** + * Conversion from floating-point to unsigned bit-vector value. + */ +class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV +{ + public: + FloatingPointToUBV(unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToUBV(const FloatingPointToBV& old) : FloatingPointToBV(old) {} +}; + +/** + * Conversion from floating-point to signed bit-vector value. + */ +class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV +{ + public: + FloatingPointToSBV(unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToSBV(const FloatingPointToBV& old) : FloatingPointToBV(old) {} +}; + +/** + * Conversion from floating-point to unsigned bit-vector value (total version). + */ +class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV +{ + public: + FloatingPointToUBVTotal(unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToUBVTotal(const FloatingPointToBV& old) : FloatingPointToBV(old) + { } +}; + +/** + * Conversion from floating-point to signed bit-vector value (total version). + */ +class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV +{ + public: + FloatingPointToSBVTotal(unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToSBVTotal(const FloatingPointToBV& old) : FloatingPointToBV(old) + { + } +}; + +/** + * Hash function for floating-point to bit-vector conversions. + */ +template +struct CVC4_PUBLIC FloatingPointToBVHashFunction +{ + inline size_t operator()(const FloatingPointToBV& fptbv) const + { + UnsignedHashFunction< ::CVC4::BitVectorSize> f; + return (key ^ 0x46504256) ^ f(fptbv.d_bv_size); + } +}; /* struct FloatingPointToBVHashFunction */ + +/* Note: It is not possible to pack a number without a size to pack to, + * thus it is difficult to implement output stream operator overloads for + * FloatingPointLiteral in a sensible way. Use FloatingPoint instead. */ + +/** Output stream operator overloading for floating-point values. */ +std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC; + +/** Output stream operator overloading for floating-point formats. */ +std::ostream& operator<<(std::ostream& os, + const FloatingPointSize& fps) CVC4_PUBLIC; + +/** Output stream operator overloading for floating-point conversion sorts. */ +std::ostream& operator<<(std::ostream& os, + const FloatingPointConvertSort& fpcs) CVC4_PUBLIC; -}/* CVC4 namespace */ +} // namespace CVC4 #endif /* CVC4__FLOATINGPOINT_H */