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: De Morgan fallback for complement of R*.S (termination fix)

Browse source 
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>
This commit is contained in:
Margus Veanes 2026-07-04 10:30:00 +03:00
parent c0fbca4f41
commit 10cab8b70d
1 changed files with 18 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

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