mirror of
https://github.com/Z3Prover/z3
synced 2025-08-02 09:20:22 +00:00
avoid double collecting the stats
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
119e54f3a9
commit
00ff00bd05
6 changed files with 47 additions and 66 deletions
|
@ -2315,16 +2315,20 @@ void cmd_context::flush_statistics() {
|
||||||
// Force aggregation of theory statistics AND collect them into our singleton
|
// Force aggregation of theory statistics AND collect them into our singleton
|
||||||
// This ensures detailed theory stats are preserved even on timeout/interruption
|
// 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
|
// Try m_check_sat_result first
|
||||||
if (m_check_sat_result) {
|
if (m_check_sat_result) {
|
||||||
m_check_sat_result->flush_statistics();
|
m_check_sat_result->flush_statistics();
|
||||||
|
|
||||||
// Also collect the statistics immediately into our singleton
|
// Also collect the statistics immediately into our singleton
|
||||||
m_check_sat_result->collect_statistics(m_global_stats);
|
m_check_sat_result->collect_statistics(m_global_stats);
|
||||||
|
collected_from_check_sat = true;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Also try m_solver which might have the theories
|
// Also try m_solver which might have the theories (but avoid duplication)
|
||||||
if (m_solver) {
|
if (m_solver && (!collected_from_check_sat || m_solver.get() != m_check_sat_result)) {
|
||||||
m_solver->flush_statistics();
|
m_solver->flush_statistics();
|
||||||
|
|
||||||
// Also collect the statistics immediately into our singleton
|
// 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
|
// 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
|
// m_opt->flush_statistics(); // Not implemented for optimization
|
||||||
|
|
||||||
// But we can still collect stats
|
// But we can still collect stats
|
||||||
|
|
|
@ -40,7 +40,6 @@ extern bool g_display_statistics;
|
||||||
extern bool g_display_model;
|
extern bool g_display_model;
|
||||||
static clock_t g_start_time;
|
static clock_t g_start_time;
|
||||||
static cmd_context * g_cmd_context = nullptr;
|
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() {
|
static void display_statistics() {
|
||||||
lock_guard lock(*display_stats_mux);
|
lock_guard lock(*display_stats_mux);
|
||||||
|
@ -66,20 +65,17 @@ static void display_model() {
|
||||||
static void on_timeout() {
|
static void on_timeout() {
|
||||||
// Force aggregation of theory statistics before displaying them
|
// 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();
|
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();
|
display_statistics();
|
||||||
_Exit(0);
|
_Exit(0);
|
||||||
}
|
}
|
||||||
|
@ -90,15 +86,6 @@ static void STD_CALL on_ctrl_c(int) {
|
||||||
raise(SIGINT);
|
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() {
|
void help_tactics() {
|
||||||
struct cmp {
|
struct cmp {
|
||||||
bool operator()(tactic_cmd* a, tactic_cmd* b) const {
|
bool operator()(tactic_cmd* a, tactic_cmd* b) const {
|
||||||
|
|
|
@ -49,6 +49,9 @@ Revision History:
|
||||||
|
|
||||||
namespace smt {
|
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):
|
context::context(ast_manager & m, smt_params & p, params_ref const & _p):
|
||||||
m(m),
|
m(m),
|
||||||
m_fparams(p),
|
m_fparams(p),
|
||||||
|
@ -100,7 +103,7 @@ namespace smt {
|
||||||
m_model_generator->set_context(this);
|
m_model_generator->set_context(this);
|
||||||
|
|
||||||
// Register this SMT context for timeout statistics collection
|
// Register this SMT context for timeout statistics collection
|
||||||
register_smt_context(this);
|
g_smt_context = this;
|
||||||
}
|
}
|
||||||
|
|
||||||
/**
|
/**
|
||||||
|
@ -193,7 +196,9 @@ namespace smt {
|
||||||
|
|
||||||
context::~context() {
|
context::~context() {
|
||||||
// Unregister this SMT context
|
// Unregister this SMT context
|
||||||
unregister_smt_context();
|
if (g_smt_context == this) {
|
||||||
|
g_smt_context = nullptr;
|
||||||
|
}
|
||||||
flush();
|
flush();
|
||||||
m_asserted_formulas.finalize();
|
m_asserted_formulas.finalize();
|
||||||
}
|
}
|
||||||
|
@ -3058,11 +3063,7 @@ namespace smt {
|
||||||
|
|
||||||
// Aggregate statistics from all theories before cleanup
|
// Aggregate statistics from all theories before cleanup
|
||||||
// This ensures that detailed theory statistics are preserved even on timeout/interruption
|
// 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";
|
flush_statistics();
|
||||||
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_relevancy_propagator = nullptr;
|
||||||
m_model_generator->reset();
|
m_model_generator->reset();
|
||||||
|
@ -3529,11 +3530,7 @@ namespace smt {
|
||||||
|
|
||||||
// Aggregate statistics from all theories at the end of search
|
// Aggregate statistics from all theories at the end of search
|
||||||
// This ensures that theory statistics are collected even if search was interrupted
|
// 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";
|
flush_statistics();
|
||||||
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());
|
display_profile(verbose_stream());
|
||||||
if (r == l_true && get_cancel_flag())
|
if (r == l_true && get_cancel_flag())
|
||||||
|
@ -4821,6 +4818,10 @@ namespace smt {
|
||||||
if (m_model && p.user_functions() && smtlib2_compliant != "true")
|
if (m_model && p.user_functions() && smtlib2_compliant != "true")
|
||||||
m_model->add_rec_funs();
|
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;
|
||||||
|
}
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -130,6 +130,7 @@ namespace smt {
|
||||||
class parallel* m_par = nullptr;
|
class parallel* m_par = nullptr;
|
||||||
unsigned m_par_index = 0;
|
unsigned m_par_index = 0;
|
||||||
bool m_internalizing_assertions = false;
|
bool m_internalizing_assertions = false;
|
||||||
|
bool m_statistics_collected = false; // prevent double collection of theory statistics
|
||||||
lbool m_internal_completed = l_undef;
|
lbool m_internal_completed = l_undef;
|
||||||
|
|
||||||
|
|
||||||
|
@ -1894,6 +1895,9 @@ namespace smt {
|
||||||
|
|
||||||
std::ostream& operator<<(std::ostream& out, enode_pp const& p);
|
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();
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -27,11 +27,18 @@ Revision History:
|
||||||
|
|
||||||
namespace smt {
|
namespace smt {
|
||||||
void context::flush_statistics() {
|
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
|
// Force aggregation of theory statistics into m_aux_stats
|
||||||
// This ensures that detailed theory statistics are available even on timeout/interruption
|
// This ensures that detailed theory statistics are available even on timeout/interruption
|
||||||
for (theory* t : m_theory_set) {
|
for (theory* t : m_theory_set) {
|
||||||
t->collect_statistics(m_aux_stats);
|
t->collect_statistics(m_aux_stats);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
m_statistics_collected = true;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::ostream& context::display_last_failure(std::ostream& out) const {
|
std::ostream& context::display_last_failure(std::ostream& out) const {
|
||||||
|
@ -431,10 +438,16 @@ namespace smt {
|
||||||
st.update("mk bool var", m_stats.m_num_mk_bool_var ? m_stats.m_num_mk_bool_var - 1 : 0);
|
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_qmanager->collect_statistics(st);
|
||||||
m_asserted_formulas.collect_statistics(st);
|
m_asserted_formulas.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) {
|
for (theory* th : m_theory_set) {
|
||||||
th->collect_statistics(st);
|
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 {
|
void context::display_statistics(std::ostream & out) const {
|
||||||
::statistics st;
|
::statistics st;
|
||||||
|
|
|
@ -3446,7 +3446,6 @@ public:
|
||||||
}
|
}
|
||||||
|
|
||||||
void set_conflict() {
|
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;
|
literal_vector core;
|
||||||
set_conflict_or_lemma(core, true);
|
set_conflict_or_lemma(core, true);
|
||||||
}
|
}
|
||||||
|
@ -3459,7 +3458,6 @@ public:
|
||||||
// lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
|
// lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
|
||||||
++m_num_conflicts;
|
++m_num_conflicts;
|
||||||
++m_stats.m_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,
|
TRACE(arith_conflict,
|
||||||
tout << "@" << ctx().get_scope_level() << (is_conflict ? " conflict":" lemma");
|
tout << "@" << ctx().get_scope_level() << (is_conflict ? " conflict":" lemma");
|
||||||
for (auto const& p : m_params) tout << " " << p;
|
for (auto const& p : m_params) tout << " " << p;
|
||||||
|
@ -4153,34 +4151,9 @@ public:
|
||||||
}
|
}
|
||||||
|
|
||||||
void collect_statistics(::statistics & st) const {
|
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_arith_eq_adapter.collect_statistics(st);
|
||||||
m_stats.collect_statistics(st);
|
m_stats.collect_statistics(st);
|
||||||
lp().settings().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);
|
m_imp->display(out);
|
||||||
}
|
}
|
||||||
void theory_lra::collect_statistics(::statistics & st) const {
|
void theory_lra::collect_statistics(::statistics & st) const {
|
||||||
std::cout << "[DEBUG] theory_lra::collect_statistics() called\n";
|
|
||||||
m_imp->collect_statistics(st);
|
m_imp->collect_statistics(st);
|
||||||
}
|
}
|
||||||
theory_lra::inf_eps theory_lra::value(theory_var v) {
|
theory_lra::inf_eps theory_lra::value(theory_var v) {
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue