mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

set up pattern to notify batch manager so worker threads can update their params according

Browse source 
ly
This commit is contained in:
Ilana Shapiro 2025-10-29 23:22:20 -07:00
parent e72cf2ec09
commit f9ae39ec49
2 changed files with 18 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/smt_parallel.cpp
View file

@ -155,7 +155,8 @@ namespace smt {
unsigned best_param_state_idx = replay_proof_prefixes(candidate_param_states); unsigned best_param_state_idx = replay_proof_prefixes(candidate_param_states);
if (best_param_state_idx != 0) { if (best_param_state_idx != 0) {
best_param_state = candidate_param_states[best_param_state_idx]; m_param_state = candidate_param_states[best_param_state_idx];
b.set_param_state(m_param_state);
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state at index " << best_param_state_idx << "\n"); IF_VERBOSE(1, verbose_stream() << " PARAM TUNER found better param state at index " << best_param_state_idx << "\n");
} else { } else {
IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n"); IF_VERBOSE(1, verbose_stream() << " PARAM TUNER retained current param state\n");
@ -192,6 +193,13 @@ namespace smt {
check_cube_start: check_cube_start:
LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n"); LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n");
// apply current best param state from batch manager
smt_params params = b.get_best_param_state();
params_ref p;
params.updt_params(p);
ctx->updt_params(p);
lbool r = check_cube(cube); lbool r = check_cube(cube);
if (!m.inc()) { if (!m.inc()) {
@ -424,6 +432,11 @@ namespace smt {
} }
} }
smt_params parallel::batch_manager::get_best_param_state() {
std::scoped_lock lock(mux);
return m_param_state;
}
void parallel::worker::collect_shared_clauses() { void parallel::worker::collect_shared_clauses() {
expr_ref_vector new_clauses = b.return_shared_clauses(m_g2l, m_shared_clause_limit, id); expr_ref_vector new_clauses = b.return_shared_clauses(m_g2l, m_shared_clause_limit, id);
// iterate over new clauses and assert them in the local context // iterate over new clauses and assert them in the local context

5
src/smt/smt_parallel.h
View file

@ -80,6 +80,7 @@ namespace smt {
std::mutex mux; std::mutex mux;
state m_state = state::is_running; state m_state = state::is_running;
stats m_stats; stats m_stats;
smt_params m_param_state;
using node = search_tree::node<cube_config>; using node = search_tree::node<cube_config>;
search_tree::tree<cube_config> m_search_tree; search_tree::tree<cube_config> m_search_tree;
@ -104,8 +105,10 @@ namespace smt {
void set_sat(ast_translation& l2g, model& m); void set_sat(ast_translation& l2g, model& m);
void set_exception(std::string const& msg); void set_exception(std::string const& msg);
void set_exception(unsigned error_code); void set_exception(unsigned error_code);
void set_param_state(smt_params const& p) { m_param_state = p; }
void collect_statistics(::statistics& st) const; void collect_statistics(::statistics& st) const;
smt_params get_best_param_state();
bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, node*& n); bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, node*& n);
void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n); void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n);
void split(ast_translation& l2g, unsigned id, node* n, expr* atom); void split(ast_translation& l2g, unsigned id, node* n, expr* atom);