From 4bdba195950858dc1b2b9afa80d216dc58c66b68 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 17 Nov 2020 16:45:39 -0800 Subject: 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. --- src/theory/fp/fp_converter.cpp | 4 +- src/theory/fp/theory_fp_rewriter.cpp | 73 ++++++++++++++++++++---------------- src/theory/fp/theory_fp_type_rules.h | 49 +++++++++++++----------- 3 files changed, 70 insertions(+), 56 deletions(-) (limited to 'src/theory') 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; -- cgit v1.2.3