From 3e1fd56ca288824c92b6765f2847b1a4c84f8b52 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Aug 2026 20:20:58 -0700 Subject: [PATCH] Add monadic regex statistics Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 2bcccba7-ac7d-476e-8dfe-718a21d37554 --- src/ast/rewriter/seq_monadic.cpp | 73 ++++++++++++++++++++++++++++---- src/ast/rewriter/seq_monadic.h | 16 +++++++ src/smt/seq_regex.h | 1 + src/smt/theory_seq.cpp | 1 + 4 files changed, 82 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 285ce91d37..1ec4335f95 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -92,9 +92,11 @@ lbool seq_monadic::nullable(expr* r) { } expr_ref_pair_vector const& seq_monadic::derivative_cofactors(expr* r) { + ++m_stats.m_cofactor_calls; expr_ref_pair_vector* v = nullptr; if (m_cofactors.find(r, v)) return *v; + ++m_stats.m_states; v = alloc(expr_ref_pair_vector, m); if (m_config.m_mode == transition_mode::light_antimirov) m_rw.light_ant_derivative_cofactors(r, *v); @@ -122,7 +124,14 @@ bool seq_monadic::live_states(expr* R, expr_ref_vector& out) { intern(R); const unsigned STATE_CAP = 1u << 12; for (unsigned i = 0; i < states.size(); ++i) { - if (states.size() > STATE_CAP || !m.inc()) return false; + if (states.size() > STATE_CAP) { + m_stats.inc_bail(bail_reason::state_cap); + return false; + } + if (!m.inc()) { + m_stats.inc_bail(bail_reason::resource); + return false; + } expr_ref_pair_vector const& cof = derivative_cofactors(states.get(i)); for (auto const& [g, t] : cof) { if (re().is_empty(t)) continue; @@ -280,7 +289,11 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w guard_set nacc = acc; nacc.conjoin(g); lbool ne = nacc.eval(nullptr); - if (ne == l_undef) { bail = true; return; } // non-range / unknown guard + if (ne == l_undef) { + m_stats.inc_bail(bail_reason::guard); + bail = true; + return; + } if (ne == l_false) continue; // empty joint guard: prune cur[i] = t; rec(i + 1, nacc); @@ -289,7 +302,16 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w }; while (!work.empty()) { - if (m_budget == 0 || !m.inc()) { m_giveup = true; return l_undef; } + if (m_budget == 0) { + m_stats.inc_bail(bail_reason::budget); + m_giveup = true; + return l_undef; + } + if (!m.inc()) { + m_stats.inc_bail(bail_reason::resource); + m_giveup = true; + return l_undef; + } --m_budget; for (unsigned i = n; i-- > 0; ) { st[i] = work.back(); @@ -300,8 +322,10 @@ lbool seq_monadic::product_nonempty(svector const& comps, expr_ref* w *witness_word = reconstruct(fill_key(st)); return l_true; } - if (undecided) + if (undecided) { + m_stats.inc_bail(bail_reason::nullability); return l_undef; + } for (unsigned i = 0; i < n; ++i) branches[i] = &derivative_cofactors(st[i]); @@ -373,16 +397,24 @@ void seq_monadic::reset_search() { bool seq_monadic::prepare(membership_vec const& memberships) { reset_search(); for (auto const& [term, regex, d] : memberships) { - if (!u().is_re(regex, m_seq_sort)) + if (!u().is_re(regex, m_seq_sort)) { + m_stats.inc_bail(bail_reason::unsupported); return false; - if (!u().is_seq(m_seq_sort, m_elem_sort)) + } + if (!u().is_seq(m_seq_sort, m_elem_sort)) { + m_stats.inc_bail(bail_reason::unsupported); return false; + } vector atoms; expr* the_var = nullptr; - if (!parse_term(term, atoms, the_var)) + if (!parse_term(term, atoms, the_var)) { + m_stats.inc_bail(bail_reason::unsupported); return false; - if (!the_var) + } + if (!the_var) { + m_stats.inc_bail(bail_reason::unsupported); return false; // no variable: ground membership, not our case + } m_regexes.push_back(regex); m_atoms.push_back(atoms); m_pin.push_back(regex); @@ -460,7 +492,13 @@ lbool seq_monadic::dfs_membership(unsigned mi) { lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { if (m_giveup) return l_undef; // unwind the whole search, don't keep branching - if (m_budget == 0 || !m.inc()) { + if (m_budget == 0) { + m_stats.inc_bail(bail_reason::budget); + m_giveup = true; + return l_undef; + } + if (!m.inc()) { + m_stats.inc_bail(bail_reason::resource); m_giveup = true; return l_undef; } @@ -472,6 +510,7 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { return dfs_membership(mi + 1); if (nb == l_false) return l_false; + m_stats.inc_bail(bail_reason::nullability); return l_undef; // undecidable nullability } atom const& a = atoms[i]; @@ -622,3 +661,19 @@ lbool seq_monadic::check() { minimize_core(m_memberships); return r; } + +void seq_monadic::collect_statistics(::statistics& st) const { + static char const* const bail_names[] = { + "seq monadic bail unsupported", + "seq monadic bail state cap", + "seq monadic bail dnf cap", + "seq monadic bail budget", + "seq monadic bail resource", + "seq monadic bail nullability", + "seq monadic bail guard" + }; + st.update("seq monadic cofactor calls", m_stats.m_cofactor_calls); + st.update("seq monadic states", m_stats.m_states); + for (unsigned i = 0; i < static_cast(bail_reason::num_reasons); ++i) + st.update(bail_names[i], m_stats.m_bails[i]); +} diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index a3086187c1..f85e30c075 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -70,6 +70,7 @@ Author: #include "util/obj_pair_hashtable.h" #include "util/dependency.h" #include "util/trail.h" +#include "util/statistics.h" #include #include #include @@ -115,6 +116,18 @@ private: config(transition_mode mode) : m_mode(mode) {} }; + enum class bail_reason { unsupported, state_cap, dnf_cap, budget, resource, nullability, guard, num_reasons }; + + struct statistics { + unsigned m_cofactor_calls = 0; + unsigned m_states = 0; + unsigned m_bails[static_cast(bail_reason::num_reasons)] = {}; + + void inc_bail(bail_reason reason) { + ++m_bails[static_cast(reason)]; + } + }; + ast_manager& m; seq_rewriter& m_rw; th_rewriter m_thrw; // normalizes constant-element derivatives (folds @@ -126,6 +139,7 @@ private: unsigned m_budget = 0; // global work budget (search nodes + product pops) bool m_giveup = false; // set when the budget is exhausted config m_config; + statistics m_stats; obj_map m_model; // last extracted model (var -> witness); see get_model() cofactor_cache m_cofactors; // memoizes derivative_cofactors per regex (see class above) guard_set::cache m_rp_cache; // cofactor guard -> range predicate @@ -266,6 +280,8 @@ public: ~seq_monadic() { reset_live_cache(); } + void collect_statistics(::statistics &st) const; + transition_mode mode() const { return m_config.m_mode; } // Enable/disable model generation (default: enabled). When enabled, a successful diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h index 25b0041141..e38f09eacc 100644 --- a/src/smt/seq_regex.h +++ b/src/smt/seq_regex.h @@ -261,6 +261,7 @@ namespace smt { bool can_propagate() const { return false; } bool propagate() const { return false; } final_check_status final_check(); + void collect_statistics(::statistics& st) const { m_monadic.collect_statistics(st); } void propagate_in_re(literal lit); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 559a8fb2b9..a9fe2f6fce 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1954,6 +1954,7 @@ std::ostream& theory_seq::display_deps(std::ostream& out, dependency* dep) const } void theory_seq::collect_statistics(::statistics & st) const { + m_regex.collect_statistics(st); st.update("seq num splits", m_stats.m_num_splits); st.update("seq num reductions", m_stats.m_num_reductions); st.update("seq length coherence", m_stats.m_check_length_coherence);