t0

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

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<std::pair<expr*,expr*>> cmd_context::tracked_assertions() {
     vector<std::pair<expr*,expr*>> result;

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);

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);
 }

src/smt/smt_context.cpp

@@ -3049,6 +3049,15 @@ namespace smt {
     void context::flush() {
         flet<bool> 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;

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;
 

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);

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() {
     }

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.
         */

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);

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) {

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(); }