From ef66acc6b54144f10d6f64e9b557142ff438a31a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Jun 2026 12:43:58 -0700 Subject: [PATCH] change calculation of threads to use total threads indicated by parameter or processor count, subtract from worker threads based on backbone and core threads Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 21 ++++++++++++++++----- src/solver/parallel_tactical.cpp | 8 ++++++++ 2 files changed, 24 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index e8a3e83072..ed51e21271 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -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; diff --git a/src/solver/parallel_tactical.cpp b/src/solver/parallel_tactical.cpp index eab95aa586..972379ea7c 100644 --- a/src/solver/parallel_tactical.cpp +++ b/src/solver/parallel_tactical.cpp @@ -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";);