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>

7 files changed, 72 insertions, 68 deletions

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 343f6e4f8..c23041914 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -155,19 +155,19 @@ void BaseSolver::checkInit()
                   std::vector<Node> exp;
                   // explain empty components
                   bool foundNEmpty = false;
-                  for (const Node& nc : n)
+                  for (const Node& nnc : n)
                   {
-                    if (d_state.areEqual(nc, d_emptyString))
+                    if (d_state.areEqual(nnc, d_emptyString))
                     {
-                      if (nc != d_emptyString)
+                      if (nnc != d_emptyString)
                       {
-                        exp.push_back(nc.eqNode(d_emptyString));
+                        exp.push_back(nnc.eqNode(d_emptyString));
                       }
                     }
                     else
                     {
                       Assert(!foundNEmpty);
-                      ns = nc;
+                      ns = nnc;
                       foundNEmpty = true;
                     }
                   }
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 723520b67..5414c9b98 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -485,10 +485,10 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector<
             if( eqc==d_emptyString ){
               //for empty eqc, ensure all components are empty
               if( nr!=d_emptyString ){
-                std::vector< Node > exp;
-                exp.push_back( n.eqNode( d_emptyString ) );
+                std::vector<Node> exps;
+                exps.push_back(n.eqNode(d_emptyString));
                 d_im.sendInference(
-                    exp, n[i].eqNode(d_emptyString), "I_CYCLE_E");
+                    exps, n[i].eqNode(d_emptyString), "I_CYCLE_E");
                 return Node::null();
               }
             }else{
@@ -1576,9 +1576,9 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
   }
 
   Node split_eq;
-  for (unsigned r = 0; r < 2; r++)
+  for (unsigned i = 0; i < 2; i++)
   {
-    Node t = r == 0 ? veci[loop_index] : t_yz;
+    Node t = i == 0 ? veci[loop_index] : t_yz;
     split_eq = t.eqNode(d_emptyString);
     Node split_eqr = Rewriter::rewrite(split_eq);
     // the equality could rewrite to false
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index b04b88b31..af114e361 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -570,16 +570,16 @@ void ExtfSolver::checkExtfInference(Node n,
           {
             bool do_infer = false;
             conc = conc.negate();
-            bool pol = conc.getKind() != NOT;
-            Node lit = pol ? conc : conc[0];
+            bool pol2 = conc.getKind() != NOT;
+            Node lit = pol2 ? conc : conc[0];
             if (lit.getKind() == EQUAL)
             {
-              do_infer = pol ? !d_state.areEqual(lit[0], lit[1])
-                             : !d_state.areDisequal(lit[0], lit[1]);
+              do_infer = pol2 ? !d_state.areEqual(lit[0], lit[1])
+                              : !d_state.areDisequal(lit[0], lit[1]);
             }
             else
             {
-              do_infer = !d_state.areEqual(lit, pol ? d_true : d_false);
+              do_infer = !d_state.areEqual(lit, pol2 ? d_true : d_false);
             }
             if (do_infer)
             {
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 1942938c3..86995736e 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -303,15 +303,15 @@ Node RegExpElimination::eliminateConcat(Node atom)
       // process the non-greedy find variables
       if (!non_greedy_find_vars.empty())
       {
-        std::vector<Node> children;
+        std::vector<Node> children2;
         for (const Node& v : non_greedy_find_vars)
         {
           Node bound = nm->mkNode(
               AND, nm->mkNode(LEQ, d_zero, v), nm->mkNode(LT, v, lenx));
-          children.push_back(bound);
+          children2.push_back(bound);
         }
-        children.push_back(res);
-        Node body = nm->mkNode(AND, children);
+        children2.push_back(res);
+        Node body = nm->mkNode(AND, children2);
         Node bvl = nm->mkNode(BOUND_VAR_LIST, non_greedy_find_vars);
         res = nm->mkNode(EXISTS, bvl, body);
       }
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 0e8347281..530564a35 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -772,8 +772,8 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
           firstChars(r[i], cset, vset);
           Node n = r[i];
           Node exp;
-          int r = delta( n, exp );
-          if(r != 1) {
+          if (delta(n, exp) != 1)
+          {
             break;
           }
         }
@@ -826,15 +826,15 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
 
   if(Trace.isOn("regexp-fset")) {
     Trace("regexp-fset") << "END FSET(" << mkString(r) << ") = {";
-    for (std::set<unsigned>::const_iterator itr = pcset.begin();
-         itr != pcset.end();
-         ++itr)
+    for (std::set<unsigned>::const_iterator it = pcset.begin();
+         it != pcset.end();
+         ++it)
     {
-      if (itr != pcset.begin())
+      if (it != pcset.begin())
       {
         Trace("regexp-fset") << ",";
       }
-      Trace("regexp-fset") << (*itr);
+      Trace("regexp-fset") << (*it);
       }
     Trace("regexp-fset") << "}" << std::endl;
   }
@@ -1191,7 +1191,6 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes
         } else if(r[0].getKind() == kind::REGEXP_SIGMA) {
           conc = d_true;
         } else {
-          NodeManager* nm = NodeManager::currentNM();
           Node se = s.eqNode(d_emptyString);
           Node sinr = nm->mkNode(kind::STRING_IN_REGEXP, s, r[0]);
           Node sk1 = nm->mkSkolem(
@@ -1495,24 +1494,25 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
         }
         if(Trace.isOn("regexp-int-debug")) {
           Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {";
-          for (std::vector<unsigned>::const_iterator itr = cset.begin();
-               itr != cset.end();
-               ++itr)
+          for (std::vector<unsigned>::const_iterator it = cset.begin();
+               it != cset.end();
+               ++it)
           {
-            if(itr != cset.begin()) {
+            if (it != cset.begin())
+            {
               Trace("regexp-int-debug") << ", ";
             }
-            Trace("regexp-int-debug") << ( *itr );
+            Trace("regexp-int-debug") << (*it);
           }
           Trace("regexp-int-debug") << std::endl;
         }
         std::map< PairNodes, Node > cacheX;
-        for (std::vector<unsigned>::const_iterator itr = cset.begin();
-             itr != cset.end();
-             ++itr)
+        for (std::vector<unsigned>::const_iterator it = cset.begin();
+             it != cset.end();
+             ++it)
         {
           std::vector<unsigned> cvec;
-          cvec.push_back(String::convertCodeToUnsignedInt(*itr));
+          cvec.push_back(String::convertCodeToUnsignedInt(*it));
           String c(cvec);
           Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl;
           Node r1l = derivativeSingle(r1, c);
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 5b41feacb..9d9c66ec2 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -100,15 +100,15 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
   Trace("regexp-process") << "Checking Memberships ... " << std::endl;
   for (const std::pair<const Node, std::vector<Node> >& mr : mems)
   {
-    std::vector<Node> mems = mr.second;
+    std::vector<Node> mems2 = mr.second;
     Trace("regexp-process")
         << "Memberships(" << mr.first << ") = " << mr.second << std::endl;
-    if (!checkEqcInclusion(mems))
+    if (!checkEqcInclusion(mems2))
     {
       // conflict discovered, return
       return;
     }
-    if (!checkEqcIntersect(mems))
+    if (!checkEqcIntersect(mems2))
     {
       // conflict discovered, return
       return;
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 26721229f..f05c9165b 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -195,8 +195,9 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren,
                     std::reverse( mchildren_ss.begin(), mchildren_ss.end() );
                     std::reverse( children_ss.begin(), children_ss.end() );
                   }
-                  Node ret = simpleRegexpConsume( mchildren_ss, children_ss, t );
-                  if( ret.isNull() ){
+                  if (simpleRegexpConsume(mchildren_ss, children_ss, t)
+                          .isNull())
+                  {
                     can_skip = true;
                   }
                 }
@@ -1252,10 +1253,13 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
     }
     case kind::REGEXP_STAR: {
       if( s.size() != index_start ) {
-        for(unsigned k=s.size() - index_start; k>0; --k) {
-          CVC4::String t = s.substr(index_start, k);
+        for (unsigned i = s.size() - index_start; i > 0; --i)
+        {
+          CVC4::String t = s.substr(index_start, i);
           if( testConstStringInRegExp( t, 0, r[0] ) ) {
-            if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r ) ) {
+            if (index_start + i == s.size()
+                || testConstStringInRegExp(s, index_start + i, r))
+            {
               return true;
             }
           }
@@ -1409,8 +1413,8 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) {
           {
             nb << nm->mkNode(STRING_IN_REGEXP, xc, r);
           }
-          Node retNode = nb.constructNode();
-          return returnRewrite(node, retNode, "re-in-dist-char-star");
+          return returnRewrite(
+              node, nb.constructNode(), "re-in-dist-char-star");
         }
       }
     }
@@ -2245,19 +2249,19 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
         if (nc2.size() > 1)
         {
           Node emp = nm->mkConst(CVC4::String(""));
-          NodeBuilder<> nb(kind::AND);
+          NodeBuilder<> nb2(kind::AND);
           for (const Node& n2 : nc2)
           {
             if (n2 == n)
             {
-              nb << nm->mkNode(kind::EQUAL, node[0], node[1]);
+              nb2 << nm->mkNode(kind::EQUAL, node[0], node[1]);
             }
             else
             {
-              nb << nm->mkNode(kind::EQUAL, emp, n2);
+              nb2 << nm->mkNode(kind::EQUAL, emp, n2);
             }
           }
-          ret = nb.constructNode();
+          ret = nb2.constructNode();
         }
         else
         {
@@ -2770,14 +2774,14 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
           //   str.replace( str.++( x, "ab" ), "a", y ) --->
           //   str.++( str.replace( str.++( x, "a" ), "a", y ), "b" )
           // this is independent of whether the second argument may be empty
-          std::vector<Node> cc;
-          cc.push_back(NodeManager::currentNM()->mkNode(
+          std::vector<Node> scc;
+          scc.push_back(NodeManager::currentNM()->mkNode(
               kind::STRING_STRREPL,
               utils::mkConcat(STRING_CONCAT, children0),
               node[1],
               node[2]));
-          cc.insert(cc.end(), ce.begin(), ce.end());
-          Node ret = utils::mkConcat(STRING_CONCAT, cc);
+          scc.insert(scc.end(), ce.begin(), ce.end());
+          Node ret = utils::mkConcat(STRING_CONCAT, scc);
           return returnRewrite(node, ret, "rpl-cctn");
         }
       }
@@ -2968,8 +2972,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
         return returnRewrite(node, node[0], "repl-repl2-inv-id");
       }
       bool dualReplIteSuccess = false;
-      Node cmp_con = checkEntailContains(node[1][0], node[1][2]);
-      if (!cmp_con.isNull() && !cmp_con.getConst<bool>())
+      Node cmp_con2 = checkEntailContains(node[1][0], node[1][2]);
+      if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
       {
         // str.contains( x, z ) ---> false
         //   implies
@@ -2983,11 +2987,11 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
         //   implies
         // str.replace( x, str.replace( x, y, z ), w ) --->
         // ite( str.contains( x, y ), x, w )
-        cmp_con = checkEntailContains(node[1][1], node[1][2]);
-        if (!cmp_con.isNull() && !cmp_con.getConst<bool>())
+        cmp_con2 = checkEntailContains(node[1][1], node[1][2]);
+        if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
         {
-          cmp_con = checkEntailContains(node[1][2], node[1][1]);
-          if (!cmp_con.isNull() && !cmp_con.getConst<bool>())
+          cmp_con2 = checkEntailContains(node[1][2], node[1][1]);
+          if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
           {
             dualReplIteSuccess = true;
           }
@@ -3016,8 +3020,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
         // str.contains(y, z) ----> false and ( y == w or x == w ) implies
         //   implies
         // str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w)
-        Node cmp_con = checkEntailContains(node[1][0], node[1][2]);
-        invSuccess = !cmp_con.isNull() && !cmp_con.getConst<bool>();
+        Node cmp_con2 = checkEntailContains(node[1][0], node[1][2]);
+        invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>();
       }
     }
     else
@@ -3025,11 +3029,11 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
       // str.contains(x, z) ----> false and str.contains(x, w) ----> false
       //   implies
       // str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u)
-      Node cmp_con = checkEntailContains(node[0], node[1][1]);
-      if (!cmp_con.isNull() && !cmp_con.getConst<bool>())
+      Node cmp_con2 = checkEntailContains(node[0], node[1][1]);
+      if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
       {
-        cmp_con = checkEntailContains(node[0], node[1][2]);
-        invSuccess = !cmp_con.isNull() && !cmp_con.getConst<bool>();
+        cmp_con2 = checkEntailContains(node[0], node[1][2]);
+        invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>();
       }
     }
     if (invSuccess)
@@ -3044,8 +3048,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) {
     {
       // str.contains( z, w ) ----> false implies
       // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z )
-      Node cmp_con = checkEntailContains(node[1], node[2][0]);
-      if (!cmp_con.isNull() && !cmp_con.getConst<bool>())
+      Node cmp_con2 = checkEntailContains(node[1], node[2][0]);
+      if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
       {
         Node res =
             nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]);