From 7dea14f732311963a8da38691633112bfb941219 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Mar 2026 20:09:19 -0700 Subject: [PATCH] move statistics Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 34 +++++++++++++++++++++++++++++++++- src/smt/seq/seq_nielsen.h | 1 + src/smt/theory_nseq.cpp | 30 ++---------------------------- 3 files changed, 36 insertions(+), 29 deletions(-) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index 588bf66be..3473fbb49 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -27,6 +27,7 @@ Author: #include "ast/rewriter/seq_rewriter.h" #include "ast/rewriter/th_rewriter.h" #include "util/hashtable.h" +#include "util/statistics.h" #include #include #include @@ -2142,7 +2143,7 @@ namespace seq { ++m_stats.m_num_unknown; return search_result::unknown; } - catch(const std::exception& ex) { + catch(const std::exception&) { #ifdef Z3DEBUG std::string dot = to_dot(); #endif @@ -4451,4 +4452,35 @@ namespace seq { return true; } + // ----------------------------------------------------------------------- + // Statistics collection + // ----------------------------------------------------------------------- + + void nielsen_graph::collect_statistics(::statistics& st) const { + st.update("nseq solve calls", m_stats.m_num_solve_calls); + st.update("nseq dfs nodes", m_stats.m_num_dfs_nodes); + st.update("nseq sat", m_stats.m_num_sat); + st.update("nseq unsat", m_stats.m_num_unsat); + st.update("nseq unknown", m_stats.m_num_unknown); + st.update("nseq simplify clash", m_stats.m_num_simplify_conflict); + st.update("nseq extensions", m_stats.m_num_extensions); + st.update("nseq fresh vars", m_stats.m_num_fresh_vars); + st.update("nseq max depth", m_stats.m_max_depth); + + // modifier breakdown + st.update("nseq mod det", m_stats.m_mod_det); + st.update("nseq mod power epsilon", m_stats.m_mod_power_epsilon); + st.update("nseq mod num cmp", m_stats.m_mod_num_cmp); + st.update("nseq mod const num unwind", m_stats.m_mod_const_num_unwinding); + st.update("nseq mod eq split", m_stats.m_mod_eq_split); + st.update("nseq mod star intr", m_stats.m_mod_star_intr); + st.update("nseq mod gpower intr", m_stats.m_mod_gpower_intr); + st.update("nseq mod const nielsen", m_stats.m_mod_const_nielsen); + st.update("nseq mod regex char", m_stats.m_mod_regex_char_split); + st.update("nseq mod regex var", m_stats.m_mod_regex_var_split); + st.update("nseq mod power split", m_stats.m_mod_power_split); + st.update("nseq mod var nielsen", m_stats.m_mod_var_nielsen); + st.update("nseq mod var num unwind", m_stats.m_mod_var_num_unwinding); + } + } diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h index 922a91a97..772be0989 100644 --- a/src/smt/seq/seq_nielsen.h +++ b/src/smt/seq/seq_nielsen.h @@ -879,6 +879,7 @@ namespace seq { // accumulated search statistics nielsen_stats const& stats() const { return m_stats; } void reset_stats() { m_stats.reset(); } + void collect_statistics(::statistics& st) const; // generate arithmetic length constraints from the root node's string // equalities and regex memberships. For each non-trivial equation lhs = rhs, diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index dcfc20674..dac1a1fa0 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -522,34 +522,8 @@ namespace smt { st.update("nseq conflicts", m_num_conflicts); st.update("nseq final checks", m_num_final_checks); st.update("nseq length axioms", m_num_length_axioms); - - // Nielsen graph search metrics - auto const& ns = m_nielsen.stats(); - st.update("nseq solve calls", ns.m_num_solve_calls); - st.update("nseq dfs nodes", ns.m_num_dfs_nodes); - st.update("nseq sat", ns.m_num_sat); - st.update("nseq unsat", ns.m_num_unsat); - st.update("nseq unknown", ns.m_num_unknown); - st.update("nseq simplify clash", ns.m_num_simplify_conflict); - st.update("nseq extensions", ns.m_num_extensions); - st.update("nseq fresh vars", ns.m_num_fresh_vars); - st.update("nseq max depth", ns.m_max_depth); - - // modifier breakdown - st.update("nseq mod det", ns.m_mod_det); - st.update("nseq mod power epsilon", ns.m_mod_power_epsilon); - st.update("nseq mod num cmp", ns.m_mod_num_cmp); - st.update("nseq mod const num unwind", ns.m_mod_const_num_unwinding); - st.update("nseq mod eq split", ns.m_mod_eq_split); - st.update("nseq mod star intr", ns.m_mod_star_intr); - st.update("nseq mod gpower intr", ns.m_mod_gpower_intr); - st.update("nseq mod const nielsen", ns.m_mod_const_nielsen); - st.update("nseq mod regex char", ns.m_mod_regex_char_split); - st.update("nseq mod regex var", ns.m_mod_regex_var_split); - st.update("nseq mod power split", ns.m_mod_power_split); - st.update("nseq mod var nielsen", ns.m_mod_var_nielsen); - st.update("nseq mod var num unwind", ns.m_mod_var_num_unwinding); - st.update("nseq ho unfolds", m_num_ho_unfolds); + st.update("nseq ho unfolds", m_num_ho_unfolds); + m_nielsen.collect_statistics(st); } void theory_nseq::display(std::ostream& out) const {