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

reinstate legacy params for smt_parallel to use for the regression tests

Browse source
This commit is contained in:
Ilana Shapiro 2026-06-20 23:18:26 -07:00
parent 6417930af5
commit ac12384d00
3 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/CMakeLists.txt
View file

@ -27,6 +27,7 @@ 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 Normal file
View file

@ -0,0 +1,12 @@
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'),
))

3
src/solver/parallel_tactical2.cpp
View file

@ -1249,8 +1249,7 @@ class parallel_solver {
goto check_cube_start;
expr_ref atom = get_split_atom(lease, cube);
if (atom) {
b.try_split(m_l2g, id, lease, atom.get(),
m_config.m_threads_max_conflicts);
b.try_split(m_l2g, id, lease, atom.get(), m_config.m_threads_max_conflicts);
}
else {
goto check_cube_start;