diff options
| author | Tim King <taking@google.com> | 2015-11-09 11:16:47 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2015-11-09 11:16:47 -0800 |
| commit | 50c8533760bfd5b1f803d52bc4318c544521e6af (patch) | |
| tree | b089e94f6607c25b3b77207ffcb605cc531be3d7 /src/theory/uf | |
| parent | 6b2e8be53f0839809a2f76df0754b37a7e56db08 (diff) | |
Replacing an inefficient use of std::find(...) to use std::set's find() instead.
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index bd85b735d..d5e18ed14 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -743,7 +743,7 @@ SymmetryBreaker::selectMostPromisingTerm(Terms& terms) { void SymmetryBreaker::insertUsedIn(Term term, const Permutation& p, set<Node>& cts) { // insert terms from p used in term into cts //Debug("ufsymm") << "UFSYMM usedIn(): " << term << " , " << p << endl; - if(find(p.begin(), p.end(), term) != p.end()) { + if (p.find(term) != p.end()) { cts.insert(term); } else { for(TNode::iterator i = term.begin(); i != term.end(); ++i) { |