Merge remote-tracking branch 'origin/c3-split-perf' into c3-rewrote-regex-unwinding

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

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);
 
     /**

src/ast/rewriter/seq_split.cpp

@@ -18,8 +18,10 @@ 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"
 #include "util/stack.h"
 
 seq_split::seq_split(seq_rewriter& rw) :
@@ -177,8 +179,11 @@ seq_util::rex& seq_split::re()  const { return m_rw.u().re; }
 
 // Add <d, n> 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,7 +191,12 @@ 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();
+    // Dedup the cross-product: a split-set denotes the UNION of its <D,N> pairs,
+    // so identical (perfectly-shared) pairs are redundant.  Skipping them keeps
+    // the De Morgan fold from accumulating exponentially many equal splits.
+    obj_pair_hashtable<expr, expr> seen;
     for (auto const& p1 : s1) {
         for (auto const& p2 : s2) {
             if (r.is_empty(p1.m_d) || r.is_empty(p2.m_d) ||
@@ -194,9 +204,18 @@ 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;
+            std::pair<expr*, expr*> 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)
+            if (result.size() > threshold) {
+                ++m_stats.m_threshold_overruns;
                 return false;
+            }
         }
     }
     return true;
@@ -210,6 +229,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 +253,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;
@@ -244,8 +266,112 @@ 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, unsigned threshold, bool& ok) {
+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)).  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);
+}
+
+// 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<expr>& 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);
+}
+
+// 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, unsigned threshold, bool& ok, obj_hashtable<expr>& deriv_memo) {
     ok = true;
+    ++m_stats.m_sigma_expand;
     seq_util& sq = seq();
     seq_util::rex& rex = re();
 
@@ -376,8 +502,14 @@ expr_ref seq_split::expand_fromre(expr* r, unsigned threshold, bool& ok) {
         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));
@@ -387,9 +519,19 @@ expr_ref seq_split::expand_fromre(expr* r, unsigned threshold, bool& ok) {
         return acc;
     }
 
-    // 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) 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 (!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;
+        }
+        return mk_compl(mk_fromre(a));                     // De Morgan fallback
+    }
 
     // abbreviation
     // difference: a \ b = a & ~b ; sigma(a \ b) = sigma(a) cap ~sigma(b).
@@ -473,7 +615,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<expr>& deriv_memo) {
     ok = true;
     expr *a = nullptr, *b = nullptr, *r = nullptr, *s = nullptr;
 
@@ -484,23 +627,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, threshold, ok);
+        expr_ref e = expand_fromre(r, threshold, 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);
@@ -551,15 +694,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);
@@ -588,9 +735,10 @@ 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;
             return false;
         }
 
@@ -598,14 +746,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)) {
@@ -664,6 +817,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.

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 <functional>
 
 class seq_rewriter;
@@ -57,6 +58,26 @@ enum class split_mode { weak, strong };
 // default) keeps everything, so sigma is unchanged.  See seq_split::compute.
 typedef std::function<bool(expr* D, expr* N)> 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 <D,N> 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_dedup_drops = 0;        // duplicate <D,N> pairs skipped in intersect
+    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 +102,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;
@@ -118,19 +140,38 @@ class seq_split {
     // immediate subterms.  `ok` is set false on an unsupported shape or on a
     // loop bound exceeding `threshold` (the loop rule unfolds eagerly into one
     // branch per copy, so it must be capped before allocation).
-    expr_ref expand_fromre(expr* r, unsigned threshold, bool& ok);
+    expr_ref expand_fromre(expr* r, unsigned threshold, bool& ok, obj_hashtable<expr>& deriv_memo);
+
+    // 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);
+
+    // 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<expr>& 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);
+
     // Materialized split-set -> a `union` of `single`s.
     expr_ref from_split_set(split_set const& s);
+
     // Reduce `t` until its head is empty | single | union (one outermost level
     // for the lazy nodes; inter/compl are expanded eagerly via `materialize`,
     // since the paper's De Morgan / cross-product cannot yield a split lazily).
     // `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<expr>& 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,
@@ -156,6 +197,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 <D, N> one at a time, on demand, instead of computing
     // them all up front.  Obtain one from seq_split::iterate (or construct it
@@ -185,6 +230,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<expr> m_deriv_memo;
     public:
         iterator(seq_split& engine, expr* node, split_mode mode,
                  unsigned threshold, split_oracle oracle);

src/smt/seq/seq_nielsen.cpp

@@ -6518,6 +6518,23 @@ 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 dedup-drops",      sp.m_dedup_drops);
+        st.update("nseq split simplify",         sp.m_simplify);
     }
 
 }

src/smt/theory_nseq.cpp

@@ -2164,7 +2164,7 @@ namespace smt {
                     expr_ref not_divides(m.mk_not(m_autil.mk_divides(g_expr, len_minus_l)), m);
                     prop_expr = m.mk_or(len_lt_l, not_divides);
                     m_th_rewriter(prop_expr);  // the divisibility predicate needs to be rewritten as it won't happen
-                                               // automatically
+                    // automatically
 
                     m_gradient_cache[s] = 1;  // Reset gradient cache
                 }
@@ -2180,9 +2180,9 @@ namespace smt {
                 enode_pair_vector eqs;
                 literal_vector dep_lits;
 
-                for (unsigned idx : mem_indices)
+                for (unsigned idx : mem_indices) {
                     seq::deps_to_lits(m_nielsen.dep_mgr(), mems[idx].m_dep, eqs, dep_lits);
-
+                }
 
                 set_propagate(eqs, dep_lits, lit_prop);
 

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