From fd4cc176892fd9b62926eddeb627d0a24d64c970 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 30 Jun 2025 13:52:52 -0700 Subject: [PATCH] t0 Signed-off-by: Lev Nachmanson --- src/cmd_context/cmd_context.cpp | 14 ++++++++++++++ src/cmd_context/cmd_context.h | 1 + src/shell/smtlib_frontend.cpp | 6 ++++++ src/smt/smt_context.cpp | 18 ++++++++++++++++++ src/smt/smt_context.h | 2 ++ src/smt/smt_context_pp.cpp | 11 ++++++++++- src/smt/smt_kernel.cpp | 5 +++++ src/smt/smt_kernel.h | 5 +++++ src/smt/smt_solver.cpp | 5 +++++ src/smt/theory_lra.cpp | 4 ++++ src/solver/check_sat_result.h | 1 + 11 files changed, 71 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 4f093e749..4d71172d1 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2306,6 +2306,20 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) { st.display_smt2(regular_stream()); } +void cmd_context::flush_statistics() { + // Force aggregation of theory statistics before displaying them + // This ensures detailed theory stats are available even on timeout/interruption + if (m_check_sat_result) { + m_check_sat_result->flush_statistics(); + } + else if (m_solver) { + m_solver->flush_statistics(); + } + else if (m_opt) { + // m_opt->flush_statistics(); // Not implemented for optimization + } +} + vector> cmd_context::tracked_assertions() { vector> result; diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 5e5f30028..1d99f5201 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -508,6 +508,7 @@ public: void display_assertions(); void display_statistics(bool show_total_time = false, double total_time = 0.0); + void flush_statistics(); // Force aggregation of theory statistics void display_dimacs(); void display_parameters(std::ostream& out); void reset(bool finalize = false); diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index 008142c1a..df6186072 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -62,6 +62,12 @@ static void display_model() { } static void on_timeout() { + // Force aggregation of theory statistics before displaying them + std::cout << "[DEBUG] on_timeout() called - forcing statistics aggregation\n"; + if (g_cmd_context) { + std::cout << "[DEBUG] Calling g_cmd_context->flush_statistics()\n"; + g_cmd_context->flush_statistics(); + } display_statistics(); _Exit(0); } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 3afc40d81..1c81457cc 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3049,6 +3049,15 @@ namespace smt { void context::flush() { flet l1(m_flushing, true); TRACE(flush, tout << "m_scope_lvl: " << m_scope_lvl << "\n";); + + // 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); + } + m_relevancy_propagator = nullptr; m_model_generator->reset(); for (theory* t : m_theory_set) { @@ -3511,6 +3520,15 @@ namespace smt { m_case_split_queue->display(tout << "case splits\n"); ); m_search_finalized = true; + + // 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); + } + display_profile(verbose_stream()); if (r == l_true && get_cancel_flag()) r = l_undef; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 3dbadc1cb..5fd373973 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1836,6 +1836,8 @@ namespace smt { void collect_statistics(::statistics & st) const; + void flush_statistics(); // Force aggregation of theory statistics + void display_statistics(std::ostream & out) const; void display_istatistics(std::ostream & out) const; diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 853dc4de3..9ef8485fe 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -27,7 +27,6 @@ Revision History: namespace smt { - std::ostream& context::display_last_failure(std::ostream& out) const { switch(m_last_search_failure) { case OK: @@ -430,6 +429,16 @@ namespace smt { } } + void context::flush_statistics() { + // Force aggregation of theory statistics into m_aux_stats + // This ensures detailed theory stats are available even on timeout/interruption + std::cout << "[DEBUG] context::flush_statistics() - 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); + } + } + void context::display_statistics(std::ostream & out) const { ::statistics st; collect_statistics(st); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 85efd5620..da7c8bcba 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -256,6 +256,11 @@ namespace smt { void kernel::collect_statistics(::statistics & st) const { m_imp->m_kernel.collect_statistics(st); } + + void kernel::flush_statistics() { + std::cout << "[DEBUG] smt::kernel::flush_statistics() called\n"; + m_imp->m_kernel.flush_statistics(); + } void kernel::reset_statistics() { } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 92dac74d5..322a06c18 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -270,6 +270,11 @@ namespace smt { */ void collect_statistics(::statistics & st) const; + /** + \brief Force aggregation of theory statistics. + */ + void flush_statistics(); + /** \brief Reset kernel statistics. */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index f7737b8a6..cfcf541a0 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -146,6 +146,11 @@ namespace { m_context.collect_statistics(st); } + void flush_statistics() override { + // Force aggregation of theory statistics before collecting them + m_context.flush_statistics(); + } + lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) override { expr_ref_vector unfixed(m_context.m()); return m_context.get_consequences(assumptions, vars, conseq, unfixed); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f3d9a5169..97c6f3306 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3446,6 +3446,7 @@ 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); } @@ -3458,6 +3459,7 @@ 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; @@ -4151,6 +4153,7 @@ 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"; m_arith_eq_adapter.collect_statistics(st); m_stats.collect_statistics(st); lp().settings().stats().collect_statistics(st); @@ -4316,6 +4319,7 @@ 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) { diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index 8a48d3277..6ab1aad2d 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -54,6 +54,7 @@ public: lbool set_status(lbool r) { return m_status = r; } lbool status() const { return m_status; } virtual void collect_statistics(statistics & st) const = 0; + virtual void flush_statistics() {} // Force aggregation of theory statistics virtual void get_unsat_core(expr_ref_vector & r) = 0; void set_model_converter(model_converter* mc) { m_mc0 = mc; } model_converter* mc0() const { return m_mc0.get(); }