mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 04:56:03 +00:00
Code Activity

move l2g and g2l to worker constructor to avoid race condition in ast_translation constructor

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-08-17 11:30:02 -07:00
parent c4607c2ba3
commit d0d8e4d9f3
2 changed files with 21 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/smt/smt_parallel.cpp
View file

@ -44,14 +44,12 @@ namespace smt {
namespace smt { namespace smt {
void parallel::worker::run() { void parallel::worker::run() {
ast_translation g2l(p.ctx.m, m); // global to local context -- MUST USE p.ctx.m, not ctx->m, AS GLOBAL MANAGER!!!
ast_translation l2g(m, p.ctx.m); // local to global context
while (m.inc()) { // inc: increase the limit and check if it is canceled, vs m.limit().is_canceled() is readonly. the .limit() is also not necessary (m.inc() etc provides a convenience wrapper) while (m.inc()) { // inc: increase the limit and check if it is canceled, vs m.limit().is_canceled() is readonly. the .limit() is also not necessary (m.inc() etc provides a convenience wrapper)
vector<expr_ref_vector> cubes; vector<expr_ref_vector> cubes;
b.get_cubes(g2l, cubes); b.get_cubes(m_g2l, cubes);
if (cubes.empty()) if (cubes.empty())
return; return;
collect_shared_clauses(g2l); collect_shared_clauses(m_g2l);
for (auto& cube : cubes) { for (auto& cube : cubes) {
if (!m.inc()) { if (!m.inc()) {
b.set_exception("context cancelled"); b.set_exception("context cancelled");
@ -75,7 +73,7 @@ namespace smt {
vector<expr_ref_vector> returned_cubes; vector<expr_ref_vector> returned_cubes;
returned_cubes.push_back(cube); returned_cubes.push_back(cube);
auto split_atoms = get_split_atoms(); auto split_atoms = get_split_atoms();
b.return_cubes(l2g, returned_cubes, split_atoms); b.return_cubes(m_l2g, returned_cubes, split_atoms);
} }
update_max_thread_conflicts(); update_max_thread_conflicts();
break; break;
@ -84,7 +82,7 @@ namespace smt {
LOG_WORKER(1, " found sat cube\n"); LOG_WORKER(1, " found sat cube\n");
model_ref mdl; model_ref mdl;
ctx->get_model(mdl); ctx->get_model(mdl);
b.set_sat(l2g, *mdl); b.set_sat(m_l2g, *mdl);
return; return;
} }
case l_false: { case l_false: {
@ -98,29 +96,31 @@ namespace smt {
// unsatisfiability does not depend on the current cube and the entire problem is unsat. // unsatisfiability does not depend on the current cube and the entire problem is unsat.
if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) {
LOG_WORKER(1, " determined formula unsat\n"); LOG_WORKER(1, " determined formula unsat\n");
b.set_unsat(l2g, unsat_core); b.set_unsat(m_l2g, unsat_core);
return; return;
} }
for (expr* e : unsat_core) for (expr* e : unsat_core)
if (asms.contains(e)) if (asms.contains(e))
b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core b.report_assumption_used(m_l2g, e); // report assumptions used in unsat core, so they can be used in final core
LOG_WORKER(1, " found unsat cube\n"); LOG_WORKER(1, " found unsat cube\n");
if (m_config.m_share_conflicts) if (m_config.m_share_conflicts)
b.collect_clause(l2g, id, mk_not(mk_and(unsat_core))); b.collect_clause(m_l2g, id, mk_not(mk_and(unsat_core)));
break; break;
} }
} }
} }
if (m_config.m_share_units) if (m_config.m_share_units)
share_units(l2g); share_units(m_l2g);
} }
} }
parallel::worker::worker(unsigned id, parallel& p, expr_ref_vector const& _asms): id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m) { parallel::worker::worker(unsigned id, parallel& p, expr_ref_vector const& _asms):
ast_translation g2l(p.ctx.m, m); id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m),
m_g2l(p.ctx.m, m),
m_l2g(m, p.ctx.m) {
for (auto e : _asms) for (auto e : _asms)
asms.push_back(g2l(e)); asms.push_back(m_g2l(e));
LOG_WORKER(1, " created with " << asms.size() << " assumptions\n"); LOG_WORKER(1, " created with " << asms.size() << " assumptions\n");
m_smt_params.m_preprocess = false; m_smt_params.m_preprocess = false;
ctx = alloc(context, m, m_smt_params, p.ctx.get_params()); ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
@ -134,6 +134,8 @@ namespace smt {
m_config.m_never_cube = pp.never_cube(); m_config.m_never_cube = pp.never_cube();
m_config.m_share_conflicts = pp.share_conflicts(); m_config.m_share_conflicts = pp.share_conflicts();
m_config.m_share_units = pp.share_units(); m_config.m_share_units = pp.share_units();
} }
void parallel::worker::share_units(ast_translation& l2g) { void parallel::worker::share_units(ast_translation& l2g) {
@ -159,10 +161,10 @@ namespace smt {
void parallel::batch_manager::init_parameters_state() { void parallel::batch_manager::init_parameters_state() {
auto& smt_params = p.ctx.get_fparams(); auto& smt_params = p.ctx.get_fparams();
std::function<std::function<void(void)>(unsigned&)> inc = [](unsigned& v) { std::function<void(void)> clo = [&]() { ++v; }; return clo; }; std::function<std::function<void(void)>(unsigned&)> inc = [](unsigned& v) { return [&]() -> void { ++v; }; };
std::function<std::function<void(void)>(unsigned&)> dec = [](unsigned& v) { std::function<void(void)> clo = [&]() { if (v > 0) --v; }; return clo; }; std::function<std::function<void(void)>(unsigned&)> dec = [](unsigned& v) { return [&]() -> void { if (v > 0) --v; }; };
std::function<std::function<void(void)>(bool&)> incb = [](bool& v) { std::function<void(void)> clo = [&]() { v = true; }; return clo; }; std::function<std::function<void(void)>(bool&)> incb = [](bool& v) { return [&]() -> void { v = true; }; };
std::function<std::function<void(void)>(bool&)> decb = [](bool& v) { std::function<void(void)> clo = [&]() { v = false; }; return clo; }; std::function<std::function<void(void)>(bool&)> decb = [](bool& v) { return [&]() -> void { v = false; }; };
std::function<parameter_state(unsigned&)> unsigned_parameter = [&](unsigned& p) -> parameter_state { std::function<parameter_state(unsigned&)> unsigned_parameter = [&](unsigned& p) -> parameter_state {
return { { { p , 1.0}}, return { { { p , 1.0}},
{ { 1.0, inc(p) }, { 1.0, dec(p) }} { { 1.0, inc(p) }, { 1.0, dec(p) }}
@ -174,11 +176,9 @@ namespace smt {
}; };
}; };
parameter_state s1 = unsigned_parameter(smt_params.m_arith_branch_cut_ratio); parameter_state s1 = unsigned_parameter(smt_params.m_arith_branch_cut_ratio);
parameter_state s2 = bool_parameter(smt_params.m_arith_eager_eq_axioms); parameter_state s2 = bool_parameter(smt_params.m_arith_eager_eq_axioms);
// arith.enable_hnf(bool) (default: true) // arith.enable_hnf(bool) (default: true)
// arith.greatest_error_pivot(bool) (default: false) // arith.greatest_error_pivot(bool) (default: false)
// arith.int_eq_branch(bool) (default: false) // arith.int_eq_branch(bool) (default: false)

1
src/smt/smt_parallel.h
View file

@ -113,6 +113,7 @@ namespace smt {
smt_params m_smt_params; smt_params m_smt_params;
config m_config; config m_config;
scoped_ptr<context> ctx; scoped_ptr<context> ctx;
ast_translation m_g2l, m_l2g;
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);