mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-29 20:59:01 +00:00
Code Activity

add more params

Browse source
This commit is contained in:
Ilana Shapiro 2025-08-15 12:09:24 -07:00
parent 4362f2d8cb
commit 72501467bf
2 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/params/smt_parallel_params.pyg
View file

@ -4,4 +4,6 @@ def_module_params('smt_parallel',
params=( params=(
('share_units', BOOL, True, 'share units'), ('share_units', BOOL, True, 'share units'),
('share_conflicts', BOOL, True, 'share conflicts'), ('share_conflicts', BOOL, True, 'share conflicts'),
('never_cube', BOOL, False, 'never cube'),
('only_eager_cube', BOOL, False, 'only eager cube'),
)) ))

3
src/smt/smt_parallel.cpp
View file

@ -344,6 +344,9 @@ namespace smt {
// currenly, the code just implements the greedy strategy // currenly, the code just implements the greedy strategy
void parallel::batch_manager::return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& C_worker, expr_ref_vector const& A_worker) { void parallel::batch_manager::return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& C_worker, expr_ref_vector const& A_worker) {
if (smt_parallel_params(p.ctx.m_params).never_cube())
return; // portfolio only
auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) { auto atom_in_cube = [&](expr_ref_vector const& cube, expr* atom) {
return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); }); return any_of(cube, [&](expr* e) { return e == atom || (m.is_not(e, e) && e == atom); });
}; };