mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-22 16:40:29 +00:00
Code Activity

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

Browse source
This commit is contained in:
Ilana Shapiro 2026-06-21 15:06:23 -07:00
parent 85fa14774a
commit e846b2a9e7
3 changed files with 13 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/CMakeLists.txt
View file

@ -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

12
src/params/smt_parallel_params.pyg
View file

@ -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'),
))

32
src/smt/smt_parallel.cpp
View file

@ -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 <cmath>
#include <mutex>
@ -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
#endif