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

fix seq::derive::intersect_intervals dropping kept intervals on disjoint case

Browse source 
The intersect_intervals routine in seq_derive.cpp maintains a path-tracking
disjoint union of character intervals.  When intersecting the active suffix
with a new constraint [lo, hi], it iterated the suffix and, on encountering
the first interval disjoint from [lo, hi], reset the output cursor to the
end-marker and broke out of the loop.  This both threw away the intervals it
had already kept and skipped every remaining interval, so e.g.
[(0, 96), (98, max)] intersected with [98, 98] became empty instead of
[(98, 98)].

Inside derive that silently killed valid branches of symbolic derivatives.
For example D(a|b) collapsed to ite(c='a', eps, empty) -- the 'b' branch
vanished -- which made the bisimulation procedure conclude bogus equalities
such as a* == (a|b)*.  On the regex-equivalence corpus this single bug
accounted for ~510 false-unsat results vs master.

Fix: drop only the disjoint interval and continue scanning the rest of the
suffix.  Add a small assertion-based regression test that builds D(a|b),
checks both branches survive, and runs bisim on a* vs (a|b)*.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Margus Veanes 2026-06-15 01:38:55 -07:00
parent cf0e43ab38
commit fb6470a1a1
4 changed files with 81 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1246,21 +1246,18 @@ namespace seq {
// Intersect the active suffix m_intervals[m_intervals_start..end] with [lo, hi]
void derive::intersect_intervals(unsigned lo, unsigned hi) {
// Copy active suffix to end, update start, then filter
unsigned old_start = m_intervals_start;
unsigned old_sz = m_intervals.size();
for (unsigned i = old_start; i < old_sz; ++i)
for (unsigned i = m_intervals_start; i < old_sz; ++i)
m_intervals.push_back(m_intervals[i]);
m_intervals_start = old_sz;
// Filter in-place within new suffix
// Filter in-place within new suffix: drop intervals disjoint from [lo,hi],
// keep the intersection for overlapping ones.
unsigned j = m_intervals_start;
for (unsigned i = m_intervals_start; i < m_intervals.size(); ++i) {
auto [lo1, hi1] = m_intervals[i];
if (hi < lo1 || lo > hi1) {
j = old_sz;
break;
}
if (hi1 >= lo)
m_intervals[j++] = {std::max(lo1, lo), std::min(hi1, hi)};
if (hi < lo1 || lo > hi1)
continue; // disjoint with this interval — drop it
m_intervals[j++] = {std::max(lo1, lo), std::min(hi1, hi)};
}
m_intervals.shrink(j);
}