diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-03-05 11:42:54 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-05 11:42:54 -0800 |
commit | 04039407e6308070c148de0d5e93640ec1b0a341 (patch) | |
tree | b66f63d49df0713b1ca2a440bec89f1d60af32a4 /src/theory/rewriter.cpp | |
parent | 18fe192c29a9a2c37d1925730af01e906b9888c5 (diff) |
Enable -Wshadow and fix warnings. (#3909)
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 113 |
1 files changed, 58 insertions, 55 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index e5d6748aa..765c2b4c8 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -52,33 +52,33 @@ struct RewriteStackElement { * Construct a fresh stack element. */ RewriteStackElement(TNode node, TheoryId theoryId) - : node(node), - original(node), - theoryId(theoryId), - originalTheoryId(theoryId), - nextChild(0) + : d_node(node), + d_original(node), + d_theoryId(theoryId), + d_originalTheoryId(theoryId), + d_nextChild(0) { } - TheoryId getTheoryId() { return static_cast<TheoryId>(theoryId); } + TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); } TheoryId getOriginalTheoryId() { - return static_cast<TheoryId>(originalTheoryId); + return static_cast<TheoryId>(d_originalTheoryId); } /** The node we're currently rewriting */ - Node node; + Node d_node; /** Original node */ - Node original; + Node d_original; /** Id of the theory that's currently rewriting this node */ - unsigned theoryId : 8; + unsigned d_theoryId : 8; /** Id of the original theory that started the rewrite */ - unsigned originalTheoryId : 8; + unsigned d_originalTheoryId : 8; /** Index of the child this node is done rewriting */ - unsigned nextChild : 32; + unsigned d_nextChild : 32; /** Builder for this node */ - NodeBuilder<> builder; + NodeBuilder<> d_builder; }; Node Rewriter::rewrite(TNode node) { @@ -140,71 +140,73 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Trace("rewriter") << "Rewriter::rewriting: " << rewriteStackTop.getTheoryId() << "," - << rewriteStackTop.node << std::endl; + << rewriteStackTop.d_node << std::endl; // Before rewriting children we need to do a pre-rewrite of the node - if (rewriteStackTop.nextChild == 0) { - + if (rewriteStackTop.d_nextChild == 0) + { // Check if the pre-rewrite has already been done (it's in the cache) - Node cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), - rewriteStackTop.node); + cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), + rewriteStackTop.d_node); if (cached.isNull()) { // Rewrite until fix-point is reached for(;;) { // Perform the pre-rewrite RewriteResponse response = d_theoryRewriters[rewriteStackTop.getTheoryId()]->preRewrite( - rewriteStackTop.node); + rewriteStackTop.d_node); // Put the rewritten node to the top of the stack - rewriteStackTop.node = response.d_node; - TheoryId newTheory = theoryOf(rewriteStackTop.node); + rewriteStackTop.d_node = response.d_node; + TheoryId newTheory = theoryOf(rewriteStackTop.d_node); // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite if (newTheory == rewriteStackTop.getTheoryId() && response.d_status == REWRITE_DONE) { break; } - rewriteStackTop.theoryId = newTheory; + rewriteStackTop.d_theoryId = newTheory; } // Cache the rewrite setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(), - rewriteStackTop.original, - rewriteStackTop.node); + rewriteStackTop.d_original, + rewriteStackTop.d_node); } // Otherwise we're have already been pre-rewritten (in pre-rewrite cache) else { // Continue with the cached version - rewriteStackTop.node = cached; - rewriteStackTop.theoryId = theoryOf(cached); + rewriteStackTop.d_node = cached; + rewriteStackTop.d_theoryId = theoryOf(cached); } } - rewriteStackTop.original =rewriteStackTop.node; + rewriteStackTop.d_original = rewriteStackTop.d_node; // Now it's time to rewrite the children, check if this has already been done - Node cached = getPostRewriteCache(rewriteStackTop.getTheoryId(), - rewriteStackTop.node); + cached = getPostRewriteCache(rewriteStackTop.getTheoryId(), + rewriteStackTop.d_node); // If not, go through the children if(cached.isNull()) { // The child we need to rewrite - unsigned child = rewriteStackTop.nextChild++; + unsigned child = rewriteStackTop.d_nextChild++; // To build the rewritten expression we set up the builder if(child == 0) { - if (rewriteStackTop.node.getNumChildren() > 0) { + if (rewriteStackTop.d_node.getNumChildren() > 0) + { // The children will add themselves to the builder once they're done - rewriteStackTop.builder << rewriteStackTop.node.getKind(); - kind::MetaKind metaKind = rewriteStackTop.node.getMetaKind(); + rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind(); + kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind(); if (metaKind == kind::metakind::PARAMETERIZED) { - rewriteStackTop.builder << rewriteStackTop.node.getOperator(); + rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator(); } } } // Process the next child - if(child < rewriteStackTop.node.getNumChildren()) { + if (child < rewriteStackTop.d_node.getNumChildren()) + { // The child node - Node childNode = rewriteStackTop.node[child]; + Node childNode = rewriteStackTop.d_node[child]; // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now) rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode))); // Go on with the rewriting @@ -212,10 +214,11 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } // Incorporate the children if necessary - if (rewriteStackTop.node.getNumChildren() > 0) { - Node rewritten = rewriteStackTop.builder; - rewriteStackTop.node = rewritten; - rewriteStackTop.theoryId = theoryOf(rewriteStackTop.node); + if (rewriteStackTop.d_node.getNumChildren() > 0) + { + Node rewritten = rewriteStackTop.d_builder; + rewriteStackTop.d_node = rewritten; + rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node); } // Done with all pre-rewriting, so let's do the post rewrite @@ -223,14 +226,14 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Do the post-rewrite RewriteResponse response = d_theoryRewriters[rewriteStackTop.getTheoryId()]->postRewrite( - rewriteStackTop.node); + rewriteStackTop.d_node); // We continue with the response we got TheoryId newTheoryId = theoryOf(response.d_node); if (newTheoryId != rewriteStackTop.getTheoryId() || response.d_status == REWRITE_AGAIN_FULL) { // In the post rewrite if we've changed theories, we must do a full rewrite - Assert(response.d_node != rewriteStackTop.node); + Assert(response.d_node != rewriteStackTop.d_node); //TODO: this is not thread-safe - should make this assertion dependent on sequential build #ifdef CVC4_ASSERTIONS Assert(d_rewriteStack->find(response.d_node) @@ -238,7 +241,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { d_rewriteStack->insert(response.d_node); #endif Node rewritten = rewriteTo(newTheoryId, response.d_node); - rewriteStackTop.node = rewritten; + rewriteStackTop.d_node = rewritten; #ifdef CVC4_ASSERTIONS d_rewriteStack->erase(response.d_node); #endif @@ -251,36 +254,36 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { d_theoryRewriters[newTheoryId]->postRewrite(response.d_node); Assert(r2.d_node == response.d_node); #endif - rewriteStackTop.node = response.d_node; + rewriteStackTop.d_node = response.d_node; break; } // Check for trivial rewrite loops of size 1 or 2 - Assert(response.d_node != rewriteStackTop.node); + Assert(response.d_node != rewriteStackTop.d_node); Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()] ->postRewrite(response.d_node) .d_node - != rewriteStackTop.node); - rewriteStackTop.node = response.d_node; + != rewriteStackTop.d_node); + rewriteStackTop.d_node = response.d_node; } // We're done with the post rewrite, so we add to the cache setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(), - rewriteStackTop.original, - rewriteStackTop.node); + rewriteStackTop.d_original, + rewriteStackTop.d_node); } else { // We were already in cache, so just remember it - rewriteStackTop.node = cached; - rewriteStackTop.theoryId = theoryOf(cached); + rewriteStackTop.d_node = cached; + rewriteStackTop.d_theoryId = theoryOf(cached); } // If this is the last node, just return if (rewriteStack.size() == 1) { - Assert(!isEquality || rewriteStackTop.node.getKind() == kind::EQUAL - || rewriteStackTop.node.isConst()); - return rewriteStackTop.node; + Assert(!isEquality || rewriteStackTop.d_node.getKind() == kind::EQUAL + || rewriteStackTop.d_node.isConst()); + return rewriteStackTop.d_node; } // We're done with this node, append it to the parent - rewriteStack[rewriteStack.size() - 2].builder << rewriteStackTop.node; + rewriteStack[rewriteStack.size() - 2].d_builder << rewriteStackTop.d_node; rewriteStack.pop_back(); } |