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

Simplify parallel_tactical2.cpp: fix naming, cast, and expr_ref construction

Browse source 
- Rename shared_clause_trail → m_shared_clause_trail and
  shared_clause_set → m_shared_clause_set to match the m_ member
  naming convention used throughout batch_manager
- Replace C-style (unsigned) cast with static_cast<unsigned> for
  consistency with the same pattern on line 476
- Simplify two-step expr_ref construction in get_cube loop:
  combine default-init + assignment into a single direct construction

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
github-actions[bot] 2026-05-13 05:35:41 +00:00 • committed by GitHub
parent 85465dcc66
commit 4626b7cf22
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 13 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/solver/parallel_tactical2.cpp
View file

@ -157,8 +157,8 @@ class parallel_solver {
vector<node_lease> m_worker_leases; vector<node_lease> m_worker_leases;
/* shared clause pool (guarded by mux) */ /* shared clause pool (guarded by mux) */
vector<shared_clause> shared_clause_trail; vector<shared_clause> m_shared_clause_trail;
obj_hashtable<expr> shared_clause_set; obj_hashtable<expr> m_shared_clause_set;
/* shared backbone / unit pool (guarded by mux) */ /* shared backbone / unit pool (guarded by mux) */
obj_hashtable<expr> m_global_backbones; obj_hashtable<expr> m_global_backbones;
@ -202,10 +202,10 @@ class parallel_solver {
unsigned source_worker_id, unsigned source_worker_id,
expr* clause) { expr* clause) {
expr* g_clause = l2g(clause); expr* g_clause = l2g(clause);
if (!shared_clause_set.contains(g_clause)) { if (!m_shared_clause_set.contains(g_clause)) {
shared_clause_set.insert(g_clause); m_shared_clause_set.insert(g_clause);
shared_clause sc{source_worker_id, expr_ref(g_clause, m)}; shared_clause sc{source_worker_id, expr_ref(g_clause, m)};
shared_clause_trail.push_back(std::move(sc)); m_shared_clause_trail.push_back(std::move(sc));
} }
} }
@ -230,8 +230,8 @@ class parallel_solver {
m_search_tree.set_effort_unit(initial_max_thread_conflicts); m_search_tree.set_effort_unit(initial_max_thread_conflicts);
m_worker_leases.reset(); m_worker_leases.reset();
m_worker_leases.resize(num_workers); m_worker_leases.resize(num_workers);
shared_clause_trail.reset(); m_shared_clause_trail.reset();
shared_clause_set.reset(); m_shared_clause_set.reset();
m_global_backbones.reset(); m_global_backbones.reset();
m_model = nullptr; m_model = nullptr;
m_unsat_core.reset(); m_unsat_core.reset();
@ -300,9 +300,7 @@ class parallel_solver {
for (auto* cur = t; cur; cur = cur->parent()) { for (auto* cur = t; cur; cur = cur->parent()) {
if (solver_cube_config::literal_is_null(cur->get_literal())) if (solver_cube_config::literal_is_null(cur->get_literal()))
break; break;
expr_ref lit(g2l.to()); cube.push_back(expr_ref(g2l(cur->get_literal().get()), g2l.to()));
lit = g2l(cur->get_literal().get());
cube.push_back(std::move(lit));
} }
return true; return true;
} }
@ -391,11 +389,11 @@ class parallel_solver {
unsigned worker_id) { unsigned worker_id) {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
expr_ref_vector result(g2l.to()); expr_ref_vector result(g2l.to());
for (unsigned i = worker_limit; i < shared_clause_trail.size(); ++i) { for (unsigned i = worker_limit; i < m_shared_clause_trail.size(); ++i) {
if (shared_clause_trail[i].source_worker_id != worker_id) if (m_shared_clause_trail[i].source_worker_id != worker_id)
result.push_back(g2l(shared_clause_trail[i].clause.get())); result.push_back(g2l(m_shared_clause_trail[i].clause.get()));
} }
worker_limit = shared_clause_trail.size(); worker_limit = m_shared_clause_trail.size();
return result; return result;
} }
@ -731,7 +729,7 @@ public:
parallel_params pp(m_params); parallel_params pp(m_params);
unsigned num_threads = std::min( unsigned num_threads = std::min(
(unsigned)std::thread::hardware_concurrency(), static_cast<unsigned>(std::thread::hardware_concurrency()),
pp.threads_max()); pp.threads_max());
if (num_threads < 2) num_threads = 2; if (num_threads < 2) num_threads = 2;