mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

work-coop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-08 16:10:16 -07:00
parent 49e4c2e9eb
commit 189a03c94a
2 changed files with 25 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_parallel2.cpp
View file

@ -203,6 +203,8 @@ namespace smt {
g_core.push_back(expr_ref(l2g(c), m));
}
m_search_tree.backtrack(node, g_core);
IF_VERBOSE(1, m_search_tree.display(verbose_stream() << core << "\n"););
if (m_search_tree.is_closed()) {
m_state = state::is_unsat;
cancel_workers();
@ -400,6 +402,11 @@ namespace smt {
cv.notify_all();
return false;
}
t = m_search_tree.find_active_node();
if (t) {
IF_VERBOSE(1, verbose_stream() << "found active node\n";);
break;
}
IF_VERBOSE(1, verbose_stream() << "waiting... " << id << "\n";);
cv.wait(lock);
IF_VERBOSE(1, verbose_stream() << "release... " << id << "\n";);

18
src/util/search_tree.h
View file

@ -69,6 +69,20 @@ namespace search_tree {
node* right() const { return m_right; }
node* parent() const { return m_parent; }
node* find_active_node() {
if (m_status == status::active)
return this;
if (m_status != status::open)
return nullptr;
node* nodes[2] = { m_left, m_right };
for (unsigned i = 0; i < 2; ++i) {
auto res = nodes[i] ? nodes[i]->find_active_node() : nullptr;
if (res)
return res;
}
return nullptr;
}
void display(std::ostream& out, unsigned indent) const {
for (unsigned i = 0; i < indent; ++i)
out << " ";
@ -218,6 +232,10 @@ namespace search_tree {
return nullptr;
}
node<Config>* find_active_node() {
return m_root->find_active_node();
}
bool is_closed() const {
return m_root->get_status() == status::closed;
}