diff options
Diffstat (limited to 'src/theory/fp/fp_converter.cpp')
| -rw-r--r-- | src/theory/fp/fp_converter.cpp | 411 |
1 files changed, 217 insertions, 194 deletions
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index e4e485fd9..665635c38 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -731,10 +731,10 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract( return symbolicBitVector<isSigned>(construct); } -floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode t) - : FloatingPointSize(t.getConst<FloatingPointSize>()) +floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode type) + : FloatingPointSize(type.getConst<FloatingPointSize>()) { - PRECONDITION(t.isFloatingPoint()); + PRECONDITION(type.isFloatingPoint()); } floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig) : FloatingPointSize(exp, sig) @@ -751,14 +751,14 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const } } -FpConverter::FpConverter(context::UserContext *user) +FpConverter::FpConverter(context::UserContext* user) : #ifdef CVC4_USE_SYMFPU - f(user), - r(user), - b(user), - u(user), - s(user), + d_fpMap(user), + d_rmMap(user), + d_boolMap(user), + d_ubvMap(user), + d_sbvMap(user), #endif d_additionalAssertions(user) { @@ -863,9 +863,9 @@ Node FpConverter::convert(TNode node) if (t.isRoundingMode()) { - rmMap::const_iterator i(r.find(current)); + rmMap::const_iterator i(d_rmMap.find(current)); - if (i == r.end()) + if (i == d_rmMap.end()) { if (Theory::isLeafOf(current, THEORY_FP)) { @@ -875,14 +875,20 @@ Node FpConverter::convert(TNode node) switch (current.getConst<RoundingMode>()) { case roundNearestTiesToEven: - r.insert(current, traits::RNE()); + d_rmMap.insert(current, traits::RNE()); break; case roundNearestTiesToAway: - r.insert(current, traits::RNA()); + d_rmMap.insert(current, traits::RNA()); + break; + case roundTowardPositive: + d_rmMap.insert(current, traits::RTP()); + break; + case roundTowardNegative: + d_rmMap.insert(current, traits::RTN()); + break; + case roundTowardZero: + d_rmMap.insert(current, traits::RTZ()); break; - case roundTowardPositive: r.insert(current, traits::RTP()); break; - case roundTowardNegative: r.insert(current, traits::RTN()); break; - case roundTowardZero: r.insert(current, traits::RTZ()); break; default: Unreachable() << "Unknown rounding mode"; break; } } @@ -890,7 +896,7 @@ Node FpConverter::convert(TNode node) { /******** Variables ********/ rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, current)); - r.insert(current, tmp); + d_rmMap.insert(current, tmp); d_additionalAssertions.push_back(tmp.valid()); } } @@ -903,23 +909,23 @@ Node FpConverter::convert(TNode node) } else if (t.isFloatingPoint()) { - fpMap::const_iterator i(f.find(current)); + fpMap::const_iterator i(d_fpMap.find(current)); - if (i == f.end()) + if (i == d_fpMap.end()) { if (Theory::isLeafOf(current, THEORY_FP)) { if (current.getKind() == kind::CONST_FLOATINGPOINT) { /******** Constants ********/ - f.insert(current, - symfpu::unpackedFloat<traits>( - current.getConst<FloatingPoint>().getLiteral())); + d_fpMap.insert(current, + symfpu::unpackedFloat<traits>( + current.getConst<FloatingPoint>().getLiteral())); } else { /******** Variables ********/ - f.insert(current, buildComponents(current)); + d_fpMap.insert(current, buildComponents(current)); } } else @@ -937,9 +943,9 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_ABS: case kind::FLOATINGPOINT_NEG: { - fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current); workStack.push_back(current[0]); @@ -949,14 +955,14 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_ABS: - f.insert(current, - symfpu::absolute<traits>(fpt(current.getType()), - (*arg1).second)); + d_fpMap.insert(current, + symfpu::absolute<traits>( + fpt(current.getType()), (*arg1).second)); break; case kind::FLOATINGPOINT_NEG: - f.insert(current, - symfpu::negate<traits>(fpt(current.getType()), - (*arg1).second)); + d_fpMap.insert(current, + symfpu::negate<traits>(fpt(current.getType()), + (*arg1).second)); break; default: Unreachable() << "Unknown unary floating-point function"; @@ -968,18 +974,19 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_SQRT: case kind::FLOATINGPOINT_RTI: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -989,13 +996,13 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_SQRT: - f.insert(current, - symfpu::sqrt<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second)); + d_fpMap.insert(current, + symfpu::sqrt<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second)); break; case kind::FLOATINGPOINT_RTI: - f.insert( + d_fpMap.insert( current, symfpu::roundToIntegral<traits>(fpt(current.getType()), (*mode).second, @@ -1011,25 +1018,26 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_REM: { - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - f.insert( + d_fpMap.insert( current, symfpu::remainder<traits>( fpt(current.getType()), (*arg1).second, (*arg2).second)); @@ -1039,20 +1047,21 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_MIN_TOTAL: case kind::FLOATINGPOINT_MAX_TOTAL: { - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); // current[2] is a bit-vector so we do not need to recurse down it - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1062,19 +1071,19 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_MAX_TOTAL: - f.insert(current, - symfpu::max<traits>(fpt(current.getType()), - (*arg1).second, - (*arg2).second, - prop(current[2]))); + d_fpMap.insert(current, + symfpu::max<traits>(fpt(current.getType()), + (*arg1).second, + (*arg2).second, + prop(current[2]))); break; case kind::FLOATINGPOINT_MIN_TOTAL: - f.insert(current, - symfpu::min<traits>(fpt(current.getType()), - (*arg1).second, - (*arg2).second, - prop(current[2]))); + d_fpMap.insert(current, + symfpu::min<traits>(fpt(current.getType()), + (*arg1).second, + (*arg2).second, + prop(current[2]))); break; default: @@ -1090,24 +1099,25 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_MULT: case kind::FLOATINGPOINT_DIV: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - fpMap::const_iterator arg2(f.find(current[2])); - bool recurseNeeded = - (mode == r.end()) || (arg1 == f.end()) || (arg2 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + fpMap::const_iterator arg2(d_fpMap.find(current[2])); + bool recurseNeeded = (mode == d_rmMap.end()) + || (arg1 == d_fpMap.end()) + || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[2]); } @@ -1117,12 +1127,12 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_PLUS: - f.insert(current, - symfpu::add<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second, - prop(true))); + d_fpMap.insert(current, + symfpu::add<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + prop(true))); break; case kind::FLOATINGPOINT_SUB: @@ -1133,22 +1143,23 @@ Node FpConverter::convert(TNode node) break; case kind::FLOATINGPOINT_MULT: - f.insert(current, - symfpu::multiply<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second)); + d_fpMap.insert( + current, + symfpu::multiply<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); break; case kind::FLOATINGPOINT_DIV: - f.insert(current, - symfpu::divide<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second)); + d_fpMap.insert(current, + symfpu::divide<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); break; case kind::FLOATINGPOINT_REM: /* - f.insert(current, + d_fpMap.insert(current, symfpu::remainder<traits>(fpt(current.getType()), (*mode).second, (*arg1).second, @@ -1169,66 +1180,68 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_FMA: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - fpMap::const_iterator arg2(f.find(current[2])); - fpMap::const_iterator arg3(f.find(current[3])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()) - || (arg2 == f.end() || (arg3 == f.end())); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + fpMap::const_iterator arg2(d_fpMap.find(current[2])); + fpMap::const_iterator arg3(d_fpMap.find(current[3])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()) + || (arg2 == d_fpMap.end() || (arg3 == d_fpMap.end())); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[2]); } - if (arg3 == f.end()) + if (arg3 == d_fpMap.end()) { workStack.push_back(current[3]); } continue; // i.e. recurse! } - f.insert(current, - symfpu::fma<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second, - (*arg3).second)); + d_fpMap.insert(current, + symfpu::fma<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + (*arg3).second)); } break; /******** Conversions ********/ case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - f.insert( + d_fpMap.insert( current, symfpu::convertFloatToFloat<traits>(fpt(current[1].getType()), fpt(current.getType()), @@ -1241,27 +1254,28 @@ Node FpConverter::convert(TNode node) { Node IEEEBV(nm->mkNode( kind::BITVECTOR_CONCAT, current[0], current[1], current[2])); - f.insert(current, - symfpu::unpack<traits>(fpt(current.getType()), IEEEBV)); + d_fpMap.insert( + current, + symfpu::unpack<traits>(fpt(current.getType()), IEEEBV)); } break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: - f.insert(current, - symfpu::unpack<traits>(fpt(current.getType()), - ubv(current[0]))); + d_fpMap.insert(current, + symfpu::unpack<traits>(fpt(current.getType()), + ubv(current[0]))); break; case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: { - rmMap::const_iterator mode(r.find(current[0])); - bool recurseNeeded = (mode == r.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + bool recurseNeeded = (mode == d_rmMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } @@ -1271,7 +1285,7 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: - f.insert( + d_fpMap.insert( current, symfpu::convertSBVToFloat<traits>(fpt(current.getType()), (*mode).second, @@ -1279,7 +1293,7 @@ Node FpConverter::convert(TNode node) break; case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: - f.insert( + d_fpMap.insert( current, symfpu::convertUBVToFloat<traits>(fpt(current.getType()), (*mode).second, @@ -1296,7 +1310,7 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_TO_FP_REAL: { - f.insert(current, buildComponents(current)); + d_fpMap.insert(current, buildComponents(current)); // Rely on the real theory and theory combination // to handle the value } @@ -1316,9 +1330,9 @@ Node FpConverter::convert(TNode node) } else if (t.isBoolean()) { - boolMap::const_iterator i(b.find(current)); + boolMap::const_iterator i(d_boolMap.find(current)); - if (i == b.end()) + if (i == d_boolMap.end()) { switch (current.getKind()) { @@ -1329,49 +1343,52 @@ Node FpConverter::convert(TNode node) if (childType.isFloatingPoint()) { - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - b.insert(current, - symfpu::smtlibEqual<traits>( - fpt(childType), (*arg1).second, (*arg2).second)); + d_boolMap.insert( + current, + symfpu::smtlibEqual<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); } else if (childType.isRoundingMode()) { - rmMap::const_iterator arg1(r.find(current[0])); - rmMap::const_iterator arg2(r.find(current[1])); - bool recurseNeeded = (arg1 == r.end()) || (arg2 == r.end()); + rmMap::const_iterator arg1(d_rmMap.find(current[0])); + rmMap::const_iterator arg2(d_rmMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_rmMap.end()) || (arg2 == d_rmMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == r.end()) + if (arg1 == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg2 == r.end()) + if (arg2 == d_rmMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - b.insert(current, (*arg1).second == (*arg2).second); + d_boolMap.insert(current, (*arg1).second == (*arg2).second); } else { @@ -1386,18 +1403,19 @@ Node FpConverter::convert(TNode node) { TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1407,15 +1425,17 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_LEQ: - b.insert(current, - symfpu::lessThanOrEqual<traits>( - fpt(childType), (*arg1).second, (*arg2).second)); + d_boolMap.insert( + current, + symfpu::lessThanOrEqual<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); break; case kind::FLOATINGPOINT_LT: - b.insert(current, - symfpu::lessThan<traits>( - fpt(childType), (*arg1).second, (*arg2).second)); + d_boolMap.insert( + current, + symfpu::lessThan<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); break; default: @@ -1434,9 +1454,9 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_ISPOS: { TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current); workStack.push_back(current[0]); @@ -1446,42 +1466,43 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_ISN: - b.insert( + d_boolMap.insert( current, symfpu::isNormal<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISSN: - b.insert(current, - symfpu::isSubnormal<traits>(fpt(childType), - (*arg1).second)); + d_boolMap.insert(current, + symfpu::isSubnormal<traits>(fpt(childType), + (*arg1).second)); break; case kind::FLOATINGPOINT_ISZ: - b.insert( + d_boolMap.insert( current, symfpu::isZero<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISINF: - b.insert( + d_boolMap.insert( current, symfpu::isInfinite<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISNAN: - b.insert(current, - symfpu::isNaN<traits>(fpt(childType), (*arg1).second)); + d_boolMap.insert( + current, + symfpu::isNaN<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISPOS: - b.insert( + d_boolMap.insert( current, symfpu::isPositive<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISNEG: - b.insert( + d_boolMap.insert( current, symfpu::isNegative<traits>(fpt(childType), (*arg1).second)); break; @@ -1513,7 +1534,7 @@ Node FpConverter::convert(TNode node) break; } - i = b.find(current); + i = d_boolMap.find(current); } result = (*i).second; @@ -1526,22 +1547,23 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_TO_UBV_TOTAL: { TypeNode childType(current[1].getType()); - ubvMap::const_iterator i(u.find(current)); + ubvMap::const_iterator i(d_ubvMap.find(current)); - if (i == u.end()) + if (i == d_ubvMap.end()) { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1551,13 +1573,13 @@ Node FpConverter::convert(TNode node) FloatingPointToUBVTotal info = current.getOperator().getConst<FloatingPointToUBVTotal>(); - u.insert(current, - symfpu::convertFloatToUBV<traits>(fpt(childType), - (*mode).second, - (*arg1).second, - info.bvs, - ubv(current[2]))); - i = u.find(current); + d_ubvMap.insert(current, + symfpu::convertFloatToUBV<traits>(fpt(childType), + (*mode).second, + (*arg1).second, + info.bvs, + ubv(current[2]))); + i = d_ubvMap.find(current); } result = (*i).second; @@ -1567,22 +1589,23 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_TO_SBV_TOTAL: { TypeNode childType(current[1].getType()); - sbvMap::const_iterator i(s.find(current)); + sbvMap::const_iterator i(d_sbvMap.find(current)); - if (i == s.end()) + if (i == d_sbvMap.end()) { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1592,14 +1615,14 @@ Node FpConverter::convert(TNode node) FloatingPointToSBVTotal info = current.getOperator().getConst<FloatingPointToSBVTotal>(); - s.insert(current, - symfpu::convertFloatToSBV<traits>(fpt(childType), - (*mode).second, - (*arg1).second, - info.bvs, - sbv(current[2]))); + d_sbvMap.insert(current, + symfpu::convertFloatToSBV<traits>(fpt(childType), + (*mode).second, + (*arg1).second, + info.bvs, + sbv(current[2]))); - i = s.find(current); + i = d_sbvMap.find(current); } result = (*i).second; @@ -1639,9 +1662,9 @@ Node FpConverter::convert(TNode node) // (via auxiliary constraints) TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current); workStack.push_back(current[0]); @@ -1689,9 +1712,9 @@ Node FpConverter::getValue(Valuation &val, TNode var) if (t.isRoundingMode()) { - rmMap::const_iterator i(r.find(var)); + rmMap::const_iterator i(d_rmMap.find(var)); - if (i == r.end()) + if (i == d_rmMap.end()) { Unreachable() << "Asking for the value of an unregistered expression"; } @@ -1703,9 +1726,9 @@ Node FpConverter::getValue(Valuation &val, TNode var) } else if (t.isFloatingPoint()) { - fpMap::const_iterator i(f.find(var)); + fpMap::const_iterator i(d_fpMap.find(var)); - if (i == f.end()) + if (i == d_fpMap.end()) { Unreachable() << "Asking for the value of an unregistered expression"; } |