diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/fp/fp_converter.cpp | 4 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 73 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_type_rules.h | 49 |
3 files changed, 70 insertions, 56 deletions
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<traits>(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<traits>(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>()); FloatingPoint arg2(node[2].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[2].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg3(node[3].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[2].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - 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>()); FloatingPoint arg2(node[1].getConst<FloatingPoint>()); - 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<FloatingPointToFPIEEEBitVector>(); const BitVector &bv = node[0].getConst<BitVector>(); - - 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<FloatingPoint>()); FloatingPointToFPFloatingPoint info = node.getOperator().getConst<FloatingPointToFPFloatingPoint>(); - 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<RoundingMode>()); Rational arg(node[1].getConst<Rational>()); - 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<RoundingMode>()); BitVector arg(node[1].getConst<BitVector>()); - 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<RoundingMode>()); BitVector arg(node[1].getConst<BitVector>()); - 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<RoundingMode>()); FloatingPoint arg(node[1].getConst<FloatingPoint>()); - 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<RoundingMode>()); FloatingPoint arg(node[1].getConst<FloatingPoint>()); - 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>()); - 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>()); - 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<FloatingPoint>(); - 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<FloatingPointSize>(); - 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<FloatingPointSize>(); - 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; |