see the stats

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/cmd_context/cmd_context.cpp

@@ -17,6 +17,8 @@ Notes:
 --*/
 
 #include<signal.h>
+#include<typeinfo>
+#include "smt/smt_context.h"
 #include "util/tptr.h"
 #include "util/cancel_eh.h"
 #include "util/scoped_ctrl_c.h"
@@ -606,7 +608,8 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_manager(m),
     m_own_manager(m == nullptr),
     m_regular("stdout", std::cout),
-    m_diagnostic("stderr", std::cerr) {
+    m_diagnostic("stderr", std::cerr),
+    m_stats_collected(false) {
     SASSERT(m != 0 || !has_manager());
     install_basic_cmds(*this);
     install_ext_basic_cmds(*this);
@@ -2288,43 +2291,88 @@ void cmd_context::set_solver_factory(solver_factory * f) {
 }
 
 void cmd_context::display_statistics(bool show_total_time, double total_time) {
-    statistics st;
+    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
     if (show_total_time)
-        st.update("total time", total_time);
-    st.update("time", get_seconds());
-    get_memory_statistics(st);
-    get_rlimit_statistics(m().limit(), st);
-    if (m_check_sat_result) {
-        m_check_sat_result->collect_statistics(st);
-    }
-    else if (m_solver) {
-        m_solver->collect_statistics(st);
-    }
-    else if (m_opt) {
-        m_opt->collect_statistics(st);
-    }
-    st.display_smt2(regular_stream());
+        m_global_stats.update("total time", total_time);
+    m_global_stats.update("time", get_seconds());
+    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() {
-    // Force aggregation of theory statistics before displaying them
-    // This ensures detailed theory stats are available even on timeout/interruption
-    std::cout << "[DEBUG] cmd_context::flush_statistics() called\n";
+    // 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] Calling m_check_sat_result->flush_statistics()\n";
+        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";
     }
-    else if (m_solver) {
-        std::cout << "[DEBUG] Calling m_solver->flush_statistics()\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";
     }
-    else if (m_opt) {
+    
+    // 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";
     }
-    else {
-        std::cout << "[DEBUG] No solver object found!\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;
 }
 
 

src/cmd_context/cmd_context.h

@@ -23,6 +23,7 @@ Notes:
 #include<sstream>
 #include<vector>
 #include "util/stopwatch.h"
+#include "util/stats.h"
 #include "util/cmd_context_types.h"
 #include "util/event_handler.h"
 #include "util/sexpr.h"
@@ -43,6 +44,9 @@ Notes:
 #include "cmd_context/tactic_manager.h"
 #include "params/context_params.h"
 
+namespace smt {
+    class context;
+}
 
 class func_decls {
     func_decl * m_decls { nullptr };
@@ -302,6 +306,11 @@ protected:
     ref<opt_wrapper>             m_opt;
 
     stopwatch                    m_watch;
+    
+    // Singleton statistics object to accumulate stats throughout the run
+    // This ensures theory statistics collected during timeout are preserved
+    statistics                   m_global_stats;
+    bool                         m_stats_collected;
 
     class dt_eh : public new_datatype_eh {
         cmd_context &             m_owner;
@@ -509,6 +518,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 collect_smt_statistics(smt::context& smt_ctx);  // Collect stats from SMT context into singleton
     void display_dimacs();
     void display_parameters(std::ostream& out);
     void reset(bool finalize = false);

src/shell/smtlib_frontend.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include "util/timeout.h"
 #include "util/mutex.h"
 #include "parsers/smt2/smt2parser.h"
+#include "smt/smt_context.h"
 #include "muz/fp/dl_cmds.h"
 #include "cmd_context/extra_cmds/dbg_cmds.h"
 #include "cmd_context/extra_cmds/proof_cmds.h"
@@ -39,6 +40,7 @@ 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);
@@ -64,10 +66,26 @@ 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();
     _Exit(0);
 }
@@ -78,6 +96,17 @@ 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;
+    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;
+}
+
 void help_tactics() {
     struct cmp {
         bool operator()(tactic_cmd* a, tactic_cmd* b) const {

src/shell/smtlib_frontend.h

@@ -18,6 +18,8 @@ Revision History:
 --*/
 #pragma once
 
+namespace smt { class context; }
+
 unsigned read_smtlib_file(char const * benchmark_file);
 unsigned read_smtlib2_commands(char const * command_file);
 void help_tactics();
@@ -26,4 +28,8 @@ void help_probes();
 void help_tactic(char const* name, bool markdown);
 void help_simplifier(char const* name, bool markdown);
 
+// Functions to register/unregister the active SMT context for timeout handling
+void register_smt_context(smt::context* ctx);
+void unregister_smt_context();
+
 

src/smt/smt_context.cpp

@@ -28,6 +28,7 @@ Revision History:
 #include "ast/recfun_decl_plugin.h"
 #include "ast/proofs/proof_checker.h"
 #include "ast/ast_util.h"
+#include "shell/smtlib_frontend.h"
 #include "ast/well_sorted.h"
 #include "model/model_params.hpp"
 #include "model/model.h"
@@ -97,6 +98,9 @@ namespace smt {
             m_fparams.m_relevancy_lemma = false;
 
         m_model_generator->set_context(this);
+        
+        // Register this SMT context for timeout statistics collection
+        register_smt_context(this);
     }
 
     /**
@@ -188,6 +192,8 @@ namespace smt {
     }
 
     context::~context() {
+        // Unregister this SMT context
+        unregister_smt_context();
         flush();
         m_asserted_formulas.finalize();
     }

src/smt/smt_context_pp.cpp

@@ -26,6 +26,29 @@ Revision History:
 #endif
 
 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 {
         switch(m_last_search_failure) {
@@ -405,7 +428,9 @@ 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);
@@ -429,16 +454,6 @@ 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);

src/smt/theory_lra.cpp

@@ -4154,9 +4154,33 @@ 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";
+            }
+        }
     }        
 
     /*