extract stats with finalize for parallel mode

Z3Prover · Dec 13, 2024 · 538f74d · 538f74d
1 parent b429562
commit 538f74d
Show file tree

Hide file tree

Showing 5 changed files with 18 additions and 30 deletions.
diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp
@@ -99,7 +99,6 @@ namespace sls {
         if (!m_ddfw)
             return;
         m_result = m_ddfw->check(0, nullptr);
-        m_ddfw->collect_statistics(m_st);
         IF_VERBOSE(1, verbose_stream() << "sls-result " << m_result << "\n");
         for (auto v : m_shared_bool_vars) {
             auto w = m_smt_bool_var2sls_bool_var[v];
@@ -115,7 +114,7 @@ namespace sls {
         m_ddfw->rlimit().pop();
     }
 
-    void smt_plugin::finalize(model_ref& mdl) {
+    void smt_plugin::finalize(model_ref& mdl, ::statistics& st) {
         auto* d = m_ddfw;
         if (!d)
             return;
@@ -127,6 +126,7 @@ namespace sls {
             m_thread.join();
         SASSERT(m_completed);
         mdl = nullptr;
+        m_ddfw->collect_statistics(st);
         if (m_result == l_true && m_sls_model) {
             ast_translation tr(m_sls, m);
             mdl = m_sls_model->translate(tr);
@@ -139,10 +139,6 @@ namespace sls {
         dealloc(d); 
     }
 
-    void smt_plugin::collect_statistics(::statistics& st) const {
-        st.copy(m_st);
-    }
-
     void smt_plugin::get_shared_clauses(vector<sat::literal_vector>& _clauses) {
         _clauses.reset();
         for (auto const& clause : clauses()) {

diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
@@ -65,7 +65,6 @@ namespace sls {
 
         sat::literal_vector m_units;
         model_ref m_sls_model;
-        ::statistics m_st;
 
         bool m_new_clause_added = false; 
         unsigned m_min_unsat_size = UINT_MAX;
@@ -106,8 +105,7 @@ namespace sls {
 
         // interface to calling solver:
         void check(expr_ref_vector const& fmls, vector <sat::literal_vector> const& clauses);
-        void collect_statistics(::statistics& st) const;
-        void finalize(model_ref& md);
+        void finalize(model_ref& md, ::statistics& st);
         void get_shared_clauses(vector<sat::literal_vector>& clauses);
         void updt_params(params_ref& p) {}
         std::ostream& display(std::ostream& out) override;

diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp
@@ -72,8 +72,7 @@ namespace sls {
         if (!m_smt_plugin)
             return;
 
-        m_smt_plugin->collect_statistics(m_st);
-        m_smt_plugin->finalize(m_model);
+        m_smt_plugin->finalize(m_model, m_st);
         m_model = nullptr;
         m_smt_plugin = nullptr;
     }
@@ -90,8 +89,7 @@ namespace sls {
             return false;
         if (!m_smt_plugin->completed())
             return false;
-        m_smt_plugin->collect_statistics(m_st);
-        m_smt_plugin->finalize(m_model);
+        m_smt_plugin->finalize(m_model, m_st);
         m_smt_plugin = nullptr;
         return true;
     }

diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp
@@ -80,12 +80,10 @@ namespace smt {
         m_init_search = true;
     }
 
-    void theory_sls::finalize() {
+    void theory_sls::finalize() const {
         if (!m_smt_plugin)
             return;
-
-        m_smt_plugin->collect_statistics(m_st);
-        m_smt_plugin->finalize(m_model);
+        m_smt_plugin->finalize(m_model, m_st);
         m_model = nullptr;
         m_smt_plugin = nullptr;        
         m_init_search = false;
@@ -108,8 +106,7 @@ namespace smt {
         else if (!m_parallel_mode) 
             propagate_local_search();
         else if (m_smt_plugin->completed()) {
-            m_smt_plugin->collect_statistics(m_st);
-            m_smt_plugin->finalize(m_model);
+            m_smt_plugin->finalize(m_model, m_st);
             m_smt_plugin = nullptr;
             m_init_search = false;
         }
@@ -197,10 +194,8 @@ namespace smt {
     }
 
     void theory_sls::collect_statistics(::statistics& st) const {
-        if (m_smt_plugin)
-            m_smt_plugin->collect_statistics(st);
-        else
-            st.copy(m_st);
+        finalize();
+        st.copy(m_st);
         st.update("sls-num-guided-search", m_stats.m_num_guided_sls);
         st.update("sls-num-restart-search", m_stats.m_num_restart_sls);
     }
@@ -222,8 +217,7 @@ namespace smt {
     void theory_sls::bounded_run(unsigned num_steps) {       
         m_smt_plugin->bounded_run(num_steps);
         if (m_smt_plugin->result() == l_true) {
-            m_smt_plugin->collect_statistics(m_st);
-            m_smt_plugin->finalize(m_model);
+            m_smt_plugin->finalize(m_model, m_st);
             m_smt_plugin = nullptr;
             m_init_search = false;
         }

diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h
@@ -55,8 +55,8 @@ namespace smt {
             unsigned m_num_restart_sls = 0;
         };
         stats m_stats;
-        model_ref m_model;
-        sls::smt_plugin* m_smt_plugin = nullptr;
+        mutable model_ref m_model;
+        mutable sls::smt_plugin* m_smt_plugin = nullptr;
         unsigned m_trail_lim = 0;
         bool m_checking = false;
         bool m_parallel_mode = true;
@@ -72,11 +72,11 @@ namespace smt {
         unsigned m_after_resolve_decide_count = 0;
         unsigned m_resolve_count = 0;
         unsigned m_resolve_gap = 0;
-        bool     m_init_search = false;
-        ::statistics m_st;
+        mutable bool     m_init_search = false;
+        mutable ::statistics m_st;
         vector<sat::literal_vector> m_shared_clauses;
 
-        void finalize();
+
         void bounded_run(unsigned num_steps);
         void inc_restart_ls_steps() {
             if (m_restart_ls_steps < m_restart_ls_steps_max)
@@ -92,10 +92,12 @@ namespace smt {
         void propagate_local_search();
 
         void run_guided_sls();
+        void finalize() const;
 
     public:
         theory_sls(context& ctx);
         ~theory_sls() override;
+
         model_ref get_model() { return m_model; }
 
         // smt::theory interface