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

change calculation of threads to use total threads indicated by parameter or processor count, subtract from worker threads based on backbone and core threads

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-28 12:43:58 -07:00
parent 6daebef4e4
commit ef66acc6b5
2 changed files with 24 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/smt/smt_parallel.cpp
View file

@ -1860,14 +1860,25 @@ namespace smt {
lbool parallel::operator()(expr_ref_vector const &asms) {
parallel_params pp(ctx.m_params);
unsigned num_global_bb_batch_threads = pp.num_bb_threads();
if (num_global_bb_batch_threads > 2)
unsigned num_global_bb_threads = pp.num_bb_threads();
if (num_global_bb_threads > 2)
throw default_exception("parallel.num_bb_threads must be 0, 1, or 2");
unsigned num_workers = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads);
unsigned total_threads = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads);
unsigned num_workers = total_threads;
unsigned num_sls_threads = 0;
unsigned num_core_min_threads = (pp.core_minimize() ? 1 : 0);
unsigned num_global_bb_threads = num_global_bb_batch_threads;
unsigned total_threads = num_workers + num_sls_threads + num_core_min_threads + num_global_bb_threads;
if (num_workers > 2 + num_core_min_threads)
num_workers -= num_core_min_threads;
else
num_core_min_threads = 0;
if (num_workers > 2 + num_global_bb_threads)
num_workers -= num_global_bb_threads;
else
num_global_bb_threads = 0;
if (num_workers > 2 + num_sls_threads)
num_workers -= num_sls_threads;
else
num_sls_threads = 0;
IF_VERBOSE(1, verbose_stream() << "Parallel SMT with " << total_threads << " threads\n";);
ast_manager &m = ctx.m;

8
src/solver/parallel_tactical.cpp
View file

@ -1950,6 +1950,14 @@ public:
unsigned num_bb_threads = pp.num_bb_threads();
if (num_bb_threads > 2)
throw default_exception("parallel.num_bb_threads must be 0, 1, or 2");
if (num_threads > num_bb_threads + 2)
num_threads -= num_bb_threads;
else
num_bb_threads = 0;
if (core_minimize && num_threads > 2)
num_threads -= 1;
else
core_minimize = false;
unsigned total_threads = num_threads + (core_minimize ? 1 : 0) + num_bb_threads;
IF_VERBOSE(1, verbose_stream() << "Parallel tactical2 with " << total_threads << " threads\n";);