mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

ablate to no backtracking on stale leases

Browse source
This commit is contained in:
Ilana Shapiro 2026-04-13 15:49:54 -07:00 • committed by Ilana Shapiro
parent dec2f2ec99
commit 60b4dff428
2 changed files with 11 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_parallel.cpp
View file

@ -358,7 +358,13 @@ namespace smt {
g_core.push_back(expr_ref(l2g(c), m));
}
release_lease_unlocked(worker_id, lease.node, lease.epoch);
if (lease.node && !m_search_tree.is_lease_canceled(lease.node, lease.cancel_epoch))
// only backtrack if the lease is still valid (i.e., the worker has not been given a new node to work on or the lease has not been canceled by another worker)
// this means we can potentially delay backtracking for some unsat cubes until another worker (whose lease is valid) determines it UNSAT.
// Empirically, this is better than aggressively backtracking on every unsat cube, for now.
if (lease.node &&
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);
cancel_closed_leases_unlocked(worker_id);

4
src/util/search_tree.h
View file

@ -557,6 +557,10 @@ namespace search_tree {
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 {
return !n || n->get_status() == status::closed || n->get_cancel_epoch() != cancel_epoch;
}