diff options
author | MikolasJanota <MikolasJanota@users.noreply.github.com> | 2021-09-04 00:59:46 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-03 22:59:46 +0000 |
commit | 5cef06bd2beff38a911c74ec082d9789eed83421 (patch) | |
tree | a632c89f65c6a0b9cf845e56ac2ac40cc232be5c /src/theory | |
parent | 54212c1402e43d3a414d20f3e418f2a0fec10a8d (diff) |
Avoiding duplicate search in maps (#7055)
This commit identifies a couple of scenarios where an operation required
2 searches into a map/hashmap and replaces them with a single search.
This also makes the code shorter.
Signed-off-by: Mikolas Janota <mikolas.janota@gmail.com>
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/term_pools.cpp | 4 |
2 files changed, 6 insertions, 12 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index be1633d16..0daf53d2d 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -589,19 +589,13 @@ bool Instantiate::recordInstantiationInternal(Node q, std::vector<Node>& terms) { Trace("inst-add-debug") << "Adding into context-dependent inst trie" << std::endl; - CDInstMatchTrie* imt; - std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q); - if (it != d_c_inst_match_trie.end()) - { - imt = it->second; - } - else + const auto res = d_c_inst_match_trie.insert({q, nullptr}); + if (res.second) { - imt = new CDInstMatchTrie(d_qstate.getUserContext()); - d_c_inst_match_trie[q] = imt; + res.first->second = new CDInstMatchTrie(d_qstate.getUserContext()); } d_c_inst_match_trie_dom.insert(q); - return imt->addInstMatch(d_qstate, q, terms); + return res.first->second->addInstMatch(d_qstate, q, terms); } Trace("inst-add-debug") << "Adding into inst trie" << std::endl; return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms); diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp index 883161f1a..2d95c8b20 100644 --- a/src/theory/quantifiers/term_pools.cpp +++ b/src/theory/quantifiers/term_pools.cpp @@ -103,9 +103,9 @@ void TermPools::getTermsForPool(Node p, std::vector<Node>& terms) for (const Node& t : dom.d_terms) { Node r = d_qs.getRepresentative(t); - if (reps.find(r) == reps.end()) + const auto i = reps.insert(r); + if (i.second) { - reps.insert(r); dom.d_currTerms.push_back(t); } } |