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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-15 11:19:23 -07:00
commit e508cf3d8b
1 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/rewriter/seq_regex_bisim.cpp
View file

@ -86,9 +86,15 @@ namespace seq {
} }
/* /*
Collect the leaves of a t-regex der (an ITE / antimirov union / Collect the leaves of a t-regex der (an ITE-tree whose leaves are
union-tree with regex leaves) into the output vector. Empty regex expressions) into the output vector. Empty (re.empty) leaves
(re.empty) leaves are dropped. are dropped.
Each leaf is treated as a single bisimulation state regardless of
its top-level shape (including re.union and re.antimirov_union):
descending into a union at the leaf would split one state into
several, which is semantically unsound for the bisimulation /
union-find merging that follows.
Returns false if we encountered an unexpected node (e.g. a free Returns false if we encountered an unexpected node (e.g. a free
variable creeping in) — in that case the caller should bail out. variable creeping in) — in that case the caller should bail out.
@ -102,9 +108,7 @@ namespace seq {
expr* e = work.back(); expr* e = work.back();
work.pop_back(); work.pop_back();
expr* c = nullptr, * t = nullptr, * f = nullptr; expr* c = nullptr, * t = nullptr, * f = nullptr;
if (m.is_ite(e, c, t, f) || if (m.is_ite(e, c, t, f)) {
m_util.re.is_union(e, t, f) ||
m_util.re.is_antimirov_union(e, t, f)) {
if (seen.insert_if_not_there(t)) if (seen.insert_if_not_there(t))
work.push_back(t); work.push_back(t);
if (seen.insert_if_not_there(f)) if (seen.insert_if_not_there(f))