mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-30 07:49:53 +00:00
Code Activity

add user params

Browse source
This commit is contained in:
Ilana Shapiro 2025-12-16 10:41:06 -08:00
parent 77cb70a082
commit 0782563e0c
3 changed files with 33 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/params/CMakeLists.txt
View file

@ -28,6 +28,7 @@ z3_add_component(params
seq_rewriter_params.pyg
sls_params.pyg
smt_params_helper.pyg
smt_parallel_params.pyg
solver_params.pyg
tactic_params.pyg
EXTRA_REGISTER_MODULE_HEADERS

25
src/params/smt_parallel_params.pyg Normal file
View file

@ -0,0 +1,25 @@
def_module_params('smt_parallel',
export=True,
description='Experimental parameters for parallel solving',
params=(
('share_units', BOOL, True, 'share units'),
('share_conflicts', BOOL, True, 'share conflicts'),
('never_cube', BOOL, False, 'never cube'),
('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'),
('relevant_units_only', BOOL, True, 'only share relvant units'),
('max_conflict_mul', DOUBLE, 1.5, 'increment multiplier for max-conflicts'),
('share_units_initial_only', BOOL, True, 'share only initial Boolean atoms as units'),
('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms'),
('max_cube_depth', UINT, 20, 'maximum depth (size) of a cube to share'),
('max_greedy_cubes', UINT, 1000, 'maximum number of cube to greedily share before switching to frugal'),
('num_split_lits', UINT, 2, 'how many literals, k, we split on to create 2^k cubes'),
('depth_splitting_only', BOOL, False, 'only apply frugal cube strategy, and only on deepest (biggest) cubes from the batch manager'),
('backbone_detection', BOOL, False, 'apply backbone literal heuristic'),
('iterative_deepening', BOOL, False, 'deepen cubes based on iterative hardness cutoff heuristic'),
('beam_search', BOOL, False, 'use beam search with PQ to rank cubes given to threads'),
('explicit_hardness', BOOL, False, 'use explicit hardness metric for cube'),
('cubetree', BOOL, False, 'use cube tree data structure for storing cubes'),
('searchtree', BOOL, False, 'use search tree implementation (parallel2)'),
('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'),
('inprocessing_delay', UINT, 0, 'number of undef before invoking simplification'),
))

8
src/smt/smt_parallel.cpp
View file

@ -25,6 +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 <cmath>
#include <mutex>
@ -121,8 +122,10 @@ namespace smt {
break;
}
}
if (m_config.m_share_units)
if (m_config.m_share_units) {
IF_VERBOSE(1, verbose_stream() << " Sharing units\n");
share_units();
}
}
}
@ -141,6 +144,9 @@ namespace smt {
m_num_shared_units = ctx->assigned_literals().size();
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_share_units = pp.share_units();
}
void parallel::worker::share_units() {