From 8992d5fc53677593f9747e68ab4a42fb6e4d3eb1 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 3 Jul 2026 16:05:31 +0300 Subject: [PATCH 1/7] seq_split: add behaviour-neutral perf counters, surfaced via nseq -st Adds a split_stats struct to seq_split (make/sigma-expand/materialize/splits/pushes/oracle-prunes/intersect/intersect-pairs/complement/giveups/threshold-overruns/max-split-set/simplify) and reports them in nielsen_graph::collect_statistics as 'nseq split *'. Read-only counters; solver behaviour is unchanged (verified: L11 sat, L14 unsat, gen cssfunc sat). Diagnosis on gen-lb L15 negcount: the De Morgan complement -> intersect cross-product blows up to 2^16 split-set pairs (1.3M intersect-pairs) while simplify() and the oracle never fire on that path. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_rewriter.h | 4 ++++ src/ast/rewriter/seq_split.cpp | 28 +++++++++++++++++++++++++--- src/ast/rewriter/seq_split.h | 24 ++++++++++++++++++++++++ src/smt/seq/seq_nielsen.cpp | 16 ++++++++++++++++ 4 files changed, 69 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index d295c201e0..205f9826fd 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -439,6 +439,10 @@ public: return m_split.split_membership(str, regex, threshold, result); } + // split-algebra performance counters (surfaced via nseq -st) + split_stats const& get_split_stats() const { return m_split.stats(); } + void reset_split_stats() { m_split.reset_stats(); } + expr_ref mk_symmetric_diff(expr *r1, expr *r2); /** diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index c7f997c65f..43f61f26a8 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -177,8 +177,11 @@ seq_util::rex& seq_split::re() const { return m_rw.u().re; } // Add unless the (optional) lookahead oracle prunes it. void seq_split::push(split_set& out, split_oracle const& oracle, expr* d, expr* n) const { + ++m_stats.m_pushes; if (!oracle || oracle(d, n)) out.push_back(split_pair(d, n, m)); + else + ++m_stats.m_oracle_prunes; } // Cross-product intersection of two split-sets (split algebra): @@ -186,6 +189,7 @@ void seq_split::push(split_set& out, split_oracle const& oracle, expr* d, expr* // Pairs where any component is bottom (the empty regex) are dropped. bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& result, unsigned threshold, split_oracle const& oracle) const { + ++m_stats.m_intersect; const seq_util::rex& r = re(); for (auto const& p1 : s1) { for (auto const& p2 : s2) { @@ -194,9 +198,12 @@ bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& r continue; const expr_ref di(m_rw.mk_regex_inter_normalize(p1.m_d, p2.m_d), m); const expr_ref ni(m_rw.mk_regex_inter_normalize(p1.m_n, p2.m_n), m); + ++m_stats.m_intersect_pairs; push(result, oracle, di, ni); - if (result.size() > threshold) + if (result.size() > threshold) { + ++m_stats.m_threshold_overruns; return false; + } } } return true; @@ -210,6 +217,7 @@ bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& r bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& result, const unsigned threshold, split_oracle const& oracle) const { + ++m_stats.m_complement; seq_util::rex& r = re(); sort* re_sort = r.mk_re(seq_sort); const expr_ref full(r.mk_full_seq(re_sort), m); // .* @@ -233,8 +241,10 @@ bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& resul acc = std::move(tmp); if (acc.empty()) // intersection empty => ~S is empty break; - if (acc.size() > threshold) + if (acc.size() > threshold) { + ++m_stats.m_threshold_overruns; return false; + } } result.append(acc); return true; @@ -246,6 +256,7 @@ bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& resul // decided when `head_normalize` reaches an inter / compl node. expr_ref seq_split::expand_fromre(expr* r, bool& ok) { ok = true; + ++m_stats.m_sigma_expand; seq_util& sq = seq(); seq_util::rex& rex = re(); @@ -538,15 +549,19 @@ expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold, bool seq_split::materialize(expr* node, split_mode mode, unsigned threshold, split_oracle const& oracle, split_set& out) { + ++m_stats.m_materialize; iterator it(*this, node, mode, threshold, oracle); expr_ref d(m), n(m); while (it.next(d, n)) out.push_back(split_pair(d, n, m)); + if (out.size() > m_stats.m_max_split_set) + m_stats.m_max_split_set = out.size(); return !it.gave_up(); } expr_ref seq_split::make(expr* r) { SASSERT(r); + ++m_stats.m_make; sort* seq_sort = nullptr; if (!seq().is_re(r, seq_sort)) return expr_ref(m); @@ -578,6 +593,7 @@ bool seq_split::iterator::next(expr_ref& out_d, expr_ref& out_n) { expr_ref hn = m_engine.head_normalize(t, m_mode, m_threshold, m_oracle, ok); if (!ok) { m_giveup = true; // unsupported / weak Boolean / overrun + ++m_engine.m_stats.m_giveups; return false; } @@ -585,14 +601,19 @@ bool seq_split::iterator::next(expr_ref& out_d, expr_ref& out_n) { if (m_engine.is_empty_ss(hn)) continue; if (m_engine.is_single(hn, d, n)) { - if (m_oracle && !m_oracle(d, n)) + if (m_oracle && !m_oracle(d, n)) { + ++m_engine.m_stats.m_oracle_prunes; continue; // pruned by lookahead + } if (++m_count > m_threshold) { m_giveup = true; // safety cap against space bloat + ++m_engine.m_stats.m_giveups; + ++m_engine.m_stats.m_threshold_overruns; return false; } out_d = d; out_n = n; + ++m_engine.m_stats.m_splits; return true; } if (m_engine.is_union(hn, a, b)) { @@ -651,6 +672,7 @@ void seq_split::merge_by(split_set& pairs, const bool by_left) const { } void seq_split::simplify(split_set& pairs) const { + ++m_stats.m_simplify; seq_util::rex& r = re(); // 1. drop pairs with a bottom (empty-language) component. diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index f3b7a57675..86953a250f 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -57,6 +57,25 @@ enum class split_mode { weak, strong }; // default) keeps everything, so sigma is unchanged. See seq_split::compute. typedef std::function split_oracle; +// Lightweight performance counters for the split algebra (surfaced via -st in +// the nseq solver; behaviour-neutral). See seq_split.cpp for where each fires. +struct split_stats { + unsigned m_make = 0; // make(): suspended sigma(r) built + unsigned m_sigma_expand = 0; // expand_fromre(): one sigma rule level + unsigned m_materialize = 0; // materialize(): a split-set drained + unsigned m_splits = 0; // splits produced by iterator::next() + unsigned m_pushes = 0; // candidate offered to push() + unsigned m_oracle_prunes = 0; // candidates dropped by the lookahead oracle + unsigned m_intersect = 0; // intersect() calls + unsigned m_intersect_pairs = 0; // pairs formed by intersect() cross-products + unsigned m_complement = 0; // complement() calls + unsigned m_giveups = 0; // iterator give-ups (unsupported/weak/overrun) + unsigned m_threshold_overruns = 0; // threshold hits (intersect/complement/iterator) + unsigned m_max_split_set = 0; // largest materialized split-set seen + unsigned m_simplify = 0; // simplify() calls + void reset() { *this = split_stats(); } +}; + class seq_split { ast_manager& m; seq_rewriter& m_rw; // for mk_re_append + manager / seq_util access @@ -81,6 +100,7 @@ class seq_split { func_decl_ref m_d_empty, m_d_single, m_d_fromre, m_d_union, m_d_inter, m_d_compl, m_d_lcat, m_d_rcat; expr_ref m_empty_app; // cached nullary `empty` term + mutable split_stats m_stats; // performance counters (see -st) seq_util& seq() const; seq_util::rex& re() const; @@ -151,6 +171,10 @@ class seq_split { public: explicit seq_split(seq_rewriter& rw); + // Performance counters (read via nseq -st). + split_stats const& stats() const { return m_stats; } + void reset_stats() { m_stats.reset(); } + // Lazy split enumerator. Holds the suspended split-set worklist and produces // the concrete splits one at a time, on demand, instead of computing // them all up front. Obtain one from seq_split::iterate (or construct it diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index b96e4990e3..e36a01326f 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -6004,6 +6004,22 @@ namespace seq { st.update("nseq unsat-cache hits", m_num_cache_hits); st.update("nseq sibling cuts", m_stats.m_num_sibling_cut); st.update("nseq sibling closures", m_stats.m_num_sibling_closure); + + // split-algebra (sigma) counters, from the shared seq_split engine. + split_stats const& sp = m_split_rw.get_split_stats(); + st.update("nseq split make", sp.m_make); + st.update("nseq split sigma-expand", sp.m_sigma_expand); + st.update("nseq split materialize", sp.m_materialize); + st.update("nseq split splits", sp.m_splits); + st.update("nseq split pushes", sp.m_pushes); + st.update("nseq split oracle-prunes", sp.m_oracle_prunes); + st.update("nseq split intersect", sp.m_intersect); + st.update("nseq split intersect-pairs", sp.m_intersect_pairs); + st.update("nseq split complement", sp.m_complement); + st.update("nseq split giveups", sp.m_giveups); + st.update("nseq split threshold-overruns", sp.m_threshold_overruns); + st.update("nseq split max-split-set", sp.m_max_split_set); + st.update("nseq split simplify", sp.m_simplify); } } From 07c797c32be68ce678e71cc0f6a8ebdfd9d1b829 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 3 Jul 2026 19:40:26 +0300 Subject: [PATCH 2/7] seq_split: dedup identical pairs in intersect (sound, memory-only) A split-set denotes the UNION of its pairs, so identical (hash-consed) pairs are redundant; skipping them in the De Morgan cross-product cuts the materialized split-set ~7x on L15 negcount (65536 -> 9216) with no behaviour change (verified L11 sat / L14 unsat). NOTE: memory-only -- it does not fix the underlying combinatorial blow-up of complement()'s structural De Morgan on a concatenation of predicates (root cause; see spec analysis). Adds nseq-split-dedup-drops counter. Easily reverted if a derivative/minterm-based complement supersedes the cross-product. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_split.cpp | 11 +++++++++++ src/ast/rewriter/seq_split.h | 1 + src/smt/seq/seq_nielsen.cpp | 1 + 3 files changed, 13 insertions(+) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 43f61f26a8..c2984e905b 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -20,6 +20,7 @@ Author: #include "ast/rewriter/seq_rewriter.h" #include "ast/ast_pp.h" #include "util/obj_hashtable.h" +#include "util/obj_pair_hashtable.h" #include "util/stack.h" seq_split::seq_split(seq_rewriter& rw) : @@ -191,6 +192,10 @@ bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& r unsigned threshold, split_oracle const& oracle) const { ++m_stats.m_intersect; const seq_util::rex& r = re(); + // Dedup the cross-product: a split-set denotes the UNION of its pairs, + // so identical (perfectly-shared) pairs are redundant. Skipping them keeps + // the De Morgan fold from accumulating exponentially many equal splits. + obj_pair_hashtable seen; for (auto const& p1 : s1) { for (auto const& p2 : s2) { if (r.is_empty(p1.m_d) || r.is_empty(p2.m_d) || @@ -199,6 +204,12 @@ bool seq_split::intersect(split_set const& s1, split_set const& s2, split_set& r const expr_ref di(m_rw.mk_regex_inter_normalize(p1.m_d, p2.m_d), m); const expr_ref ni(m_rw.mk_regex_inter_normalize(p1.m_n, p2.m_n), m); ++m_stats.m_intersect_pairs; + std::pair key(di.get(), ni.get()); + if (seen.contains(key)) { + ++m_stats.m_dedup_drops; + continue; + } + seen.insert(key); push(result, oracle, di, ni); if (result.size() > threshold) { ++m_stats.m_threshold_overruns; diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 86953a250f..046bde3c15 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -72,6 +72,7 @@ struct split_stats { unsigned m_giveups = 0; // iterator give-ups (unsupported/weak/overrun) unsigned m_threshold_overruns = 0; // threshold hits (intersect/complement/iterator) unsigned m_max_split_set = 0; // largest materialized split-set seen + unsigned m_dedup_drops = 0; // duplicate pairs skipped in intersect unsigned m_simplify = 0; // simplify() calls void reset() { *this = split_stats(); } }; diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index e36a01326f..55c14f280a 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -6019,6 +6019,7 @@ namespace seq { st.update("nseq split giveups", sp.m_giveups); st.update("nseq split threshold-overruns", sp.m_threshold_overruns); st.update("nseq split max-split-set", sp.m_max_split_set); + st.update("nseq split dedup-drops", sp.m_dedup_drops); st.update("nseq split simplify", sp.m_simplify); } From 22eb098cd9c8aebbc21f90fd1a2829ee865ec763 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 3 Jul 2026 22:33:29 +0300 Subject: [PATCH 3/7] WIP seq_split: derivative-based complement split (NOT for merge - soundness bug) Prototype of the notes.md redesign: Split(~a) for star-free a via r = E(~a) | RE(LF(delta(~a))) using brz_derivative_cofactors, of_pred(lambda) char-classes, per-iterator memo (threaded through head_normalize) + De Morgan fallback at ~(R*)/cyclic revisit. RESULT: De Morgan split blow-up ELIMINATED (L15: complement/max-split-set 65536 -> 0), validating the core idea. BUT: (1) SOUNDNESS BUG - concat membership over a derivative-split complement returns spurious unsat ((x.y) in ~([0-9]^2): default sat, nseq unsat; single-var x in ~([0-9]^2) is correct). Split-set not collapsed (49 splits) so of_pred not empty-dropped; fault is downstream handling of of_pred(lambda) char-classes in the concat split/primitive path. (2) bottleneck moved to DFS nodes (7 -> 33071). FIX DIRECTION: represent the cofactor char-class as range/union-of-ranges nseq fully supports, not of_pred(lambda). Do not build on this until fixed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_split.cpp | 50 ++++++++++++++++++++++++++++------ src/ast/rewriter/seq_split.h | 13 +++++++-- 2 files changed, 52 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index c2984e905b..11b4cf657a 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -265,7 +265,16 @@ bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& resul // emits *suspended* split-algebra terms (from_re / lcat / rcat / inter / compl) for // the subterms instead of recursing. `mode` is irrelevant here: weak vs. strong is // decided when `head_normalize` reaches an inter / compl node. -expr_ref seq_split::expand_fromre(expr* r, bool& ok) { +// Single-character regex for a cofactor path condition `pred` (a Boolean over the +// character (:var 0)): of_pred(lambda (c) . pred). +expr_ref seq_split::mk_charclass_re(expr* pred) { + sort* cs = seq().mk_char_sort(); + symbol nm("c"); + expr_ref lam(m.mk_lambda(1, &cs, &nm, pred), m); + return expr_ref(re().mk_of_pred(lam), m); +} + +expr_ref seq_split::expand_fromre(expr* r, bool& ok, obj_hashtable& deriv_memo) { ok = true; ++m_stats.m_sigma_expand; seq_util& sq = seq(); @@ -410,8 +419,30 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok) { } // complement: sigma(~a) = ~sigma(a). - if (rex.is_complement(r, a)) - return mk_compl(mk_fromre(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); // 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); + } + return mk_compl(mk_fromre(a)); // De Morgan fallback + } // abbreviation // difference: a \ b = a & ~b ; sigma(a \ b) = sigma(a) cap ~sigma(b). @@ -487,7 +518,8 @@ expr_ref seq_split::from_split_set(split_set const& s) { } expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold, - split_oracle const& oracle, bool& ok) { + split_oracle const& oracle, bool& ok, + obj_hashtable& deriv_memo) { ok = true; expr *a = nullptr, *b = nullptr, *r = nullptr, *s = nullptr; @@ -498,23 +530,23 @@ expr_ref seq_split::head_normalize(expr* t, split_mode mode, unsigned threshold, // from_re(r): one level of sigma; recurse to settle a non-frontier head // (plus / inter / compl / diff expand to lcat / inter / compl nodes). if (is_fromre(t, r)) { - expr_ref e = expand_fromre(r, ok); + expr_ref e = expand_fromre(r, ok, deriv_memo); if (!ok) return expr_ref(m); if (is_frontier(e)) return e; - return head_normalize(e, mode, threshold, oracle, ok); + return head_normalize(e, mode, threshold, oracle, ok, deriv_memo); } // r.S : head-normalize S, then distribute r over the frontier. if (is_lcat(t, r, s)) { - expr_ref hs = head_normalize(s, mode, threshold, oracle, ok); + expr_ref hs = head_normalize(s, mode, threshold, oracle, ok, deriv_memo); if (!ok) return expr_ref(m); return distribute_lcat(r, hs); } if (is_rcat(t, s, r)) { - expr_ref hs = head_normalize(s, mode, threshold, oracle, ok); + expr_ref hs = head_normalize(s, mode, threshold, oracle, ok, deriv_memo); if (!ok) return expr_ref(m); return distribute_rcat(hs, r); @@ -601,7 +633,7 @@ bool seq_split::iterator::next(expr_ref& out_d, expr_ref& out_n) { m_work.pop_back(); bool ok = true; - expr_ref hn = m_engine.head_normalize(t, m_mode, m_threshold, m_oracle, ok); + expr_ref hn = m_engine.head_normalize(t, m_mode, m_threshold, m_oracle, ok, m_deriv_memo); if (!ok) { m_giveup = true; // unsupported / weak Boolean / overrun ++m_engine.m_stats.m_giveups; diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 046bde3c15..27b447b726 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -27,6 +27,7 @@ Author: #include "ast/seq_decl_plugin.h" #include "ast/rewriter/seq_subset.h" +#include "util/obj_hashtable.h" #include class seq_rewriter; @@ -134,7 +135,10 @@ class seq_split { // One level of the sigma rules: from_re(r) -> a SplitSet term built from the // immediate subterms. `ok` is set false on an unsupported shape. - expr_ref expand_fromre(expr* r, bool& ok); + expr_ref expand_fromre(expr* r, bool& ok, obj_hashtable& deriv_memo); + // Build the single-character regex of_pred(lambda c. pred) from a cofactor + // path condition `pred` (a Boolean over the character (:var 0)). + expr_ref mk_charclass_re(expr* pred); // 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); @@ -146,7 +150,8 @@ class seq_split { // `ok` is set false on a give-up (unsupported shape, weak-mode Boolean, or // threshold overrun). expr_ref head_normalize(expr* t, split_mode mode, unsigned threshold, - split_oracle const& oracle, bool& ok); + split_oracle const& oracle, bool& ok, + obj_hashtable& deriv_memo); // Fully drain a suspended split-set into `out` (used for inter/compl bodies). // Runs an `iterator` to exhaustion; returns false on a give-up. bool materialize(expr* node, split_mode mode, unsigned threshold, @@ -204,6 +209,10 @@ public: expr_ref_vector m_work; // GC-safe worklist of suspended split-sets unsigned m_count = 0; // splits produced so far (vs. threshold) bool m_giveup = false; + // Complement ~-regex states already expanded via the symbolic-derivative + // rule; re-encountering one (a cycle) falls back to the De Morgan rule so + // the lazy unfolding terminates. Per-iterator (iterators run concurrently). + obj_hashtable m_deriv_memo; public: iterator(seq_split& engine, expr* node, split_mode mode, unsigned threshold, split_oracle oracle); From 07451d89225b42321f446f727cc6e27cf292abf8 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 3 Jul 2026 23:44:09 +0300 Subject: [PATCH 4/7] seq_split: fix derivative-complement soundness+perf via canonical range_predicate Resolves the WIP soundness bug. Root cause: the char-classes emitted for cofactor conditions were non-canonical and unrecognized downstream (of_pred(lambda) -> opaque select(lambda,ele); raw range unions carried (and true RANGE) that is_char_const_range rejected). Fix: mk_charclass_re maps the cofactor condition (true/false/and/or/not/=/char.<=) to the canonical seq::range_predicate via its Boolean ops, then range_predicate_to_regex (seq_range_collapse.h) yields a canonical char-class regex the derivative/emptiness/primitive path handles natively. Also: derive_of_pred beta-reduces select(lambda,ele) (general of_pred soundness fix). RESULT on gen-lb (119): 0 default disagreements, 0 nseq spurious-unsat. L15 negcount family (27) timeout->solved: e.g. l15-digit-m3-dash now sat in 0.02s (dfs-nodes 33071->55, split complement/max-split-set eliminated). No regression (L11 sat, L14 unsat). Validates the notes.md derivative-based split redesign for star-free complements. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/rewriter/seq_derive.cpp | 20 ++++++++--- src/ast/rewriter/seq_split.cpp | 63 ++++++++++++++++++++++++++++++--- src/ast/rewriter/seq_split.h | 9 +++-- 3 files changed, 81 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index bd39e042a3..2b0a5b56fa 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -427,10 +427,22 @@ namespace seq { expr_ref empty(re().mk_empty(re_sort), m); expr_ref eps(re().mk_to_re(u().str.mk_empty(seq_sort)), m); - // Apply predicate to the element - array_util autil(m); - expr* args[2] = { pred, m_ele }; - expr_ref cond(autil.mk_select(2, args), m); + // Apply the predicate to the current element. When `pred` is a lambda, + // beta-reduce select(lambda, ele) so the resulting character condition is + // in the range/eq form the derivative's condition analysis + // (is_char_const_range / eval_path_cond) understands; a raw + // (select (lambda ..) ele) would be opaque and mishandled downstream. + expr_ref cond(m); + if (is_lambda(pred)) { + var_subst subst(m); + expr* arg = m_ele; + cond = subst(to_quantifier(pred)->get_expr(), 1, &arg); + } + else { + array_util autil(m); + expr* args[2] = { pred, m_ele }; + cond = autil.mk_select(2, args); + } return mk_ite(cond, eps, empty); } diff --git a/src/ast/rewriter/seq_split.cpp b/src/ast/rewriter/seq_split.cpp index 11b4cf657a..f264237506 100644 --- a/src/ast/rewriter/seq_split.cpp +++ b/src/ast/rewriter/seq_split.cpp @@ -18,6 +18,7 @@ Author: #include "ast/rewriter/seq_split.h" #include "ast/rewriter/seq_rewriter.h" +#include "ast/rewriter/seq_range_collapse.h" #include "ast/ast_pp.h" #include "util/obj_hashtable.h" #include "util/obj_pair_hashtable.h" @@ -265,10 +266,64 @@ bool seq_split::complement(sort* seq_sort, split_set const& sp, split_set& resul // emits *suspended* split-algebra terms (from_re / lcat / rcat / inter / compl) for // the subterms instead of recursing. `mode` is irrelevant here: weak vs. strong is // decided when `head_normalize` reaches an inter / compl node. +namespace { + // Cofactor path condition `pred` (a Boolean over x = (:var 0)) -> the canonical + // range_predicate (union of ranges) of the characters satisfying it. Returns + // false on a construct outside {true,false,and,or,not,=,char.<=} over x. + static bool pred_to_rp(ast_manager& m, seq_util& sq, expr* x, expr* pred, + unsigned maxc, seq::range_predicate& out) { + expr* a = nullptr, * b = nullptr; unsigned c = 0; + if (m.is_true(pred)) { out = seq::range_predicate::top(maxc); return true; } + if (m.is_false(pred)) { out = seq::range_predicate::empty(maxc); return true; } + if (m.is_eq(pred, a, b)) { + if (a == x && sq.is_const_char(b, c)) { out = seq::range_predicate::singleton(c, maxc); return true; } + if (b == x && sq.is_const_char(a, c)) { out = seq::range_predicate::singleton(c, maxc); return true; } + return false; + } + if (sq.is_char_le(pred, a, b)) { + if (b == x && sq.is_const_char(a, c)) { out = seq::range_predicate::range(c, maxc, maxc); return true; } + if (a == x && sq.is_const_char(b, c)) { out = seq::range_predicate::range(0, c, maxc); return true; } + return false; + } + if (m.is_not(pred, a)) { + seq::range_predicate s(maxc); + if (!pred_to_rp(m, sq, x, a, maxc, s)) return false; + out = ~s; return true; + } + if (m.is_and(pred)) { + out = seq::range_predicate::top(maxc); + for (expr* arg : *to_app(pred)) { + seq::range_predicate s(maxc); + if (!pred_to_rp(m, sq, x, arg, maxc, s)) return false; + out = out & s; + } + return true; + } + if (m.is_or(pred)) { + out = seq::range_predicate::empty(maxc); + for (expr* arg : *to_app(pred)) { + seq::range_predicate s(maxc); + if (!pred_to_rp(m, sq, x, arg, maxc, s)) return false; + out = out | s; + } + return true; + } + return false; + } +} + // Single-character regex for a cofactor path condition `pred` (a Boolean over the -// character (:var 0)): of_pred(lambda (c) . pred). -expr_ref seq_split::mk_charclass_re(expr* pred) { - sort* cs = seq().mk_char_sort(); +// character (:var 0)). Materialized via the canonical seq::range_predicate as a +// union-of-ranges regex (fully supported by the derivative / emptiness / primitive +// path, and canonical so equivalent classes share AST identity). Falls back to +// of_pred(lambda) only for predicates outside the recognized range fragment. +expr_ref seq_split::mk_charclass_re(expr* pred, sort* seq_sort) { + seq_util& sq = seq(); + sort* cs = sq.mk_char_sort(); + expr_ref var0(m.mk_var(0, cs), m); + seq::range_predicate rp(sq.max_char()); + if (pred_to_rp(m, sq, var0, pred, sq.max_char(), rp)) + return seq::range_predicate_to_regex(sq, rp, seq_sort); symbol nm("c"); expr_ref lam(m.mk_lambda(1, &cs, &nm, pred), m); return expr_ref(re().mk_of_pred(lam), m); @@ -435,7 +490,7 @@ expr_ref seq_split::expand_fromre(expr* r, bool& ok, obj_hashtable& deriv_ 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); // single-char regex + 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); } diff --git a/src/ast/rewriter/seq_split.h b/src/ast/rewriter/seq_split.h index 27b447b726..cb28fd5056 100644 --- a/src/ast/rewriter/seq_split.h +++ b/src/ast/rewriter/seq_split.h @@ -136,9 +136,12 @@ class seq_split { // One level of the sigma rules: from_re(r) -> a SplitSet term built from the // immediate subterms. `ok` is set false on an unsupported shape. expr_ref expand_fromre(expr* r, bool& ok, obj_hashtable& deriv_memo); - // Build the single-character regex of_pred(lambda c. pred) from a cofactor - // path condition `pred` (a Boolean over the character (:var 0)). - expr_ref mk_charclass_re(expr* pred); + // Build the single-character regex for a cofactor path condition `pred` (a + // Boolean over the character (:var 0)). Prefer a range / union-of-ranges + // (which nseq's emptiness/primitive/length path fully supports); fall back to + // of_pred(lambda) only for predicates that are not a single (possibly negated) + // range. + expr_ref mk_charclass_re(expr* pred, sort* seq_sort); // 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); From 2865e5f64dacd99dacf38b1d7260badeeaccfae9 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sat, 4 Jul 2026 01:04:41 +0300 Subject: [PATCH 5/7] seq_split: derivative-based split for intersection (r = E(r) | RE(LF(delta(r)))) 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> --- src/ast/rewriter/seq_split.cpp | 55 +++++++++++++++++++++++----------- src/ast/rewriter/seq_split.h | 6 ++++ src/test/seq_split.cpp | 38 ++++++++++++++--------- 3 files changed, 67 insertions(+), 32 deletions(-) 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()); } From c0fbca4f41c228f6e42817236faa1581e0de8a44 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sat, 4 Jul 2026 08:01:09 +0300 Subject: [PATCH 6/7] theory_nseq: drop stray std::cout debug print in check_length_coherence Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/smt/theory_nseq.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 2bdfe67dd5..81de182037 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -2101,7 +2101,6 @@ namespace smt { literal_vector dep_lits; for (unsigned idx : mem_indices) { - std::cout << seq::mem_pp(mems[idx]) << std::endl; seq::deps_to_lits(m_nielsen.dep_mgr(), mems[idx].m_dep, eqs, dep_lits); } From 10cab8b70d39810eb5b034180d7d6ae257a51136 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Sat, 4 Jul 2026 10:30:00 +0300 Subject: [PATCH 7/7] 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; }