mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 03:16:21 +00:00
Code Activity

Simplify backbone/parallel code from PR #9343

Browse source 
- search_tree.h: move #pragma once before includes (correct ordering)
- search_tree.h: replace nested ternary in display() with switch statement
- search_tree.h: move find_nonclosed_nodes_with_literal_rec to private section
- smt_parallel.cpp: simplify check_backbone return to single expression
- smt_parallel.cpp: use vector constructor instead of resize for threads
- smt_parallel.h: move comment inside update_max_thread_conflicts body

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
github-actions[bot] 2026-04-20 21:05:12 +00:00 • committed by GitHub
parent 19e95f40af
commit e10109443b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 19 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_parallel.cpp
View file

@ -601,14 +601,7 @@ namespace smt {
LOG_BB_WORKER(1, " RESULT: " << r << " FOR CANDIDATE: " << mk_bounded_pp(bb_candidate, m, 3) << "\n");
if (r == l_false) {
auto core = ctx->unsat_core();
if (core.size() == 1) {
return true;
}
}
return false;
return r == l_false && ctx->unsat_core().size() == 1;
}
void parallel::worker::share_units() {
@ -1241,8 +1234,7 @@ namespace smt {
m_batch_manager.initialize(num_global_bb_threads);
// Launch threads
vector<std::thread> threads;
threads.resize(total_threads);
vector<std::thread> threads(total_threads);
unsigned thread_idx = 0;
for (auto* w : m_workers)
threads[thread_idx++] = std::thread([&, w]() { w->run(); });

3
src/smt/smt_parallel.h
View file

@ -234,8 +234,9 @@ namespace smt {
void share_units();
void update_max_thread_conflicts() {
// allow for backoff scheme of conflicts within the thread for cube timeouts.
m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
} // allow for backoff scheme of conflicts within the thread for cube timeouts.
}
void simplify();
bb_candidates find_backbone_candidates(unsigned k = 10);

28
src/util/search_tree.h
View file

@ -32,9 +32,9 @@ Author:
--*/
#pragma once
#include "util/util.h"
#include "util/vector.h"
#pragma once
namespace search_tree {
@ -100,7 +100,11 @@ namespace search_tree {
for (unsigned i = 0; i < indent; ++i)
out << " ";
Config::display_literal(out, m_literal);
out << (get_status() == status::open ? " (o)" : get_status() == status::closed ? " (c)" : " (a)");
switch (get_status()) {
case status::open: out << " (o)"; break;
case status::closed: out << " (c)"; break;
default: out << " (a)"; break;
}
out << "\n";
if (m_left)
m_left->display(out, indent + 2);
@ -428,6 +432,15 @@ namespace search_tree {
return res;
}
void find_nonclosed_nodes_with_literal_rec(node<Config>* n, literal const& lit, ptr_vector<node<Config>>& out) {
if (!n)
return;
if (!Config::literal_is_null(n->get_literal()) && n->get_literal() == lit && n->get_status() != status::closed)
out.push_back(n);
find_nonclosed_nodes_with_literal_rec(n->left(), lit, out);
find_nonclosed_nodes_with_literal_rec(n->right(), lit, out);
}
public:
tree(literal const &null_literal) : m_null_literal(null_literal) {
reset();
@ -528,17 +541,6 @@ namespace search_tree {
find_nonclosed_nodes_with_literal_rec(m_root.get(), lit, out);
}
void find_nonclosed_nodes_with_literal_rec(node<Config>* n, literal const& lit, ptr_vector<node<Config>>& out) {
if (!n)
return;
if (!Config::literal_is_null(n->get_literal()) && n->get_literal() == lit && n->get_status() != status::closed)
out.push_back(n);
find_nonclosed_nodes_with_literal_rec(n->left(), lit, out);
find_nonclosed_nodes_with_literal_rec(n->right(), lit, out);
}
void dec_active_workers(node<Config>* n) {
if (!n)
return;