mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 21:36:09 +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 c0f7dc7e4c
commit 8d6fdcd3ee
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)); 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) { void mark_non_select(app* a, expr_mark& non_select) {
if (m_autil.is_select(a)) { if (m_autil.is_select(a)) {
bool first = true; bool first = true;
expr_mark visited;
for (expr* arg : *a) { for (expr* arg : *a) {
if (first) if (first)
first = false; first = false;
else else
non_select.mark(arg, true); mark_non_select_rec(arg, visited, non_select);
} }
} }
else { else {