mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

seq_split: derivative-based split for intersection (r = E(r) | RE(LF(delta(r))))

Browse source 
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>
This commit is contained in:
Margus Veanes 2026-07-04 01:04:41 +03:00
parent 07451d8922
commit 2865e5f64d
3 changed files with 67 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

55
src/ast/rewriter/seq_split.cpp
View file

@ -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<expr>& 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<expr>& 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<expr>& 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<expr>& 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
}

6
src/ast/rewriter/seq_split.h
View file

@ -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<expr>& 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);

38
src/test/seq_split.cpp
View file

@ -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());
}