From 04039407e6308070c148de0d5e93640ec1b0a341 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Thu, 5 Mar 2020 11:42:54 -0800 Subject: Enable -Wshadow and fix warnings. (#3909) Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally. Co-authored-by: Clark Barrett Co-authored-by: Andres Noetzli Co-authored-by: Aina Niemetz Co-authored-by: Alex Ozdemir Co-authored-by: makaimann Co-authored-by: yoni206 Co-authored-by: Andrew Reynolds Co-authored-by: AleksandarZeljic Co-authored-by: Caleb Donovick Co-authored-by: Amalee Co-authored-by: Scott Kovach Co-authored-by: ntsis --- src/theory/uf/equality_engine.cpp | 30 +++++++---- src/theory/uf/ho_extension.cpp | 4 +- src/theory/uf/symmetry_breaker.cpp | 102 ++++++++++++++++++++++--------------- src/theory/uf/theory_uf_model.cpp | 22 +++++--- 4 files changed, 95 insertions(+), 63 deletions(-) (limited to 'src/theory/uf') diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 63aa81097..479e3400d 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1002,15 +1002,22 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { std::vector> orderedChildren; bool nullCongruenceFound = false; - for (unsigned i = 0; i < eqpc->d_children.size(); ++i) { - if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && - eqpc->d_children[i]->d_node.isNull()) { + for (const auto& child : eqpc->d_children) + { + if (child->d_id == eq::MERGED_THROUGH_CONGRUENCE + && child->d_node.isNull()) + { nullCongruenceFound = true; - Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl; - orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]); - orderedChildren.push_back(eqpc->d_children[i]->d_children[1]); - } else { - orderedChildren.push_back(eqpc->d_children[i]); + Debug("pf::ee") + << "Have congruence with empty d_node. Splitting..." + << std::endl; + orderedChildren.insert(orderedChildren.begin(), + child->d_children[0]); + orderedChildren.push_back(child->d_children[1]); + } + else + { + orderedChildren.push_back(child); } } @@ -1935,11 +1942,12 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) newSetTriggersSize = 0; // Copy into to new one, and insert the new tag/id unsigned i = 0; - Theory::Set tags = newSetTags; + Theory::Set tags2 = newSetTags; TheoryId current; - while ((current = Theory::setPop(tags)) != THEORY_LAST) { + while ((current = Theory::setPop(tags2)) != THEORY_LAST) + { // Remove from the tags - tags = Theory::setRemove(current, tags); + tags2 = Theory::setRemove(current, tags2); // Insert the id into the triggers newSetTriggers[newSetTriggersSize++] = current == tag ? eqNodeId : triggerSet.d_triggers[i++]; diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 6d6f49c7f..23b7b9217 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -336,8 +336,8 @@ unsigned HoExtension::checkAppCompletion() { if (n[k].getType().isFunction()) { - TNode rop = ee->getRepresentative(n[k]); - curr_rops[rop] = true; + TNode rop2 = ee->getRepresentative(n[k]); + curr_rops[rop2] = true; } } } diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 49ceebfd6..27d045120 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -400,18 +400,17 @@ void SymmetryBreaker::assertFormula(TNode phi) { } } unordered_map, TNodeHashFunction>& ps = t.partitions(); - for(unordered_map, TNodeHashFunction>::iterator i = ps.begin(); - i != ps.end(); - ++i) { - Debug("ufsymm") << "UFSYMM partition*: " << (*i).first; - set& p = (*i).second; + for (auto& kv : ps) + { + Debug("ufsymm") << "UFSYMM partition*: " << kv.first; + set& p = kv.second; for(set::iterator j = p.begin(); j != p.end(); ++j) { Debug("ufsymm") << " " << *j; } Debug("ufsymm") << endl; - p.insert((*i).first); + p.insert(kv.first); Permutations::iterator pi = d_permutations.find(p); if(pi == d_permutations.end()) { d_permutations.insert(p); @@ -473,11 +472,9 @@ void SymmetryBreaker::apply(std::vector& newClauses) { } } - for(Permutations::iterator i = d_permutations.begin(); - i != d_permutations.end(); - ++i) { + for (const Permutation& p : d_permutations) + { ++(d_stats.d_permutationSetsConsidered); - const Permutation& p = *i; Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl; size_t n = p.size() - 1; if(invariantByPermutations(p)) { @@ -529,11 +526,12 @@ void SymmetryBreaker::apply(std::vector& newClauses) { if(i != p.end() || p.size() != cts.size()) { Debug("ufsymm") << "UFSYMM cts != p" << endl; NodeBuilder<> disj(kind::OR); - for(set::const_iterator i = cts.begin(); - i != cts.end(); - ++i) { - if(t != *i) { - disj << NodeManager::currentNM()->mkNode(kind::EQUAL, t, *i); + NodeManager* nm = NodeManager::currentNM(); + for (const Node& nn : cts) + { + if (t != nn) + { + disj << nm->mkNode(kind::EQUAL, t, nn); } } Node d; @@ -596,20 +594,29 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.push_back(p1); repls.push_back(p1); repls.push_back(p0); - for(vector::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { - Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + for (const Node nn : d_phi) + { + Node s = + nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); Node n = norm(s); - if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { - Debug("ufsymm") << "UFSYMM P_swap is NOT an inv perm op for " << p << endl - << "UFSYMM because this node: " << *i << endl - << "UFSYMM rewrite-norms to : " << n << endl - << "UFSYMM which is not in our set of normalized assertions" << endl; + if (nn != n && d_phiSet.find(n) == d_phiSet.end()) + { + Debug("ufsymm") + << "UFSYMM P_swap is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << nn << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" << endl; return false; - } else if(Debug.isOn("ufsymm:p")) { - if(*i == s) { - Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << *i << endl; - } else { - Debug("ufsymm:p") << "UFSYMM P_swap passes: " << *i << endl + } + else if (Debug.isOn("ufsymm:p")) + { + if (nn == s) + { + Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << nn << endl; + } + else + { + Debug("ufsymm:p") << "UFSYMM P_swap passes: " << nn << endl << "UFSYMM rewrites: " << s << endl << "UFSYMM norms: " << n << endl; } @@ -622,30 +629,41 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.clear(); repls.clear(); bool first = true; - for(Permutation::const_iterator i = p.begin(); i != p.end(); ++i) { - subs.push_back(*i); + for (const Node& nn : p) + { + subs.push_back(nn); if(!first) { - repls.push_back(*i); + repls.push_back(nn); } else { first = false; } } repls.push_back(*p.begin()); Assert(subs.size() == repls.size()); - for(vector::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { - Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + for (const Node& nn : d_phi) + { + Node s = + nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); Node n = norm(s); - if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { - Debug("ufsymm") << "UFSYMM P_circ is NOT an inv perm op for " << p << endl - << "UFSYMM because this node: " << *i << endl - << "UFSYMM rewrite-norms to : " << n << endl - << "UFSYMM which is not in our set of normalized assertions" << endl; + if (nn != n && d_phiSet.find(n) == d_phiSet.end()) + { + Debug("ufsymm") + << "UFSYMM P_circ is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << nn << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" + << endl; return false; - } else if(Debug.isOn("ufsymm:p")) { - if(*i == s) { - Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << *i << endl; - } else { - Debug("ufsymm:p") << "UFSYMM P_circ passes: " << *i << endl + } + else if (Debug.isOn("ufsymm:p")) + { + if (nn == s) + { + Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << nn << endl; + } + else + { + Debug("ufsymm:p") << "UFSYMM P_circ passes: " << nn << endl << "UFSYMM rewrites: " << s << endl << "UFSYMM norms: " << n << endl; } diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index ffe3730c4..d667aea7e 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -153,14 +153,20 @@ void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){ } } //now see if any children can be removed, and simplify the ones that cannot - for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - if( !it->first.isNull() ){ - if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ - eraseData.push_back( it->first ); - }else{ - it->second.simplify( op, defaultVal, argIndex+1 ); - if( it->second.isEmpty() ){ - eraseData.push_back( it->first ); + for (auto& kv : d_data) + { + if (!kv.first.isNull()) + { + if (!defaultVal.isNull() && kv.second.d_value == defaultVal) + { + eraseData.push_back(kv.first); + } + else + { + kv.second.simplify(op, defaultVal, argIndex + 1); + if (kv.second.isEmpty()) + { + eraseData.push_back(kv.first); } } } -- cgit v1.2.3