mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-20 15:40:37 +00:00
Code Activity

block ackermann over nested selects

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-19 10:41:56 -07:00
parent 9e505edb66
commit a05be8a291
1 changed files with 13 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ackermannization/ackr_helper.h
View file

@ -52,14 +52,26 @@ public:
return m_autil.is_select(a) && is_uninterp_const(a->get_arg(0));
}
void mark_non_select_rec(expr* t, expr_mark& visited, expr_mark& non_select) {
if (visited.is_marked(t))
return;
visited.mark(t, true);
non_select.mark(t, true);
if (is_app(t)) {
for (expr *arg : *to_app(t))
mark_non_select_rec(arg, visited,non_select);
}
}
void mark_non_select(app* a, expr_mark& non_select) {
if (m_autil.is_select(a)) {
bool first = true;
expr_mark visited;
for (expr* arg : *a) {
if (first)
first = false;
else
non_select.mark(arg, true);
mark_non_select_rec(arg, visited, non_select);
}
}
else {