From e846b2a9e7036e4daf87b7d5288dee4f31b4d374 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Sun, 21 Jun 2026 15:06:23 -0700 Subject: [PATCH] smt_parallel is back to using parallel_params only, removing smt_parallel_params.pyg, legacy params (e.g. inprocessing, sls, failed_literal_mode for bb) are hardcoded --- src/params/CMakeLists.txt | 1 - src/params/smt_parallel_params.pyg | 12 ----------- src/smt/smt_parallel.cpp | 32 ++++++++++++------------------ 3 files changed, 13 insertions(+), 32 deletions(-) delete mode 100644 src/params/smt_parallel_params.pyg diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt index 98c006279..9aea5b918 100644 --- a/src/params/CMakeLists.txt +++ b/src/params/CMakeLists.txt @@ -27,7 +27,6 @@ z3_add_component(params sat_params.pyg seq_rewriter_params.pyg sls_params.pyg - smt_parallel_params.pyg smt_params_helper.pyg solver_params.pyg tactic_params.pyg diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg deleted file mode 100644 index b8b47cb55..000000000 --- a/src/params/smt_parallel_params.pyg +++ /dev/null @@ -1,12 +0,0 @@ -def_module_params('smt_parallel', - export=True, - description='Experimental parameters for parallel solving', - params=( - ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'), - ('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'), - ('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'), - ('num_global_bb_batch_threads', UINT, 2, 'run Janota-style chunking backbone worker threads; defaults to parallel.num_bb_threads when unset; supported values are 0 (off), 1 (negative mode only) or 2 (negative and positive mode)'), - ('local_backbones', BOOL, False, 'enable local backbones experiment within the search tree parallelism'), - ('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking; defaults to parallel.core_minimize when unset'), - ('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'), - )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index fdad743e3..6d53b96a2 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -25,7 +25,7 @@ Author: #include "smt/smt_parallel.h" #include "smt/smt_lookahead.h" #include "solver/solver_preprocess.h" -#include "params/smt_parallel_params.hpp" +#include "solver/parallel_params.hpp" #include #include @@ -854,10 +854,10 @@ namespace smt { m_num_initial_atoms = ctx->get_num_bool_vars(); ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged - smt_parallel_params pp(p.ctx.m_params); - m_config.m_inprocessing = pp.inprocessing(); - m_config.m_global_backbones = pp.num_global_bb_batch_threads() > 0 || pp.num_global_bb_fl_threads() > 0; - m_config.m_local_backbones = pp.local_backbones(); + parallel_params pp(p.ctx.m_params); + m_config.m_inprocessing = false; + m_config.m_global_backbones = pp.num_bb_threads() > 0; + m_config.m_local_backbones = false; m_config.m_core_minimize = pp.core_minimize(); m_config.m_ablate_backtracking = pp.ablate_backtracking(); @@ -889,8 +889,7 @@ namespace smt { m_num_initial_atoms = ctx->get_num_bool_vars(); ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged - smt_parallel_params pp(p.ctx.m_params); - m_use_failed_literal_test = pp.num_global_bb_fl_threads() > 0; + m_use_failed_literal_test = false; } parallel::bb_candidates parallel::worker::find_backbone_candidates(unsigned k) { @@ -1779,7 +1778,7 @@ namespace smt { m_worker_leases.reset(); m_worker_leases.resize(p.m_workers.size()); - smt_parallel_params pp(p.ctx.m_params); + parallel_params pp(p.ctx.m_params); m_ablate_backtracking = pp.ablate_backtracking(); } @@ -1794,19 +1793,14 @@ namespace smt { } lbool parallel::operator()(expr_ref_vector const &asms) { - smt_parallel_params pp(ctx.m_params); - unsigned num_global_bb_batch_threads = pp.num_global_bb_batch_threads(); + parallel_params pp(ctx.m_params); + unsigned num_global_bb_batch_threads = pp.num_bb_threads(); if (num_global_bb_batch_threads > 2) - throw default_exception("smt_parallel.num_global_bb_batch_threads must be 0, 1, or 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 num_sls_threads = (pp.sls() ? 1 : 0); + unsigned num_sls_threads = 0; unsigned num_core_min_threads = (pp.core_minimize() ? 1 : 0); - unsigned num_global_bb_fl_threads = pp.num_global_bb_fl_threads(); - if (num_global_bb_fl_threads > 2) - throw default_exception("smt_parallel.num_global_bb_fl_threads must be 0, 1, or 2"); - if (num_global_bb_fl_threads > 0 && num_global_bb_batch_threads > 0) - throw default_exception("smt_parallel.num_global_bb_fl_threads and smt_parallel.num_global_bb_batch_threads cannot both be enabled"); - unsigned num_global_bb_threads = num_global_bb_fl_threads > 0 ? num_global_bb_fl_threads : num_global_bb_batch_threads; + 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_VERBOSE(1, verbose_stream() << "Parallel SMT with " << total_threads << " threads\n";); @@ -1888,4 +1882,4 @@ namespace smt { } } // namespace smt -#endif \ No newline at end of file +#endif