From: Aina Niemetz Date: Tue, 29 Jun 2021 16:18:55 +0000 (-0700) Subject: FP: Refactor, rewrite and clean up word blasting. (#6802) X-Git-Tag: cvc5-1.0.0~1549 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=877b75447b27da04d81ff3ee91eaad7bf00ea083;p=cvc5.git FP: Refactor, rewrite and clean up word blasting. (#6802) This rewrites the word blasting function FpConverter::convert to be easier to follow and read. It further cleans up several things. This additionally prepares for allowing to convert incoming facts rather than terms registered with theory FP. That is, when word blasting more lazily, in preNotifyFact rather than in registerTerm. --- diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 0e196c0e0..e309ab2e4 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -820,868 +820,469 @@ FpConverter::uf FpConverter::buildComponents(TNode current) return tmp; } -// Non-convertible things should only be added to the stack at the very start, -// thus... -#define CVC5_FPCONV_PASSTHROUGH Assert(workStack.empty()) - Node FpConverter::convert(TNode node) { - std::vector workStack; - TNode result = node; - - workStack.push_back(node); + std::vector visit; + std::unordered_map visited; + NodeManager* nm = NodeManager::currentNM(); - NodeManager *nm = NodeManager::currentNM(); + visit.push_back(node); - while (!workStack.empty()) + while (!visit.empty()) { - TNode current = workStack.back(); - workStack.pop_back(); - result = current; + TNode cur = visit.back(); + visit.pop_back(); + TypeNode t(cur.getType()); + + /* Already word-blasted, skip. */ + if ((t.isBoolean() && d_boolMap.find(cur) != d_boolMap.end()) + || (t.isRoundingMode() && d_rmMap.find(cur) != d_rmMap.end()) + || (t.isBitVector() + && (d_sbvMap.find(cur) != d_sbvMap.end() + || d_ubvMap.find(cur) != d_ubvMap.end())) + || (t.isFloatingPoint() && d_fpMap.find(cur) != d_fpMap.end())) + { + continue; + } + + Kind kind = cur.getKind(); - TypeNode t(current.getType()); + if (t.isReal() && kind != kind::FLOATINGPOINT_TO_REAL_TOTAL) + { + // The only nodes with Real sort in Theory FP are of kind + // kind::FLOATINGPOINT_TO_REAL_TOTAL (kind::FLOATINGPOINT_TO_REAL is + // rewritten to kind::FLOATINGPOINT_TO_REAL_TOTAL). + // We don't need to do anything explicitly with them since they will be + // treated as an uninterpreted function by the Real theory and we don't + // need to bit-blast the float expression unless we need to say something + // about its value. + // + // We still have to word blast it's arguments, though. + // + // All other Real expressions can be skipped. + continue; + } - if (t.isRoundingMode()) + auto it = visited.find(cur); + if (it == visited.end()) + { + visited.emplace(cur, 0); + visit.push_back(cur); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + else if (it->second == false) { - rmMap::const_iterator i(d_rmMap.find(current)); + it->second = true; - if (i == d_rmMap.end()) + if (t.isRoundingMode()) { - if (Theory::isLeafOf(current, THEORY_FP)) + /* ---- RoundingMode constants and variables -------------- */ + Assert(Theory::isLeafOf(cur, THEORY_FP)); + if (kind == kind::CONST_ROUNDINGMODE) { - if (current.getKind() == kind::CONST_ROUNDINGMODE) + switch (cur.getConst()) { - /******** Constants ********/ - switch (current.getConst()) - { - case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: - d_rmMap.insert(current, traits::RNE()); - break; - case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: - d_rmMap.insert(current, traits::RNA()); - break; - case RoundingMode::ROUND_TOWARD_POSITIVE: - d_rmMap.insert(current, traits::RTP()); - break; - case RoundingMode::ROUND_TOWARD_NEGATIVE: - d_rmMap.insert(current, traits::RTN()); - break; - case RoundingMode::ROUND_TOWARD_ZERO: - d_rmMap.insert(current, traits::RTZ()); - break; - default: Unreachable() << "Unknown rounding mode"; break; - } - } - else - { - /******** Variables ********/ - rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, current)); - d_rmMap.insert(current, tmp); - d_additionalAssertions.push_back(tmp.valid()); + case RoundingMode::ROUND_NEAREST_TIES_TO_EVEN: + d_rmMap.insert(cur, traits::RNE()); + break; + case RoundingMode::ROUND_NEAREST_TIES_TO_AWAY: + d_rmMap.insert(cur, traits::RNA()); + break; + case RoundingMode::ROUND_TOWARD_POSITIVE: + d_rmMap.insert(cur, traits::RTP()); + break; + case RoundingMode::ROUND_TOWARD_NEGATIVE: + d_rmMap.insert(cur, traits::RTN()); + break; + case RoundingMode::ROUND_TOWARD_ZERO: + d_rmMap.insert(cur, traits::RTZ()); + break; + default: Unreachable() << "Unknown rounding mode"; break; } } else { - Unreachable() << "Unknown kind of type RoundingMode"; + rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, cur)); + d_rmMap.insert(cur, tmp); + d_additionalAssertions.push_back(tmp.valid()); } } - // Returns a rounding-mode type so don't alter the return value - } - else if (t.isFloatingPoint()) - { - fpMap::const_iterator i(d_fpMap.find(current)); - - if (i == d_fpMap.end()) + else if (t.isFloatingPoint()) { - if (Theory::isLeafOf(current, THEORY_FP)) + /* ---- FloatingPoint constants and variables ------------- */ + if (Theory::isLeafOf(cur, THEORY_FP)) { - if (current.getKind() == kind::CONST_FLOATINGPOINT) + if (kind == kind::CONST_FLOATINGPOINT) { - /******** Constants ********/ d_fpMap.insert( - current, - symfpu::unpackedFloat(current.getConst() - .getLiteral() - ->getSymUF())); + cur, + symfpu::unpackedFloat( + cur.getConst().getLiteral()->getSymUF())); } else { - /******** Variables ********/ - d_fpMap.insert(current, buildComponents(current)); + d_fpMap.insert(cur, buildComponents(cur)); } } else { - switch (current.getKind()) + /* ---- FloatingPoint operators --------------------------- */ + Assert(kind != kind::CONST_FLOATINGPOINT); + Assert(kind != kind::VARIABLE); + Assert(kind != kind::BOUND_VARIABLE && kind != kind::SKOLEM); + + switch (kind) { - case kind::CONST_FLOATINGPOINT: - case kind::VARIABLE: - case kind::BOUND_VARIABLE: - case kind::SKOLEM: - Unreachable() << "Kind should have been handled as a leaf."; + /* ---- Arithmetic operators ---- */ + case kind::FLOATINGPOINT_ABS: + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + d_fpMap.insert( + cur, + symfpu::absolute(fpt(t), + (*d_fpMap.find(cur[0])).second)); break; - /******** Operations ********/ - case kind::FLOATINGPOINT_ABS: case kind::FLOATINGPOINT_NEG: - { - fpMap::const_iterator arg1(d_fpMap.find(current[0])); - - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current); - workStack.push_back(current[0]); - continue; // i.e. recurse! - } - - switch (current.getKind()) - { - case kind::FLOATINGPOINT_ABS: - d_fpMap.insert(current, - symfpu::absolute( - fpt(current.getType()), (*arg1).second)); - break; - case kind::FLOATINGPOINT_NEG: - d_fpMap.insert(current, - symfpu::negate(fpt(current.getType()), - (*arg1).second)); - break; - default: - Unreachable() << "Unknown unary floating-point function"; - break; - } - } - break; + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + d_fpMap.insert( + cur, + symfpu::negate(fpt(t), + (*d_fpMap.find(cur[0])).second)); + break; case kind::FLOATINGPOINT_SQRT: + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + d_fpMap.insert( + cur, + symfpu::sqrt(fpt(t), + (*d_rmMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second)); + break; + case kind::FLOATINGPOINT_RTI: - { - 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 == d_rmMap.end()) - { - workStack.push_back(current[0]); - } - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - continue; // i.e. recurse! - } - - switch (current.getKind()) - { - case kind::FLOATINGPOINT_SQRT: - d_fpMap.insert(current, - symfpu::sqrt(fpt(current.getType()), - (*mode).second, - (*arg1).second)); - break; - case kind::FLOATINGPOINT_RTI: - d_fpMap.insert( - current, - symfpu::roundToIntegral(fpt(current.getType()), - (*mode).second, - (*arg1).second)); - break; - default: - Unreachable() - << "Unknown unary rounded floating-point function"; - break; - } - } - break; + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + d_fpMap.insert(cur, + symfpu::roundToIntegral( + fpt(t), + (*d_rmMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second)); + break; case kind::FLOATINGPOINT_REM: - { - 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 == d_fpMap.end()) - { - workStack.push_back(current[0]); - } - if (arg2 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - continue; // i.e. recurse! - } - + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); d_fpMap.insert( - current, - symfpu::remainder( - fpt(current.getType()), (*arg1).second, (*arg2).second)); - } - break; + cur, + symfpu::remainder(fpt(t), + (*d_fpMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second)); + break; - case kind::FLOATINGPOINT_MIN_TOTAL: case kind::FLOATINGPOINT_MAX_TOTAL: - { - 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 == d_fpMap.end()) || (arg2 == d_fpMap.end()); - - if (recurseNeeded) - { - workStack.push_back(current); - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current[0]); - } - if (arg2 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - continue; // i.e. recurse! - } - - switch (current.getKind()) - { - case kind::FLOATINGPOINT_MAX_TOTAL: - d_fpMap.insert(current, - symfpu::max(fpt(current.getType()), - (*arg1).second, - (*arg2).second, - prop(current[2]))); - break; - - case kind::FLOATINGPOINT_MIN_TOTAL: - d_fpMap.insert(current, - symfpu::min(fpt(current.getType()), - (*arg1).second, - (*arg2).second, - prop(current[2]))); - break; - - default: - Unreachable() - << "Unknown binary floating-point partial function"; - break; - } - } - break; + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + Assert(cur[2].getType().isBitVector()); + d_fpMap.insert(cur, + symfpu::max(fpt(t), + (*d_fpMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second, + prop(cur[2]))); + break; + + case kind::FLOATINGPOINT_MIN_TOTAL: + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + Assert(cur[2].getType().isBitVector()); + d_fpMap.insert(cur, + symfpu::min(fpt(t), + (*d_fpMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second, + prop(cur[2]))); + break; case kind::FLOATINGPOINT_ADD: - case kind::FLOATINGPOINT_SUB: + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[2]) != d_fpMap.end()); + d_fpMap.insert(cur, + symfpu::add(fpt(t), + (*d_rmMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second, + (*d_fpMap.find(cur[2])).second, + prop(true))); + break; + case kind::FLOATINGPOINT_MULT: + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[2]) != d_fpMap.end()); + d_fpMap.insert( + cur, + symfpu::multiply(fpt(t), + (*d_rmMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second, + (*d_fpMap.find(cur[2])).second)); + break; + case kind::FLOATINGPOINT_DIV: - { - 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 == d_rmMap.end()) - { - workStack.push_back(current[0]); - } - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - if (arg2 == d_fpMap.end()) - { - workStack.push_back(current[2]); - } - continue; // i.e. recurse! - } - - switch (current.getKind()) - { - case kind::FLOATINGPOINT_ADD: - d_fpMap.insert(current, - symfpu::add(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second, - prop(true))); - break; - - case kind::FLOATINGPOINT_SUB: - // Should have been removed by the rewriter - Unreachable() - << "Floating-point subtraction should be removed by the " - "rewriter."; - break; - - case kind::FLOATINGPOINT_MULT: - d_fpMap.insert( - current, - symfpu::multiply(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second)); - break; - case kind::FLOATINGPOINT_DIV: - d_fpMap.insert(current, - symfpu::divide(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second)); - break; - case kind::FLOATINGPOINT_REM: - /* - d_fpMap.insert(current, - symfpu::remainder(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second)); - */ - Unimplemented() - << "Remainder with rounding mode not yet supported by " - "SMT-LIB"; - break; - - default: - Unreachable() - << "Unknown binary rounded floating-point function"; - break; - } - } - break; + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[2]) != d_fpMap.end()); + d_fpMap.insert( + cur, + symfpu::divide(fpt(t), + (*d_rmMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second, + (*d_fpMap.find(cur[2])).second)); + break; case kind::FLOATINGPOINT_FMA: - { - 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 == d_rmMap.end()) - { - workStack.push_back(current[0]); - } - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - if (arg2 == d_fpMap.end()) - { - workStack.push_back(current[2]); - } - if (arg3 == d_fpMap.end()) - { - workStack.push_back(current[3]); - } - continue; // i.e. recurse! - } - - d_fpMap.insert(current, - symfpu::fma(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second, - (*arg3).second)); - } - break; - - /******** Conversions ********/ - case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: - { - 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 == d_rmMap.end()) - { - workStack.push_back(current[0]); - } - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - continue; // i.e. recurse! - } + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[2]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[3]) != d_fpMap.end()); d_fpMap.insert( - current, - symfpu::convertFloatToFloat(fpt(current[1].getType()), - fpt(current.getType()), - (*mode).second, - (*arg1).second)); - } - break; + cur, + symfpu::fma(fpt(t), + (*d_rmMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second, + (*d_fpMap.find(cur[2])).second, + (*d_fpMap.find(cur[3])).second)); + break; + + /* ---- Conversions ---- */ + case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + d_fpMap.insert(cur, + symfpu::convertFloatToFloat( + fpt(cur[1].getType()), + fpt(t), + (*d_rmMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second)); + break; case kind::FLOATINGPOINT_FP: { - Node IEEEBV(nm->mkNode( - kind::BITVECTOR_CONCAT, current[0], current[1], current[2])); + Assert(cur[0].getType().isBitVector()); + Assert(cur[1].getType().isBitVector()); + Assert(cur[2].getType().isBitVector()); + + Node IEEEBV( + nm->mkNode(kind::BITVECTOR_CONCAT, cur[0], cur[1], cur[2])); d_fpMap.insert( - current, - symfpu::unpack(fpt(current.getType()), IEEEBV)); + cur, symfpu::unpack(fpt(t), IEEEBV)); } break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: - d_fpMap.insert(current, - symfpu::unpack(fpt(current.getType()), - ubv(current[0]))); + Assert(cur[0].getType().isBitVector()); + d_fpMap.insert( + cur, symfpu::unpack(fpt(t), ubv(cur[0]))); break; case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + d_fpMap.insert(cur, + symfpu::convertSBVToFloat( + fpt(t), + (*d_rmMap.find(cur[0])).second, + sbv(cur[1]))); + break; + case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: - { - rmMap::const_iterator mode(d_rmMap.find(current[0])); - bool recurseNeeded = (mode == d_rmMap.end()); - - if (recurseNeeded) - { - workStack.push_back(current); - if (mode == d_rmMap.end()) - { - workStack.push_back(current[0]); - } - continue; // i.e. recurse! - } - - switch (current.getKind()) - { - case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: - d_fpMap.insert( - current, - symfpu::convertSBVToFloat(fpt(current.getType()), - (*mode).second, - sbv(current[1]))); - break; - - case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: - d_fpMap.insert( - current, - symfpu::convertUBVToFloat(fpt(current.getType()), - (*mode).second, - ubv(current[1]))); - break; - - default: - Unreachable() << "Unknown converstion from bit-vector to " - "floating-point"; - break; - } - } - break; + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + d_fpMap.insert(cur, + symfpu::convertUBVToFloat( + fpt(t), + (*d_rmMap.find(cur[0])).second, + ubv(cur[1]))); + break; case kind::FLOATINGPOINT_TO_FP_REAL: - { - d_fpMap.insert(current, buildComponents(current)); + d_fpMap.insert(cur, buildComponents(cur)); // Rely on the real theory and theory combination // to handle the value - } - break; - - case kind::FLOATINGPOINT_TO_FP_GENERIC: - Unreachable() << "Generic to_fp not removed"; break; - default: - Unreachable() << "Unknown kind of type FloatingPoint"; - break; + default: Unreachable() << "Unhandled kind " << kind; break; } } } - // Returns a floating-point type so don't alter the return value - } - else if (t.isBoolean()) - { - boolMap::const_iterator i(d_boolMap.find(current)); - - if (i == d_boolMap.end()) + else if (t.isBoolean()) { - switch (current.getKind()) + switch (kind) { - /******** Comparisons ********/ + /* ---- Comparisons --------------------------------------- */ case kind::EQUAL: { - TypeNode childType(current[0].getType()); + TypeNode childType(cur[0].getType()); if (childType.isFloatingPoint()) { - 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 == d_fpMap.end()) - { - workStack.push_back(current[0]); - } - if (arg2 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - continue; // i.e. recurse! - } - + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); d_boolMap.insert( - current, - symfpu::smtlibEqual( - fpt(childType), (*arg1).second, (*arg2).second)); + cur, + symfpu::smtlibEqual(fpt(childType), + (*d_fpMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second)); } else if (childType.isRoundingMode()) { - 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 == d_rmMap.end()) - { - workStack.push_back(current[0]); - } - if (arg2 == d_rmMap.end()) - { - workStack.push_back(current[1]); - } - continue; // i.e. recurse! - } - - d_boolMap.insert(current, (*arg1).second == (*arg2).second); - } - else - { - CVC5_FPCONV_PASSTHROUGH; - return result; + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_rmMap.find(cur[1]) != d_rmMap.end()); + d_boolMap.insert(cur, + (*d_rmMap.find(cur[0])).second + == (*d_rmMap.find(cur[1])).second); } + // else do nothing } break; case kind::FLOATINGPOINT_LEQ: - case kind::FLOATINGPOINT_LT: - { - TypeNode childType(current[0].getType()); - - 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 == d_fpMap.end()) - { - workStack.push_back(current[0]); - } - if (arg2 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - continue; // i.e. recurse! - } + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + d_boolMap.insert(cur, + symfpu::lessThanOrEqual( + fpt(cur[0].getType()), + (*d_fpMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second)); + break; - switch (current.getKind()) - { - case kind::FLOATINGPOINT_LEQ: - d_boolMap.insert( - current, - symfpu::lessThanOrEqual( - fpt(childType), (*arg1).second, (*arg2).second)); - break; - - case kind::FLOATINGPOINT_LT: - d_boolMap.insert( - current, - symfpu::lessThan( - fpt(childType), (*arg1).second, (*arg2).second)); - break; - - default: - Unreachable() << "Unknown binary floating-point relation"; - break; - } - } - break; + case kind::FLOATINGPOINT_LT: + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + d_boolMap.insert( + cur, + symfpu::lessThan(fpt(cur[0].getType()), + (*d_fpMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second)); + break; + /* ---- Tester -------------------------------------------- */ case kind::FLOATINGPOINT_ISN: + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + d_boolMap.insert( + cur, + symfpu::isNormal(fpt(cur[0].getType()), + (*d_fpMap.find(cur[0])).second)); + break; + case kind::FLOATINGPOINT_ISSN: + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + d_boolMap.insert( + cur, + symfpu::isSubnormal(fpt(cur[0].getType()), + (*d_fpMap.find(cur[0])).second)); + break; + case kind::FLOATINGPOINT_ISZ: - case kind::FLOATINGPOINT_ISINF: - case kind::FLOATINGPOINT_ISNAN: - case kind::FLOATINGPOINT_ISNEG: - case kind::FLOATINGPOINT_ISPOS: - { - TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(d_fpMap.find(current[0])); + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + d_boolMap.insert( + cur, + symfpu::isZero(fpt(cur[0].getType()), + (*d_fpMap.find(cur[0])).second)); + break; - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current); - workStack.push_back(current[0]); - continue; // i.e. recurse! - } + case kind::FLOATINGPOINT_ISINF: + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + d_boolMap.insert( + cur, + symfpu::isInfinite(fpt(cur[0].getType()), + (*d_fpMap.find(cur[0])).second)); + break; - switch (current.getKind()) - { - case kind::FLOATINGPOINT_ISN: - d_boolMap.insert( - current, - symfpu::isNormal(fpt(childType), (*arg1).second)); - break; - - case kind::FLOATINGPOINT_ISSN: - d_boolMap.insert(current, - symfpu::isSubnormal(fpt(childType), - (*arg1).second)); - break; - - case kind::FLOATINGPOINT_ISZ: - d_boolMap.insert( - current, - symfpu::isZero(fpt(childType), (*arg1).second)); - break; - - case kind::FLOATINGPOINT_ISINF: - d_boolMap.insert( - current, - symfpu::isInfinite(fpt(childType), (*arg1).second)); - break; - - case kind::FLOATINGPOINT_ISNAN: - d_boolMap.insert( - current, - symfpu::isNaN(fpt(childType), (*arg1).second)); - break; - - case kind::FLOATINGPOINT_ISPOS: - d_boolMap.insert( - current, - symfpu::isPositive(fpt(childType), (*arg1).second)); - break; - - case kind::FLOATINGPOINT_ISNEG: - d_boolMap.insert( - current, - symfpu::isNegative(fpt(childType), (*arg1).second)); - break; - - default: - Unreachable() << "Unknown unary floating-point relation"; - break; - } - } - break; + case kind::FLOATINGPOINT_ISNAN: + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + d_boolMap.insert( + cur, + symfpu::isNaN(fpt(cur[0].getType()), + (*d_fpMap.find(cur[0])).second)); + break; - case kind::FLOATINGPOINT_EQ: - case kind::FLOATINGPOINT_GEQ: - case kind::FLOATINGPOINT_GT: - Unreachable() << "Kind should have been removed by rewriter."; + case kind::FLOATINGPOINT_ISNEG: + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + d_boolMap.insert( + cur, + symfpu::isNegative(fpt(cur[0].getType()), + (*d_fpMap.find(cur[0])).second)); break; - // Components will be registered as they are owned by - // the floating-point theory. No action is required. - case kind::FLOATINGPOINT_COMPONENT_NAN: - case kind::FLOATINGPOINT_COMPONENT_INF: - case kind::FLOATINGPOINT_COMPONENT_ZERO: - case kind::FLOATINGPOINT_COMPONENT_SIGN: - /* Fall through... */ - - default: - CVC5_FPCONV_PASSTHROUGH; - return result; + case kind::FLOATINGPOINT_ISPOS: + Assert(d_fpMap.find(cur[0]) != d_fpMap.end()); + d_boolMap.insert( + cur, + symfpu::isPositive(fpt(cur[0].getType()), + (*d_fpMap.find(cur[0])).second)); break; - } - i = d_boolMap.find(current); + default:; // do nothing + } } - - result = (*i).second; - } - else if (t.isBitVector()) - { - switch (current.getKind()) + else if (t.isBitVector()) { - /******** Conversions ********/ - case kind::FLOATINGPOINT_TO_UBV_TOTAL: + /* ---- Conversions --------------------------------------- */ + if (kind == kind::FLOATINGPOINT_TO_UBV_TOTAL) { - TypeNode childType(current[1].getType()); - ubvMap::const_iterator i(d_ubvMap.find(current)); - - if (i == d_ubvMap.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 == d_rmMap.end()) - { - workStack.push_back(current[0]); - } - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - continue; // i.e. recurse! - } - - FloatingPointToUBVTotal info = - current.getOperator().getConst(); - - d_ubvMap.insert(current, - symfpu::convertFloatToUBV(fpt(childType), - (*mode).second, - (*arg1).second, - info.d_bv_size, - ubv(current[2]))); - i = d_ubvMap.find(current); - } - - result = (*i).second; + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + FloatingPointToUBVTotal info = + cur.getOperator().getConst(); + d_ubvMap.insert( + cur, + symfpu::convertFloatToUBV(fpt(cur[1].getType()), + (*d_rmMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second, + info.d_bv_size, + ubv(cur[2]))); } - break; - - case kind::FLOATINGPOINT_TO_SBV_TOTAL: + else if (kind == kind::FLOATINGPOINT_TO_SBV_TOTAL) { - TypeNode childType(current[1].getType()); - sbvMap::const_iterator i(d_sbvMap.find(current)); - - if (i == d_sbvMap.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 == d_rmMap.end()) - { - workStack.push_back(current[0]); - } - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current[1]); - } - continue; // i.e. recurse! - } - - FloatingPointToSBVTotal info = - current.getOperator().getConst(); - - d_sbvMap.insert(current, - symfpu::convertFloatToSBV(fpt(childType), - (*mode).second, - (*arg1).second, - info.d_bv_size, - sbv(current[2]))); - - i = d_sbvMap.find(current); - } - - result = (*i).second; + Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); + Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); + FloatingPointToSBVTotal info = + cur.getOperator().getConst(); + + d_sbvMap.insert( + cur, + symfpu::convertFloatToSBV(fpt(cur[1].getType()), + (*d_rmMap.find(cur[0])).second, + (*d_fpMap.find(cur[1])).second, + info.d_bv_size, + sbv(cur[2]))); } - break; - - case kind::FLOATINGPOINT_TO_UBV: - Unreachable() - << "Partially defined fp.to_ubv should have been removed by " - "expandDefinition"; - break; - - case kind::FLOATINGPOINT_TO_SBV: - Unreachable() - << "Partially defined fp.to_sbv should have been removed by " - "expandDefinition"; - break; - - // Again, no action is needed - case kind::FLOATINGPOINT_COMPONENT_EXPONENT: - case kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND: - case kind::ROUNDINGMODE_BITBLAST: - /* Fall through ... */ - - default: CVC5_FPCONV_PASSTHROUGH; break; - } - } - else if (t.isReal()) - { - switch (current.getKind()) - { - /******** Conversions ********/ - case kind::FLOATINGPOINT_TO_REAL_TOTAL: - { - // We need to recurse so that any variables that are only - // used under this will have components created - // (via auxiliary constraints) - - TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(d_fpMap.find(current[0])); - - if (arg1 == d_fpMap.end()) - { - workStack.push_back(current); - workStack.push_back(current[0]); - continue; // i.e. recurse! - } - - // However we don't need to do anything explicitly with - // this as it will be treated as an uninterpreted function - // by the real theory and we don't need to bit-blast the - // float expression unless we need to say something about - // its value. - } - - break; - - case kind::FLOATINGPOINT_TO_REAL: - Unreachable() - << "Partially defined fp.to_real should have been removed by " - "expandDefinition"; - break; - - default: CVC5_FPCONV_PASSTHROUGH; break; + // else do nothing } } else { - CVC5_FPCONV_PASSTHROUGH; + Assert(visited.at(cur) == 1); + continue; } } - return result; + if (d_boolMap.find(node) != d_boolMap.end()) + { + Assert(node.getType().isBoolean()); + return (*d_boolMap.find(node)).second; + } + if (d_sbvMap.find(node) != d_sbvMap.end()) + { + Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL); + return (*d_sbvMap.find(node)).second; + } + if (d_ubvMap.find(node) != d_ubvMap.end()) + { + Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL); + return (*d_ubvMap.find(node)).second; + } + return node; } -#undef CVC5_FPCONV_PASSTHROUGH - Node FpConverter::getValue(Valuation &val, TNode var) { Assert(Theory::isLeafOf(var, THEORY_FP));