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

Fix UNKNOWN bug in search tree about inconsistent end state (#8214)

Browse source 
* restore more aggressive pruning in search tree

* restore where we close children to be correct

* add core strengthening check

* fix recursion bug

* less strict core propagation

* old search tree version

* restore search tree patch

* remove flag

* debugging inconsistent end state with search, some changes need to be made in search tree, only backtrack should be closing nodes, I think the bug is when we do find_highest_attach for nonchronological backjumping, you might get to a point where the sibling is closed, so then we need to resolve further up the tree

* clean up code, fix deadlock

* delete test files

* clean up

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
This commit is contained in:
Ilana Shapiro 2026-01-16 10:41:13 -08:00 • committed by GitHub
parent 596cd23efc
commit b1b7270686
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 45 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_parallel.cpp
View file

@ -276,6 +276,7 @@ namespace smt {
IF_VERBOSE(1, m_search_tree.display(verbose_stream() << bounded_pp_exprs(core) << "\n"););
if (m_search_tree.is_closed()) {
IF_VERBOSE(1, verbose_stream() << "Search tree closed, setting UNSAT\n");
m_state = state::is_unsat;
SASSERT(p.ctx.m_unsat_core.empty());
for (auto e : m_search_tree.get_core_from_root())

51
src/util/search_tree.h
View file

@ -89,7 +89,7 @@ namespace search_tree {
node *find_active_node() {
if (m_status == status::active)
return this;
if (m_status != status::open)
if (m_status == status::closed)
return nullptr;
node *nodes[2] = {m_left, m_right};
for (unsigned i = 0; i < 2; ++i) {
@ -132,7 +132,6 @@ namespace search_tree {
random_gen m_rand;
// return an active node in the subtree rooted at n, or nullptr if there is none
// close nodes that are fully explored (whose children are all closed)
node<Config> *activate_from_root(node<Config> *n) {
if (!n)
return nullptr;
@ -152,8 +151,6 @@ namespace search_tree {
child = activate_from_root(nodes[1 - index]);
if (child)
return child;
if (left && right && left->get_status() == status::closed && right->get_status() == status::closed)
n->set_status(status::closed);
return nullptr;
}
@ -190,6 +187,39 @@ namespace search_tree {
return attach_here;
}
// Propagate closure upward via sibling resolution starting at node `cur`.
// Returns true iff global UNSAT was detected.
bool propagate_closure_upward(node<Config>* cur) {
while (true) {
node<Config>* parent = cur->parent();
if (!parent)
return false;
auto left = parent->left();
auto right = parent->right();
if (!left || !right)
return false;
if (left->get_status() != status::closed ||
right->get_status() != status::closed)
return false;
if (left->get_core().empty() ||
right->get_core().empty())
return false;
auto res = compute_sibling_resolvent(left, right);
if (res.empty()) {
close(m_root.get(), res); // global UNSAT
return true;
}
close(parent, res);
cur = parent; // keep bubbling
}
}
void close(node<Config> *n, vector<literal> const &C) {
if (!n || n->get_status() == status::closed)
return;
@ -245,6 +275,11 @@ namespace search_tree {
auto attach = find_highest_attach(p, resolvent);
close(attach, resolvent);
// try to propagate the highest attach node upward *with sibling resolution*
// this handles the case when non-chronological backjumping takes us to a node whose sibling was closed by another thread
node<Config>* cur = attach;
propagate_closure_upward(cur);
}
// Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x,
@ -312,6 +347,7 @@ namespace search_tree {
};
SASSERT(all_of(conflict, [&](auto const &a) { return on_path(a); })););
// Walk upward to find the nearest ancestor whose decision participates in the conflict
while (n) {
if (any_of(conflict, [&](auto const &a) { return a == n->get_literal(); })) {
// close the subtree under n (preserves core attached to n), and attempt to resolve upwards
@ -339,9 +375,10 @@ namespace search_tree {
auto p = n->parent();
while (p) {
if (p->left() && p->left()->get_status() == status::closed && p->right() &&
p->right()->get_status() == status::closed) {
p->set_status(status::closed);
if (p->left() && p->left()->get_status() == status::closed &&
p->right() && p->right()->get_status() == status::closed) {
if (p->get_status() != status::closed)
return nullptr; // inconsistent state
n = p;
p = n->parent();
continue;