mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

iterator -> for

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-09 05:40:12 +03:00
parent 0c9711aad7
commit ed6e23f153
1 changed files with 13 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
src/smt/smt_solver.cpp
View file

@ -264,14 +264,14 @@ namespace smt {
void compute_assrtn_fds(ptr_vector<expr> & core, vector<func_decl_set> & assrtn_fds) { void compute_assrtn_fds(ptr_vector<expr> & core, vector<func_decl_set> & assrtn_fds) {
assrtn_fds.resize(m_name2assertion.size()); assrtn_fds.resize(m_name2assertion.size());
obj_map<expr, expr*>::iterator ait = m_name2assertion.begin(); unsigned i = 0;
obj_map<expr, expr*>::iterator aend = m_name2assertion.end(); for (auto & kv : m_name2assertion) {
for (unsigned i = 0; ait != aend; ait++, i++) { if (!core.contains(kv.m_key)) {
if (core.contains(ait->m_key)) collect_fds_proc p(m, assrtn_fds[i]);
continue; expr_fast_mark1 visited;
collect_fds_proc p(m, assrtn_fds[i]); quick_for_each_expr(p, visited, kv.m_value);
expr_fast_mark1 visited; }
quick_for_each_expr(p, visited, ait->m_value); ++i;
} }
} }
@ -293,9 +293,8 @@ namespace smt {
for (unsigned d = 0; d < m_core_extend_patterns_max_distance; d++) { for (unsigned d = 0; d < m_core_extend_patterns_max_distance; d++) {
new_core_literals.reset(); new_core_literals.reset();
unsigned sz = core.size(); for (expr* c : core) {
for (unsigned i = 0; i < sz; i++) { expr_ref name(c, m);
expr_ref name(core[i], m);
SASSERT(m_name2assertion.contains(name)); SASSERT(m_name2assertion.contains(name));
expr_ref assrtn(m_name2assertion.find(name), m); expr_ref assrtn(m_name2assertion.find(name), m);
collect_pattern_fds(assrtn, pattern_fds); collect_pattern_fds(assrtn, pattern_fds);
@ -305,12 +304,12 @@ namespace smt {
if (assrtn_fds.empty()) if (assrtn_fds.empty())
compute_assrtn_fds(core, assrtn_fds); compute_assrtn_fds(core, assrtn_fds);
obj_map<expr, expr*>::iterator ait = m_name2assertion.begin(); unsigned i = 0;
obj_map<expr, expr*>::iterator aend = m_name2assertion.end(); for (auto & kv : m_name2assertion) {
for (unsigned i = 0; ait != aend; ait++, i++) {
if (!core.contains(ait->m_key) && if (!core.contains(ait->m_key) &&
fds_intersect(pattern_fds, assrtn_fds[i])) fds_intersect(pattern_fds, assrtn_fds[i]))
new_core_literals.push_back(ait->m_key); new_core_literals.push_back(ait->m_key);
++i;
} }
} }