mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-17 09:35:38 +00:00
Code Activity

clean up code and add some comments

Browse source
This commit is contained in:
Ilana Shapiro 2026-04-13 13:56:06 -07:00
parent 013f1db739
commit ae1a456372
3 changed files with 23 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/smt_parallel.cpp
View file

@ -563,7 +563,8 @@ namespace smt {
bool parallel::batch_manager::get_cube(ast_translation &g2l, unsigned id, expr_ref_vector &cube, node_lease &lease) {
cube.reset();
std::unique_lock<std::mutex> lock(mux);
std::scoped_lock lock(mux);
if (m_search_tree.is_closed()) {
IF_VERBOSE(1, verbose_stream() << "all done\n";);
return false;
@ -572,16 +573,21 @@ namespace smt {
IF_VERBOSE(1, verbose_stream() << "aborting get_cube\n";);
return false;
}
node *t = m_search_tree.activate_node(lease.node);
if (!t)
return false;
IF_VERBOSE(1, m_search_tree.display(verbose_stream()); verbose_stream() << "\n";);
lease.node = t;
lease.epoch = t->epoch();
lease.cancel_epoch = t->cancel_epoch();
lease.cancel_epoch = t->get_cancel_epoch();
if (id >= m_worker_leases.size())
m_worker_leases.resize(id + 1);
m_worker_leases[id] = lease;
while (t) {
if (cube_config::literal_is_null(t->get_literal()))
break;
@ -590,6 +596,7 @@ namespace smt {
cube.push_back(std::move(lit));
t = t->parent();
}
return true;
}

12
src/smt/smt_parallel.h
View file

@ -45,8 +45,16 @@ namespace smt {
struct node_lease {
search_tree::node<cube_config>* node = nullptr;
unsigned epoch = 0;
unsigned cancel_epoch = 0;
// Version counter for structural mutations of this node (e.g., split/close).
// Used to detect stale leases: if a worker's lease.epoch != node.epoch,
// the node has changed since it was acquired and must not be mutated.
unsigned epoch = 0;
// Cancellation generation counter for this node/subtree.
// Incremented when the node is closed; used to signal that all
// workers holding leases on this node (or its descendants)
// must abandon work immediately.
unsigned cancel_epoch = 0;
};
class batch_manager {

8
src/util/search_tree.h
View file

@ -165,7 +165,7 @@ namespace search_tree {
void bump_epoch() {
++m_epoch;
}
unsigned cancel_epoch() const {
unsigned get_cancel_epoch() const {
return m_cancel_epoch;
}
void bump_cancel_epoch() {
@ -229,6 +229,8 @@ namespace search_tree {
select_next_node(cur->right(), target_status, best);
}
// Try to select an open node using the select_next_node policy
// If there are no open nodes, try to select an active node for portfolio solving
node<Config>* activate_best_node() {
candidate best;
select_next_node(m_root.get(), status::open, best);
@ -542,8 +544,6 @@ namespace search_tree {
}
// return an active node in the tree, or nullptr if there is none
// first check if there is a node to activate under n,
// if not, go up the tree and try to activate a sibling subtree
node<Config> *activate_node(node<Config> *n) {
if (!n) {
if (m_root->get_status() == status::active) {
@ -565,7 +565,7 @@ namespace search_tree {
}
bool is_lease_canceled(node<Config>* n, unsigned cancel_epoch) const {
return !n || n->get_status() == status::closed || n->cancel_epoch() != cancel_epoch;
return !n || n->get_status() == status::closed || n->get_cancel_epoch() != cancel_epoch;
}
vector<literal> const &get_core_from_root() const {