From 119e54f3a99589565b65f554d07c6c2dcd6c20b1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 30 Jun 2025 15:39:00 -0700 Subject: [PATCH] remove some debug output Signed-off-by: Lev Nachmanson --- src/cmd_context/cmd_context.cpp | 25 ------------------------- src/shell/smtlib_frontend.cpp | 8 -------- src/smt/smt_context_pp.cpp | 18 ------------------ src/smt/smt_solver.cpp | 1 - 4 files changed, 52 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 86b432e26..a0bf38715 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2291,14 +2291,9 @@ void cmd_context::set_solver_factory(solver_factory * f) { } void cmd_context::display_statistics(bool show_total_time, double total_time) { - std::cout << "[DEBUG] cmd_context::display_statistics() called - singleton has " << m_global_stats.size() << " entries\n"; - // If statistics haven't been collected yet, collect them now if (!m_stats_collected) { - std::cout << "[DEBUG] Statistics not yet collected, calling flush_statistics()\n"; flush_statistics(); - } else { - std::cout << "[DEBUG] Using already collected singleton statistics\n"; } // Add time and memory statistics @@ -2308,70 +2303,50 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) { get_memory_statistics(m_global_stats); get_rlimit_statistics(m().limit(), m_global_stats); - std::cout << "[DEBUG] Final singleton statistics has " << m_global_stats.size() << " entries\n"; m_global_stats.display_smt2(regular_stream()); } void cmd_context::flush_statistics() { // Only collect statistics once to avoid duplication if (m_stats_collected) { - std::cout << "[DEBUG] cmd_context::flush_statistics() - Statistics already collected, skipping\n"; return; } // Force aggregation of theory statistics AND collect them into our singleton // This ensures detailed theory stats are preserved even on timeout/interruption - std::cout << "[DEBUG] cmd_context::flush_statistics() called - collecting into singleton\n"; // Try m_check_sat_result first if (m_check_sat_result) { - std::cout << "[DEBUG] m_check_sat_result exists, calling flush_statistics() on " << typeid(*m_check_sat_result).name() << "\n"; m_check_sat_result->flush_statistics(); // Also collect the statistics immediately into our singleton - std::cout << "[DEBUG] Collecting statistics from m_check_sat_result into singleton\n"; m_check_sat_result->collect_statistics(m_global_stats); - } else { - std::cout << "[DEBUG] m_check_sat_result is null\n"; } // Also try m_solver which might have the theories if (m_solver) { - std::cout << "[DEBUG] m_solver exists, calling flush_statistics() on " << typeid(*m_solver).name() << "\n"; m_solver->flush_statistics(); // Also collect the statistics immediately into our singleton - std::cout << "[DEBUG] Collecting statistics from m_solver into singleton\n"; m_solver->collect_statistics(m_global_stats); - } else { - std::cout << "[DEBUG] m_solver is null\n"; } // Try to get access to any other solver contexts if (m_opt) { - std::cout << "[DEBUG] m_opt exists but flush_statistics not implemented\n"; // m_opt->flush_statistics(); // Not implemented for optimization // But we can still collect stats - std::cout << "[DEBUG] Collecting statistics from m_opt into singleton\n"; m_opt->collect_statistics(m_global_stats); - } else { - std::cout << "[DEBUG] m_opt is null\n"; } - std::cout << "[DEBUG] Singleton statistics now has " << m_global_stats.size() << " entries\n"; m_stats_collected = true; } void cmd_context::collect_smt_statistics(smt::context& smt_ctx) { // Collect statistics from SMT context directly into our singleton - std::cout << "[DEBUG] cmd_context::collect_smt_statistics() called\n"; - std::cout << "[DEBUG] Singleton before SMT collection has " << m_global_stats.size() << " entries\n"; - // Collect from the SMT context which should have aggregated theory stats smt_ctx.collect_statistics(m_global_stats); - std::cout << "[DEBUG] Singleton after SMT collection has " << m_global_stats.size() << " entries\n"; m_stats_collected = true; } diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index 4e9aefaac..80aa789d1 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -65,25 +65,19 @@ 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(); } // Try to access the SMT context directly if available if (g_smt_context) { - std::cout << "[DEBUG] Found g_smt_context! Calling flush_statistics() directly\n"; g_smt_context->flush_statistics(); // Also collect the aggregated stats into the cmd_context singleton if (g_cmd_context) { - std::cout << "[DEBUG] Collecting SMT context stats into cmd_context singleton\n"; g_cmd_context->collect_smt_statistics(*g_smt_context); } - } else { - std::cout << "[DEBUG] g_smt_context is null\n"; } display_statistics(); @@ -99,11 +93,9 @@ static void STD_CALL on_ctrl_c(int) { // Functions to register/unregister the active SMT context for timeout handling void register_smt_context(smt::context* ctx) { g_smt_context = ctx; - std::cout << "[DEBUG] Registered SMT context: " << (void*)ctx << "\n"; } void unregister_smt_context() { - std::cout << "[DEBUG] Unregistered SMT context: " << (void*)g_smt_context << "\n"; g_smt_context = nullptr; } diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 5711ca12b..26a073291 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -29,25 +29,9 @@ namespace smt { void context::flush_statistics() { // Force aggregation of theory statistics into m_aux_stats // This ensures that detailed theory statistics are available even on timeout/interruption - std::cout << "[DEBUG] smt::context::flush_statistics() called - Aggregating statistics from " << m_theory_set.size() << " theories\n"; - - // Show current m_aux_stats before aggregation - std::cout << "[DEBUG] m_aux_stats before aggregation has " << m_aux_stats.size() << " entries\n"; - for (theory* t : m_theory_set) { - std::cout << "[DEBUG] Collecting stats from theory: " << t->get_name() << "\n"; - - // Count stats before collecting from this theory - unsigned before_count = m_aux_stats.size(); - t->collect_statistics(m_aux_stats); - - // Count stats after collecting from this theory - unsigned after_count = m_aux_stats.size(); - std::cout << "[DEBUG] Theory " << t->get_name() << " added " << (after_count - before_count) << " statistics entries\n"; } - - std::cout << "[DEBUG] m_aux_stats after aggregation has " << m_aux_stats.size() << " total entries\n"; } std::ostream& context::display_last_failure(std::ostream& out) const { @@ -428,9 +412,7 @@ namespace smt { } void context::collect_statistics(::statistics & st) const { - std::cout << "[DEBUG] smt::context::collect_statistics() called - m_aux_stats has " << m_aux_stats.size() << " entries\n"; st.copy(m_aux_stats); - std::cout << "[DEBUG] After copying m_aux_stats, st has " << st.size() << " entries\n"; st.update("conflicts", m_stats.m_num_conflicts); st.update("decisions", m_stats.m_num_decisions); st.update("propagations", m_stats.m_num_propagations + m_stats.m_num_bin_propagations); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index c1b944286..cfcf541a0 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -148,7 +148,6 @@ namespace { void flush_statistics() override { // Force aggregation of theory statistics before collecting them - std::cout << "[DEBUG] smt_solver::flush_statistics() called\n"; m_context.flush_statistics(); }