diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt index 9aea5b918..98c006279 100644 --- a/src/params/CMakeLists.txt +++ b/src/params/CMakeLists.txt @@ -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 diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg new file mode 100644 index 000000000..b8b47cb55 --- /dev/null +++ b/src/params/smt_parallel_params.pyg @@ -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'), + )) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 79c50c5bb..dafcfa759 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -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;