mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-20 23:44:41 +00:00
Code Activity

Refactor der.cpp topological sort to use structured bindings (#8401)

Browse source 
* Initial plan

* Refactor der.cpp to use structured bindings for expression/index pairs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix comment to refer to 'e' instead of 't' after structured binding refactor

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-28 19:38:58 -08:00 • committed by Nikolaj Bjorner
parent 5dd01acb42
commit 1853cdeb3d
1 changed files with 18 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/ast/rewriter/der.cpp
View file

@ -272,36 +272,35 @@ static void der_sort_vars(ptr_vector<var> & vars, expr_ref_vector & definitions,
todo.push_back(frame(v, 0)); todo.push_back(frame(v, 0));
while (!todo.empty()) { while (!todo.empty()) {
start: start:
frame & fr = todo.back(); auto& [e, idx] = todo.back();
expr * t = fr.first; if (done.is_marked(e)) {
if (done.is_marked(t)) {
todo.pop_back(); todo.pop_back();
continue; continue;
} }
switch (t->get_kind()) { switch (e->get_kind()) {
case AST_VAR: case AST_VAR:
vidx = to_var(t)->get_idx(); vidx = to_var(e)->get_idx();
if (fr.second == 0) { if (idx == 0) {
CTRACE(der_bug, vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); CTRACE(der_bug, vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
// Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula. // Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
if (definitions.get(vidx, nullptr) != nullptr) { if (definitions.get(vidx, nullptr) != nullptr) {
if (visiting.is_marked(t)) { if (visiting.is_marked(e)) {
// cycle detected: remove t // cycle detected: remove e
visiting.reset_mark(t); visiting.reset_mark(e);
definitions[vidx] = nullptr; definitions[vidx] = nullptr;
} }
else { else {
visiting.mark(t); visiting.mark(e);
fr.second = 1; idx = 1;
todo.push_back(frame(definitions.get(vidx), 0)); todo.push_back(frame(definitions.get(vidx), 0));
goto start; goto start;
} }
} }
} }
else { else {
SASSERT(fr.second == 1); SASSERT(idx == 1);
if (definitions.get(vidx, nullptr) != nullptr) { if (definitions.get(vidx, nullptr) != nullptr) {
visiting.reset_mark(t); visiting.reset_mark(e);
order.push_back(vidx); order.push_back(vidx);
} }
else { else {
@ -309,7 +308,7 @@ static void der_sort_vars(ptr_vector<var> & vars, expr_ref_vector & definitions,
// do nothing // do nothing
} }
} }
done.mark(t); done.mark(e);
todo.pop_back(); todo.pop_back();
break; break;
case AST_QUANTIFIER: case AST_QUANTIFIER:
@ -317,16 +316,16 @@ static void der_sort_vars(ptr_vector<var> & vars, expr_ref_vector & definitions,
todo.pop_back(); todo.pop_back();
break; break;
case AST_APP: case AST_APP:
num = to_app(t)->get_num_args(); num = to_app(e)->get_num_args();
while (fr.second < num) { while (idx < num) {
expr * arg = to_app(t)->get_arg(fr.second); expr * arg = to_app(e)->get_arg(idx);
fr.second++; idx++;
if (done.is_marked(arg)) if (done.is_marked(arg))
continue; continue;
todo.push_back(frame(arg, 0)); todo.push_back(frame(arg, 0));
goto start; goto start;
} }
done.mark(t); done.mark(e);
todo.pop_back(); todo.pop_back();
break; break;
default: default: