diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 19:11:31 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-26 19:11:31 -0600 |
commit | d41d2a817f884e0f6c8d5cb3b87b4298bc1b56f5 (patch) | |
tree | 5cfe4336c5aa40cac613238a2625b1fb4aa55d31 /src/theory/fp | |
parent | 4b7de240edeee362a0b9ca440c22a8b0744cf34b (diff) |
Initial work towards -Wshadow (#3817)
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 2 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.cpp | 111 | ||||
-rw-r--r-- | src/theory/fp/theory_fp_rewriter.h | 2 |
3 files changed, 65 insertions, 50 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 788545b3c..2632a6f38 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -962,7 +962,7 @@ void TheoryFp::check(Effort level) { while (!done() && !d_conflict) { // Get all the assertions Assertion assertion = get(); - TNode fact = assertion.assertion; + TNode fact = assertion.d_assertion; Debug("fp") << "TheoryFp::check(): processing " << fact << std::endl; diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 8854b400d..338c1c871 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -46,9 +46,12 @@ namespace rewrite { RewriteResponse then (TNode node, bool isPreRewrite) { RewriteResponse result(first(node, isPreRewrite)); - if (result.status == REWRITE_DONE) { - return second(result.node, isPreRewrite); - } else { + if (result.d_status == REWRITE_DONE) + { + return second(result.d_node, isPreRewrite); + } + else + { return result; } } @@ -1268,9 +1271,11 @@ TheoryFpRewriter::TheoryFpRewriter() RewriteResponse TheoryFpRewriter::preRewrite(TNode node) { Trace("fp-rewrite") << "TheoryFpRewriter::preRewrite(): " << node << std::endl; RewriteResponse res = d_preRewriteTable[node.getKind()](node, true); - if (res.node != node) { + if (res.d_node != node) + { Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): before " << node << std::endl; - Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after " << res.node << std::endl; + Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after " + << res.d_node << std::endl; } return res; } @@ -1301,46 +1306,52 @@ TheoryFpRewriter::TheoryFpRewriter() RewriteResponse TheoryFpRewriter::postRewrite(TNode node) { Trace("fp-rewrite") << "TheoryFpRewriter::postRewrite(): " << node << std::endl; RewriteResponse res = d_postRewriteTable[node.getKind()](node, false); - if (res.node != node) { + if (res.d_node != node) + { Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before " << node << std::endl; - Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after " << res.node << std::endl; + Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after " + << res.d_node << std::endl; } - if (res.status == REWRITE_DONE) { + if (res.d_status == REWRITE_DONE) + { bool allChildrenConst = true; bool apartFromRoundingMode = false; bool apartFromPartiallyDefinedArgument = false; - for (Node::const_iterator i = res.node.begin(); - i != res.node.end(); - ++i) { - - if ((*i).getMetaKind() != kind::metakind::CONSTANT) { + for (Node::const_iterator i = res.d_node.begin(); i != res.d_node.end(); + ++i) + { + if ((*i).getMetaKind() != kind::metakind::CONSTANT) { if ((*i).getType().isRoundingMode() && !apartFromRoundingMode) { apartFromRoundingMode = true; - } else if ((res.node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL || - res.node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL || - res.node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL || - res.node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL || - res.node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL) && - ((*i).getType().isBitVector() || - (*i).getType().isReal()) && - !apartFromPartiallyDefinedArgument) { - apartFromPartiallyDefinedArgument = true; - } else { - allChildrenConst = false; + } + else if ((res.d_node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL + || res.d_node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL + || res.d_node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL + || res.d_node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL + || res.d_node.getKind() + == kind::FLOATINGPOINT_TO_REAL_TOTAL) + && ((*i).getType().isBitVector() || (*i).getType().isReal()) + && !apartFromPartiallyDefinedArgument) + { + apartFromPartiallyDefinedArgument = true; + } + else + { + allChildrenConst = false; break; - } - } + } + } } if (allChildrenConst) { RewriteStatus rs = REWRITE_DONE; // This is a bit messy because - Node rn = res.node; // RewriteResponse is too functional.. + Node rn = res.d_node; // RewriteResponse is too functional.. - if (apartFromRoundingMode) { - if (!(res.node.getKind() == kind::EQUAL) + if (apartFromRoundingMode) { + if (!(res.d_node.getKind() == kind::EQUAL) && // Avoid infinite recursion... - !(res.node.getKind() == kind::ROUNDINGMODE_BITBLAST)) + !(res.d_node.getKind() == kind::ROUNDINGMODE_BITBLAST)) { // Don't eliminate the bit-blast // We are close to being able to constant fold this // and in many cases the rounding mode really doesn't matter. @@ -1354,16 +1365,15 @@ TheoryFpRewriter::TheoryFpRewriter() Node RTN(nm->mkConst(roundTowardNegative)); Node RTP(nm->mkConst(roundTowardZero)); - TNode RM(res.node[0]); - - Node wRNE(res.node.substitute(RM, TNode(RNE))); - Node wRNA(res.node.substitute(RM, TNode(RNA))); - Node wRTZ(res.node.substitute(RM, TNode(RTZ))); - Node wRTN(res.node.substitute(RM, TNode(RTN))); - Node wRTP(res.node.substitute(RM, TNode(RTP))); + TNode RM(res.d_node[0]); + Node wRNE(res.d_node.substitute(RM, TNode(RNE))); + Node wRNA(res.d_node.substitute(RM, TNode(RNA))); + Node wRTZ(res.d_node.substitute(RM, TNode(RTZ))); + Node wRTN(res.d_node.substitute(RM, TNode(RTN))); + Node wRTP(res.d_node.substitute(RM, TNode(RTP))); - rs = REWRITE_AGAIN_FULL; + rs = REWRITE_AGAIN_FULL; rn = nm->mkNode(kind::ITE, nm->mkNode(kind::EQUAL, RM, RNE), wRNE, @@ -1380,19 +1390,24 @@ TheoryFpRewriter::TheoryFpRewriter() } } else { RewriteResponse tmp = - d_constantFoldTable[res.node.getKind()](res.node, false); - rs = tmp.status; - rn = tmp.node; - } + d_constantFoldTable[res.d_node.getKind()](res.d_node, false); + rs = tmp.d_status; + rn = tmp.d_node; + } RewriteResponse constRes(rs,rn); - if (constRes.node != res.node) { - Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before constant fold " << res.node << std::endl; - Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after constant fold " << constRes.node << std::endl; - } - - return constRes; + if (constRes.d_node != res.d_node) + { + Debug("fp-rewrite") + << "TheoryFpRewriter::postRewrite(): before constant fold " + << res.d_node << std::endl; + Debug("fp-rewrite") + << "TheoryFpRewriter::postRewrite(): after constant fold " + << constRes.d_node << std::endl; + } + + return constRes; } } diff --git a/src/theory/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h index 790e9d83d..732eeab0a 100644 --- a/src/theory/fp/theory_fp_rewriter.h +++ b/src/theory/fp/theory_fp_rewriter.h @@ -42,7 +42,7 @@ class TheoryFpRewriter : public TheoryRewriter Node rewriteEquality(TNode equality) { // often this will suffice - return postRewrite(equality).node; + return postRewrite(equality).d_node; } protected: |