mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-19 16:53:18 +00:00
Code Activity

Migrate iterator-based for loops to range-based for loops in 11 files

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-17 20:16:25 +00:00
parent 96bd239af9
commit bef113254c
9 changed files with 35 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/c++/z3++.h
View file

@ -3431,7 +3431,7 @@ namespace z3 {
Z3_optimize_inc_ref(c, m_opt);
add(expr_vector(c, src.assertions()));
expr_vector v(c, src.objectives());
for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
for (auto& e : v) minimize(e);
}
optimize& operator=(optimize const& o) {
Z3_optimize_inc_ref(o.ctx(), o.m_opt);
@ -3447,7 +3447,7 @@ namespace z3 {
Z3_optimize_assert(ctx(), m_opt, e);
}
void add(expr_vector const& es) {
for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
for (auto& e : es) add(e);
}
void add(expr const& e, expr const& t) {
assert(e.is_bool());

18
src/ast/rewriter/bv_bounds.cpp
View file

@ -238,9 +238,8 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
}
void bv_bounds::reset() {
intervals_map::iterator it = m_negative_intervals.begin();
const intervals_map::iterator end = m_negative_intervals.end();
for (; it != end; ++it) dealloc(it->m_value);
for (auto& [key, value] : m_negative_intervals)
dealloc(value);
}
br_status bv_bounds::rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result) {
@ -312,9 +311,7 @@ br_status bv_bounds::rewrite(unsigned limit, func_decl * f, unsigned num, expr *
if (nargs.size() == num && !has_singls) return BR_FAILED;
expr_ref eq(m_m);
for (bv_bounds::bound_map::iterator i = m_singletons.begin(); i != m_singletons.end(); ++i) {
app * const v = i->m_key;
const rational val = i->m_value;
for (auto& [v, val] : m_singletons) {
eq = m_m.mk_eq(v, bvu().mk_numeral(val, v->get_decl()->get_range()));
if (negated) eq = m_m.mk_not(eq);
nargs.push_back(eq);
@ -568,20 +565,17 @@ bool bv_bounds::is_sat() {
obj_hashtable<app> seen;
obj_hashtable<app>::entry *dummy;
for (bound_map::iterator i = m_unsigned_lowers.begin(); i != m_unsigned_lowers.end(); ++i) {
app * const v = i->m_key;
for (auto& [v, _] : m_unsigned_lowers) {
if (!seen.insert_if_not_there_core(v, dummy)) continue;
if (!is_sat(v)) return false;
}
for (bound_map::iterator i = m_unsigned_uppers.begin(); i != m_unsigned_uppers.end(); ++i) {
app * const v = i->m_key;
for (auto& [v, _] : m_unsigned_uppers) {
if (!seen.insert_if_not_there_core(v, dummy)) continue;
if (!is_sat(v)) return false;
}
for (intervals_map::iterator i = m_negative_intervals.begin(); i != m_negative_intervals.end(); ++i) {
app * const v = i->m_key;
for (auto& [v, _] : m_negative_intervals) {
if (!seen.insert_if_not_there_core(v, dummy)) continue;
if (!is_sat(v)) return false;
}

6
src/ast/sls/bvsls_opt_engine.h
View file

@ -57,10 +57,8 @@ protected:
mpz top_score() {
mpz res(0);
obj_hashtable<expr> const & top_exprs = m_obj_tracker.get_top_exprs();
for (obj_hashtable<expr>::iterator it = top_exprs.begin();
it != top_exprs.end();
++it)
m_mpz_manager.add(res, m_obj_tracker.get_value(*it), res);
for (auto* e : top_exprs)
m_mpz_manager.add(res, m_obj_tracker.get_value(e), res);
return res;
}

9
src/ast/sls/sls_bv_tracker.h
View file

@ -648,11 +648,10 @@ public:
void randomize(ptr_vector<expr> const & as) {
TRACE(sls_verbose, tout << "Abandoned model:" << std::endl; show_model(tout); );
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); ++it) {
func_decl * fd = it->m_key;
for (auto& [fd, ep] : m_entry_points) {
sort * s = fd->get_range();
mpz temp = get_random(s);
set_value(it->m_value, temp);
set_value(ep, temp);
m_mpz_manager.del(temp);
}
@ -662,8 +661,8 @@ public:
void reset(ptr_vector<expr> const & as) {
TRACE(sls_verbose, tout << "Abandoned model:" << std::endl; show_model(tout); );
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); ++it) {
set_value(it->m_value, m_zero);
for (auto& [fd, ep] : m_entry_points) {
set_value(ep, m_zero);
}
}

18
src/muz/rel/aig_exporter.cpp
View file

@ -23,14 +23,11 @@ namespace datalog {
m_latch_vars(m), m_latch_varsp(m), m_ruleid_var_set(m), m_ruleid_varp_set(m)
{
std::set<func_decl*> predicates;
for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(),
E = m_rules.end_grouped_rules(); I != E; ++I) {
predicates.insert(I->m_key);
}
for (auto& [pred, _] : m_rules.get_grouped_rules())
predicates.insert(pred);
for (fact_vector::const_iterator I = facts->begin(), E = facts->end(); I != E; ++I) {
predicates.insert(I->first);
}
for (auto& [pred, _] : *facts)
predicates.insert(pred);
// reserve pred id = 0 for initialization purposes
unsigned num_preds = (unsigned)predicates.size() + 1;
@ -101,11 +98,8 @@ namespace datalog {
expr_ref_vector exprs(m);
substitution subst(m);
for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(),
E = m_rules.end_grouped_rules(); I != E; ++I) {
for (rule_vector::iterator II = I->get_value()->begin(),
EE = I->get_value()->end(); II != EE; ++II) {
rule *r = *II;
for (auto& [pred, rules] : m_rules.get_grouped_rules()) {
for (rule* r : *rules) {
unsigned numqs = r->get_positive_tail_size();
if (numqs > 1) {
throw default_exception("non-linear clauses not supported");

6
src/muz/spacer/spacer_qe_project.cpp
View file

@ -2139,10 +2139,8 @@ class array_project_selects_util {
}
// dealloc
sel_map::iterator begin = m_sel_terms.begin(), end = m_sel_terms.end();
for (sel_map::iterator it = begin; it != end; ++it) {
dealloc(it->m_value);
}
for (auto& [key, value] : m_sel_terms)
dealloc(value);
m_sel_terms.reset();
}
};

13
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -580,20 +580,19 @@ namespace datalog {
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
bool done_something = false;
rule_set::iterator rend = rules->end();
for (rule_set::iterator rit = rules->begin(); rit!=rend; ++rit) {
rule_ref r(*rit, m_rm);
for (rule* r : *rules) {
rule_ref rl(r, m_rm);
rule_ref replacement(m_rm);
while (r && do_eager_inlining(r, *rules, replacement)) {
r = replacement;
while (rl && do_eager_inlining(rl, *rules, replacement)) {
rl = replacement;
done_something = true;
}
if (!r) {
if (!rl) {
continue;
}
res->add_rule(r);
res->add_rule(rl);
}
if (done_something) {
rules = res.detach();

12
src/muz/transforms/dl_mk_subsumption_checker.cpp
View file

@ -100,9 +100,7 @@ namespace datalog {
//(discovering a total relation might reveal other total relations)
do {
new_discovered = false;
rule_set::iterator rend = rules.end();
for(rule_set::iterator rit = rules.begin(); rit!=rend; ++rit) {
rule * r = *rit;
for (rule* r : rules) {
func_decl * head_pred = r->get_decl();
if(is_total_rule(r) && !m_total_relations.contains(head_pred)) {
on_discovered_total_relation(head_pred, r);
@ -261,9 +259,7 @@ namespace datalog {
func_decl_set const& candidate_preds = m_context.get_predicates();
func_decl_set::iterator end = candidate_preds.end();
for(func_decl_set::iterator it = candidate_preds.begin(); it!=end; ++it) {
func_decl * pred = *it;
for (func_decl* pred : candidate_preds) {
unsigned rel_sz;
if (m_total_relations.contains(pred)) { continue; } // already total
@ -306,9 +302,7 @@ namespace datalog {
void mk_subsumption_checker::collect_ground_unconditional_rule_heads(const rule_set & rules)
{
rule_set::iterator rend = rules.end();
for(rule_set::iterator rit = rules.begin(); rit!=rend; ++rit) {
rule * r = *rit;
for (rule* r : rules) {
func_decl * pred = r->get_decl();
if(r->get_tail_size()!=0) { continue; }

8
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -327,11 +327,11 @@ public:
if (!(m_unsigned_lowers.empty() && m_unsigned_uppers.empty())) {
TRACE(bv_size_reduction,
tout << "m_unsigned_lowers: " << std::endl;
for (obj_map<app, numeral>::iterator it = m_unsigned_lowers.begin(); it != m_unsigned_lowers.end(); ++it)
tout << mk_ismt2_pp(it->m_key, m) << " >= " << it->m_value.to_string() << std::endl;
for (auto& [key, value] : m_unsigned_lowers)
tout << mk_ismt2_pp(key, m) << " >= " << value.to_string() << std::endl;
tout << "m_unsigned_uppers: " << std::endl;
for (obj_map<app, numeral>::iterator it = m_unsigned_uppers.begin(); it != m_unsigned_uppers.end(); ++it)
tout << mk_ismt2_pp(it->m_key, m) << " <= " << it->m_value.to_string() << std::endl;
for (auto& [key, value] : m_unsigned_uppers)
tout << mk_ismt2_pp(key, m) << " <= " << value.to_string() << std::endl;
);
obj_map<app, numeral>::iterator it = m_unsigned_uppers.begin();