From 10cab8b70d39810eb5b034180d7d6ae257a51136 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sat, 4 Jul 2026 10:30:00 +0300 Subject: [PATCH] seq_split: De Morgan fallback for complement of R*.S (termination fix) The derivative-based complement split peels one character through ~a and recurses. For a body a = R*.S that starts with an unbounded loop, delta_c(R*.S) = delta_c(R).R*.S | [eps in R*] delta_c(S) regenerates R*.S (the R* self-loops), so the peel never collapses to a bare ~(R*) (where the star guard fires) and never terminates: the derivative-state terms grow (accumulating delta(R) prefixes and De-Morgan intersections), so the memo cannot catch the cycle either. This diverged on nested complements over stars, e.g. ~( a* . ~( b* . ~((ab)*) ) ) (levels/L3-03): 27k DFS nodes / 44k intersect-pairs / 5.4 GB -> timeout, where the De Morgan route solves in ~6s (base: 5 nodes). Fix: broaden the complement De Morgan fallback from "body IS a bare star/plus" to "body STARTS WITH an unbounded star/plus" (complement_body_diverges: leftmost concat factor is is_star/is_plus). Bounded loops (re.loop m m) still terminate under the derivative and stay on the fast path, so the L15 negcount complement wins are preserved. Validated on resplit/paper/bench (325): the only status changes vs the prior build are L3-02 (unknown->unsat) and L3-03 (timeout->sat); no other benchmark changes; no new soundness contradictions (the 2 pre-existing length-coupling spurious unsats remain). L15 negcount stays fast (0.07-1.16s). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_split.cpp | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 43fe9208e8..87081cb376 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -356,6 +356,19 @@ expr_ref seq_split::try_derivative_split(expr* r, sort* seq_sort, obj_hashtable< return mk_fromre(unfolded); } +// The complemented body `a` "starts with an unbounded loop" (R*.S / R+.S) when its +// leftmost concat factor is a star or plus. delta(~(R*.S)) regenerates R*.S (the +// R* self-loops) and never collapses to a bare ~(R*), so the forward derivative +// peel of such a complement does NOT terminate. Route these through the De Morgan +// rule instead (which sends R* to the star rule / Nielsen star-introduction). +// Bounded loops (re.loop m m, e.g. the L15 counted-membership benchmarks) DO +// terminate under the derivative and are intentionally NOT matched here. +static bool complement_body_diverges(seq_util::rex& rex, expr* a) { + while (rex.is_concat(a) && to_app(a)->get_num_args() > 0) + a = to_app(a)->get_arg(0); // descend to the leftmost factor + return rex.is_star(a) || rex.is_plus(a); +} + expr_ref seq_split::expand_fromre(expr* r, bool& ok, obj_hashtable& deriv_memo) { ok = true; ++m_stats.m_sigma_expand; @@ -508,10 +521,12 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok, obj_hashtable& deriv_ // 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). + // recurse. Fall back to the De Morgan rule sigma(~a)=~sigma(a) when the body + // starts with an unbounded loop R*.S / R+.S (the derivative regenerates R*.S + // and diverges -- a termination flaw of the peel, see complement_body_diverges) + // or on a cyclic revisit (both keep it terminating). if (rex.is_complement(r, a)) { - if (!rex.is_star(a) && !rex.is_plus(a) && !deriv_memo.contains(r)) { + if (!complement_body_diverges(rex, a) && !deriv_memo.contains(r)) { expr_ref d = try_derivative_split(r, seq_sort, deriv_memo); if (d.get()) return d; }