mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-21 05:06:39 +00:00
Code Activity

clean up comments

Browse source
This commit is contained in:
Ilana Shapiro 2025-10-03 16:39:32 -07:00
parent b42db215c4
commit 5143ba0118
1 changed files with 1 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/util/search_tree.h
View file

@ -163,9 +163,6 @@ namespace search_tree {
}
// Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, ¬x}
// if there are other complements in the union of the cores, they are not removed, but that is ok, because the core is
// strengthened, and these complements came from a higher-up branch, which will be resolved away recursively as we move up the tree
// in conclusion: the sibling resolvent only promises to eliminate the split variable’s literal/complement.Other complements may still appear, which is ok since they just reflect conflicts from higher up the path.
vector<literal> compute_sibling_resolvent(node<Config>* left, node<Config>* right) {
vector<literal> res;
@ -216,7 +213,7 @@ namespace search_tree {
// empty resolvent → subtree is UNSAT
if (resolvent.empty()) {
p->set_core(resolvent); // empty core
p->set_core(resolvent); // empty core
close_node(p);
p = p->parent();
continue;
@ -226,10 +223,8 @@ namespace search_tree {
if (p->has_core() && resolvent == p->get_core())
return;
//
// Bubble to the highest ancestor where ALL literals in the resolvent
// are present somewhere on the path from that ancestor to root
//
node<Config>* candidate = p;
node<Config>* attach_here = p; // fallback