mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

fix bug about needing to bubble resolvent upwards to highest ancestor

Browse source
This commit is contained in:
Ilana Shapiro 2025-10-03 10:48:47 -07:00
parent 0898813f8c
commit 279c7d4d46
1 changed files with 24 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/util/search_tree.h
View file

@ -228,12 +228,31 @@ namespace search_tree {
if (resolvent == p->get_core()) return; if (resolvent == p->get_core()) return;
} }
// attach sibling resolvent to parent p and close p node<Config>* bubble = p;
p->set_core(resolvent);
close_node(p);
// continue upward to see if parent can further resolve // is every literal in resolvent on the path from bubble up to root?
p = p->parent(); // If yes, move bubble up. If not, stop.
// Eventually, the resolvent is attached at the lowest ancestor that “covers” all those literals.
bool can_bubble = true;
while (bubble) {
for (auto const& l : resolvent) {
bool found = false;
for (node<Config>* q = bubble; q; q = q->parent()) {
if (q->get_literal() == l) { found = true; break; }
}
if (!found) { can_bubble = false; break; }
}
if (!can_bubble) break;
bubble = bubble->parent();
}
if (!bubble) bubble = p; // fallback in case nothing bubbled
// attach resolvent to the bubbled node and close it
bubble->set_core(resolvent);
close_node(bubble);
// continue upward from parent of bubbled node
p = bubble->parent();
} }
} }