From 52fd59df1b0d628b16515725adc90f790f9921cd Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Sat, 11 Oct 2025 06:58:14 -0700 Subject: [PATCH 1/6] Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960) * draft attempt at optimizing cube tree with resolvents. have not tested/ran yet * adding comments * fix bug about needing to bubble resolvent upwards to highest ancestor * fix bug where we need to cover the whole resolvent in the path when bubbling up * clean up comments * close entire tree when sibling resolvent is empty * integrate asms directly into cube tree, remove separate tracking * try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function * separate the logic again to avoid mutual recursion --- src/smt/smt_parallel.cpp | 27 ++---- src/smt/smt_parallel.h | 7 -- src/util/search_tree.h | 177 ++++++++++++++++++++++++++++++++------- 3 files changed, 156 insertions(+), 55 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 5d1f61586..74aa43d1c 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -115,10 +115,6 @@ namespace smt { b.set_unsat(m_l2g, unsat_core); return; } - // report assumptions used in unsat core, so they can be used in final core - for (expr *e : unsat_core) - if (asms.contains(e)) - b.report_assumption_used(m_l2g, e); LOG_WORKER(1, " found unsat cube\n"); b.backtrack(m_l2g, unsat_core, node); @@ -260,8 +256,7 @@ namespace smt { vector g_core; for (auto c : core) { expr_ref g_c(l2g(c), m); - if (!is_assumption(g_c)) - g_core.push_back(expr_ref(l2g(c), m)); + g_core.push_back(expr_ref(l2g(c), m)); } m_search_tree.backtrack(node, g_core); @@ -411,11 +406,6 @@ namespace smt { cancel_workers(); } - void parallel::batch_manager::report_assumption_used(ast_translation &l2g, expr *assumption) { - std::scoped_lock lock(mux); - p.m_assumptions_used.insert(l2g(assumption)); - } - lbool parallel::batch_manager::get_result() const { if (m.limit().is_canceled()) return l_undef; // the main context was cancelled, so we return undef. @@ -424,11 +414,12 @@ namespace smt { // means all cubes were unsat if (!m_search_tree.is_closed()) throw default_exception("inconsistent end state"); - if (!p.m_assumptions_used.empty()) { - // collect unsat core from assumptions used, if any --> case when all cubes were unsat, but depend on - // nonempty asms, so we need to add these asms to final unsat core - SASSERT(p.ctx.m_unsat_core.empty()); - for (auto a : p.m_assumptions_used) + + // case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core + // these asms are stored in the cube tree, at the root node + if (p.ctx.m_unsat_core.empty()) { + SASSERT(root && root->is_closed()); + for (auto a : m_search_tree.get_core_from_root()) p.ctx.m_unsat_core.push_back(a); } return l_false; @@ -496,16 +487,12 @@ namespace smt { scoped_clear(parallel &p) : p(p) {} ~scoped_clear() { p.m_workers.reset(); - p.m_assumptions_used.reset(); - p.m_assumptions.reset(); } }; scoped_clear clear(*this); m_batch_manager.initialize(); m_workers.reset(); - for (auto e : asms) - m_assumptions.insert(e); scoped_limits sl(m.limit()); flet _nt(ctx.m_fparams.m_threads, 1); SASSERT(num_threads > 1); diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 5851835b7..3c47d818d 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -79,10 +79,6 @@ namespace smt { void init_parameters_state(); - bool is_assumption(expr* e) const { - return p.m_assumptions.contains(e); - } - public: batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)) { } @@ -98,7 +94,6 @@ namespace smt { void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n); void split(ast_translation& l2g, unsigned id, node* n, expr* atom); - void report_assumption_used(ast_translation& l2g, expr* assumption); void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause); expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id); @@ -162,8 +157,6 @@ namespace smt { }; - obj_hashtable m_assumptions_used; // assumptions used in unsat cores, to be used in final core - obj_hashtable m_assumptions; // all assumptions batch_manager m_batch_manager; scoped_ptr_vector m_workers; diff --git a/src/util/search_tree.h b/src/util/search_tree.h index c2bae663c..2f0d29bec 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -41,6 +41,7 @@ namespace search_tree { literal m_literal; node* m_left = nullptr, * m_right = nullptr, * m_parent = nullptr; status m_status; + vector m_core; public: node(literal const& l, node* parent) : m_literal(l), m_parent(parent), m_status(status::open) {} @@ -96,6 +97,13 @@ namespace search_tree { if (m_right) m_right->display(out, indent + 2); } + + bool has_core() const { return !m_core.empty(); } + void set_core(vector const &core) { + m_core = core; + } + vector const & get_core() const { return m_core; } + void clear_core() { m_core.clear(); } }; template @@ -131,31 +139,139 @@ namespace search_tree { return nullptr; } - void close_node(node* n) { - if (!n) - return; - if (n->get_status() == status::closed) - return; - 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; - } - } + // Invariants: + // Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption literals. + // If a parent is open, then the one of the children is open. + void close_with_core(node* n, vector const &C, bool allow_resolve = true) { + if (!n || n->get_status() == status::closed) + return; + + n->set_core(C); + n->set_status(status::closed); + + close_with_core(n->left(), C, false); + close_with_core(n->right(), C, false); + + // stop at root + if (!n->parent()) return; + + node* p = n->parent(); + if (!p) return; // root reached + + auto is_literal_in_core = [](literal const& l, vector const& C) { + for (unsigned i = 0; i < C.size(); ++i) + if (C[i] == l) return true; + return false; + }; + + // case 1: current splitting literal not in the conflict core + if (!is_literal_in_core(n->get_literal(), C)) { + close_with_core(p, C); + // case 2: both siblings closed -> resolve + } else if (allow_resolve && p->left()->get_status() == status::closed && p->right()->get_status() == status::closed) { + try_resolve_upwards(p); + } + } + + // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, ¬x} + vector compute_sibling_resolvent(node* left, node* right) { + vector res; + + if (!left->has_core() || !right->has_core()) return res; + + bool are_sibling_complements = left->parent() == right->parent(); + if (!are_sibling_complements) + return res; + + auto &core_l = left->get_core(); + auto &core_r = right->get_core(); + + auto contains = [](vector const &v, literal const &l) { + for (unsigned i = 0; i < v.size(); ++i) + if (v[i] == l) return true; + return false; + }; + + auto lit_l = left->get_literal(); + auto lit_r = right->get_literal(); + + // Add literals from left core, skipping lit_l + for (unsigned i = 0; i < core_l.size(); ++i) { + if (core_l[i] != lit_l && !contains(res, core_l[i])) + res.push_back(core_l[i]); + } + + // Add literals from right core, skipping lit_r + for (unsigned i = 0; i < core_r.size(); ++i) { + if (core_r[i] != lit_r && !contains(res, core_r[i])) + res.push_back(core_r[i]); + } + + return res; + } + + void try_resolve_upwards(node* p) { + while (p) { + auto left = p->left(); + auto right = p->right(); + if (!left || !right) return; + + // only attempt when both children are closed and each has a core + if (left->get_status() != status::closed || right->get_status() != status::closed) return; + if (!left->has_core() || !right->has_core()) return; + + auto resolvent = compute_sibling_resolvent(left, right); + + // empty resolvent of sibling complement (i.e. tautology) -> global UNSAT + if (resolvent.empty()) { + close_with_core(m_root.get(), resolvent, false); + return; + } + + // if p already has the same core, nothing more to do + 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* candidate = p; + node* attach_here = p; // fallback + + while (candidate) { + bool all_found = true; + + for (auto const& r : resolvent) { + bool found = false; + for (node* q = candidate; q; q = q->parent()) { + if (q->get_literal() == r) { + found = true; + break; + } + } + if (!found) { + all_found = false; + break; + } + } + + if (all_found) { + attach_here = candidate; // bubble up to this node + } + + candidate = candidate->parent(); + } + + // attach the resolvent and close the subtree at attach_here + if (!attach_here->has_core() || attach_here->get_core() != resolvent) { + close_with_core(attach_here, resolvent, false); + } + + // continue upward from parent of attach_here + p = attach_here->parent(); + } + } public: - tree(literal const& null_literal) : m_null_literal(null_literal) { reset(); } @@ -176,11 +292,10 @@ namespace search_tree { } // conflict is given by a set of literals. - // they are a subset of literals on the path from root to n + // they are subsets of the literals on the path from root to n AND the external assumption literals void backtrack(node* n, vector const& conflict) { if (conflict.empty()) { - close_node(m_root.get()); - m_root->set_status(status::closed); + close_with_core(m_root.get(), conflict); return; } SASSERT(n != m_root.get()); @@ -198,12 +313,14 @@ namespace search_tree { }; SASSERT(all_of(conflict, [&](auto const& a) { return on_path(a); })); ); - + while (n) { if (any_of(conflict, [&](auto const& a) { return a == n->get_literal(); })) { - close_node(n); + // close the subtree under n (preserves core attached to n), and attempt to resolve upwards + close_with_core(n, conflict); return; } + n = n->parent(); } UNREACHABLE(); @@ -252,6 +369,10 @@ namespace search_tree { return m_root->find_active_node(); } + vector const& get_core_from_root() const { + return m_root->get_core(); + } + bool is_closed() const { return m_root->get_status() == status::closed; } From e4cc27810f35007a48fe3dd8c9084f26a8b433a9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Oct 2025 15:42:20 -0700 Subject: [PATCH 2/6] Refactor search tree closure and resolution logic Refactor close_with_core to simplify logic and remove unnecessary parameters. Update sibling resolvent computation and try_resolve_upwards for clarity. --- src/util/search_tree.h | 134 ++++++++++------------------------------- 1 file changed, 33 insertions(+), 101 deletions(-) diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 2f0d29bec..a6ac17af7 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -139,136 +139,68 @@ namespace search_tree { return nullptr; } + void close(node* n) { + if (!n || n->get_status() == status::closed) + return; + n->set_status(status::closed); + close(n->left); + close(n->right); + } + // Invariants: // Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption literals. // If a parent is open, then the one of the children is open. - void close_with_core(node* n, vector const &C, bool allow_resolve = true) { + void close_with_core(node* n, vector const &C) { if (!n || n->get_status() == status::closed) return; - + node* p = n->parent(); + if (p && any_of(C, [](auto const& l) { return l == n->get_literal(); }})) { + close_with_core(p, C); + return; + } + close(n->left()); + close(n->right()); n->set_core(C); n->set_status(status::closed); - close_with_core(n->left(), C, false); - close_with_core(n->right(), C, false); - - // stop at root - if (!n->parent()) return; - - node* p = n->parent(); - if (!p) return; // root reached - - auto is_literal_in_core = [](literal const& l, vector const& C) { - for (unsigned i = 0; i < C.size(); ++i) - if (C[i] == l) return true; - return false; - }; - - // case 1: current splitting literal not in the conflict core - if (!is_literal_in_core(n->get_literal(), C)) { - close_with_core(p, C); - // case 2: both siblings closed -> resolve - } else if (allow_resolve && p->left()->get_status() == status::closed && p->right()->get_status() == status::closed) { - try_resolve_upwards(p); - } + if (p) + try_resolve_upwards(p); } // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, ¬x} vector compute_sibling_resolvent(node* left, node* right) { vector res; - if (!left->has_core() || !right->has_core()) return res; - - bool are_sibling_complements = left->parent() == right->parent(); - if (!are_sibling_complements) - return res; - auto &core_l = left->get_core(); auto &core_r = right->get_core(); - - auto contains = [](vector const &v, literal const &l) { - for (unsigned i = 0; i < v.size(); ++i) - if (v[i] == l) return true; - return false; - }; + + if (core_l.empty() || core_r.empty() || left->parent() != right->parent()) + return res; auto lit_l = left->get_literal(); auto lit_r = right->get_literal(); - // Add literals from left core, skipping lit_l - for (unsigned i = 0; i < core_l.size(); ++i) { - if (core_l[i] != lit_l && !contains(res, core_l[i])) - res.push_back(core_l[i]); - } - - // Add literals from right core, skipping lit_r - for (unsigned i = 0; i < core_r.size(); ++i) { - if (core_r[i] != lit_r && !contains(res, core_r[i])) - res.push_back(core_r[i]); - } - + for (auto const& lit : core_l) + if (lit != lit_l && !res.contains(lit)) + res.push_back(lit); + for (auto const& lit : core_r) + if (lit != lit_l && !res.contains(lit)) + res.push_back(lit); return res; } void try_resolve_upwards(node* p) { - while (p) { auto left = p->left(); auto right = p->right(); - if (!left || !right) return; + if (!left || !right) + return; // only attempt when both children are closed and each has a core - if (left->get_status() != status::closed || right->get_status() != status::closed) return; - if (!left->has_core() || !right->has_core()) return; + if (left->get_status() != status::closed || right->get_status() != status::closed) + return; auto resolvent = compute_sibling_resolvent(left, right); - - // empty resolvent of sibling complement (i.e. tautology) -> global UNSAT - if (resolvent.empty()) { - close_with_core(m_root.get(), resolvent, false); - return; - } - - // if p already has the same core, nothing more to do - 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* candidate = p; - node* attach_here = p; // fallback - - while (candidate) { - bool all_found = true; - - for (auto const& r : resolvent) { - bool found = false; - for (node* q = candidate; q; q = q->parent()) { - if (q->get_literal() == r) { - found = true; - break; - } - } - if (!found) { - all_found = false; - break; - } - } - - if (all_found) { - attach_here = candidate; // bubble up to this node - } - - candidate = candidate->parent(); - } - - // attach the resolvent and close the subtree at attach_here - if (!attach_here->has_core() || attach_here->get_core() != resolvent) { - close_with_core(attach_here, resolvent, false); - } - - // continue upward from parent of attach_here - p = attach_here->parent(); - } + close_with_core(p, resolvent); } public: @@ -383,4 +315,4 @@ namespace search_tree { } }; -} \ No newline at end of file +} From e95162b05409b67b23143b4c914bb97b90401c97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Oct 2025 01:00:41 +0200 Subject: [PATCH 3/6] apply formatting Signed-off-by: Nikolaj Bjorner --- src/util/search_tree.h | 392 ++++++++++++++++++++++------------------- 1 file changed, 206 insertions(+), 186 deletions(-) diff --git a/src/util/search_tree.h b/src/util/search_tree.h index a6ac17af7..91a81bd60 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -14,7 +14,7 @@ Abstract: - Closed nodes are fully explored (both children are closed). - Active nodes have no children and are currently being explored. - Open nodes either have children that are open or are leaves. - + A node can be split if it is active. After splitting, it becomes open and has two open children. Backtracking on a conflict closes all nodes below the last node whose atom is in the conflict set. @@ -35,26 +35,33 @@ namespace search_tree { enum class status { open, closed, active }; - template - class node { + template class node { typedef typename Config::literal literal; literal m_literal; - node* m_left = nullptr, * m_right = nullptr, * m_parent = nullptr; + node *m_left = nullptr, *m_right = nullptr, *m_parent = nullptr; status m_status; vector m_core; + public: - node(literal const& l, node* parent) : - m_literal(l), m_parent(parent), m_status(status::open) {} + node(literal const &l, node *parent) : m_literal(l), m_parent(parent), m_status(status::open) {} ~node() { dealloc(m_left); dealloc(m_right); } - status get_status() const { return m_status; } - void set_status(status s) { m_status = s; } - literal const& get_literal() const { return m_literal; } - bool literal_is_null() const { return Config::is_null(m_literal); } - void split(literal const& a, literal const& b) { + status get_status() const { + return m_status; + } + void set_status(status s) { + m_status = s; + } + literal const &get_literal() const { + return m_literal; + } + bool literal_is_null() const { + return Config::is_null(m_literal); + } + void split(literal const &a, literal const &b) { SASSERT(!Config::literal_is_null(a)); SASSERT(!Config::literal_is_null(b)); if (m_status != status::active) @@ -66,16 +73,22 @@ namespace search_tree { m_status = status::open; } - node* left() const { return m_left; } - node* right() const { return m_right; } - node* parent() const { return m_parent; } + node *left() const { + return m_left; + } + node *right() const { + return m_right; + } + node *parent() const { + return m_parent; + } - node* find_active_node() { + node *find_active_node() { if (m_status == status::active) return this; if (m_status != status::open) return nullptr; - node* nodes[2] = { m_left, m_right }; + node *nodes[2] = {m_left, m_right}; for (unsigned i = 0; i < 2; ++i) { auto res = nodes[i] ? nodes[i]->find_active_node() : nullptr; if (res) @@ -86,7 +99,7 @@ namespace search_tree { return nullptr; } - void display(std::ostream& out, unsigned indent) const { + void display(std::ostream &out, unsigned indent) const { for (unsigned i = 0; i < indent; ++i) out << " "; Config::display_literal(out, m_literal); @@ -98,16 +111,21 @@ namespace search_tree { m_right->display(out, indent + 2); } - bool has_core() const { return !m_core.empty(); } - void set_core(vector const &core) { + bool has_core() const { + return !m_core.empty(); + } + void set_core(vector const &core) { m_core = core; } - vector const & get_core() const { return m_core; } - void clear_core() { m_core.clear(); } + vector const &get_core() const { + return m_core; + } + void clear_core() { + m_core.clear(); + } }; - template - class tree { + template class tree { typedef typename Config::literal literal; scoped_ptr> m_root = nullptr; literal m_null_literal; @@ -115,7 +133,7 @@ namespace search_tree { // 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* activate_from_root(node* n) { + node *activate_from_root(node *n) { if (!n) return nullptr; if (n->get_status() != status::open) @@ -126,7 +144,7 @@ namespace search_tree { n->set_status(status::active); return n; } - node* nodes[2] = { left, right }; + node *nodes[2] = {left, right}; unsigned index = m_rand(2); auto child = activate_from_root(nodes[index]); if (child) @@ -134,185 +152,187 @@ 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); + if (left && right && left->get_status() == status::closed && right->get_status() == status::closed) + n->set_status(status::closed); return nullptr; } - void close(node* n) { - if (!n || n->get_status() == status::closed) + void close(node *n) { + if (!n || n->get_status() == status::closed) return; - n->set_status(status::closed); - close(n->left); - close(n->right); + n->set_status(status::closed); + close(n->left); + close(n->right); } - // Invariants: - // Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption literals. - // If a parent is open, then the one of the children is open. - void close_with_core(node* n, vector const &C) { - if (!n || n->get_status() == status::closed) - return; - node* p = n->parent(); - if (p && any_of(C, [](auto const& l) { return l == n->get_literal(); }})) { - close_with_core(p, C); - return; - } - close(n->left()); - close(n->right()); - n->set_core(C); - n->set_status(status::closed); - - if (p) - try_resolve_upwards(p); - } - - // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, ¬x} - vector compute_sibling_resolvent(node* left, node* right) { - vector res; - - auto &core_l = left->get_core(); - auto &core_r = right->get_core(); - - if (core_l.empty() || core_r.empty() || left->parent() != right->parent()) - return res; - - auto lit_l = left->get_literal(); - auto lit_r = right->get_literal(); - - for (auto const& lit : core_l) - if (lit != lit_l && !res.contains(lit)) - res.push_back(lit); - for (auto const& lit : core_r) - if (lit != lit_l && !res.contains(lit)) - res.push_back(lit); - return res; - } - - void try_resolve_upwards(node* p) { - auto left = p->left(); - auto right = p->right(); - if (!left || !right) - return; - - // only attempt when both children are closed and each has a core - if (left->get_status() != status::closed || right->get_status() != status::closed) - return; - - auto resolvent = compute_sibling_resolvent(left, right); - close_with_core(p, resolvent); - } - - public: - tree(literal const& null_literal) : m_null_literal(null_literal) { - reset(); - } - - void set_seed(unsigned seed) { - m_rand.set_seed(seed); - } - - void reset() { - m_root = alloc(node, m_null_literal, nullptr); - m_root->set_status(status::active); - } - - // Split current node if it is active. - // After the call, n is open and has two children. - void split(node* n, literal const& a, literal const& b) { - n->split(a, b); - } - - // conflict is given by a set of literals. - // they are subsets of the literals on the path from root to n AND the external assumption literals - void backtrack(node* n, vector const& conflict) { - if (conflict.empty()) { - close_with_core(m_root.get(), conflict); + // Invariants: + // Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption + // literals. If a parent is open, then the one of the children is open. + void close_with_core(node *n, vector const &C) { + if (!n || n->get_status() == status::closed) return; - } - SASSERT(n != m_root.get()); - // all literals in conflict are on the path from root to n - // remove assumptions from conflict to ensure this. - DEBUG_CODE( - auto on_path = [&](literal const& a) { - node* p = n; - while (p) { - if (p->get_literal() == a) - return true; - p = p->parent(); - } - return false; - }; - SASSERT(all_of(conflict, [&](auto const& a) { return on_path(a); })); - ); - - 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 - close_with_core(n, conflict); - return; - } - - n = n->parent(); - } - UNREACHABLE(); + node *p = n->parent(); + if (p && any_of(C, [](auto const& l) { + return l == n->get_literal(); } + })) { + close_with_core(p, C); + return; } + close(n->left()); + close(n->right()); + n->set_core(C); + n->set_status(status::closed); - // return an active node in the tree, or nullptr if there is none - // first check if there is a node to activate under n, - // if not, go up the tree and try to activate a sibling subtree - node* activate_node(node* n) { - if (!n) { - if (m_root->get_status() == status::active) - return m_root.get(); - n = m_root.get(); + if (p) + try_resolve_upwards(p); + } + + // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, ¬x} + vector + compute_sibling_resolvent(node *left, node *right) { + vector res; + + auto &core_l = left->get_core(); + auto &core_r = right->get_core(); + + if (core_l.empty() || core_r.empty() || left->parent() != right->parent()) + return res; + + auto lit_l = left->get_literal(); + auto lit_r = right->get_literal(); + + for (auto const &lit : core_l) + if (lit != lit_l && !res.contains(lit)) + res.push_back(lit); + for (auto const &lit : core_r) + if (lit != lit_l && !res.contains(lit)) + res.push_back(lit); + return res; + } + + void try_resolve_upwards(node *p) { + auto left = p->left(); + auto right = p->right(); + if (!left || !right) + return; + + // only attempt when both children are closed and each has a core + if (left->get_status() != status::closed || right->get_status() != status::closed) + return; + + auto resolvent = compute_sibling_resolvent(left, right); + close_with_core(p, resolvent); + } + +public: + tree(literal const &null_literal) : m_null_literal(null_literal) { + reset(); + } + + void set_seed(unsigned seed) { + m_rand.set_seed(seed); + } + + void reset() { + m_root = alloc(node, m_null_literal, nullptr); + m_root->set_status(status::active); + } + + // Split current node if it is active. + // After the call, n is open and has two children. + void split(node *n, literal const &a, literal const &b) { + n->split(a, b); + } + + // conflict is given by a set of literals. + // they are subsets of the literals on the path from root to n AND the external assumption literals + void backtrack(node *n, vector const &conflict) { + if (conflict.empty()) { + close_with_core(m_root.get(), conflict); + return; + } + SASSERT(n != m_root.get()); + // all literals in conflict are on the path from root to n + // remove assumptions from conflict to ensure this. + DEBUG_CODE(auto on_path = + [&](literal const &a) { + node *p = n; + while (p) { + if (p->get_literal() == a) + return true; + p = p->parent(); + } + return false; + }; + SASSERT(all_of(conflict, [&](auto const &a) { return on_path(a); }));); + + 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 + close_with_core(n, conflict); + return; } - auto res = activate_from_root(n); - if (res) - return res; - 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); - n = p; - p = n->parent(); - continue; - } - if (n == p->left()) { - res = activate_from_root(p->right()); - if (res) - return res; - } - else { - VERIFY(n == p->right()); - res = activate_from_root(p->left()); - if (res) - return res; - } + n = n->parent(); + } + UNREACHABLE(); + } + + // return an active node in the tree, or nullptr if there is none + // first check if there is a node to activate under n, + // if not, go up the tree and try to activate a sibling subtree + node *activate_node(node *n) { + if (!n) { + if (m_root->get_status() == status::active) + return m_root.get(); + n = m_root.get(); + } + auto res = activate_from_root(n); + if (res) + return res; + + 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); n = p; p = n->parent(); + continue; } - return nullptr; + if (n == p->left()) { + res = activate_from_root(p->right()); + if (res) + return res; + } + else { + VERIFY(n == p->right()); + res = activate_from_root(p->left()); + if (res) + return res; + } + n = p; + p = n->parent(); } + return nullptr; + } - node* find_active_node() { - return m_root->find_active_node(); - } + node *find_active_node() { + return m_root->find_active_node(); + } - vector const& get_core_from_root() const { - return m_root->get_core(); - } + vector const &get_core_from_root() const { + return m_root->get_core(); + } - bool is_closed() const { - return m_root->get_status() == status::closed; - } + bool is_closed() const { + return m_root->get_status() == status::closed; + } - std::ostream& display(std::ostream& out) const { - m_root->display(out, 0); - return out; - } + std::ostream &display(std::ostream &out) const { + m_root->display(out, 0); + return out; + } - }; +}; } From 287825366f67c29bc276fe4d6cffee5374b24449 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Oct 2025 21:27:58 -0700 Subject: [PATCH 4/6] Refactor close_with_core to use current node in lambda --- src/util/search_tree.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 91a81bd60..6ce4d66f3 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -172,7 +172,7 @@ namespace search_tree { if (!n || n->get_status() == status::closed) return; node *p = n->parent(); - if (p && any_of(C, [](auto const& l) { + if (p && any_of(C, [n](auto const& l) { return l == n->get_literal(); } })) { close_with_core(p, C); From 94cdbe5d8739e47878f3d02eb3cc01b3a88967cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Oct 2025 21:30:41 -0700 Subject: [PATCH 5/6] Fix formatting issues in search_tree.h --- src/util/search_tree.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 6ce4d66f3..3726bdbf3 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -173,8 +173,7 @@ namespace search_tree { return; node *p = n->parent(); if (p && any_of(C, [n](auto const& l) { - return l == n->get_literal(); } - })) { + return l == n->get_literal(); })) { close_with_core(p, C); return; } From c5d65cdedddfb23484175c9234f904988fa6b3fd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Oct 2025 06:56:15 +0200 Subject: [PATCH 6/6] fix build issues Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 12 +- src/util/search_tree.h | 298 +++++++++++++++++++-------------------- 2 files changed, 146 insertions(+), 164 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 74aa43d1c..aa33e73e4 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -412,17 +412,7 @@ namespace smt { switch (m_state) { case state::is_running: // batch manager is still running, but all threads have processed their cubes, which // means all cubes were unsat - if (!m_search_tree.is_closed()) - throw default_exception("inconsistent end state"); - - // case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core - // these asms are stored in the cube tree, at the root node - if (p.ctx.m_unsat_core.empty()) { - SASSERT(root && root->is_closed()); - for (auto a : m_search_tree.get_core_from_root()) - p.ctx.m_unsat_core.push_back(a); - } - return l_false; + throw default_exception("inconsistent end state"); case state::is_unsat: return l_false; case state::is_sat: diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 3726bdbf3..2b9a41b59 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -111,9 +111,6 @@ namespace search_tree { m_right->display(out, indent + 2); } - bool has_core() const { - return !m_core.empty(); - } void set_core(vector const &core) { m_core = core; } @@ -161,8 +158,8 @@ namespace search_tree { if (!n || n->get_status() == status::closed) return; n->set_status(status::closed); - close(n->left); - close(n->right); + close(n->left()); + close(n->right()); } // Invariants: @@ -172,166 +169,161 @@ namespace search_tree { if (!n || n->get_status() == status::closed) return; node *p = n->parent(); - if (p && any_of(C, [n](auto const& l) { - return l == n->get_literal(); })) { - close_with_core(p, C); - return; - } - close(n->left()); - close(n->right()); - n->set_core(C); - n->set_status(status::closed); - - if (p) - try_resolve_upwards(p); - } - - // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, ¬x} - vector - compute_sibling_resolvent(node *left, node *right) { - vector res; - - auto &core_l = left->get_core(); - auto &core_r = right->get_core(); - - if (core_l.empty() || core_r.empty() || left->parent() != right->parent()) - return res; - - auto lit_l = left->get_literal(); - auto lit_r = right->get_literal(); - - for (auto const &lit : core_l) - if (lit != lit_l && !res.contains(lit)) - res.push_back(lit); - for (auto const &lit : core_r) - if (lit != lit_l && !res.contains(lit)) - res.push_back(lit); - return res; - } - - void try_resolve_upwards(node *p) { - auto left = p->left(); - auto right = p->right(); - if (!left || !right) - return; - - // only attempt when both children are closed and each has a core - if (left->get_status() != status::closed || right->get_status() != status::closed) - return; - - auto resolvent = compute_sibling_resolvent(left, right); - close_with_core(p, resolvent); - } - -public: - tree(literal const &null_literal) : m_null_literal(null_literal) { - reset(); - } - - void set_seed(unsigned seed) { - m_rand.set_seed(seed); - } - - void reset() { - m_root = alloc(node, m_null_literal, nullptr); - m_root->set_status(status::active); - } - - // Split current node if it is active. - // After the call, n is open and has two children. - void split(node *n, literal const &a, literal const &b) { - n->split(a, b); - } - - // conflict is given by a set of literals. - // they are subsets of the literals on the path from root to n AND the external assumption literals - void backtrack(node *n, vector const &conflict) { - if (conflict.empty()) { - close_with_core(m_root.get(), conflict); - return; - } - SASSERT(n != m_root.get()); - // all literals in conflict are on the path from root to n - // remove assumptions from conflict to ensure this. - DEBUG_CODE(auto on_path = - [&](literal const &a) { - node *p = n; - while (p) { - if (p->get_literal() == a) - return true; - p = p->parent(); - } - return false; - }; - SASSERT(all_of(conflict, [&](auto const &a) { return on_path(a); }));); - - 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 - close_with_core(n, conflict); + if (p && all_of(C, [n](auto const &l) { return l != n->get_literal(); })) { + close_with_core(p, C); return; } + close(n->left()); + close(n->right()); + n->set_core(C); + n->set_status(status::closed); - n = n->parent(); - } - UNREACHABLE(); - } + if (!p) + return; + auto left = p->left(); + auto right = p->right(); + if (!left || !right) + return; - // return an active node in the tree, or nullptr if there is none - // first check if there is a node to activate under n, - // if not, go up the tree and try to activate a sibling subtree - node *activate_node(node *n) { - if (!n) { - if (m_root->get_status() == status::active) - return m_root.get(); - n = m_root.get(); + // only attempt when both children are closed and each has a core + if (left->get_status() != status::closed || right->get_status() != status::closed) + return; + + auto resolvent = compute_sibling_resolvent(left, right); + close_with_core(p, resolvent); } - auto res = activate_from_root(n); - if (res) + + // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x, + // ¬x} + vector compute_sibling_resolvent(node *left, node *right) { + vector res; + + auto &core_l = left->get_core(); + auto &core_r = right->get_core(); + + if (core_l.empty() || core_r.empty() || left->parent() != right->parent()) + return res; + + auto lit_l = left->get_literal(); + auto lit_r = right->get_literal(); + + for (auto const &lit : core_l) + if (lit != lit_l && !res.contains(lit)) + res.push_back(lit); + for (auto const &lit : core_r) + if (lit != lit_l && !res.contains(lit)) + res.push_back(lit); return res; + } - 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); + public: + tree(literal const &null_literal) : m_null_literal(null_literal) { + reset(); + } + + void set_seed(unsigned seed) { + m_rand.set_seed(seed); + } + + void reset() { + m_root = alloc(node, m_null_literal, nullptr); + m_root->set_status(status::active); + } + + // Split current node if it is active. + // After the call, n is open and has two children. + void split(node *n, literal const &a, literal const &b) { + n->split(a, b); + } + + // conflict is given by a set of literals. + // they are subsets of the literals on the path from root to n AND the external assumption literals + void backtrack(node *n, vector const &conflict) { + if (conflict.empty()) { + close_with_core(m_root.get(), conflict); + return; + } + SASSERT(n != m_root.get()); + // all literals in conflict are on the path from root to n + // remove assumptions from conflict to ensure this. + DEBUG_CODE(auto on_path = + [&](literal const &a) { + node *p = n; + while (p) { + if (p->get_literal() == a) + return true; + p = p->parent(); + } + return false; + }; + SASSERT(all_of(conflict, [&](auto const &a) { return on_path(a); }));); + + 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 + close_with_core(n, conflict); + return; + } + + n = n->parent(); + } + UNREACHABLE(); + } + + // return an active node in the tree, or nullptr if there is none + // first check if there is a node to activate under n, + // if not, go up the tree and try to activate a sibling subtree + node *activate_node(node *n) { + if (!n) { + if (m_root->get_status() == status::active) + return m_root.get(); + n = m_root.get(); + } + auto res = activate_from_root(n); + if (res) + return res; + + 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); + n = p; + p = n->parent(); + continue; + } + if (n == p->left()) { + res = activate_from_root(p->right()); + if (res) + return res; + } + else { + VERIFY(n == p->right()); + res = activate_from_root(p->left()); + if (res) + return res; + } n = p; p = n->parent(); - continue; } - if (n == p->left()) { - res = activate_from_root(p->right()); - if (res) - return res; - } - else { - VERIFY(n == p->right()); - res = activate_from_root(p->left()); - if (res) - return res; - } - n = p; - p = n->parent(); + return nullptr; } - return nullptr; - } - node *find_active_node() { - return m_root->find_active_node(); - } + node *find_active_node() { + return m_root->find_active_node(); + } - vector const &get_core_from_root() const { - return m_root->get_core(); - } + vector const &get_core_from_root() const { + return m_root->get_core(); + } - bool is_closed() const { - return m_root->get_status() == status::closed; - } + bool is_closed() const { + return m_root->get_status() == status::closed; + } - std::ostream &display(std::ostream &out) const { - m_root->display(out, 0); - return out; - } - -}; -} + std::ostream &display(std::ostream &out) const { + m_root->display(out, 0); + return out; + } + }; +} // namespace search_tree