mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-24 02:49:38 +00:00
Code Activity

close entire tree when sibling resolvent is empty

Browse source
This commit is contained in:
Ilana Shapiro 2025-10-04 09:18:22 -07:00
parent 5143ba0118
commit f75d137911
1 changed files with 5 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/util/search_tree.h
View file

@ -211,12 +211,11 @@ namespace search_tree {
auto resolvent = compute_sibling_resolvent(left, right); auto resolvent = compute_sibling_resolvent(left, right);
// empty resolvent → subtree is UNSAT // empty resolvent of sibling complement (i.e. tautology) -> global UNSAT
if (resolvent.empty()) { if (resolvent.empty()) {
p->set_core(resolvent); // empty core m_root->set_core(resolvent);
close_node(p); close_node(m_root.get());
p = p->parent(); return;
continue;
} }
// if p already has the same core, nothing more to do // if p already has the same core, nothing more to do
@ -288,12 +287,8 @@ namespace search_tree {
// they are a subset of literals on the path from root to n // they are a subset of literals on the path from root to n
void backtrack(node<Config>* n, vector<literal> const& conflict) { void backtrack(node<Config>* n, vector<literal> const& conflict) {
if (conflict.empty()) { if (conflict.empty()) {
m_root->set_core(conflict);
close_node(m_root.get()); close_node(m_root.get());
m_root->set_status(status::closed);
// store empty core at root to signal global unsat if you like
m_root->set_core(vector<literal>()); // optional
return; return;
} }
SASSERT(n != m_root.get()); SASSERT(n != m_root.get());