mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-30 20:38:56 +00:00
Code Activity

add set_canceled to smt_parallel to avoid deadlock

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-13 16:13:47 -07:00
parent 491d990ed1
commit f2d5d6fecf
2 changed files with 23 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/smt/smt_parallel.cpp
View file

@ -78,8 +78,10 @@ namespace smt {
lbool res = l_undef; lbool res = l_undef;
try { try {
if (!m.inc()) if (!m.inc()) {
b.set_canceled();
return; return;
}
res = m_sls->check(); res = m_sls->check();
} catch (z3_exception &ex) { } catch (z3_exception &ex) {
// Cancellation is normal in portfolio mode // Cancellation is normal in portfolio mode
@ -183,6 +185,7 @@ namespace smt {
if (!m.inc() || canceled()) if (!m.inc() || canceled())
break; break;
expr* atom = lit; expr* atom = lit;
m.is_not(lit, atom); m.is_not(lit, atom);
if (!ctx->b_internalized(atom)) if (!ctx->b_internalized(atom))
@ -218,11 +221,13 @@ namespace smt {
} }
if (!m.inc()) if (!m.inc())
return; break;
if (!canceled()) if (!canceled())
b.cancel_current_backbone_batch(); b.cancel_current_backbone_batch();
bb_candidates.reset(); bb_candidates.reset();
} }
if (!m.inc())
b.set_canceled();
} }
lbool parallel::backbones_worker::probe_literal(bool_var v, expr *e, bool is_retry) { lbool parallel::backbones_worker::probe_literal(bool_var v, expr *e, bool is_retry) {
@ -290,6 +295,7 @@ namespace smt {
} }
if (!m.inc() || canceled()) { if (!m.inc() || canceled()) {
ctx->get_fparams().m_max_conflicts = old_max_conflicts; ctx->get_fparams().m_max_conflicts = old_max_conflicts;
b.set_canceled();
return; return;
} }
if (!bb_candidate_lits.contains(lit)) // already handled in singleton core → backbone case below if (!bb_candidate_lits.contains(lit)) // already handled in singleton core → backbone case below
@ -391,7 +397,7 @@ namespace smt {
while (true) { while (true) {
if (!m.inc()) if (!m.inc())
return; break;
if (canceled()) if (canceled())
break; break;
@ -515,6 +521,8 @@ namespace smt {
bb_curr_batch_candidates.reset(); bb_curr_batch_candidates.reset();
} }
if (!m.inc())
b.set_canceled();
} }
void parallel::backbones_worker::cancel() { void parallel::backbones_worker::cancel() {
@ -655,6 +663,7 @@ namespace smt {
core.reset(); core.reset();
core.append(mus); core.append(mus);
core.append(unknown); core.append(unknown);
b.set_canceled();
return; return;
} }
@ -764,7 +773,7 @@ namespace smt {
bb_candidates local_candidates = find_backbone_candidates(); bb_candidates local_candidates = find_backbone_candidates();
b.collect_backbone_candidates(m_l2g, local_candidates); b.collect_backbone_candidates(m_l2g, local_candidates);
if (!m.inc()) if (!m.inc())
return; break;
} }
lbool r = check_cube(cube); lbool r = check_cube(cube);
@ -777,7 +786,7 @@ namespace smt {
} }
if (!m.inc()) if (!m.inc())
return; break;
switch (r) { switch (r) {
case l_undef: { case l_undef: {
@ -836,6 +845,8 @@ namespace smt {
if (m_config.m_share_units) if (m_config.m_share_units)
share_units(); share_units();
} }
if (!m.inc())
b.set_canceled();
} }
parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms) parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms)
@ -1684,6 +1695,11 @@ namespace smt {
cancel_background_threads(); cancel_background_threads();
} }
void parallel::batch_manager::set_canceled() {
std::scoped_lock lock(mux);
cancel_background_threads();
}
void parallel::batch_manager::set_exception(unsigned error_code) { void parallel::batch_manager::set_exception(unsigned error_code) {
std::scoped_lock lock(mux); std::scoped_lock lock(mux);
IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n"); IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n");

1
src/smt/smt_parallel.h
View file

@ -196,6 +196,7 @@ 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_canceled();
void collect_statistics(::statistics& st) const; void collect_statistics(::statistics& st) const;
void collect_backbone_candidates(ast_translation& l2g, bb_candidates& bb_candidates); void collect_backbone_candidates(ast_translation& l2g, bb_candidates& bb_candidates);