mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

extract stats with finalize for parallel mode

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-13 09:22:30 -08:00
parent b4295620b3
commit 538f74d64c
5 changed files with 18 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/sls/sls_smt_plugin.cpp
View file

@ -99,7 +99,6 @@ namespace sls {
if (!m_ddfw) if (!m_ddfw)
return; return;
m_result = m_ddfw->check(0, nullptr); m_result = m_ddfw->check(0, nullptr);
m_ddfw->collect_statistics(m_st);
IF_VERBOSE(1, verbose_stream() << "sls-result " << m_result << "\n"); IF_VERBOSE(1, verbose_stream() << "sls-result " << m_result << "\n");
for (auto v : m_shared_bool_vars) { for (auto v : m_shared_bool_vars) {
auto w = m_smt_bool_var2sls_bool_var[v]; auto w = m_smt_bool_var2sls_bool_var[v];
@ -115,7 +114,7 @@ namespace sls {
m_ddfw->rlimit().pop(); m_ddfw->rlimit().pop();
} }
void smt_plugin::finalize(model_ref& mdl) { void smt_plugin::finalize(model_ref& mdl, ::statistics& st) {
auto* d = m_ddfw; auto* d = m_ddfw;
if (!d) if (!d)
return; return;
@ -127,6 +126,7 @@ namespace sls {
m_thread.join(); m_thread.join();
SASSERT(m_completed); SASSERT(m_completed);
mdl = nullptr; mdl = nullptr;
m_ddfw->collect_statistics(st);
if (m_result == l_true && m_sls_model) { if (m_result == l_true && m_sls_model) {
ast_translation tr(m_sls, m); ast_translation tr(m_sls, m);
mdl = m_sls_model->translate(tr); mdl = m_sls_model->translate(tr);
@ -139,10 +139,6 @@ namespace sls {
dealloc(d); 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) { void smt_plugin::get_shared_clauses(vector<sat::literal_vector>& _clauses) {
_clauses.reset(); _clauses.reset();
for (auto const& clause : clauses()) { for (auto const& clause : clauses()) {

4
src/ast/sls/sls_smt_plugin.h
View file

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

6
src/sat/smt/sls_solver.cpp
View file

@ -72,8 +72,7 @@ namespace sls {
if (!m_smt_plugin) if (!m_smt_plugin)
return; return;
m_smt_plugin->collect_statistics(m_st); m_smt_plugin->finalize(m_model, m_st);
m_smt_plugin->finalize(m_model);
m_model = nullptr; m_model = nullptr;
m_smt_plugin = nullptr; m_smt_plugin = nullptr;
} }
@ -90,8 +89,7 @@ namespace sls {
return false; return false;
if (!m_smt_plugin->completed()) if (!m_smt_plugin->completed())
return false; return false;
m_smt_plugin->collect_statistics(m_st); m_smt_plugin->finalize(m_model, m_st);
m_smt_plugin->finalize(m_model);
m_smt_plugin = nullptr; m_smt_plugin = nullptr;
return true; return true;
} }

16
src/smt/theory_sls.cpp
View file

@ -80,12 +80,10 @@ namespace smt {
m_init_search = true; m_init_search = true;
} }
void theory_sls::finalize() { void theory_sls::finalize() const {
if (!m_smt_plugin) if (!m_smt_plugin)
return; return;
m_smt_plugin->finalize(m_model, m_st);
m_smt_plugin->collect_statistics(m_st);
m_smt_plugin->finalize(m_model);
m_model = nullptr; m_model = nullptr;
m_smt_plugin = nullptr; m_smt_plugin = nullptr;
m_init_search = false; m_init_search = false;
@ -108,8 +106,7 @@ namespace smt {
else if (!m_parallel_mode) else if (!m_parallel_mode)
propagate_local_search(); propagate_local_search();
else if (m_smt_plugin->completed()) { else if (m_smt_plugin->completed()) {
m_smt_plugin->collect_statistics(m_st); m_smt_plugin->finalize(m_model, m_st);
m_smt_plugin->finalize(m_model);
m_smt_plugin = nullptr; m_smt_plugin = nullptr;
m_init_search = false; m_init_search = false;
} }
@ -197,9 +194,7 @@ namespace smt {
} }
void theory_sls::collect_statistics(::statistics& st) const { void theory_sls::collect_statistics(::statistics& st) const {
if (m_smt_plugin) finalize();
m_smt_plugin->collect_statistics(st);
else
st.copy(m_st); st.copy(m_st);
st.update("sls-num-guided-search", m_stats.m_num_guided_sls); st.update("sls-num-guided-search", m_stats.m_num_guided_sls);
st.update("sls-num-restart-search", m_stats.m_num_restart_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) { void theory_sls::bounded_run(unsigned num_steps) {
m_smt_plugin->bounded_run(num_steps); m_smt_plugin->bounded_run(num_steps);
if (m_smt_plugin->result() == l_true) { if (m_smt_plugin->result() == l_true) {
m_smt_plugin->collect_statistics(m_st); m_smt_plugin->finalize(m_model, m_st);
m_smt_plugin->finalize(m_model);
m_smt_plugin = nullptr; m_smt_plugin = nullptr;
m_init_search = false; m_init_search = false;
} }

12
src/smt/theory_sls.h
View file

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