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

fix(seq_regex_bisim): treat each transition-regex leaf as a single state

Browse source 
The bisimulation worklist in regex_bisim::collect_leaves used to descend
through re.union and re.antimirov_union at the top of each leaf of the
transition regex, splitting a single bisimulation state into multiple
states before they were merged into the union-find. This contradicts the
bisimulation invariant: each leaf of a t-regex represents one state,
regardless of its top-level shape.

While the split happens to be sound when the goal is asserting
L(union(A,B)) = empty (since L(A) = empty AND L(B) = empty is
equivalent), it adds spurious merges to the union-find that distort
state-class identities, slow down convergence on hard equivalence
queries, and create latent unsoundness risk for any extension that
interprets leaves more semantically (XOR pair handling, classical-flag
propagation, future antimirov re-enable).

After the fix, on the 1523-file regex-equivalence corpus
(C:/git/bench/inputs/regex-equivalence, 5s/file timeout):
  * no SAT<->UNSAT verdict flips vs prior master,
  * 6 cases flip from timeout to sat (now decided in <1s),
  * ~10% wall-time reduction on commonly-solved files (0.902x).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Margus Veanes 2026-06-15 10:28:18 -07:00
parent f508854fe5
commit 622977814c
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 /
union-tree with regex leaves) into the output vector. Empty
(re.empty) leaves are dropped.
Collect the leaves of a t-regex der (an ITE-tree whose leaves are
regex expressions) into the output vector. Empty (re.empty) leaves
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
variable creeping in) — in that case the caller should bail out.
@ -102,9 +108,7 @@ namespace seq {
expr* e = work.back();
work.pop_back();
expr* c = nullptr, * t = nullptr, * f = nullptr;
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 (m.is_ite(e, c, t, f)) {
if (seen.insert_if_not_there(t))
work.push_back(t);
if (seen.insert_if_not_there(f))