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>

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();
   }