From 2865e5f64dacd99dacf38b1d7260badeeaccfae9 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sat, 4 Jul 2026 01:04:41 +0300 Subject: [PATCH] seq_split: derivative-based split for intersection (r = E(r) | RE(LF(delta(r)))) Extend the complement redesign to intersection. Instead of the eager cross- product Split(r1 & ... & rn) = Split(r1) cap ... cap Split(rn) -- which materialises and multiplies the operand split-sets -- peel one character through the symbolic derivative and recurse. delta distributes over &, so LF(delta(r1&r2)) has one cofactor per combined minterm with target (delta_a r1 & delta_a r2): Split(r1&...&rn) = E(.) | union_i alpha_i . (derivative continuations) Falls back to the eager cross-product only on a cyclic memo revisit. Factor the shared unfolding out of the complement case into try_derivative_split, now used by both the complement and intersection branches of expand_fromre. Like the star-free complement path, this expansion is lazy (one char peel, no operand materialisation), so it also runs in weak mode; only the eager De Morgan node ~(R*) still needs strong mode. Update the two seq_split unit tests that encoded the old "weak mode refuses intersection" contract. Validated: gen (131) + gen-lb (119) cross-check -> 0 default disagreements and no new nseq spurious results (only the pre-existing t01-border-cssfunc); L13-inter, L15-negcount and L16-nest all solved with no cross-product blow-up. test-z3 seq_split and regex_range_collapse pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_split.cpp | 55 +++++++++++++++++++++++----------- src/ast/rewriter/seq_split.h | 6 ++++ src/test/seq_split.cpp | 38 ++++++++++++++--------- 3 files changed, 67 insertions(+), 32 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index f264237506..43fe9208e8 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -329,6 +329,33 @@ expr_ref seq_split::mk_charclass_re(expr* pred, sort* seq_sort) { return expr_ref(re().mk_of_pred(lam), m); } +// r == E(r) | RE(LF(delta(r))): peel one character through the symbolic derivative +// (Brzozowski cofactors) and recurse. Shared by the complement and intersection +// cases to avoid the De Morgan / cross-product blow-up. delta distributes over +// both ~ and &, so LF(delta(r)) = { (alpha_i, tgt_i) } with tgt_i the (complement / +// intersection of) character-derivatives. Records `r` in `deriv_memo` as a cycle +// guard. Returns a null expr_ref when nullability of `r` is not statically +// decidable (the caller then falls back to its structural rule). +expr_ref seq_split::try_derivative_split(expr* r, sort* seq_sort, obj_hashtable& deriv_memo) { + seq_util::rex& rex = re(); + expr_ref nb = m_rw.is_nullable(r); + if (!m.is_true(nb) && !m.is_false(nb)) + return expr_ref(m); // undecidable -> fall back + deriv_memo.insert(r); + sort* re_sort = rex.mk_re(seq_sort); + expr_ref unfolded(m); + if (m.is_true(nb)) unfolded = rex.mk_epsilon(seq_sort); // E(r) = eps + else unfolded = rex.mk_empty(re_sort); // E(r) = bot + expr_ref_pair_vector cofs(m); + m_rw.brz_derivative_cofactors(r, cofs); // { (alpha_i, tgt_i) } = LF(delta(r)) + for (auto const& [cond, tgt] : cofs) { + expr_ref alpha = mk_charclass_re(cond, seq_sort); // single-char regex + expr_ref term(rex.mk_concat(alpha, tgt), m); // alpha_i . tgt_i + unfolded = expr_ref(rex.mk_union(unfolded, term), m); + } + return mk_fromre(unfolded); +} + expr_ref seq_split::expand_fromre(expr* r, bool& ok, obj_hashtable& deriv_memo) { ok = true; ++m_stats.m_sigma_expand; @@ -462,8 +489,14 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok, obj_hashtable& deriv_ return mk_lcat(star, mk_rcat(mk_fromre(a), star)); } - // intersection: sigma(r0 & ... & r_{n-1}) = cap from_re(ri) (re.inter may be n-ary) + // intersection: prefer the derivative rule r = E(r) | RE(LF(delta(r))) (delta + // distributes over &) to avoid the Split(r0) cap ... cap Split(r_{n-1}) cross- + // product blow-up; fall back to the eager cross-product on a cyclic revisit. if (rex.is_intersection(r)) { + if (!deriv_memo.contains(r)) { + expr_ref d = try_derivative_split(r, seq_sort, deriv_memo); + if (d.get()) return d; + } app* ap = to_app(r); const unsigned n = ap->get_num_args(); expr_ref acc = mk_fromre(ap->get_arg(0)); @@ -473,28 +506,14 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok, obj_hashtable& deriv_ return acc; } - // complement: sigma(~a) = ~sigma(a). // complement: sigma(~a). Prefer the symbolic-derivative rule to avoid the De // Morgan 2^k blow-up: r = E(~a) | RE(LF(delta(~a))), peel one character and // recurse. Fall back to the De Morgan rule sigma(~a)=~sigma(a) at a // complemented star ~(R*) or on a cyclic revisit (both keep it terminating). if (rex.is_complement(r, a)) { - expr_ref nb = m_rw.is_nullable(r); // nullable(~a) - if (!rex.is_star(a) && !rex.is_plus(a) && !deriv_memo.contains(r) - && (m.is_true(nb) || m.is_false(nb))) { - deriv_memo.insert(r); - sort* re_sort = rex.mk_re(seq_sort); - expr_ref unfolded(m); - if (m.is_true(nb)) unfolded = rex.mk_epsilon(seq_sort); // E(~a) = eps - else unfolded = rex.mk_empty(re_sort); // E(~a) = bot - expr_ref_pair_vector cofs(m); - m_rw.brz_derivative_cofactors(r, cofs); // {(alpha_i, tgt_i)} = LF(delta(~a)) - for (auto const& [cond, tgt] : cofs) { - expr_ref alpha = mk_charclass_re(cond, seq_sort); // single-char regex - expr_ref term(rex.mk_concat(alpha, tgt), m); // alpha_i . tgt_i - unfolded = expr_ref(rex.mk_union(unfolded, term), m); - } - return mk_fromre(unfolded); + if (!rex.is_star(a) && !rex.is_plus(a) && !deriv_memo.contains(r)) { + expr_ref d = try_derivative_split(r, seq_sort, deriv_memo); + if (d.get()) return d; } return mk_compl(mk_fromre(a)); // De Morgan fallback } diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index cb28fd5056..9ce50cd37f 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -142,6 +142,12 @@ class seq_split { // of_pred(lambda) only for predicates that are not a single (possibly negated) // range. expr_ref mk_charclass_re(expr* pred, sort* seq_sort); + // r == E(r) | RE(LF(delta(r))): build the suspended split-set for `r` by + // peeling one character through the symbolic derivative (Brzozowski cofactors) + // and recursing. Used for complement and intersection to avoid the De Morgan + // / cross-product blow-up. Records `r` in `deriv_memo` (cycle guard). Returns + // a null expr_ref when nullability of `r` is not statically decidable. + expr_ref try_derivative_split(expr* r, sort* seq_sort, obj_hashtable& deriv_memo); // Distribute a left/right concatenation over a head-normal split-set. expr_ref distribute_lcat(expr* r, expr* hs); expr_ref distribute_rcat(expr* hs, expr* r); diff --git a/src/test/seq_split.cpp b/src/test/seq_split.cpp index 29df0545c7..79ffd11f61 100644 --- a/src/test/seq_split.cpp +++ b/src/test/seq_split.cpp @@ -181,23 +181,30 @@ public: } void test_weak_vs_strong() { - expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m); + // ~(.*) is the complemented-star (~(R*)) case: it has no terminating + // derivative peel, so it falls back to the eager De Morgan node ~sigma(a), + // which weak mode refuses (producing even one split would materialize the + // operand split-set). Strong mode performs the eager De Morgan complement. expr_ref compl_(re().mk_complement(re().mk_star(dot())), m); + // An intersection is expanded lazily through the symbolic derivative + // r = E(r) | RE(LF(delta(r))) (delta distributes over &): one character + // peel, no operand materialization, so weak mode now handles it too. + expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m); split_set s; - ENSURE(!eager(inter, s, UINT_MAX, split_mode::weak)); - s.reset(); - ENSURE(!lazy(inter, s, UINT_MAX, split_mode::weak)); - s.reset(); - ENSURE(!eager(compl_, s, UINT_MAX, split_mode::weak)); + ENSURE(!eager(compl_, s, UINT_MAX, split_mode::weak)); // De Morgan node: weak refuses s.reset(); ENSURE(!lazy(compl_, s, UINT_MAX, split_mode::weak)); + s.reset(); + ENSURE(eager(compl_, s, UINT_MAX, split_mode::strong)); // strong: eager De Morgan - // strong mode succeeds for both + // intersection is derivative-expanded (lazy): succeeds in BOTH modes + s.reset(); + ENSURE(eager(inter, s, UINT_MAX, split_mode::weak)); + s.reset(); + ENSURE(lazy(inter, s, UINT_MAX, split_mode::weak)); s.reset(); ENSURE(eager(inter, s, UINT_MAX, split_mode::strong)); - s.reset(); - ENSURE(eager(compl_, s, UINT_MAX, split_mode::strong)); } void test_make_non_regex() { @@ -376,11 +383,14 @@ public: ENSURE(it.gave_up()); // aborted, not a clean exhaustion ENSURE(seen <= 1); // produced at most the capped number - // A weak-mode Boolean closure is likewise a give-up. - expr_ref inter(re().mk_inter(re().mk_star(rng('a', 'a')), re().mk_star(rng('b', 'b'))), m); - expr_ref inode = m_split.make(inter); - ENSURE(inode); - seq_split::iterator wit = m_split.iterate(inode, split_mode::weak, UINT_MAX, {}); + // A weak-mode eager Boolean closure is likewise a give-up: ~(.*) is the + // complemented-star case with no terminating derivative peel, so it needs + // the eager De Morgan node, which weak mode refuses. (An intersection, by + // contrast, is now derivative-expanded and succeeds in weak mode.) + expr_ref cstar(re().mk_complement(re().mk_star(dot())), m); + expr_ref cnode = m_split.make(cstar); + ENSURE(cnode); + seq_split::iterator wit = m_split.iterate(cnode, split_mode::weak, UINT_MAX, {}); ENSURE(!wit.next(d, n)); ENSURE(wit.gave_up()); }