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; }