mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-16 06:31:28 +00:00
Code Activity

merge, and remove misleading defaults

Browse source
This commit is contained in:
Ilana Shapiro 2025-08-15 14:58:12 -07:00
commit 063c09b33d
3 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/params/smt_parallel_params.pyg
View file

@ -5,5 +5,5 @@ def_module_params('smt_parallel',
('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'), ('never_cube', BOOL, False, 'never cube'),
('only_eager_cube', BOOL, False, 'only eager cube'), ('frugal_cube_only', BOOL, False, 'only apply frugal cube strategy'),
)) ))

2
src/smt/smt_parallel.cpp
View file

@ -362,7 +362,7 @@ namespace smt {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
unsigned max_cubes = 1000; unsigned max_cubes = 1000;
bool greedy_mode = (m_cubes.size() <= max_cubes); bool greedy_mode = (m_cubes.size() <= max_cubes) && !smt_parallel_params(p.ctx.m_params).frugal_cube_only();
unsigned a_worker_start_idx = 0; unsigned a_worker_start_idx = 0;
// //

4
src/smt/smt_parallel.h
View file

@ -96,8 +96,8 @@ namespace smt {
expr_ref_vector asms; expr_ref_vector asms;
smt_params m_smt_params; smt_params m_smt_params;
scoped_ptr<context> ctx; scoped_ptr<context> ctx;
unsigned m_max_conflicts = 800; // the global budget for all work this worker can do across cubes in the current run. unsigned m_max_conflicts; // the global budget for all work this worker can do across cubes in the current run. THIS GETS SET IN THE CPP FILE
unsigned m_max_thread_conflicts = 100; // the per-cube limit for how many conflicts the worker can spend on a single cube before timing out on it and moving on unsigned m_max_thread_conflicts; // the per-cube limit for how many conflicts the worker can spend on a single cube before timing out on it and moving on. THIS GETS SET IN THE CPP FILE
unsigned m_num_shared_units = 0; unsigned m_num_shared_units = 0;
unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share unsigned m_shared_clause_limit = 0; // remembers the index into shared_clause_trail marking the boundary between "old" and "new" clauses to share
void share_units(ast_translation& l2g); void share_units(ast_translation& l2g);