summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2020-03-05 11:42:54 -0800
committerGitHub <noreply@github.com>2020-03-05 11:42:54 -0800
commit04039407e6308070c148de0d5e93640ec1b0a341 (patch)
treeb66f63d49df0713b1ca2a440bec89f1d60af32a4 /src/theory/uf
parent18fe192c29a9a2c37d1925730af01e906b9888c5 (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/theory/uf')
-rw-r--r--src/theory/uf/equality_engine.cpp30
-rw-r--r--src/theory/uf/ho_extension.cpp4
-rw-r--r--src/theory/uf/symmetry_breaker.cpp102
-rw-r--r--src/theory/uf/theory_uf_model.cpp22
4 files changed, 95 insertions, 63 deletions
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<std::shared_ptr<EqProof>> 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<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions();
- for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin();
- i != ps.end();
- ++i) {
- Debug("ufsymm") << "UFSYMM partition*: " << (*i).first;
- set<TNode>& p = (*i).second;
+ for (auto& kv : ps)
+ {
+ Debug("ufsymm") << "UFSYMM partition*: " << kv.first;
+ set<TNode>& p = kv.second;
for(set<TNode>::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<Node>& 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<Node>& newClauses) {
if(i != p.end() || p.size() != cts.size()) {
Debug("ufsymm") << "UFSYMM cts != p" << endl;
NodeBuilder<> disj(kind::OR);
- for(set<Node>::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<Node>::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<Node>::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);
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback