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>

5 files changed, 75 insertions, 73 deletions

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index d6259294a..debb4d2ac 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -195,50 +195,50 @@ PreprocessingPassResult MipLibTrick::applyInternal(
   Node trueNode = nm->mkConst(true);
 
   unordered_map<TNode, Node, TNodeHashFunction> intVars;
-  for (TNode v : d_boolVars)
+  for (TNode v0 : d_boolVars)
   {
-    if (propagator->isAssigned(v))
+    if (propagator->isAssigned(v0))
     {
-      Debug("miplib") << "ineligible: " << v << " because assigned "
-                      << propagator->getAssignment(v) << endl;
+      Debug("miplib") << "ineligible: " << v0 << " because assigned "
+                      << propagator->getAssignment(v0) << endl;
       continue;
     }
 
     vector<TNode> assertions;
-    booleans::CircuitPropagator::BackEdgesMap::const_iterator j =
-        backEdges.find(v);
+    booleans::CircuitPropagator::BackEdgesMap::const_iterator j0 =
+        backEdges.find(v0);
     // if not in back edges map, the bool var is unconstrained, showing up in no
     // assertions. if maps to an empty vector, that means the bool var was
     // asserted itself.
-    if (j != backEdges.end())
+    if (j0 != backEdges.end())
     {
-      if (!(*j).second.empty())
+      if (!(*j0).second.empty())
       {
-        traceBackToAssertions(propagator, (*j).second, assertions);
+        traceBackToAssertions(propagator, (*j0).second, assertions);
       }
       else
       {
-        assertions.push_back(v);
+        assertions.push_back(v0);
       }
     }
-    Debug("miplib") << "for " << v << endl;
+    Debug("miplib") << "for " << v0 << endl;
     bool eligible = true;
     map<pair<Node, Node>, uint64_t> marks;
     map<pair<Node, Node>, vector<Rational> > coef;
     map<pair<Node, Node>, vector<Rational> > checks;
     map<pair<Node, Node>, vector<TNode> > asserts;
-    for (vector<TNode>::const_iterator j = assertions.begin();
-         j != assertions.end();
-         ++j)
+    for (vector<TNode>::const_iterator j1 = assertions.begin();
+         j1 != assertions.end();
+         ++j1)
     {
-      Debug("miplib") << "  found: " << *j << endl;
-      if ((*j).getKind() != kind::IMPLIES)
+      Debug("miplib") << "  found: " << *j1 << endl;
+      if ((*j1).getKind() != kind::IMPLIES)
       {
         eligible = false;
         Debug("miplib") << "  -- INELIGIBLE -- (not =>)" << endl;
         break;
       }
-      Node conj = BooleanSimplification::simplify((*j)[0]);
+      Node conj = BooleanSimplification::simplify((*j1)[0]);
       if (conj.getKind() == kind::AND && conj.getNumChildren() > 6)
       {
         eligible = false;
@@ -252,11 +252,11 @@ PreprocessingPassResult MipLibTrick::applyInternal(
         Debug("miplib") << "  -- INELIGIBLE -- (not /\\ or literal)" << endl;
         break;
       }
-      if ((*j)[1].getKind() != kind::EQUAL
-          || !(((*j)[1][0].isVar()
-                && (*j)[1][1].getKind() == kind::CONST_RATIONAL)
-               || ((*j)[1][0].getKind() == kind::CONST_RATIONAL
-                   && (*j)[1][1].isVar())))
+      if ((*j1)[1].getKind() != kind::EQUAL
+          || !(((*j1)[1][0].isVar()
+                && (*j1)[1][1].getKind() == kind::CONST_RATIONAL)
+               || ((*j1)[1][0].getKind() == kind::CONST_RATIONAL
+                   && (*j1)[1][1].isVar())))
       {
         eligible = false;
         Debug("miplib") << "  -- INELIGIBLE -- (=> (and X X) X)" << endl;
@@ -273,13 +273,13 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           {
             posv.push_back(*ii);
             neg[*ii] = false;
-            found_x = found_x || v == *ii;
+            found_x = found_x || v0 == *ii;
           }
           else if ((*ii).getKind() == kind::NOT && (*ii)[0].isVar())
           {
             posv.push_back((*ii)[0]);
             neg[(*ii)[0]] = true;
-            found_x = found_x || v == (*ii)[0];
+            found_x = found_x || v0 == (*ii)[0];
           }
           else
           {
@@ -303,20 +303,20 @@ PreprocessingPassResult MipLibTrick::applyInternal(
         if (!found_x)
         {
           eligible = false;
-          Debug("miplib") << "  --INELIGIBLE -- (couldn't find " << v
+          Debug("miplib") << "  --INELIGIBLE -- (couldn't find " << v0
                           << " in conjunction)" << endl;
           break;
         }
         sort(posv.begin(), posv.end());
         const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv);
-        const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL)
-                              ? (*j)[1][1]
-                              : (*j)[1][0];
+        const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
+                              ? (*j1)[1][1]
+                              : (*j1)[1][0];
         const pair<Node, Node> pos_var(pos, var);
         const Rational& constant =
-            ((*j)[1][0].getKind() == kind::CONST_RATIONAL)
-                ? (*j)[1][0].getConst<Rational>()
-                : (*j)[1][1].getConst<Rational>();
+            ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
+                ? (*j1)[1][0].getConst<Rational>()
+                : (*j1)[1][1].getConst<Rational>();
         uint64_t mark = 0;
         unsigned countneg = 0, thepos = 0;
         for (unsigned ii = 0; ii < pos.getNumChildren(); ++ii)
@@ -368,12 +368,12 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           }
           checks[pos_var][mark] = constant;
         }
-        asserts[pos_var].push_back(*j);
+        asserts[pos_var].push_back(*j1);
       }
       else
       {
         TNode x = conj;
-        if (x != v && x != (v).notNode())
+        if (x != v0 && x != (v0).notNode())
         {
           eligible = false;
           Debug("miplib")
@@ -383,14 +383,14 @@ PreprocessingPassResult MipLibTrick::applyInternal(
         const bool xneg = (x.getKind() == kind::NOT);
         x = xneg ? x[0] : x;
         Debug("miplib") << "  x:" << x << "  " << xneg << endl;
-        const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL)
-                              ? (*j)[1][1]
-                              : (*j)[1][0];
+        const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
+                              ? (*j1)[1][1]
+                              : (*j1)[1][0];
         const pair<Node, Node> x_var(x, var);
         const Rational& constant =
-            ((*j)[1][0].getKind() == kind::CONST_RATIONAL)
-                ? (*j)[1][0].getConst<Rational>()
-                : (*j)[1][1].getConst<Rational>();
+            ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
+                ? (*j1)[1][0].getConst<Rational>()
+                : (*j1)[1][1].getConst<Rational>();
         unsigned mark = (xneg ? 0 : 1);
         if ((marks[x_var] & (1u << mark)) != 0)
         {
@@ -414,7 +414,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           coef[x_var].resize(6);
           coef[x_var][0] = constant;
         }
-        asserts[x_var].push_back(*j);
+        asserts[x_var].push_back(*j1);
       }
     }
     if (eligible)
@@ -454,14 +454,15 @@ PreprocessingPassResult MipLibTrick::applyInternal(
               {
                 Rational sum = 0;
                 Debug("miplib") << k << " => " << checks[pos_var][k] << endl;
-                for (size_t v = 1, kk = k; kk != 0; ++v, kk >>= 1)
+                for (size_t v1 = 1, kk = k; kk != 0; ++v1, kk >>= 1)
                 {
                   if ((kk & 0x1) == 1)
                   {
                     Assert(pos.getKind() == kind::AND);
-                    Debug("miplib") << "var " << v << " : " << pos[v - 1]
-                                    << " coef:" << coef[pos_var][v - 1] << endl;
-                    sum += coef[pos_var][v - 1];
+                    Debug("miplib")
+                        << "var " << v1 << " : " << pos[v1 - 1]
+                        << " coef:" << coef[pos_var][v1 - 1] << endl;
+                    sum += coef[pos_var][v1 - 1];
                   }
                 }
                 Debug("miplib") << "checkSum is " << sum << " input says "
@@ -490,7 +491,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
             continue;
           }
 
-          Debug("miplib") << "  -- ELIGIBLE " << v << " , " << pos << " --"
+          Debug("miplib") << "  -- ELIGIBLE " << v0 << " , " << pos << " --"
                           << endl;
           vector<Node> newVars;
           expr::NodeSelfIterator ii, iiend;
@@ -549,10 +550,10 @@ PreprocessingPassResult MipLibTrick::applyInternal(
           if (pos.getKind() == kind::AND)
           {
             NodeBuilder<> sumb(kind::PLUS);
-            for (size_t ii = 0; ii < pos.getNumChildren(); ++ii)
+            for (size_t jj = 0; jj < pos.getNumChildren(); ++jj)
             {
               sumb << nm->mkNode(
-                  kind::MULT, nm->mkConst(coef[pos_var][ii]), newVars[ii]);
+                  kind::MULT, nm->mkConst(coef[pos_var][jj]), newVars[jj]);
             }
             sum = sumb;
           }
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 24484359a..41bb226a3 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -328,10 +328,10 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
     if (itffv != ff_var_to_ff.end())
     {
       Node ff = itffv->second;
-      Node body = Node::fromExpr(it->second);
-      Trace("sygus-infer") << "Define " << ff << " as " << body << std::endl;
+      Node body2 = Node::fromExpr(it->second);
+      Trace("sygus-infer") << "Define " << ff << " as " << body2 << std::endl;
       funs.push_back(ff);
-      sols.push_back(body);
+      sols.push_back(body2);
     }
   }
   return true;
diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp
index 8d0d04149..d0327263b 100644
--- a/src/preprocessing/passes/symmetry_detect.cpp
+++ b/src/preprocessing/passes/symmetry_detect.cpp
@@ -374,24 +374,24 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index,
           Assert(d_base_indices.find(i) == d_base_indices.end());
           d_base_indices.insert(i);
           Trace("sym-dt-debug") << i << " ";
-          const Partition& p = partitions[i];
-          children.push_back(p.d_term);
-          schildren.push_back(p.d_sterm);
+          const Partition& p2 = partitions[i];
+          children.push_back(p2.d_term);
+          schildren.push_back(p2.d_sterm);
           Assert(active_indices.find(i) != active_indices.end());
           active_indices.erase(i);
         }
         Trace("sym-dt-debug") << "}" << std::endl;
         Trace("sym-dt-debug") << "Reconstruct master partition "
                               << d_master_base_index << std::endl;
-        Partition& p = partitions[d_master_base_index];
+        Partition& p3 = partitions[d_master_base_index];
         // reconstruct the master partition
-        p.d_term = mkAssociativeNode(d_kind, children);
-        p.d_sterm = mkAssociativeNode(d_kind, schildren);
-        Assert(p.d_subvar_to_vars.size() == 1);
-        Node sb_v = p.d_subvar_to_vars.begin()->first;
+        p3.d_term = mkAssociativeNode(d_kind, children);
+        p3.d_sterm = mkAssociativeNode(d_kind, schildren);
+        Assert(p3.d_subvar_to_vars.size() == 1);
+        Node sb_v = p3.d_subvar_to_vars.begin()->first;
         Trace("sym-dt-debug") << "- set var to svar: " << merge_var << " -> "
                               << sb_v << std::endl;
-        p.addVariable(sb_v, merge_var);
+        p3.addVariable(sb_v, merge_var);
         return true;
       }
       if (mergeNewVar(curr_index + 1,
@@ -1139,7 +1139,7 @@ void SymmetryDetect::processPartitions(
           k, partitions, svee.second, active_indices, fixedSVar, fixedVar);
 
       // remove the list of fixed variables
-      for (unsigned k = 0; k < nfvars; k++)
+      for (unsigned i = 0; i < nfvars; i++)
       {
         fixedVar.pop_back();
         fixedSVar.pop_back();
@@ -1218,7 +1218,7 @@ void SymmetryDetect::processPartitions(
       // if still active
       if (active_indices.find(index) != active_indices.end())
       {
-        for (unsigned i = 0, size = fixedSVar.size(); i < size; i++)
+        for (unsigned i = 0, size2 = fixedSVar.size(); i < size2; i++)
         {
           // add variable
           partitions[index].addVariable(fixedSVar[i], fixedVar[i]);
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index f3ca65b79..7b8e61359 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -310,11 +310,11 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
         std::map<TypeNode, bool> hasArgType;
         for (unsigned j = 0, size = argListTmp.size(); j < size; j++)
         {
-          TypeNode t = argListTmp[j];
-          if (hasArgType.find(t) == hasArgType.end())
+          TypeNode tn = argListTmp[j];
+          if (hasArgType.find(tn) == hasArgType.end())
           {
-            hasArgType[t] = true;
-            argList.push_back(t);
+            hasArgType[tn] = true;
+            argList.push_back(tn);
           }
         }
       }
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 9c3db0b0d..c609eebd7 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -1252,7 +1252,6 @@ Node ITESimplifier::attemptEagerRemoval(TNode atom)
       Assert(leaves != NULL);
       if (!std::binary_search(leaves->begin(), leaves->end(), constant))
       {
-        std::pair<Node, Node> pair = make_pair(cite, constant);
         d_constantIteEqualsConstantCache[pair] = d_false;
         return d_false;
       }
@@ -1534,9 +1533,11 @@ Node ITESimplifier::simpITEAtom(TNode atom)
 
 struct preprocess_stack_element
 {
-  TNode node;
-  bool children_added;
-  preprocess_stack_element(TNode node) : node(node), children_added(false) {}
+  TNode d_node;
+  bool d_children_added;
+  preprocess_stack_element(TNode node) : d_node(node), d_children_added(false)
+  {
+  }
 }; /* struct preprocess_stack_element */
 
 Node ITESimplifier::simpITE(TNode assertion)
@@ -1555,7 +1556,7 @@ Node ITESimplifier::simpITE(TNode assertion)
     // cout << "call  " << call << " : " << iteration << endl;
     // The current node we are processing
     preprocess_stack_element& stackHead = toVisit.back();
-    TNode current = stackHead.node;
+    TNode current = stackHead.d_node;
 
     // If node has no ITE's or already in the cache we're done, pop from the
     // stack
@@ -1577,7 +1578,7 @@ Node ITESimplifier::simpITE(TNode assertion)
     }
 
     // Not yet substituted, so process
-    if (stackHead.children_added)
+    if (stackHead.d_children_added)
     {
       // Children have been processed, so substitute
       NodeBuilder<> builder(current.getKind());
@@ -1617,7 +1618,7 @@ Node ITESimplifier::simpITE(TNode assertion)
       // Mark that we have added the children if any
       if (current.getNumChildren() > 0)
       {
-        stackHead.children_added = true;
+        stackHead.d_children_added = true;
         // We need to add the children
         for (TNode::iterator child_it = current.begin();
              child_it != current.end();
@@ -1875,7 +1876,7 @@ Node ITECareSimplifier::simplifyWithCare(TNode e)
         continue;
       }
 
-      for (unsigned i = 0; i < v.getNumChildren(); ++i)
+      for (i = 0; i < v.getNumChildren(); ++i)
       {
         updateQueue(queue, v[i], cs);
       }