mirror of
https://github.com/Z3Prover/z3
synced 2026-05-26 20:06:22 +00:00
98153a8f30
* Initial plan * Simplify parallel SMT code: clean comments and deduplicate stat computation - Normalize tab to spaces on line 7 of smt_parallel_params.pyg - Remove extraneous blank line after ++m_num_core_minimize_calls - Replace informal retry-loop comments with professional descriptions - Extract repeated safe-division pattern into safe_ratio lambda in backbones_worker::collect_statistics Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/e0418d2f-7d4d-4980-897f-98d4057bddc3 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
12 lines
1.2 KiB
Text
12 lines
1.2 KiB
Text
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, 0, 'run Janota-style chunking backbone worker threads; default is 0 (off), supported values are 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'),
|
|
('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'),
|
|
))
|