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::derive): remove unsound depth limit in hoist_ite

Browse source 
The single-ITE branch of hoist_ite was gated by 'm_path_stack.size() < 8'.
When the depth limit was reached, hoist_ite returned nullptr and callers
fell back to non-path-aware structural rewrites (mk_union0 / mk_xor0).
These rewrites simplify e.g. mk_union(empty, X) -> X and return X unchanged,
preserving inner ITE branches that were built at an earlier (less constrained)
path. Subsequent derivative computation never path-prunes those branches,
which can leak unreachable epsilon-leaves into the final t-regex and cause
the bisimulation algorithm to report inequivalence for equivalent regexes.

Concrete trigger: derivatives of unions/xors with >= 9 components produce
9-deep ITE chains; at depth 8 the inner ITE returns unprocessed, leaving an
unreachable epsilon-leaf that bisim mis-interprets as a distinguishing word.

Removing the guard restores soundness. The corpus run against
regex-equivalence (1523 files) fixes 22 triangulated soundness bugs
(mut_0013, mut_0241, mut_0257, mut_0301 among others) with zero regressions.
89/89 unit tests pass.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Margus Veanes 2026-06-15 03:18:15 -07:00
parent 0b8bb98656
commit 3d2d793f1d
1 changed files with 13 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/ast/rewriter/seq_derive.cpp
View file

@ -1021,7 +1021,7 @@ namespace seq {
}
// Common ITE dispatch for binary ops (union/inter).
// Returns nullptr if neither a nor b is ITE (or depth limit reached).
// Returns nullptr if neither a nor b is ITE.
expr_ref derive::hoist_ite(expr* a, expr* b, std::function<expr_ref(expr*, expr*)> apply_op) {
expr *c1, *t1, *e1, *c2, *t2, *e2;
if (m.is_ite(a, c1, t1, e1) && m.is_ite(b, c2, t2, e2) && c1->get_id() > c2->get_id())
@ -1035,17 +1035,18 @@ namespace seq {
if (r) return r;
return expr_ref(re().mk_empty(a->get_sort()), m);
}
if (m_path_stack.size() < 8) {
if (m.is_ite(a, c1, t1, e1)) {
expr_ref r = apply_ite(c1, t1, e1, b, apply_op);
if (r) return r;
return expr_ref(re().mk_empty(a->get_sort()), m);
}
if (m.is_ite(b, c2, t2, e2)) {
expr_ref r = apply_ite(c2, t2, e2, a, apply_op);
if (r) return r;
return expr_ref(re().mk_empty(a->get_sort()), m);
}
// Single-ITE hoisting: must always recurse to maintain path-aware
// soundness — falling back to a non-path-aware structural rewrite
// here would bake unreachable branches into the result tree.
if (m.is_ite(a, c1, t1, e1)) {
expr_ref r = apply_ite(c1, t1, e1, b, apply_op);
if (r) return r;
return expr_ref(re().mk_empty(a->get_sort()), m);
}
if (m.is_ite(b, c2, t2, e2)) {
expr_ref r = apply_ite(c2, t2, e2, a, apply_op);
if (r) return r;
return expr_ref(re().mk_empty(a->get_sort()), m);
}
return expr_ref(nullptr, m);
}