From 00ff00bd05e3495b9acc2ab9646e8ded97bc9d6d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 30 Jun 2025 16:19:36 -0700 Subject: [PATCH] avoid double collecting the stats Signed-off-by: Lev Nachmanson --- src/cmd_context/cmd_context.cpp | 10 +++++++--- src/shell/smtlib_frontend.cpp | 29 ++++++++--------------------- src/smt/smt_context.cpp | 25 +++++++++++++------------ src/smt/smt_context.h | 4 ++++ src/smt/smt_context_pp.cpp | 17 +++++++++++++++-- src/smt/theory_lra.cpp | 28 ---------------------------- 6 files changed, 47 insertions(+), 66 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index a0bf38715..bf97daccb 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2315,16 +2315,20 @@ void cmd_context::flush_statistics() { // Force aggregation of theory statistics AND collect them into our singleton // This ensures detailed theory stats are preserved even on timeout/interruption + // Avoid double-collection if m_check_sat_result and m_solver point to same object + bool collected_from_check_sat = false; + // Try m_check_sat_result first if (m_check_sat_result) { m_check_sat_result->flush_statistics(); // Also collect the statistics immediately into our singleton m_check_sat_result->collect_statistics(m_global_stats); + collected_from_check_sat = true; } - // Also try m_solver which might have the theories - if (m_solver) { + // Also try m_solver which might have the theories (but avoid duplication) + if (m_solver && (!collected_from_check_sat || m_solver.get() != m_check_sat_result)) { m_solver->flush_statistics(); // Also collect the statistics immediately into our singleton @@ -2332,7 +2336,7 @@ void cmd_context::flush_statistics() { } // Try to get access to any other solver contexts - if (m_opt) { + if (m_opt && m_opt.get() != m_check_sat_result) { // m_opt->flush_statistics(); // Not implemented for optimization // But we can still collect stats diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index 80aa789d1..535bff0e0 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -40,7 +40,6 @@ extern bool g_display_statistics; extern bool g_display_model; static clock_t g_start_time; static cmd_context * g_cmd_context = nullptr; -static smt::context * g_smt_context = nullptr; // Track active SMT context for timeout stats static void display_statistics() { lock_guard lock(*display_stats_mux); @@ -66,20 +65,17 @@ static void display_model() { static void on_timeout() { // Force aggregation of theory statistics before displaying them - if (g_cmd_context) { + // Try to access the SMT context directly first (more direct path to theories) + smt::context* current_smt_ctx = smt::get_current_smt_context(); + if (current_smt_ctx && g_cmd_context) { + // Force aggregation at SMT level and collect directly into singleton + current_smt_ctx->flush_statistics(); + g_cmd_context->collect_smt_statistics(*current_smt_ctx); + } else if (g_cmd_context) { + // Fall back to normal flush if no direct SMT context access g_cmd_context->flush_statistics(); } - // Try to access the SMT context directly if available - if (g_smt_context) { - g_smt_context->flush_statistics(); - - // Also collect the aggregated stats into the cmd_context singleton - if (g_cmd_context) { - g_cmd_context->collect_smt_statistics(*g_smt_context); - } - } - display_statistics(); _Exit(0); } @@ -90,15 +86,6 @@ static void STD_CALL on_ctrl_c(int) { raise(SIGINT); } -// Functions to register/unregister the active SMT context for timeout handling -void register_smt_context(smt::context* ctx) { - g_smt_context = ctx; -} - -void unregister_smt_context() { - g_smt_context = nullptr; -} - void help_tactics() { struct cmp { bool operator()(tactic_cmd* a, tactic_cmd* b) const { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ee358848d..34d826329 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -49,6 +49,9 @@ Revision History: namespace smt { + // Global pointer to current SMT context for timeout statistics collection + static context* g_smt_context = nullptr; + context::context(ast_manager & m, smt_params & p, params_ref const & _p): m(m), m_fparams(p), @@ -100,7 +103,7 @@ namespace smt { m_model_generator->set_context(this); // Register this SMT context for timeout statistics collection - register_smt_context(this); + g_smt_context = this; } /** @@ -193,7 +196,9 @@ namespace smt { context::~context() { // Unregister this SMT context - unregister_smt_context(); + if (g_smt_context == this) { + g_smt_context = nullptr; + } flush(); m_asserted_formulas.finalize(); } @@ -3058,11 +3063,7 @@ namespace smt { // Aggregate statistics from all theories before cleanup // This ensures that detailed theory statistics are preserved even on timeout/interruption - std::cout << "[DEBUG] context::flush() - Aggregating statistics from " << m_theory_set.size() << " theories\n"; - for (theory* t : m_theory_set) { - std::cout << "[DEBUG] Collecting stats from theory: " << t->get_name() << "\n"; - t->collect_statistics(m_aux_stats); - } + flush_statistics(); m_relevancy_propagator = nullptr; m_model_generator->reset(); @@ -3529,11 +3530,7 @@ namespace smt { // Aggregate statistics from all theories at the end of search // This ensures that theory statistics are collected even if search was interrupted - std::cout << "[DEBUG] context::check_finalize() - Aggregating statistics from " << m_theory_set.size() << " theories\n"; - for (theory* t : m_theory_set) { - std::cout << "[DEBUG] Collecting stats from theory: " << t->get_name() << "\n"; - t->collect_statistics(m_aux_stats); - } + flush_statistics(); display_profile(verbose_stream()); if (r == l_true && get_cancel_flag()) @@ -4821,6 +4818,10 @@ namespace smt { if (m_model && p.user_functions() && smtlib2_compliant != "true") m_model->add_rec_funs(); } + // Function to get the current global SMT context (for timeout handling) + context* get_current_smt_context() { + return g_smt_context; + } }; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 5fd373973..0c61968f0 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -130,6 +130,7 @@ namespace smt { class parallel* m_par = nullptr; unsigned m_par_index = 0; bool m_internalizing_assertions = false; + bool m_statistics_collected = false; // prevent double collection of theory statistics lbool m_internal_completed = l_undef; @@ -1893,6 +1894,9 @@ namespace smt { std::ostream& operator<<(std::ostream& out, enode_pp const& p); + + // Function to get the current global SMT context (for timeout handling) + context* get_current_smt_context(); }; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 26a073291..3a1cb69f0 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -27,11 +27,18 @@ Revision History: namespace smt { void context::flush_statistics() { + // Only collect statistics once to avoid duplication + if (m_statistics_collected) { + return; + } + // Force aggregation of theory statistics into m_aux_stats // This ensures that detailed theory statistics are available even on timeout/interruption for (theory* t : m_theory_set) { t->collect_statistics(m_aux_stats); } + + m_statistics_collected = true; } std::ostream& context::display_last_failure(std::ostream& out) const { @@ -431,9 +438,15 @@ namespace smt { st.update("mk bool var", m_stats.m_num_mk_bool_var ? m_stats.m_num_mk_bool_var - 1 : 0); m_qmanager->collect_statistics(st); m_asserted_formulas.collect_statistics(st); - for (theory* th : m_theory_set) { - th->collect_statistics(st); + + // Only collect theory statistics if they haven't been aggregated yet by flush_statistics() + if (!m_statistics_collected) { + for (theory* th : m_theory_set) { + th->collect_statistics(st); + } } + // If theory stats were already aggregated by flush_statistics(), they are already in m_aux_stats + // which was copied to st above via st.copy(m_aux_stats) } void context::display_statistics(std::ostream & out) const { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 41504aba4..f3d9a5169 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3446,7 +3446,6 @@ public: } void set_conflict() { - std::cout << "[DEBUG] theory_lra::set_conflict() - LRA conflict detected, incrementing m_num_conflicts from " << m_num_conflicts << "\n"; literal_vector core; set_conflict_or_lemma(core, true); } @@ -3459,7 +3458,6 @@ public: // lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed ++m_num_conflicts; ++m_stats.m_conflicts; - std::cout << "[DEBUG] theory_lra conflict count incremented to: " << m_num_conflicts << ", stats conflicts: " << m_stats.m_conflicts << "\n"; TRACE(arith_conflict, tout << "@" << ctx().get_scope_level() << (is_conflict ? " conflict":" lemma"); for (auto const& p : m_params) tout << " " << p; @@ -4153,34 +4151,9 @@ public: } void collect_statistics(::statistics & st) const { - std::cout << "[DEBUG] theory_lra impl::collect_statistics() - conflicts: " << m_stats.m_conflicts << ", total: " << m_num_conflicts << "\n"; - - // Count statistics before adding - unsigned before_count = st.size(); - m_arith_eq_adapter.collect_statistics(st); m_stats.collect_statistics(st); lp().settings().stats().collect_statistics(st); - - // Count statistics after adding - unsigned after_count = st.size(); - std::cout << "[DEBUG] theory_lra impl added " << (after_count - before_count) << " statistics entries to the statistics object\n"; - - // Show a few sample statistics that were added - if (after_count > before_count) { - std::cout << "[DEBUG] Some LRA statistics added:\n"; - unsigned shown = 0; - unsigned total = st.size(); - for (unsigned i = 0; i < total && shown < 5; ++i, ++shown) { - std::cout << "[DEBUG] " << st.get_key(i) << ": "; - if (st.is_uint(i)) { - std::cout << st.get_uint_value(i); - } else { - std::cout << st.get_double_value(i); - } - std::cout << "\n"; - } - } } /* @@ -4343,7 +4316,6 @@ void theory_lra::display(std::ostream & out) const { m_imp->display(out); } void theory_lra::collect_statistics(::statistics & st) const { - std::cout << "[DEBUG] theory_lra::collect_statistics() called\n"; m_imp->collect_statistics(st); } theory_lra::inf_eps theory_lra::value(theory_var v) {