mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 12:35:59 +00:00
Code Activity

add more parameters, try to fix conflict timeout inside of nlsat solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-17 12:04:53 -07:00
parent d0d8e4d9f3
commit e76f9f2615
6 changed files with 23 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/lp_settings.cpp
View file

@ -41,4 +41,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) {
m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums();
m_dio_calls_period = lp_p.dio_calls_period();
m_dio_run_gcd = lp_p.dio_run_gcd();
m_max_conflicts = p.max_conflicts();
}

5
src/math/lp/lp_settings.h
View file

@ -137,6 +137,7 @@ struct statistics {
unsigned m_bounds_tightening_conflicts = 0;
unsigned m_bounds_tightenings = 0;
unsigned m_nla_throttled_lemmas = 0;
::statistics m_st = {};
void reset() {
@ -221,11 +222,13 @@ public:
unsigned percent_of_entering_to_check = 5; // we try to find a profitable column in a percentage of the columns
bool use_scaling = true;
unsigned max_number_of_iterations_with_no_improvements = 2000000;
double time_limit; // the maximum time limit of the total run time in seconds
double time_limit; // the maximum time limit of the total run time in seconds
// end of dual section
bool m_bound_propagation = true;
bool presolve_with_double_solver_for_lar = true;
simplex_strategy_enum m_simplex_strategy;
unsigned m_max_conflicts = 0;
int report_frequency = 1000;
bool print_statistics = false;

2
src/math/lp/nla_core.cpp
View file

@ -1595,7 +1595,7 @@ lbool core::bounded_nlsat() {
scoped_rlimit sr(m_nra_lim, 100000);
ret = m_nra.check();
}
p.set_uint("max_conflicts", UINT_MAX);
p.set_uint("max_conflicts", lp_settings().m_max_conflicts);
m_nra.updt_params(p);
lp_settings().stats().m_nra_calls++;
if (ret == l_undef)

5
src/params/smt_parallel_params.pyg
View file

@ -6,5 +6,8 @@ def_module_params('smt_parallel',
('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')
('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, False, 'share only initial Boolean atoms as units'),
('cube_initial_only', BOOL, False, 'cube only on initial Boolean atoms')
))

9
src/smt/smt_parallel.cpp
View file

@ -55,7 +55,7 @@ namespace smt {
b.set_exception("context cancelled");
return;
}
LOG_WORKER(1, " checking cube: " << mk_bounded_pp(mk_and(cube), m, 3) << "\n");
LOG_WORKER(1, " checking cube: " << mk_bounded_pp(mk_and(cube), m, 3) << " max-conflicts " << m_config.m_threads_max_conflicts << "\n");
lbool r = check_cube(cube);
if (m.limit().is_canceled()) {
LOG_WORKER(1, " context cancelled\n");
@ -134,8 +134,15 @@ namespace smt {
m_config.m_never_cube = pp.never_cube();
m_config.m_share_conflicts = pp.share_conflicts();
m_config.m_share_units = pp.share_units();
m_config.m_share_units_initial_only = pp.share_units_initial_only();
m_config.m_cube_initial_only = pp.cube_initial_only();
m_config.m_max_conflict_mul = pp.max_conflict_mul();
// don't share initial units
ctx->pop_to_base_lvl();
m_num_shared_units = ctx->assigned_literals().size();
m_num_initial_atoms = ctx->get_num_bool_vars();
}
void parallel::worker::share_units(ast_translation& l2g) {

7
src/smt/smt_parallel.h
View file

@ -104,6 +104,9 @@ namespace smt {
bool m_never_cube = false;
bool m_share_conflicts = true;
bool m_share_units = true;
double m_max_conflict_mul = 1.5;
bool m_share_units_initial_only = false;
bool m_cube_initial_only = false;
};
unsigned id; // unique identifier for the worker
parallel& p;
@ -115,11 +118,12 @@ namespace smt {
scoped_ptr<context> ctx;
ast_translation m_g2l, m_l2g;
unsigned m_num_shared_units = 0;
unsigned m_num_initial_atoms = 0;
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);
lbool check_cube(expr_ref_vector const& cube);
void update_max_thread_conflicts() {
m_config.m_threads_max_conflicts *= 2;
m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
} // allow for backoff scheme of conflicts within the thread for cube timeouts.
public:
worker(unsigned id, parallel& p, expr_ref_vector const& _asms);
@ -132,7 +136,6 @@ namespace smt {
m.limit().cancel();
}
void collect_statistics(::statistics& st) const {
IF_VERBOSE(1, verbose_stream() << "Collecting statistics for worker " << id << "\n");
ctx->collect_statistics(st);
}
reslimit& limit() {