mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-04 22:36:10 +00:00
Code Activity

fix bug about backtracking condition being too strict: The epoch guard should not block backtrack(...) the same way it blocks try_split(...). A stale worker that proves UNSAT for n should still be able to

Browse source 
close n, and that closure should then cancel the other workers on n and its subtree.

  I changed smt/smt_parallel.cpp accordingly:

  - try_split(...) still uses epoch to reject stale structural splits
  - backtrack(...) no longer requires is_lease_valid(..., epoch); it only requires that the lease is not already canceled

  So the intended asymmetry is now restored:

  - stale split: reject
  - stale unsat/backtrack: allow closure, then cancel affected workers
This commit is contained in:
Ilana Shapiro 2026-04-13 14:15:18 -07:00
parent ae1a456372
commit dec2f2ec99
2 changed files with 5 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_parallel.cpp
View file

@ -332,7 +332,7 @@ namespace smt {
auto &lease = m_worker_leases[worker_id]; auto &lease = m_worker_leases[worker_id];
if (!lease.node || lease.node != n || lease.epoch != epoch) if (!lease.node || lease.node != n || lease.epoch != epoch)
return; return;
m_search_tree.release_worker(lease.node); m_search_tree.dec_active_workers(lease.node);
lease = {}; lease = {};
} }
@ -358,9 +358,7 @@ namespace smt {
g_core.push_back(expr_ref(l2g(c), m)); g_core.push_back(expr_ref(l2g(c), m));
} }
release_lease_unlocked(worker_id, lease.node, lease.epoch); release_lease_unlocked(worker_id, lease.node, lease.epoch);
if (lease.node && if (lease.node && !m_search_tree.is_lease_canceled(lease.node, lease.cancel_epoch))
m_search_tree.is_lease_valid(lease.node, lease.epoch) &&
!m_search_tree.is_lease_canceled(lease.node, lease.cancel_epoch))
m_search_tree.backtrack(lease.node, g_core); m_search_tree.backtrack(lease.node, g_core);
cancel_closed_leases_unlocked(worker_id); cancel_closed_leases_unlocked(worker_id);

13
src/util/search_tree.h
View file

@ -143,13 +143,10 @@ namespace search_tree {
++m_num_activations; ++m_num_activations;
++m_active_workers; ++m_active_workers;
} }
void release_worker() { void dec_active_workers() {
if (m_active_workers > 0) if (m_active_workers > 0)
--m_active_workers; --m_active_workers;
} }
unsigned active_workers() const {
return m_active_workers;
}
bool has_active_workers() const { bool has_active_workers() const {
return m_active_workers > 0; return m_active_workers > 0;
} }
@ -554,14 +551,10 @@ namespace search_tree {
return activate_best_node(); return activate_best_node();
} }
void release_worker(node<Config>* n) { void dec_active_workers(node<Config>* n) {
if (!n) if (!n)
return; return;
n->release_worker(); n->dec_active_workers();
}
bool is_lease_valid(node<Config>* n, unsigned epoch) const {
return n && n->get_status() != status::closed && n->epoch() == epoch;
} }
bool is_lease_canceled(node<Config>* n, unsigned cancel_epoch) const { bool is_lease_canceled(node<Config>* n, unsigned cancel_epoch) const {