mirror of
https://github.com/Z3Prover/z3
synced 2025-10-08 17:01:55 +00:00
fix messup with closing nodes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
189a03c94a
commit
96bb3caa9e
2 changed files with 19 additions and 0 deletions
|
@ -220,6 +220,10 @@ namespace smt {
|
|||
IF_VERBOSE(1, verbose_stream() << "Batch manager splitting on literal: " << mk_bounded_pp(lit, m, 3) << "\n");
|
||||
if (m_state != state::is_running)
|
||||
return;
|
||||
// optional heuristic:
|
||||
// node->get_status() == status::active
|
||||
// and depth is 'high' enough
|
||||
// then ignore split, and instead set the status of node to open.
|
||||
m_search_tree.split(node, lit, nlit);
|
||||
cv.notify_all();
|
||||
}
|
||||
|
|
|
@ -80,6 +80,8 @@ namespace search_tree {
|
|||
if (res)
|
||||
return res;
|
||||
}
|
||||
if (m_left->get_status() == status::closed && m_right->get_status() == status::closed)
|
||||
m_status = status::closed;
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
|
@ -137,6 +139,19 @@ namespace search_tree {
|
|||
n->set_status(status::closed);
|
||||
close_node(n->left());
|
||||
close_node(n->right());
|
||||
while (n) {
|
||||
auto p = n->parent();
|
||||
if (!p)
|
||||
return;
|
||||
if (p->get_status() != status::open)
|
||||
return;
|
||||
if (p->left()->get_status() != status::closed)
|
||||
return;
|
||||
if (p->right()->get_status() != status::closed)
|
||||
return;
|
||||
p->set_status(status::closed);
|
||||
n = p;
|
||||
}
|
||||
}
|
||||
|
||||
public:
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue