mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

remove parallal_stats

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-06-11 14:51:28 -07:00
parent 6ef8660adb
commit e06ca1489e
3 changed files with 6 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_solver.cpp
View file

@ -279,18 +279,6 @@ namespace {
return const_cast<smt::kernel&>(m_context).get_context().get_fparams().m_max_conflicts;
}
void reset_parallel_statistics() override {
m_context.reset_aux_statistics();
}
void add_parallel_statistics(statistics const& st) override {
m_context.add_aux_statistics(st);
}
void collect_parallel_statistics(statistics& st) const override {
m_context.collect_statistics(st);
}
void get_backbone_candidates(vector<solver::scored_literal>& candidates, unsigned max_num) override {
ast_manager& m = get_manager();
auto& ctx = m_context.get_context();

12
src/solver/parallel_tactical2.cpp
View file

@ -1893,28 +1893,28 @@ public:
for (auto& t : threads)
t.join();
m_solver->reset_parallel_statistics();
m_solver->reset_statistics();
statistics aux;
for (auto* w : m_workers) {
aux.reset();
w->collect_statistics(aux);
m_solver->add_parallel_statistics(aux);
m_solver->add_statistics(aux);
}
aux.reset();
m_batch_manager.collect_statistics(aux);
m_solver->add_parallel_statistics(aux);
m_solver->add_statistics(aux);
if (m_core_minimizer_worker) {
aux.reset();
m_core_minimizer_worker->collect_statistics(aux);
m_solver->add_parallel_statistics(aux);
m_solver->add_statistics(aux);
}
for (auto* w : m_global_backbones_workers) {
aux.reset();
w->collect_statistics(aux);
m_solver->add_parallel_statistics(aux);
m_solver->add_statistics(aux);
}
m_stats.reset();
m_solver->collect_parallel_statistics(m_stats);
m_solver->collect_statistics(m_stats);
m_manager.limit().reset_cancel();

13
src/solver/solver.h
View file

@ -57,7 +57,6 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p, symbol const& logic
class solver : public check_sat_result, public user_propagator::core {
params_ref m_params;
symbol m_cancel_backup_file;
statistics m_parallel_stats;
public:
struct scored_literal {
expr_ref lit;
@ -330,18 +329,6 @@ public:
virtual unsigned get_max_conflicts() const { return UINT_MAX; }
virtual void reset_parallel_statistics() {
m_parallel_stats.reset();
}
virtual void add_parallel_statistics(statistics const& st) {
m_parallel_stats.copy(st);
}
virtual void collect_parallel_statistics(statistics& st) const {
st.copy(m_parallel_stats);
collect_statistics(st);
}
virtual void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) = 0;