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/preprocessing | |
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/preprocessing')
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 95 | ||||
-rw-r--r-- | src/preprocessing/passes/sygus_inference.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/passes/symmetry_detect.cpp | 22 | ||||
-rw-r--r-- | src/preprocessing/passes/synth_rew_rules.cpp | 8 | ||||
-rw-r--r-- | src/preprocessing/util/ite_utilities.cpp | 17 |
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); } |