mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Code Activity

household chores - move to iterators

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-03-24 12:35:46 -07:00
parent dee3cf8de4
commit 93cf989b78
2 changed files with 10 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/arith/degree_shift_tactic.cpp
View file

@ -169,10 +169,8 @@ class degree_shift_tactic : public tactic {
void collect(goal const & g) {
m_var2degree.reset();
expr_fast_mark1 visited;
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
collect(g.form(i), visited);
}
for (auto [f, d, p] : g)
collect(f, visited);
TRACE("degree_shift", display_candidates(tout););
}

20
src/tactic/arith/fix_dl_var_tactic.cpp
View file

@ -216,10 +216,8 @@ class fix_dl_var_tactic : public tactic {
try {
expr_fast_mark1 visited;
flet<expr_fast_mark1*> _visited(m_visited, &visited);
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
process(g.form(i));
}
for (auto [f, d, p] : g)
process(f);
return most_occs();
}
catch (const failed &) {
@ -268,15 +266,13 @@ class fix_dl_var_tactic : public tactic {
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned size = g->size();
for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) {
expr * curr = g->form(idx);
unsigned idx = 0;
for (auto [curr, d, p] : *g) {
if (g->inconsistent())
break;
m_rw(curr, new_curr, new_pr);
if (produce_proofs) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
new_pr = m.mk_modus_ponens(p, new_pr);
g->update(idx++, new_curr, new_pr, d);
}
g->inc_depth();
}