From 8992d5fc53677593f9747e68ab4a42fb6e4d3eb1 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Fri, 3 Jul 2026 16:05:31 +0300 Subject: [PATCH] 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); } }