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