From 10d8b8e1566cc7ce1854a2b85ceee98ae7659bac Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 26 Jun 2026 09:29:06 +0300 Subject: [PATCH] Push complement through union/intersection in symbolic derivative The derivative's mk_complement_core left complement over a union/intersection unfolded (e.g. d(comp(S*a)) = comp(S*a U eps)). Across successive derivatives the complemented argument grew (comp(S*a U eps U ...)), giving every loop / intersection state a fresh AST identity and defeating the state-graph dead-state detection, so str.in_re emptiness on loop-intersect-comp regexes timed out. Apply De Morgan in mk_complement_core so complement is pushed to the leaves: ~(A U B) -> ~A & ~B (keeps ~A invariant; ~(S*a U eps) -> ~(S*a) & .+) ~(A & B) -> ~A U ~B (exposes unions so antimirov non-emptiness can decide each alternative separately) This matches the form master's inline mk_derivative produces. z3test 5728 now solves in 0.13s (was timeout) and parts of 5731/5721 are resolved. Full unit suite: 92 passed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_derive.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 8b89c97546..f662ed4179 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -894,6 +894,20 @@ namespace seq { return expr_ref(re().mk_plus(re().mk_full_char(a->get_sort())), m); } + // De Morgan: push complement through union/intersection to the leaves + // so that complemented subterms stay invariant across successive + // derivatives and unions are exposed at the top. This keeps the + // symbolic derivative in transition-regex normal form and lets the + // antimirov non-emptiness check decide each union alternative + // separately. In particular ~(Σ*a ∪ ε) → ~(Σ*a) ∩ .+, so the ~(Σ*a) + // state is shared rather than growing into ~(Σ*a ∪ ε ∪ ...), which + // otherwise defeats dead-state detection on loop ∩ comp regexes. + expr* e1 = nullptr, *e2 = nullptr; + if (re().is_union(a, e1, e2)) + return mk_inter(mk_complement(e1), mk_complement(e2)); + if (re().is_intersection(a, e1, e2)) + return mk_union(mk_complement(e1), mk_complement(e2)); + return expr_ref(re().mk_complement(a), m); }