From 6ef8660adb5858c89eb8db58f3de7be23a0bf0fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 09:14:00 -0700 Subject: [PATCH 01/34] Parallel tactic (#9824) Co-authored-by: Ilana Shapiro Co-authored-by: Ilana Shapiro --- src/params/smt_parallel_params.pyg | 2 +- src/sat/sat_solver.cpp | 150 ++- src/sat/sat_solver.h | 11 +- src/sat/sat_solver/inc_sat_solver.cpp | 94 +- src/sat/smt/atom2bool_var.cpp | 7 + src/sat/smt/atom2bool_var.h | 1 + src/sat/smt/bv_ackerman.cpp | 2 +- src/sat/smt/euf_ackerman.cpp | 2 +- src/smt/smt_context.cpp | 7 + src/smt/smt_context.h | 9 +- src/smt/smt_kernel.cpp | 16 + src/smt/smt_kernel.h | 8 + src/smt/smt_parallel.cpp | 3 +- src/smt/smt_parallel.h | 7 + src/smt/smt_solver.cpp | 157 ++- src/solver/parallel_params.pyg | 3 + src/solver/parallel_tactical2.cpp | 1632 +++++++++++++++++++++---- src/solver/solver.h | 46 + src/solver/solver_pool.cpp | 4 + src/util/search_tree.h | 8 + 20 files changed, 1889 insertions(+), 280 deletions(-) diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg index dde7656ff..315d3d029 100644 --- a/src/params/smt_parallel_params.pyg +++ b/src/params/smt_parallel_params.pyg @@ -5,7 +5,7 @@ def_module_params('smt_parallel', ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'), ('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'), ('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'), - ('num_global_bb_batch_threads', UINT, 0, 'run Janota-style chunking backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'), + ('num_global_bb_batch_threads', UINT, 2, 'run Janota-style chunking backbone worker threads; default is 2 (negative and positive mode), supported values are 0 (off), 1 (negative mode only) or 2 (negative and positive mode)'), ('local_backbones', BOOL, False, 'enable local backbones experiment within the search tree parallelism'), ('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'), ('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 09f874e78..cd4793416 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -132,6 +132,8 @@ namespace sat { m_best_phase.reset(); m_phase.reset(); m_prev_phase.reset(); + m_phase_birthdate.reset(); + m_best_phase_birthdate.reset(); m_assigned_since_gc.reset(); m_last_conflict.reset(); m_last_propagation.reset(); @@ -161,6 +163,8 @@ namespace sat { m_phase[v] = src.m_phase[v]; m_best_phase[v] = src.m_best_phase[v]; m_prev_phase[v] = src.m_prev_phase[v]; + m_phase_birthdate[v] = src.m_phase_birthdate[v]; + m_best_phase_birthdate[v] = src.m_best_phase_birthdate[v]; // inherit activity: m_activity[v] = src.m_activity[v]; @@ -267,6 +271,8 @@ namespace sat { m_phase[v] = false; m_best_phase[v] = false; m_prev_phase[v] = false; + m_phase_birthdate[v] = 0; + m_best_phase_birthdate[v] = 0; m_assigned_since_gc[v] = false; m_last_conflict[v] = 0; m_last_propagation[v] = 0; @@ -308,6 +314,8 @@ namespace sat { m_phase.push_back(false); m_best_phase.push_back(false); m_prev_phase.push_back(false); + m_phase_birthdate.push_back(0); + m_best_phase_birthdate.push_back(0); m_assigned_since_gc.push_back(false); m_last_conflict.push_back(0); m_last_propagation.push_back(0); @@ -645,6 +653,17 @@ namespace sat { return 3*cls_allocator().get_allocation_size()/2 + memory::get_allocation_size() > memory::get_max_memory_size(); } + void solver::set_phase(literal l) { + if (l.var() >= num_vars()) + return; + bool value = !l.sign(); + if (m_phase[l.var()] != value) + m_phase_birthdate[l.var()] = m_stats.m_conflicts; + if (m_best_phase[l.var()] != value) + m_best_phase_birthdate[l.var()] = m_stats.m_conflicts; + m_best_phase[l.var()] = m_phase[l.var()] = value; + } + struct solver::cmp_activity { solver& s; cmp_activity(solver& s):s(s) {} @@ -896,6 +915,8 @@ namespace sat { m_assignment[(~l).index()] = l_false; bool_var v = l.var(); m_justification[v] = j; + if (m_phase[v] != !l.sign()) + m_phase_birthdate[v] = m_stats.m_conflicts; m_phase[v] = !l.sign(); m_assigned_since_gc[v] = true; m_trail.push_back(l); @@ -904,17 +925,17 @@ namespace sat { case BH_VSIDS: break; case BH_CHB: - m_last_propagation[v] = m_stats.m_conflict; + m_last_propagation[v] = m_stats.m_conflicts; break; } if (m_config.m_anti_exploration) { - uint64_t age = m_stats.m_conflict - m_canceled[v]; + uint64_t age = m_stats.m_conflicts - m_canceled[v]; if (age > 0) { double decay = pow(0.95, static_cast(age)); set_activity(v, static_cast(m_activity[v] * decay)); // NB. MapleSAT does not update canceled. - m_canceled[v] = m_stats.m_conflict; + m_canceled[v] = m_stats.m_conflicts; } } @@ -1378,8 +1399,12 @@ namespace sat { lbool r = m_local_search->check(_lits.size(), _lits.data(), nullptr); auto const& mdl = m_local_search->get_model(); if (mdl.size() == m_best_phase.size()) { - for (unsigned i = 0; i < m_best_phase.size(); ++i) - m_best_phase[i] = l_true == mdl[i]; + for (unsigned i = 0; i < m_best_phase.size(); ++i) { + bool is_true = l_true == mdl[i]; + if (m_best_phase[i] != is_true) + m_best_phase_birthdate[i] = m_stats.m_conflicts; + m_best_phase[i] = is_true; + } if (r == l_true) { m_conflicts_since_restart = 0; @@ -1671,12 +1696,12 @@ namespace sat { while (!m_case_split_queue.empty()) { if (m_config.m_anti_exploration) { next = m_case_split_queue.min_var(); - auto age = m_stats.m_conflict - m_canceled[next]; + auto age = m_stats.m_conflicts - m_canceled[next]; while (age > 0) { set_activity(next, static_cast(m_activity[next] * pow(0.95, static_cast(age)))); - m_canceled[next] = m_stats.m_conflict; + m_canceled[next] = m_stats.m_conflicts; next = m_case_split_queue.min_var(); - age = m_stats.m_conflict - m_canceled[next]; + age = m_stats.m_conflicts - m_canceled[next]; } } next = m_case_split_queue.next_var(); @@ -1714,6 +1739,32 @@ namespace sat { } } + uint64_t solver::get_preferred_phase_birthdate(bool_var v) const { + bool use_best = + m_config.m_phase == PS_FROZEN || + ((m_config.m_phase == PS_SAT_CACHING || m_config.m_phase == PS_LOCAL_SEARCH) && m_search_state == s_sat); + return use_best ? m_best_phase_birthdate[v] : m_phase_birthdate[v]; + } + + void solver::get_backbone_candidates(literal_vector& lits, unsigned max_num) { + struct candidate { + literal lit; + uint64_t age; + }; + svector cands; + uint64_t now = m_stats.m_conflicts; + for (bool_var v = 0; v < num_vars(); ++v) { + if (value(v) != l_undef || was_eliminated(v)) + continue; + bool is_pos = guess(v); + cands.push_back({ literal(v, !is_pos), now - get_preferred_phase_birthdate(v) }); + } + std::stable_sort(cands.begin(), cands.end(), + [](candidate const& a, candidate const& b) { return a.age > b.age; }); + for (unsigned i = 0; i < cands.size() && i < max_num; ++i) + lits.push_back(cands[i].lit); + } + bool solver::decide() { bool_var next; lbool phase = l_undef; @@ -2145,8 +2196,13 @@ namespace sat { for (bool_var v = 0; v < num; ++v) { if (!was_eliminated(v)) { m_model[v] = value(v); - m_phase[v] = value(v) == l_true; - m_best_phase[v] = value(v) == l_true; + bool is_true = value(v) == l_true; + if (m_phase[v] != is_true) + m_phase_birthdate[v] = m_stats.m_conflicts; + if (m_best_phase[v] != is_true) + m_best_phase_birthdate[v] = m_stats.m_conflicts; + m_phase[v] = is_true; + m_best_phase[v] = is_true; } } TRACE(sat_mc_bug, m_mc.display(tout);); @@ -2274,7 +2330,7 @@ namespace sat { m_restart_logs++; std::stringstream strm; - strm << "(sat.stats " << std::setw(6) << m_stats.m_conflict << " " + strm << "(sat.stats " << std::setw(6) << m_stats.m_conflicts << " " << std::setw(6) << m_stats.m_decision << " " << std::setw(4) << m_stats.m_restart << mk_stat(*this) @@ -2432,7 +2488,7 @@ namespace sat { m_conflicts_since_init++; m_conflicts_since_restart++; m_conflicts_since_gc++; - m_stats.m_conflict++; + m_stats.m_conflicts++; if (m_step_size > m_config.m_step_size_min) m_step_size -= m_config.m_step_size_dec; @@ -2564,7 +2620,7 @@ namespace sat { tout << "missed " << lit << "@" << lvl(lit) << "\n";); CTRACE(sat, idx == 0, display(tout);); if (idx == 0) - IF_VERBOSE(0, verbose_stream() << "num-conflicts: " << m_stats.m_conflict << "\n"); + IF_VERBOSE(0, verbose_stream() << "num-conflicts: " << m_stats.m_conflicts << "\n"); VERIFY(idx > 0); idx--; } @@ -2874,7 +2930,7 @@ namespace sat { inc_activity(var); break; case BH_CHB: - m_last_conflict[var] = m_stats.m_conflict; + m_last_conflict[var] = m_stats.m_conflicts; break; default: break; @@ -2915,13 +2971,18 @@ namespace sat { for (unsigned i = head; i < sz; ++i) { bool_var v = m_trail[i].var(); TRACE(forget_phase, tout << "forgetting phase of v" << v << "\n";); - m_phase[v] = m_rand() % 2 == 0; + bool value = m_rand() % 2 == 0; + if (m_phase[v] != value) + m_phase_birthdate[v] = m_stats.m_conflicts; + m_phase[v] = value; } if (is_sat_phase() && head >= m_best_phase_size) { m_best_phase_size = head; IF_VERBOSE(12, verbose_stream() << "sticky trail: " << head << "\n"); for (unsigned i = 0; i < head; ++i) { bool_var v = m_trail[i].var(); + if (m_best_phase[v] != m_phase[v]) + m_best_phase_birthdate[v] = m_stats.m_conflicts; m_best_phase[v] = m_phase[v]; } set_has_new_best_phase(true); @@ -2971,23 +3032,43 @@ namespace sat { void solver::do_rephase() { switch (m_config.m_phase) { case PS_ALWAYS_TRUE: - for (auto& p : m_phase) p = true; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (!m_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = true; + } break; case PS_ALWAYS_FALSE: - for (auto& p : m_phase) p = false; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (m_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = false; + } break; case PS_FROZEN: break; case PS_BASIC_CACHING: switch (m_rephase.count % 4) { case 0: - for (auto& p : m_phase) p = (m_rand() % 2) == 0; + for (unsigned i = 0; i < m_phase.size(); ++i) { + bool value = (m_rand() % 2) == 0; + if (m_phase[i] != value) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = value; + } break; case 1: - for (auto& p : m_phase) p = false; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (m_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = false; + } break; case 2: - for (auto& p : m_phase) p = !p; + for (unsigned i = 0; i < m_phase.size(); ++i) { + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = !m_phase[i]; + } break; default: break; @@ -2995,18 +3076,29 @@ namespace sat { break; case PS_SAT_CACHING: if (m_search_state == s_sat) - for (unsigned i = 0; i < m_phase.size(); ++i) - m_phase[i] = m_best_phase[i]; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (m_phase[i] != m_best_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = m_best_phase[i]; + } break; case PS_RANDOM: - for (auto& p : m_phase) p = (m_rand() % 2) == 0; + for (unsigned i = 0; i < m_phase.size(); ++i) { + bool value = (m_rand() % 2) == 0; + if (m_phase[i] != value) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = value; + } break; case PS_LOCAL_SEARCH: if (m_search_state == s_sat) { if (m_rand() % 2 == 0) bounded_local_search(); - for (unsigned i = 0; i < m_phase.size(); ++i) - m_phase[i] = m_best_phase[i]; + for (unsigned i = 0; i < m_phase.size(); ++i) { + if (m_phase[i] != m_best_phase[i]) + m_phase_birthdate[i] = m_stats.m_conflicts; + m_phase[i] = m_best_phase[i]; + } } break; @@ -3601,6 +3693,8 @@ namespace sat { m_phase.shrink(v); m_best_phase.shrink(v); m_prev_phase.shrink(v); + m_phase_birthdate.shrink(v); + m_best_phase_birthdate.shrink(v); m_assigned_since_gc.shrink(v); m_simplifier.reset_todos(); } @@ -3644,7 +3738,7 @@ namespace sat { SASSERT(value(v) == l_undef); m_case_split_queue.unassign_var_eh(v); if (m_config.m_anti_exploration) { - m_canceled[v] = m_stats.m_conflict; + m_canceled[v] = m_stats.m_conflicts; } } m_trail.shrink(old_sz); @@ -3812,7 +3906,7 @@ namespace sat { double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0); for (unsigned i = qhead; i < m_trail.size(); ++i) { auto v = m_trail[i].var(); - auto d = m_stats.m_conflict - m_last_conflict[v] + 1; + auto d = m_stats.m_conflicts - m_last_conflict[v] + 1; if (d == 0) d = 1; auto reward = multiplier / d; auto activity = m_activity[v]; @@ -4745,7 +4839,7 @@ namespace sat { st.update("sat mk var", m_mk_var); st.update("sat gc clause", m_gc_clause); st.update("sat del clause", m_del_clause); - st.update("sat conflicts", m_conflict); + st.update("sat conflicts", m_conflicts); st.update("sat decisions", m_decision); st.update("sat propagations 2ary", m_bin_propagate); st.update("sat propagations 3ary", m_ter_propagate); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 9aa00ae47..d50ee9461 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -60,7 +60,7 @@ namespace sat { unsigned m_mk_bin_clause; unsigned m_mk_ter_clause; unsigned m_mk_clause; - unsigned m_conflict; + unsigned m_conflicts; unsigned m_propagate; unsigned m_bin_propagate; unsigned m_ter_propagate; @@ -148,6 +148,8 @@ namespace sat { bool_vector m_phase; bool_vector m_best_phase; bool_vector m_prev_phase; + svector m_phase_birthdate; + svector m_best_phase_birthdate; bool m_new_best_phase = false; svector m_assigned_since_gc; search_state m_search_state; @@ -373,12 +375,17 @@ namespace sat { bool was_eliminated(bool_var v) const { return m_eliminated[v]; } void set_eliminated(bool_var v, bool f) override; bool was_eliminated(literal l) const { return was_eliminated(l.var()); } - void set_phase(literal l) override { if (l.var() < num_vars()) m_best_phase[l.var()] = m_phase[l.var()] = !l.sign(); } + void set_phase(literal l) override; bool get_phase(bool_var b) { return m_phase.get(b, false); } bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); } + uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); } + uint64_t get_best_phase_birthdate(bool_var b) const { return m_best_phase_birthdate.get(b, 0); } + uint64_t get_preferred_phase_birthdate(bool_var b) const; void set_has_new_best_phase(bool b) { m_new_best_phase = b; } bool has_new_best_phase() const { return m_new_best_phase; } void move_to_front(bool_var b); + unsigned get_activity(bool_var v) const { return m_activity[v]; } + void get_backbone_candidates(literal_vector& lits, unsigned max_num); unsigned scope_lvl() const { return m_scope_lvl; } unsigned search_lvl() const { return m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 2a98bc3ae..e8cd6d3fd 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -405,6 +405,50 @@ public: } } + unsigned get_assign_level(expr* e) const override { + expr* atom = e; + m.is_not(e, atom); + sat::bool_var bv = m_map.to_bool_var(atom); + return bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv); + } + + bool is_relevant(expr* e) const override { + expr* atom = e; + m.is_not(e, atom); + sat::bool_var bv = m_map.to_bool_var(atom); + if (bv == sat::null_bool_var) + return true; + auto* ext = dynamic_cast(m_solver.get_extension()); + return !ext || ext->is_relevant(bv); + } + + unsigned get_num_bool_vars() const override { + return m_solver.num_vars(); + } + + unsigned get_bool_var(expr* e) const override { + expr* atom = e; + m.is_not(e, atom); + sat::bool_var bv = m_map.to_bool_var(atom); + return bv == sat::null_bool_var ? UINT_MAX : bv; + } + + expr* bool_var2expr(unsigned v) const override { + return v < m_solver.num_vars() ? m_map.bool_var2expr(v) : nullptr; + } + + lbool get_assignment(unsigned v) const override { + return v < m_solver.num_vars() ? m_solver.value(v) : l_undef; + } + + double get_activity(unsigned v) const override { + return v < m_solver.num_vars() ? static_cast(m_solver.get_activity(v)) : 0.0; + } + + bool was_eliminated(unsigned v) const override { + return v < m_solver.num_vars() && m_solver.was_eliminated(v); + } + expr_ref_vector get_trail(unsigned max_level) override { expr_ref_vector result(m); unsigned sz = m_solver.trail_size(); @@ -451,8 +495,35 @@ public: vars.push_back(kv.m_value); } sat::literal_vector lits; - lbool result = m_solver.cube(vars, lits, backtrack_level); expr_ref_vector fmls(m); + if (!m_params.get_bool("cube.lookahead", false)) { + sat::bool_var best = sat::null_bool_var; + double best_activity = 0.0; + unsigned n = 0; + for (sat::bool_var v : vars) { + if (get_assignment(v) != l_undef || was_eliminated(v)) + continue; + double activity = get_activity(v); + if (best == sat::null_bool_var || activity > best_activity || (activity == best_activity && m_solver.rand()(++n) == 0)) { + best = v; + best_activity = activity; + } + } + if (best == sat::null_bool_var) + return expr_ref_vector(m); + expr* e = bool_var2expr(best); + SASSERT(e); + if (e) + fmls.push_back(e); + vs.reset(); + for (sat::bool_var v : vars) { + expr* x = bool_var2expr(v); + if (x) + vs.push_back(x); + } + return fmls; + } + lbool result = m_solver.cube(vars, lits, backtrack_level); expr_ref_vector lit2expr(m); lit2expr.resize(m_solver.num_vars() * 2); m_map.mk_inv(lit2expr); @@ -482,6 +553,27 @@ public: return fmls; } + void get_backbone_candidates(vector& candidates, unsigned max_num) override { + if (!is_internalized()) { + lbool r = internalize_formulas(); + if (r != l_true) + return; + } + convert_internalized(); + sat::literal_vector lits; + m_solver.get_backbone_candidates(lits, max_num); + expr_ref_vector lit2expr(m); + lit2expr.resize(m_solver.num_vars() * 2); + m_map.mk_inv(lit2expr); + uint64_t now = m_solver.get_stats().m_conflicts; + for (sat::literal lit : lits) { + expr* e = lit2expr.get(lit.index()); + if (!e) + continue; + candidates.push_back(scored_literal(m, e, static_cast(now - m_solver.get_phase_birthdate(lit.var())))); + } + } + expr* congruence_next(expr* e) override { return e; } expr* congruence_root(expr* e) override { return e; } expr_ref congruence_explain(expr* a, expr* b) override { return expr_ref(m.mk_eq(a, b), m); } diff --git a/src/sat/smt/atom2bool_var.cpp b/src/sat/smt/atom2bool_var.cpp index 68a263c85..b6760c943 100644 --- a/src/sat/smt/atom2bool_var.cpp +++ b/src/sat/smt/atom2bool_var.cpp @@ -49,6 +49,13 @@ sat::bool_var atom2bool_var::to_bool_var(expr * n) const { return m_mapping[idx].m_value; } +expr* atom2bool_var::bool_var2expr(sat::bool_var v) const { + for (auto const& kv : m_mapping) + if (kv.m_value == v) + return kv.m_key; + return nullptr; +} + struct collect_boolean_interface_proc { struct visitor { obj_hashtable & m_r; diff --git a/src/sat/smt/atom2bool_var.h b/src/sat/smt/atom2bool_var.h index 794429701..cee7a9882 100644 --- a/src/sat/smt/atom2bool_var.h +++ b/src/sat/smt/atom2bool_var.h @@ -29,6 +29,7 @@ public: atom2bool_var(ast_manager & m):expr2var(m) {} void insert(expr * n, sat::bool_var v) { expr2var::insert(n, v); } sat::bool_var to_bool_var(expr * n) const; + expr* bool_var2expr(sat::bool_var v) const; void mk_inv(expr_ref_vector & lit2expr) const; void mk_var_inv(expr_ref_vector & var2expr) const; // return true if the mapping contains uninterpreted atoms. diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp index a709c16f3..1bb84bc09 100644 --- a/src/sat/smt/bv_ackerman.cpp +++ b/src/sat/smt/bv_ackerman.cpp @@ -155,7 +155,7 @@ namespace bv { void ackerman::propagate() { auto* n = m_queue; vv* k = nullptr; - unsigned num_prop = static_cast(s.s().get_stats().m_conflict * s.get_config().m_dack_factor); + unsigned num_prop = static_cast(s.s().get_stats().m_conflicts * s.get_config().m_dack_factor); num_prop = std::min(num_prop, m_table.size()); for (unsigned i = 0; i < num_prop; ++i, n = k) { k = n->next(); diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index 67a98b2f6..568df6034 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -171,7 +171,7 @@ namespace euf { SASSERT(ctx.s().at_base_lvl()); auto* n = m_queue; inference* k = nullptr; - unsigned num_prop = static_cast(ctx.s().get_stats().m_conflict * ctx.m_config.m_dack_factor); + unsigned num_prop = static_cast(ctx.s().get_stats().m_conflicts * ctx.m_config.m_dack_factor); num_prop = std::min(num_prop, m_table.size()); for (unsigned i = 0; i < num_prop; ++i, n = k) { k = n->next(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 098240fc9..f95b77b2d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3652,6 +3652,13 @@ namespace smt { } } + void context::setup_for_parallel() { + // Native SMT parallel configures the parent context before cloning workers. + // context::copy then configures/internalizes each worker copy while + // preprocessing is still enabled. + setup_context(m_fparams.m_auto_config); + } + config_mode context::get_config_mode(bool use_static_features) const { if (!m_fparams.m_auto_config) return CFG_BASIC; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 6a19ab5fd..193ef7705 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -64,6 +64,7 @@ namespace smt { class model_generator; class context; + class kernel; struct oom_exception : public z3_error { oom_exception() : z3_error(ERR_MEMOUT) {} @@ -85,6 +86,7 @@ namespace smt { friend class model_generator; friend class lookahead; friend class parallel; + friend class kernel; public: statistics m_stats; @@ -452,6 +454,8 @@ namespace smt { svector const & get_activity_vector() const { return m_activity; } double get_activity(bool_var v) const { return m_activity[v]; } + unsigned get_num_assignments() const { return m_stats.m_num_assignments; } + unsigned get_birthdate(bool_var v) const { return m_birthdate[v]; } void set_activity(bool_var v, double act) { m_activity[v] = act; } @@ -538,6 +542,8 @@ namespace smt { return m_scope_lvl == m_search_lvl; } + void pop_to_search_level() { pop_to_search_lvl(); } + bool tracking_assumptions() const { return !m_assumptions.empty() && m_search_lvl > m_base_lvl; } @@ -1697,6 +1703,8 @@ namespace smt { lbool setup_and_check(bool reset_cancel = true); + void setup_for_parallel(); + void reduce_assertions(); bool resource_limits_exceeded(); @@ -1914,4 +1922,3 @@ namespace smt { }; - diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index a5ce0dcb7..fc2c87f5a 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -280,6 +280,22 @@ namespace smt { smt_params_helper::collect_param_descrs(d); } + void kernel::pop_to_base_level() { + m_imp->m_kernel.pop_to_base_lvl(); + } + + void kernel::set_preprocess(bool f) { + m_imp->m_kernel.get_fparams().m_preprocess = f; + } + + void kernel::reset_aux_statistics() { + m_imp->m_kernel.m_aux_stats.reset(); + } + + void kernel::add_aux_statistics(::statistics const& st) { + m_imp->m_kernel.m_aux_stats.copy(st); + } + context & kernel::get_context() { return m_imp->m_kernel; } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 98b677213..a1b2bfc18 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -300,6 +300,14 @@ namespace smt { */ static void collect_param_descrs(param_descrs & d); + void pop_to_base_level(); + + void set_preprocess(bool f); + + void reset_aux_statistics(); + + void add_aux_statistics(::statistics const& st); + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause); /** diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 64848d890..a7a1acf8a 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -626,7 +626,7 @@ namespace smt { ctx->set_logic(p.ctx.m_setup.get_logic()); context::copy(p.ctx, *ctx, true); ctx->pop_to_base_lvl(); - ctx->get_fparams().m_preprocess = false; + ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged } void parallel::core_minimizer_worker::cancel() { @@ -887,6 +887,7 @@ namespace smt { ctx->pop_to_base_lvl(); m_shared_units_prefix = ctx->assigned_literals().size(); m_num_initial_atoms = ctx->get_num_bool_vars(); + ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged smt_parallel_params pp(p.ctx.m_params); m_use_failed_literal_test = pp.num_global_bb_fl_threads() > 0; diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 64fcc1186..b98870e0c 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -32,6 +32,13 @@ namespace smt { struct cube_config { using literal = expr_ref; static bool literal_is_null(expr_ref const& l) { return l == nullptr; } + static bool same_atom(expr_ref const& a, expr_ref const& b) { + expr* atom_a = a.get(); + expr* atom_b = b.get(); + a.get_manager().is_not(atom_a, atom_a); + b.get_manager().is_not(atom_b, atom_b); + return atom_a == atom_b; + } static std::ostream& display_literal(std::ostream& out, expr_ref const& l) { return out << mk_bounded_pp(l, l.get_manager()); } }; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index d1e5e5a6b..81391cb34 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -22,12 +22,15 @@ Notes: #include "ast/for_each_expr.h" #include "ast/ast_pp.h" #include "ast/func_decl_dependencies.h" +#include "smt/smt_context.h" #include "smt/smt_kernel.h" #include "params/smt_params.h" #include "params/smt_params_helper.hpp" #include "solver/solver_na2as.h" #include "solver/mus.h" +#include + namespace { class smt_solver : public solver_na2as { @@ -61,6 +64,7 @@ namespace { smt_params m_smt_params; smt::kernel m_context; cuber* m_cuber; + random_gen m_rand; symbol m_logic; bool m_minimizing_core; bool m_core_extend_patterns; @@ -86,14 +90,17 @@ namespace { solver * translate(ast_manager & m, params_ref const & p) override { ast_translation translator(get_manager(), m); + params_ref init; + init.copy(get_params()); + init.copy(p); - smt_solver * result = alloc(smt_solver, m, p, m_logic); + smt_solver* result = alloc(smt_solver, m, init, m_logic); smt::kernel::copy(m_context, result->m_context, true); - if (mc0()) + if (mc0()) result->set_model_converter(mc0()->translate(translator)); - for (auto & [k, v] : m_name2assertion) { + for (auto& [k, v] : m_name2assertion) { expr* val = translator(k); expr* key = translator(v); result->assert_expr(val, key); @@ -212,6 +219,112 @@ namespace { return m_context.get_trail(max_level); } + expr_ref_vector get_assigned_literals() override { + expr_ref_vector result(m); + auto& ctx = const_cast(m_context).get_context(); + for (auto lit : ctx.assigned_literals()) { + expr* atom = ctx.bool_var2expr(lit.var()); + if (!atom) + continue; + result.push_back(lit.sign() ? m.mk_not(atom) : atom); + } + return result; + } + + unsigned get_assign_level(expr* e) const override { + auto& ctx = const_cast(m_context).get_context(); + expr* atom = e; + get_manager().is_not(e, atom); + if (!ctx.b_internalized(atom)) + return UINT_MAX; + return ctx.get_assign_level(ctx.get_bool_var(atom)); + } + + bool is_relevant(expr* e) const override { + auto& ctx = const_cast(m_context).get_context(); + expr* atom = e; + get_manager().is_not(e, atom); + return ctx.b_internalized(atom) && ctx.is_relevant(atom); + } + + unsigned get_num_bool_vars() const override { + return const_cast(m_context).get_context().get_num_bool_vars(); + } + + unsigned get_bool_var(expr* e) const override { + auto& ctx = const_cast(m_context).get_context(); + expr* atom = e; + get_manager().is_not(e, atom); + return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : UINT_MAX; + } + + void pop_to_base_level() override { + m_context.pop_to_base_level(); + } + + void setup_for_parallel() override { + const_cast(m_context).get_context().setup_for_parallel(); + } + + void set_preprocess(bool f) override { + m_context.set_preprocess(f); + } + + void set_max_conflicts(unsigned max_conflicts) override { + auto& ctx = const_cast(m_context).get_context(); + ctx.get_fparams().m_max_conflicts = max_conflicts; + } + + unsigned get_max_conflicts() const override { + return const_cast(m_context).get_context().get_fparams().m_max_conflicts; + } + + void reset_parallel_statistics() override { + m_context.reset_aux_statistics(); + } + + void add_parallel_statistics(statistics const& st) override { + m_context.add_aux_statistics(st); + } + + void collect_parallel_statistics(statistics& st) const override { + m_context.collect_statistics(st); + } + + void get_backbone_candidates(vector& candidates, unsigned max_num) override { + ast_manager& m = get_manager(); + auto& ctx = m_context.get_context(); + unsigned curr_time = ctx.get_num_assignments(); + vector all; + + for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) { + if (ctx.get_assignment(v) != l_undef && ctx.get_assign_level(v) == ctx.get_base_level()) + continue; + + expr* candidate = ctx.bool_var2expr(v); + if (!candidate) + continue; + + auto const& d = ctx.get_bdata(v); + if (d.m_phase_available && !d.m_phase) + candidate = m.mk_not(candidate); + + double age = static_cast(curr_time - ctx.get_birthdate(v)); + all.push_back(solver::scored_literal(m, candidate, age)); + } + + std::stable_sort( + all.begin(), + all.end(), + [](solver::scored_literal const& a, solver::scored_literal const& b) { + return a.score > b.score; + }); + + unsigned n = std::min(max_num, all.size()); + for (unsigned i = 0; i < n; ++i) + candidates.push_back(all[i]); + } + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { m_context.register_on_clause(ctx, on_clause); } @@ -347,6 +460,44 @@ namespace { expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override { ast_manager& m = get_manager(); + if (!get_params().get_bool("cube.lookahead", false)) { + auto& ctx = m_context.get_context(); + obj_hashtable selected_vars; + for (expr* v : vars) + selected_vars.insert(v); + expr_ref_vector candidates(m); + expr_ref result(m); + double score = 0.0; + unsigned n = 0; + + ctx.pop_to_search_level(); + for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) { + if (ctx.get_assignment(v) != l_undef) + continue; + expr* e = ctx.bool_var2expr(v); + if (!e) + continue; + if (!selected_vars.empty() && !selected_vars.contains(e)) + continue; + candidates.push_back(e); + double new_score = ctx.get_activity(v); + // Match smt_parallel: cube split tie-breaking is independent + // of the per-worker SMT search seed. + if (new_score > score || !result || (new_score == score && m_rand(++n) == 0)) { + score = new_score; + result = e; + } + } + + vars.reset(); + vars.append(candidates); + + expr_ref_vector lits(m); + if (result) + lits.push_back(result); + return lits; + } + if (!m_cuber) { m_cuber = alloc(cuber, *this); // force propagation diff --git a/src/solver/parallel_params.pyg b/src/solver/parallel_params.pyg index 2aa2acf77..e577c58e8 100644 --- a/src/solver/parallel_params.pyg +++ b/src/solver/parallel_params.pyg @@ -6,6 +6,9 @@ def_module_params('parallel', ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), ('enable2', BOOL, False, 'enable (experimental) parallel solver by default on selected tactics (for QF_BV)'), ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'), + ('num_bb_threads', UINT, 2, 'run Janota-style chunking backbone worker threads; default is 2 (negative and positive mode), supported values are 0 (off), 1 (negative mode only) or 2 (negative and positive mode)'), + ('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'), + ('cube.lookahead', BOOL, False, 'use lookahead cubing in the parallel solver; when false, use VSIDS activity to select one split literal'), ('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'), ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), ('conquer.delay', UINT, 10, 'delay of cubes until applying conquer'), diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ebae4cb57..ae5b739f4 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -7,37 +7,7 @@ Module Name: Abstract: - Parallel portfolio solver using the solver API. - - Models the internals after smt/smt_parallel.cpp but operates on generic - solver objects (smt_solver, inc_sat_solver, etc.) via the solver interface - instead of accessing smt::context internals directly. - - Key features compared to parallel_tactical.cpp: - - Search tree for coordinated non-chronological backtracking (from smt_parallel). - - Shared clause pool: learned conflict clauses are broadcast to all workers. - - Shared backbone/unit pool: base-level units propagated by one worker are - asserted as facts on every other worker's solver. - - Workers reuse their solver state across multiple cube checks, accumulating - learned clauses (same pattern as smt_parallel workers). - - Key differences from smt_parallel: - - Uses the solver API throughout (translate, check_sat, get_trail, cube, - get_model, get_unsat_core, assert_expr, push, pop, updt_params, …) - rather than accessing smt::context members directly. - - Works with any conforming solver implementation. - - Cube path management follows the assumption-based pattern from smt_parallel: - - The worker's solver base assertion set is fixed at construction (the full - problem is translated into the worker's own ast_manager once). - - Shared clauses discovered by other workers are appended to the base set via - assert_expr at any time. - - The current cube path is passed as extra assumptions on every check_sat call, - so the solver can reuse learned clauses across different cube checks. - - Split atom selection is performed by temporarily pushing the cube path onto - the solver, calling solver::cube(), retrieving the first proposed literal, and - then popping, so that the base state is preserved. + Parallel tactical, portfolio loop specialized to the solver API. Author: @@ -55,14 +25,15 @@ Author: #include "solver/solver.h" #include "solver/parallel_tactical2.h" #include "solver/parallel_params.hpp" -#include "solver/solver_preprocess.h" #include "util/search_tree.h" #include "tactic/tactic.h" -#include "tactic/tactical.h" #include "solver/solver2tactic.h" +#include #include +#include #include +#include /* ------------------------------------------------------------------ */ /* Single-threaded stub */ @@ -91,6 +62,26 @@ tactic* mk_parallel_tactic2(solver* s, params_ref const& p) { #include #include +#define LOG_WORKER(lvl, s) IF_VERBOSE(lvl, verbose_stream() << "Worker " << id << s) +#define LOG_BB_WORKER(lvl, s) IF_VERBOSE(lvl, verbose_stream() << "Backbones Worker " << id << s) + +class bounded_pp_exprs { + expr_ref_vector const &es; + +public: + bounded_pp_exprs(expr_ref_vector const &es) : es(es) {} + + std::ostream &display(std::ostream &out) const { + for (auto e : es) + out << mk_bounded_pp(e, es.get_manager()) << "\n"; + return out; + } +}; + +inline std::ostream &operator<<(std::ostream &out, bounded_pp_exprs const &pp) { + return pp.display(out); +} + /* ------------------------------------------------------------------ */ /* Search-tree literal configuration */ /* ------------------------------------------------------------------ */ @@ -98,12 +89,23 @@ tactic* mk_parallel_tactic2(solver* s, params_ref const& p) { struct solver_cube_config { using literal = expr_ref; static bool literal_is_null(expr_ref const& l) { return l == nullptr; } + static bool same_atom(expr_ref const& a, expr_ref const& b) { + expr* atom_a = a.get(); + expr* atom_b = b.get(); + a.get_manager().is_not(atom_a, atom_a); + b.get_manager().is_not(atom_b, atom_b); + return atom_a == atom_b; + } static std::ostream& display_literal(std::ostream& out, expr_ref const& l) { if (l) return out << mk_bounded_pp(l, l.get_manager()); return out << "(null)"; } }; +static bool is_cancellation_exception(char const* msg) { + return msg && (strstr(msg, "canceled") != nullptr || strstr(msg, "cancelled") != nullptr); +} + /* ------------------------------------------------------------------ */ /* parallel_solver – the core portfolio engine */ /* ------------------------------------------------------------------ */ @@ -112,11 +114,21 @@ class parallel_solver { /* ---- forward declarations ---- */ class worker; + class core_minimizer_worker; + class backbones_worker; /* ---- node lease (mirrors smt_parallel) ---- */ struct node_lease { search_tree::node* leased_node = nullptr; + + // Cancellation generation counter for this node/subtree. + // Incremented when the node is closed; used to signal that all + // workers holding leases on this node (or its descendants) + // must abandon work immediately. unsigned cancel_epoch = 0; + + // Guards against multiple inc_cancel() calls for the same lease. + // Set when cancel_lease() is signaled; cleared when a new lease is assigned. bool cancel_signaled = false; }; @@ -126,11 +138,16 @@ class parallel_solver { expr_ref clause; }; - /* ================================================================ - * batch_manager - * Coordinates workers: distributes cubes, collects clauses/units, - * stores the final result (sat model / unsat core / exception). - * ================================================================ */ + struct bb_candidate { + expr_ref lit; + double age; + unsigned hits; // how many cubes reported it + bb_candidate(ast_manager& m, expr* e, double s, unsigned h) + : lit(e, m), age(s), hits(h) {} + }; + + using bb_candidates = vector; + class batch_manager { enum state { @@ -145,6 +162,19 @@ class parallel_solver { unsigned m_num_cubes = 0; unsigned m_max_cube_depth = 0; unsigned m_backbones_found = 0; + unsigned m_core_min_jobs_enqueued = 0; + unsigned m_core_min_jobs_published = 0; + unsigned m_core_min_jobs_skipped = 0; + unsigned m_core_min_global_unsat = 0; + unsigned m_bb_candidates_enqueued = 0; + unsigned m_bb_batches_issued = 0; + }; + + struct core_min_job { + search_tree::node* source = nullptr; + expr_ref_vector core; + core_min_job(ast_manager& m, search_tree::node* source) + : source(source), core(m) {} }; ast_manager& m; @@ -156,28 +186,49 @@ class parallel_solver { search_tree::tree m_search_tree; vector m_worker_leases; - /* shared clause pool (guarded by mux) */ - vector m_shared_clause_trail; - obj_hashtable m_shared_clause_set; + vector m_shared_clause_trail; // store all shared clauses with worker IDs + obj_hashtable m_shared_clause_set; // for duplicate filtering on per-thread clause expressions - /* shared backbone / unit pool (guarded by mux) */ obj_hashtable m_global_backbones; - /* result storage (guarded by mux) */ + bb_candidates m_bb_candidates; + unsigned m_max_global_bb_candidates = 100; + unsigned m_bb_batch_size = 150; + std::atomic m_bb_candidate_epoch = 0; + std::condition_variable m_bb_cv; + bb_candidates m_bb_current_batch; + unsigned m_bb_batch_id = 0; + unsigned m_num_bb_threads = 0; + unsigned_vector m_bb_last_batch_processed; + unsigned m_bb_cancel_epoch = 0; // When a backbone worker finishes early, it increments m_bb_cancel_epoch and notifies all + + // Core minimization job queue + std::condition_variable m_core_min_cv; + scoped_ptr_vector m_core_min_jobs; + unsigned m_exception_code = 0; std::string m_exception_msg; - model_ref m_model; /* sat model translated to m */ - expr_ref_vector m_unsat_core; /* unsat core translated to m */ + model_ref m_model; + expr_ref_vector m_unsat_core; - /* ---- cancellation helpers (called under mux) ---- */ + // called from batch manager to cancel other workers if we've reached a verdict void cancel_workers_unlocked() { - IF_VERBOSE(1, verbose_stream() << "par2: canceling workers\n"); + IF_VERBOSE(1, verbose_stream() << "Canceling workers\n"); for (auto* w : p.m_workers) w->cancel(); + if (p.m_core_minimizer_worker) { + p.m_core_minimizer_worker->cancel(); + m_core_min_cv.notify_all(); + } + if (!p.m_global_backbones_workers.empty()) + IF_VERBOSE(1, verbose_stream() << "Canceling backbones workers\n"); + for (auto* w : p.m_global_backbones_workers) + w->cancel(); + if (!p.m_global_backbones_workers.empty()) + m_bb_cv.notify_all(); } - void release_lease_unlocked(unsigned worker_id, - search_tree::node* n) { + void release_lease_unlocked(unsigned worker_id, search_tree::node* n) { if (worker_id >= m_worker_leases.size()) return; auto& lease = m_worker_leases[worker_id]; if (!lease.leased_node || lease.leased_node != n) return; @@ -198,9 +249,7 @@ class parallel_solver { } } - void collect_clause_unlocked(ast_translation& l2g, - unsigned source_worker_id, - expr* clause) { + void collect_clause_unlocked(ast_translation& l2g, unsigned source_worker_id, expr* clause) { expr* g_clause = l2g(clause); if (!m_shared_clause_set.contains(g_clause)) { m_shared_clause_set.insert(g_clause); @@ -209,12 +258,184 @@ class parallel_solver { } } - bool is_global_backbone_unlocked(ast_translation& l2g, - expr* bb_cand) { + // to avoid deadlock + bool is_global_backbone_unlocked(ast_translation& l2g, expr* bb_cand) { expr_ref cand(l2g(bb_cand), m); return m_global_backbones.contains(cand.get()); } + bool is_global_backbone_or_negation_unlocked(ast_translation& l2g, expr* bb_cand) { + expr_ref cand(l2g(bb_cand), m); + expr_ref neg_cand(mk_not(m, cand), m); + return m_global_backbones.contains(cand.get()) || + m_global_backbones.contains(neg_cand.get()); + } + + void collect_matching_targets_unlocked(search_tree::node* source, + expr* lit, + vector const& core, + vector& targets) { + targets.reset(); + if (!lit) + return; + + auto is_ancestor_of = [&](search_tree::node* ancestor, + search_tree::node* cur) { + if (!ancestor) + return false; + for (auto* p = cur; p; p = p->parent()) { + if (p == ancestor) + return true; + } + return false; + }; + + auto path_contains = [&](search_tree::node* cur, + solver_cube_config::literal const& lit0) { + for (auto* p = cur; p; p = p->parent()) { + if (p->get_literal() == lit0) + return true; + } + return false; + }; + + auto path_contains_core = [&](search_tree::node* cur) { + return all_of(core, [&](solver_cube_config::literal const& c) { + return path_contains(cur, c); + }); + }; + + ptr_vector> matches; + m_search_tree.find_nonclosed_nodes_with_literal(expr_ref(lit, m), matches); + for (auto* t : matches) { + if (!t || t == source) + continue; + if (m_search_tree.is_lease_canceled(t, t->get_cancel_epoch())) + continue; + + // When source is provided, keep only external matches. Nodes in the + // same branch are already closed by backtracking on the source node. + if (source && (is_ancestor_of(source, t) || is_ancestor_of(t, source))) + continue; + + // Reusing a conflict on another branch is sound only if that + // the path from that node->root contains every literal in the core. + // Matching on the closing literal alone is insufficient: F & a & l + // may be UNSAT while F & c & l is SAT. + if (!path_contains_core(t)) + continue; + + // Keep only highest matching nodes: closing an ancestor also closes + // all of its matching descendants. + bool is_highest_ancestor = true; + for (auto* p = t->parent(); p; p = p->parent()) { + if (any_of(targets, [&](node_lease const& target) { return target.leased_node == p; })) { + is_highest_ancestor = false; + break; + } + } + if (!is_highest_ancestor) + continue; + + targets.push_back({ t, t->get_cancel_epoch() }); + } + } + + // Given a newly closed node, source, and its core, find the lowest ancestor of source that + // contains a core literal, and return it as the source for the core minimization job + search_tree::node* find_core_source_unlocked( + ast_translation& l2g, search_tree::node* source, expr_ref_vector const& core) { + if (!source) + return nullptr; + + vector g_core; + for (expr* c : core) + g_core.push_back(expr_ref(l2g(c), m)); + + for (auto* cur = source; cur; cur = cur->parent()) { + if (solver_cube_config::literal_is_null(cur->get_literal())) + continue; + if (any_of(g_core, [&](solver_cube_config::literal const& lit) { return lit == cur->get_literal(); })) + return cur; + } + return nullptr; + } + + unsigned select_best_core_min_job_unlocked() const { + SASSERT(!m_core_min_jobs.empty()); + unsigned best_idx = 0; + auto* best_source = m_core_min_jobs[0]->source; + unsigned best_depth = best_source ? best_source->depth() : 0; + unsigned best_core_size = m_core_min_jobs[0]->core.size(); + + for (unsigned i = 1; i < m_core_min_jobs.size(); ++i) { + auto* job = m_core_min_jobs[i]; + auto* job_source = job->source; + unsigned job_depth = job_source ? job_source->depth() : 0; + unsigned job_core_size = job->core.size(); + + // rank first by core source node depth (deepest -> shallowest), then by core size (largest -> smallest) + if (job_depth > best_depth || + (job_depth == best_depth && job_core_size > best_core_size)) { + best_idx = i; + best_depth = job_depth; + best_core_size = job_core_size; + } + } + return best_idx; + } + + void backtrack_unlocked(ast_translation& l2g, unsigned worker_id, + expr_ref_vector const& core, + node_lease const* lease = nullptr, + vector const* targets = nullptr) { + if (m_state != state::is_running) + return; + + vector g_core; + for (expr* c : core) + g_core.push_back(expr_ref(l2g(c), m)); + + SASSERT(lease != nullptr || targets != nullptr); + bool did_backtrack = false; + + if (lease && !m_search_tree.is_lease_canceled(lease->leased_node, lease->cancel_epoch)) { + // we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled + // i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack + did_backtrack = true; + release_lease_unlocked(worker_id, lease->leased_node); + m_search_tree.backtrack(lease->leased_node, g_core); + } + if (targets) { + for (auto const& target : *targets) { + if (m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch)) + continue; + did_backtrack = true; + m_search_tree.backtrack(target.leased_node, g_core); + } + } + if (!did_backtrack) + return; + + // terminate on-demand the workers that are currently exploring the now-closed nodes + cancel_closed_leases_unlocked(worker_id); + + IF_VERBOSE(2, + for (expr* e : core) + verbose_stream() << mk_bounded_pp(e, core.get_manager()) << "\n"; + m_search_tree.display(verbose_stream() << "\n"); + ); + + if (m_search_tree.is_closed()) { + IF_VERBOSE(1, verbose_stream() << "Search tree closed, setting UNSAT\n"); + m_state = state::is_unsat; + SASSERT(m_unsat_core.empty()); + for (auto& e : m_search_tree.get_core_from_root()) + m_unsat_core.push_back(e.get()); + cancel_workers_unlocked(); + } + } + public: batch_manager(ast_manager& m, parallel_solver& p) @@ -222,25 +443,31 @@ class parallel_solver { m_search_tree(expr_ref(m)), m_unsat_core(m) {} - /* ---- initialisation ---- */ - void initialize(unsigned num_workers, - unsigned initial_max_thread_conflicts = 1000) { + void initialize(unsigned num_bb_threads, unsigned initial_max_thread_conflicts = 1000) { m_state = state::is_running; m_search_tree.reset(); m_search_tree.set_effort_unit(initial_max_thread_conflicts); m_worker_leases.reset(); - m_worker_leases.resize(num_workers); + m_worker_leases.resize(p.m_workers.size()); m_shared_clause_trail.reset(); m_shared_clause_set.reset(); m_global_backbones.reset(); + m_bb_candidates.reset(); + m_bb_current_batch.reset(); + m_bb_batch_id = 0; + m_num_bb_threads = num_bb_threads; + m_bb_last_batch_processed.reset(); + m_bb_last_batch_processed.resize(num_bb_threads); + m_bb_cancel_epoch = 0; + m_bb_candidate_epoch.store(0, std::memory_order_release); + m_core_min_jobs.reset(); m_model = nullptr; m_unsat_core.reset(); } - /* ---- result setters (called by workers, guarded by mux) ---- */ void set_sat(ast_translation& l2g, model& mdl) { std::scoped_lock lock(mux); - IF_VERBOSE(1, verbose_stream() << "par2: batch_manager SAT\n"); + IF_VERBOSE(1, verbose_stream() << "Batch manager setting SAT.\n"); if (m_state != state::is_running) return; m_state = state::is_sat; m_model = mdl.translate(l2g); @@ -250,7 +477,7 @@ class parallel_solver { void set_unsat(ast_translation& l2g, expr_ref_vector const& core) { std::scoped_lock lock(mux); - IF_VERBOSE(1, verbose_stream() << "par2: batch_manager UNSAT\n"); + IF_VERBOSE(1, verbose_stream() << "Batch manager setting UNSAT.\n"); if (m_state != state::is_running) return; m_state = state::is_unsat; SASSERT(m_unsat_core.empty()); @@ -261,7 +488,7 @@ class parallel_solver { void set_exception(std::string const& msg) { std::scoped_lock lock(mux); - IF_VERBOSE(1, verbose_stream() << "par2: batch_manager exception: " << msg << "\n"); + IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception msg: " << msg << ".\n"); if (m_state != state::is_running) return; m_state = state::is_exception_msg; m_exception_msg = msg; @@ -270,13 +497,13 @@ class parallel_solver { void set_exception(unsigned error_code) { std::scoped_lock lock(mux); + IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n"); if (m_state != state::is_running) return; m_state = state::is_exception_code; m_exception_code = error_code; cancel_workers_unlocked(); } - /* ---- cube distribution (called by workers) ---- */ bool get_cube(ast_translation& g2l, unsigned id, expr_ref_vector& cube, bool is_first_run, node_lease& lease) { @@ -296,7 +523,6 @@ class parallel_solver { m_worker_leases.resize(id + 1); m_worker_leases[id] = lease; - /* build cube from path root → t */ for (auto* cur = t; cur; cur = cur->parent()) { if (solver_cube_config::literal_is_null(cur->get_literal())) break; @@ -305,37 +531,139 @@ class parallel_solver { return true; } - /* ---- backtrack on conflict (called by workers) ---- */ void backtrack(ast_translation& l2g, unsigned worker_id, expr_ref_vector const& core, node_lease const& lease) { std::scoped_lock lock(mux); if (m_state != state::is_running) return; - vector g_core; - for (auto c : core) + for (expr* c : core) g_core.push_back(expr_ref(l2g(c), m)); - if (!m_search_tree.is_lease_canceled( - lease.leased_node, lease.cancel_epoch)) { - release_lease_unlocked(worker_id, lease.leased_node); - m_search_tree.backtrack(lease.leased_node, g_core); + vector targets; + expr* lit = lease.leased_node ? lease.leased_node->get_literal().get() : nullptr; + collect_matching_targets_unlocked(lease.leased_node, lit, g_core, targets); + backtrack_unlocked(l2g, worker_id, core, &lease, targets.empty() ? nullptr : &targets); + } + + void enqueue_core_minimization(ast_translation& l2g, + search_tree::node* source, + expr_ref_vector const& core) { + std::scoped_lock lock(mux); + if (m_state != state::is_running || !p.m_core_minimizer_worker || !source || core.empty()) + return; + if (core.size() <= 1) { + ++m_stats.m_core_min_jobs_skipped; + return; } - cancel_closed_leases_unlocked(worker_id); + source = find_core_source_unlocked(l2g, source, core); + if (!source) { + ++m_stats.m_core_min_jobs_skipped; + return; + } - IF_VERBOSE(2, m_search_tree.display(verbose_stream() << "\n");); + scoped_ptr job = alloc(core_min_job, m, source); + for (expr* c : core) + job->core.push_back(l2g(c)); + m_core_min_jobs.push_back(job.detach()); + ++m_stats.m_core_min_jobs_enqueued; + m_core_min_cv.notify_one(); + } - if (m_search_tree.is_closed()) { - IF_VERBOSE(1, verbose_stream() << "par2: search tree closed → UNSAT\n"); + bool wait_for_core_min_job(ast_translation& g2l, + search_tree::node*& source, + expr_ref_vector& core, + reslimit& lim) { + std::unique_lock lock(mux); + m_core_min_cv.wait(lock, [&]() { + return lim.is_canceled() || m_state != state::is_running || !m_core_min_jobs.empty(); + }); + + if (lim.is_canceled() || m_state != state::is_running) + return false; + + unsigned best_idx = select_best_core_min_job_unlocked(); + m_core_min_jobs.swap(best_idx, m_core_min_jobs.size() - 1); + core_min_job* job = m_core_min_jobs.detach_back(); + m_core_min_jobs.pop_back(); + SASSERT(job); + source = job->source; + core.reset(); + for (expr* c : job->core) + core.push_back(g2l(c)); + dealloc(job); + return source != nullptr; + } + + void publish_minimized_core(ast_translation& l2g, + expr_ref_vector const& asms, + search_tree::node* source, + unsigned original_core_size, + expr_ref_vector const& minimized_core) { + std::scoped_lock lock(mux); + if (m_state != state::is_running || !source || minimized_core.size() >= original_core_size) { + ++m_stats.m_core_min_jobs_skipped; + return; + } + + vector g_core; + for (expr* c : minimized_core) + g_core.push_back(expr_ref(l2g(c), m)); + + // don't publish a minimized core if the node already has an equal-or-smaller core by the time the minimizer thread finishes + // (e.g. from another thread or from backtracking resolution propagation) + if (source->get_core().size() <= g_core.size()) { + ++m_stats.m_core_min_jobs_skipped; + return; + } + + if (all_of(g_core, [&](solver_cube_config::literal const& lit) { return asms.contains(lit.get()); })) { + IF_VERBOSE(1, verbose_stream() << "Minimized core removed all path literals, setting UNSAT\n"); m_state = state::is_unsat; + SASSERT(m_unsat_core.empty()); + for (expr* e : minimized_core) + m_unsat_core.push_back(l2g(e)); + ++m_stats.m_core_min_jobs_published; + ++m_stats.m_core_min_global_unsat; + cancel_workers_unlocked(); + return; + } + + // do not backtrack through the batch manager since this only handles non-closed leases + // and the batch manager also tries to search for external matching targets in the tree + // which is a problem since we must backtrack only on the source node or the core is invalid + m_search_tree.backtrack(source, g_core); + + vector targets; + if (!g_core.empty()) { + collect_matching_targets_unlocked(source, g_core[0].get(), g_core, targets); + for (auto const& target : targets) { + if (!m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch)) + m_search_tree.backtrack(target.leased_node, g_core); + } + } + + ++m_stats.m_core_min_jobs_published; + cancel_closed_leases_unlocked(UINT_MAX); + + IF_VERBOSE(1, verbose_stream() << "Batch manager publishing minimized core " + << original_core_size << " -> " << minimized_core.size() << "\n"); + IF_VERBOSE(2, + for (expr* e : minimized_core) + verbose_stream() << mk_bounded_pp(e, minimized_core.get_manager()) << "\n"; + m_search_tree.display(verbose_stream() << "\n"); + ); + if (m_search_tree.is_closed()) { + IF_VERBOSE(1, verbose_stream() << "Search tree closed by minimized core, setting UNSAT\n"); + m_state = state::is_unsat; + SASSERT(m_unsat_core.empty()); for (auto& e : m_search_tree.get_core_from_root()) m_unsat_core.push_back(e.get()); cancel_workers_unlocked(); } } - /* ---- try to split (called on undef) ---- */ void try_split(ast_translation& l2g, unsigned worker_id, node_lease const& lease, expr* atom, unsigned effort) { @@ -347,6 +675,8 @@ class parallel_solver { expr_ref lit(m), nlit(m); lit = l2g(atom); nlit = mk_not(m, lit); + VERIFY(!lease.leased_node->path_contains_atom(lit)); + VERIFY(!lease.leased_node->path_contains_atom(nlit)); bool did_split = m_search_tree.try_split( lease.leased_node, lease.cancel_epoch, @@ -359,8 +689,7 @@ class parallel_solver { m_stats.m_max_cube_depth = std::max( m_stats.m_max_cube_depth, lease.leased_node->depth() + 1); - IF_VERBOSE(1, verbose_stream() << "par2: split on " - << mk_bounded_pp(lit, m, 3) << "\n"); + IF_VERBOSE(1, verbose_stream() << "Batch manager splitting on literal: " << mk_bounded_pp(lit, m, 3) << "\n"); } } @@ -376,7 +705,6 @@ class parallel_solver { lease.leased_node, lease.cancel_epoch); } - /* ---- clause sharing ---- */ void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause) { @@ -384,41 +712,178 @@ class parallel_solver { collect_clause_unlocked(l2g, source_worker_id, clause); } - expr_ref_vector return_shared_clauses(ast_translation& g2l, - unsigned& worker_limit, - unsigned worker_id) { + expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id) { std::scoped_lock lock(mux); expr_ref_vector result(g2l.to()); for (unsigned i = worker_limit; i < m_shared_clause_trail.size(); ++i) { if (m_shared_clause_trail[i].source_worker_id != worker_id) result.push_back(g2l(m_shared_clause_trail[i].clause.get())); } - worker_limit = m_shared_clause_trail.size(); + worker_limit = m_shared_clause_trail.size(); // update the worker limit to the end of the current trail return result; } - /* ---- backbone / unit sharing ---- */ - bool collect_global_backbone(ast_translation& l2g, - expr_ref const& backbone, - unsigned source_worker_id = UINT_MAX) { + bool collect_global_backbone(ast_translation& l2g, expr_ref const& backbone, unsigned source_worker_id = UINT_MAX) { std::scoped_lock lock(mux); + IF_VERBOSE(1, verbose_stream() << "collect-global-backbone\n"); if (is_global_backbone_unlocked(l2g, backbone.get())) return false; expr_ref g_bb(l2g(backbone.get()), m); m_global_backbones.insert(g_bb.get()); ++m_stats.m_backbones_found; - IF_VERBOSE(2, verbose_stream() << "par2: new backbone " - << mk_bounded_pp(g_bb, m, 3) << "\n"); - /* share it as a unit clause so other workers pick it up */ + IF_VERBOSE(1, verbose_stream() << " Found and sharing new global backbone: " << mk_bounded_pp(g_bb, m, 3) << "\n"); collect_clause_unlocked(l2g, source_worker_id, backbone.get()); + + expr_ref neg_g_bb(mk_not(m, g_bb), m); + vector g_core; + g_core.push_back(neg_g_bb); + vector targets; + collect_matching_targets_unlocked(nullptr, neg_g_bb, g_core, targets); + + if (!targets.empty()) { + IF_VERBOSE(1, verbose_stream() << " Closing negation of the new global backbone: " + << mk_bounded_pp(g_bb, m, 3) << "\n"); + expr_ref_vector l_core(l2g.from()); + l_core.push_back(mk_not(backbone)); + backtrack_unlocked(l2g, UINT_MAX, l_core, nullptr, &targets); + } + + return true; + } + + bool is_global_backbone_or_negation(ast_translation& l2g, expr* bb_cand) { + std::scoped_lock lock(mux); + return is_global_backbone_or_negation_unlocked(l2g, bb_cand); + } + + bool has_new_backbone_candidates(unsigned epoch) { + return m_bb_candidate_epoch.load(std::memory_order_acquire) != epoch; + } + + unsigned get_bb_candidate_epoch() const { + return m_bb_candidate_epoch.load(std::memory_order_acquire); + } + + void cancel_current_backbone_batch() { + std::scoped_lock lock(mux); + ++m_bb_cancel_epoch; + m_bb_cv.notify_all(); + } + + unsigned get_cancel_epoch() { + std::scoped_lock lock(mux); + return m_bb_cancel_epoch; + } + + expr_ref_vector get_global_backbones_snapshot(ast_translation& g2l) { + std::scoped_lock lock(mux); + expr_ref_vector snapshot(g2l.to()); + for (expr* gb : m_global_backbones) + snapshot.push_back(g2l(gb)); + return snapshot; + } + + void collect_backbone_candidates(ast_translation& l2g, + bb_candidates& bb_candidates) { + std::scoped_lock lock(mux); + bool changed = false; + + auto find_existing_candidate_idx = [&](expr* e) -> int { + for (unsigned i = 0; i < m_bb_candidates.size(); ++i) { + if (m_bb_candidates[i].lit.get() == e) + return i; + } + return -1; + }; + + auto rank_of = [&](bb_candidate const& c) { + return c.age * std::log2(2.0 + c.hits); + }; + + for (auto const& c : bb_candidates) { + expr_ref g_lit(l2g(c.lit.get()), m); + if (is_global_backbone_or_negation_unlocked(l2g, c.lit.get())) + continue; + + double age = c.age; + int idx = find_existing_candidate_idx(g_lit.get()); + if (idx >= 0) { + auto& existing = m_bb_candidates[idx]; + existing.age = (existing.age * existing.hits + age) / (existing.hits + 1); + existing.hits++; + continue; + } + + if (m_bb_candidates.size() < m_max_global_bb_candidates) { + m_bb_candidates.push_back(bb_candidate(m, g_lit.get(), age, 1)); + changed = true; + continue; + } + + bb_candidate incoming(m, g_lit.get(), age, 1); + auto worst_it = std::min_element( + m_bb_candidates.begin(), + m_bb_candidates.end(), + [&](bb_candidate const& a, bb_candidate const& b) { + return rank_of(a) < rank_of(b); + }); + if (worst_it != m_bb_candidates.end() && rank_of(incoming) > rank_of(*worst_it)) { + *worst_it = incoming; + changed = true; + } + } + + if (changed && !m_bb_candidates.empty()) { + m_bb_candidate_epoch.fetch_add(1, std::memory_order_release); + std::sort( + m_bb_candidates.begin(), + m_bb_candidates.end(), + [&](bb_candidate const& a, bb_candidate const& b) { + return rank_of(a) < rank_of(b); + }); + m_bb_cv.notify_all(); + } + } + + bool wait_for_backbone_job(unsigned bb_thread_id, ast_translation& g2l, + bb_candidates& out, reslimit& lim) { + out.reset(); + std::unique_lock lock(mux); + m_bb_cv.wait(lock, [&]() { + return lim.is_canceled() || + m_state != state::is_running || + m_bb_last_batch_processed[bb_thread_id] < m_bb_batch_id || + !m_bb_candidates.empty(); + }); + + if (lim.is_canceled() || m_state != state::is_running) + return false; + + if (m_bb_last_batch_processed[bb_thread_id] == m_bb_batch_id) { + unsigned n = std::min(m_bb_batch_size, m_bb_candidates.size()); + m_bb_current_batch.reset(); + for (unsigned i = 0; i < n; ++i) { + m_bb_current_batch.push_back(m_bb_candidates.back()); + m_bb_candidates.pop_back(); + } + ++m_bb_batch_id; + m_bb_cv.notify_all(); + } + + for (auto const& gc : m_bb_current_batch) { + expr_ref l_lit(g2l(gc.lit.get()), g2l.to()); + out.push_back(bb_candidate(g2l.to(), l_lit, gc.age, gc.hits)); + } + m_bb_last_batch_processed[bb_thread_id] = m_bb_batch_id; return true; } - /* ---- result accessors ---- */ lbool get_result() const { - if (m.limit().is_canceled()) return l_undef; + if (m.limit().is_canceled()) + return l_undef; // the main context was cancelled, so we return undef. switch (m_state) { - case state::is_running: + case state::is_running: // batch manager is still running, but all threads have processed their cubes, which + // means all cubes were unsat throw default_exception("par2: inconsistent end state"); case state::is_sat: return l_true; case state::is_unsat: return l_false; @@ -437,11 +902,15 @@ class parallel_solver { expr_ref_vector const& get_unsat_core() const { return m_unsat_core; } void collect_statistics(statistics& st) const { - st.update("par2-cubes", m_stats.m_num_cubes); - st.update("par2-cube-depth", m_stats.m_max_cube_depth); - st.update("par2-backbones", m_stats.m_backbones_found); + st.update("parallel-num_cubes", m_stats.m_num_cubes); + st.update("parallel-max-cube-size", m_stats.m_max_cube_depth); + st.update("bb-backbones-found", m_stats.m_backbones_found); + st.update("parallel-core-min-jobs-enqueued", m_stats.m_core_min_jobs_enqueued); + st.update("parallel-core-min-jobs-published", m_stats.m_core_min_jobs_published); + st.update("parallel-core-min-jobs-skipped", m_stats.m_core_min_jobs_skipped); + st.update("parallel-core-min-global-unsat", m_stats.m_core_min_global_unsat); } - }; // class batch_manager + }; /* ================================================================ * worker @@ -450,50 +919,48 @@ class parallel_solver { * batch_manager (mutex-protected). * ================================================================ */ class worker { - struct config { - unsigned m_threads_max_conflicts = 1000; - double m_max_conflict_mul = 1.5; - unsigned m_max_conflicts = UINT_MAX; - bool m_share_units = true; - bool m_share_conflicts = true; - unsigned m_max_cube_depth = 20; + struct config { + unsigned m_threads_max_conflicts = 1000; + double m_max_conflict_mul = 1.5; + unsigned m_max_conflicts = UINT_MAX; + bool m_share_units = true; + bool m_share_conflicts = true; + bool m_share_units_relevant_only = true; + bool m_share_units_initial_only = true; + bool m_core_minimize = false; + bool m_global_backbones = false; + unsigned m_max_cube_depth = 20; }; unsigned id; - parallel_solver& p; batch_manager& b; ast_manager m; /* worker-local manager */ ref s; /* translated solver copy */ expr_ref_vector asms; /* translated assumptions */ ast_translation m_g2l, m_l2g; /* global↔local translations */ config m_config; - expr_mark m_known_units; /* units already shared by this worker */ + uint_set m_known_units; /* bool vars already shared by this worker */ unsigned m_shared_clause_limit = 0; + unsigned m_shared_units_prefix = 0; + unsigned m_num_initial_atoms = 0; - void update_max_conflicts() { + void update_max_thread_conflicts() { m_config.m_threads_max_conflicts = static_cast( m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts); - /* cap at the configured global maximum to prevent runaway cube checks */ - if (m_config.m_threads_max_conflicts > m_config.m_max_conflicts) - m_config.m_threads_max_conflicts = m_config.m_max_conflicts; } - /* Check the current cube (passed as additional assumptions). - * The solver's conflict budget is set via updt_params before - * each call so that long-running cubes are interrupted. */ lbool check_cube(expr_ref_vector const& cube) { - params_ref p; - p.set_uint("max_conflicts", - std::min(m_config.m_threads_max_conflicts, - m_config.m_max_conflicts)); - s->updt_params(p); + s->set_max_conflicts(std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts)); expr_ref_vector combined(m); combined.append(asms); combined.append(cube); - IF_VERBOSE(2, verbose_stream() << "par2 worker " << id - << ": checking cube of size " << cube.size() << "\n"); + IF_VERBOSE(1, verbose_stream() << " Checking cube\n" + << bounded_pp_exprs(cube) + << "with max_conflicts: " + << std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts) + << "\n";); lbool r = l_undef; try { r = s->check_sat(combined); @@ -503,94 +970,141 @@ class parallel_solver { b.set_exception(err.error_code()); } catch (z3_exception& ex) { - if (!m.limit().is_canceled()) + if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what())) b.set_exception(ex.what()); } - IF_VERBOSE(2, verbose_stream() << "par2 worker " << id - << ": cube result " << r << "\n"); + LOG_WORKER(1, " DONE checking cube " << r << "\n";); return r; } - /* Assert shared clauses discovered by other workers into the - * base assertion set of this worker's solver. The solver - * automatically re-uses them on the next check_sat call. */ void collect_shared_clauses() { - expr_ref_vector nc = b.return_shared_clauses( - m_g2l, m_shared_clause_limit, id); + expr_ref_vector nc = b.return_shared_clauses(m_g2l, m_shared_clause_limit, id); for (expr* e : nc) { - IF_VERBOSE(4, verbose_stream() << "par2 worker " << id - << ": asserting shared clause " - << mk_bounded_pp(e, m, 3) << "\n"); + LOG_WORKER(4, " asserting shared clause: " << mk_bounded_pp(e, m, 3) << "\n"); s->assert_expr(e); } } - /* Propagate any new base-level units (backbone literals) this - * worker has learned to the shared backbone pool. - * - * Uses solver::get_trail(0) which returns all literals - * propagated at decision level 0. */ void share_units() { - if (!m_config.m_share_units) return; - expr_ref_vector trail = s->get_trail(0); - for (expr* e : trail) { - /* get_trail may include ground terms; skip complex ones */ + if (!m_config.m_share_units) + return; + expr_ref_vector trail = s->get_assigned_literals(); + unsigned sz = trail.size(); + unsigned prefix_sz = std::min(m_shared_units_prefix, sz); + bool at_prefix = true; + + for (unsigned i = m_shared_units_prefix; i < sz; ++i) { + expr* e = trail.get(i); + if (s->get_assign_level(e) > 0) { + at_prefix = false; + continue; + } + + if (at_prefix) + ++prefix_sz; + expr* atom = e; m.is_not(e, atom); - if (!is_uninterp_const(atom)) continue; - if (m_known_units.is_marked(e)) continue; - m_known_units.mark(e); + + if (m.is_and(atom) || m.is_or(atom) || m.is_ite(atom) || m.is_iff(atom)) + continue; + + unsigned v = s->get_bool_var(atom); + if (v == UINT_MAX) + continue; + if (m_known_units.contains(v)) + continue; + m_known_units.insert(v); + + if (m_config.m_share_units_relevant_only && !s->is_relevant(atom)) + continue; + if (m_config.m_share_units_initial_only && v >= m_num_initial_atoms) + continue; + expr_ref lit(e, m); b.collect_global_backbone(m_l2g, lit, id); } + m_shared_units_prefix = prefix_sz; } - /* Select a split atom using solver::cube() on a temporary - * solver state that includes the current cube path. - * - * We push the cube literals, call cube(), take the first - * literal, then pop to restore the base state. */ expr_ref get_split_atom(expr_ref_vector const& cube) { if (cube.size() >= m_config.m_max_cube_depth) return expr_ref(nullptr, m); - s->push(); - for (expr* c : cube) - s->assert_expr(c); - expr_ref_vector vars(m); - expr_ref_vector c = s->cube(vars, UINT_MAX); + obj_hashtable rejected_atoms; + while (true) { + expr_ref_vector cands = s->cube(vars, 1); + bool rejected = false; + for (expr* lit : cands) { + if (!lit) + continue; + if (m.is_true(lit) || m.is_false(lit)) + continue; + if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) { + expr* atom = lit; + m.is_not(lit, atom); + rejected_atoms.insert(atom); + rejected = true; + continue; + } + return expr_ref(lit, m); + } - s->pop(1); + if (!rejected || vars.empty()) + return expr_ref(nullptr, m); - /* solver::cube() convention: an empty result means done; a result - * whose last element is true means the problem is trivially sat; - * a result whose last element is false means unsat was detected. - * In all other cases every element (including index 0) is a - * valid literal that can serve as a split atom. */ - if (c.empty() || m.is_true(c.back()) || m.is_false(c.back())) - return expr_ref(nullptr, m); + expr_ref_vector next_vars(m); + for (expr* v : vars) { + expr* atom = v; + m.is_not(v, atom); + if (!rejected_atoms.contains(atom)) + next_vars.push_back(v); + } + if (next_vars.empty() || next_vars.size() == vars.size()) + return expr_ref(nullptr, m); + vars.reset(); + vars.append(next_vars); + } + } - return expr_ref(c.get(0), m); + bb_candidates find_backbone_candidates(expr_ref_vector const& cube, unsigned k = 10) { + bb_candidates result; + vector cands; + s->get_backbone_candidates(cands, s->get_num_bool_vars()); + + for (auto const& cand : cands) { + expr* lit = cand.lit.get(); + if (m_config.m_global_backbones && + b.is_global_backbone_or_negation(m_l2g, lit)) + continue; + result.push_back(bb_candidate(m, lit, cand.score, 1)); + if (result.size() >= k) + break; + } + return result; } public: - worker(unsigned id, parallel_solver& p, - solver& src, params_ref const& params, - expr_ref_vector const& src_asms) - : id(id), p(p), b(p.m_batch_manager), - asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) - { - /* create translated solver copy */ - s = src.translate(m, params); + worker(unsigned id, parallel_solver& p, solver& src, params_ref const& params, expr_ref_vector const& src_asms) + : id(id), b(p.m_batch_manager), asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { + parallel_params pp(params); + m_config.m_core_minimize = pp.core_minimize(); + m_config.m_global_backbones = pp.num_bb_threads() > 0; + + s = src.translate(m, params); + // don't share initial units + s->pop_to_base_level(); + m_shared_units_prefix = s->get_assigned_literals().size(); + m_num_initial_atoms = s->get_num_bool_vars(); + // avoid preprocessing lemmas that are exchanged + s->set_preprocess(false); - /* translate assumptions */ for (expr* a : src_asms) asms.push_back(m_g2l(a)); - IF_VERBOSE(1, verbose_stream() << "par2: worker " << id - << " created (" << asms.size() << " assumptions)\n"); + LOG_WORKER(1, " created with " << asms.size() << " assumptions\n"); } void run() { @@ -600,19 +1114,23 @@ class parallel_solver { while (true) { if (!b.get_cube(m_g2l, id, cube, is_first_run, lease)) { - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": no more cubes\n"); + LOG_WORKER(1, " no more cubes\n"); return; } is_first_run = false; - collect_shared_clauses(); - + check_cube_start: + LOG_WORKER(1, " CUBE SIZE IN MAIN LOOP: " << cube.size() << "\n"); + if (m_config.m_global_backbones) { + bb_candidates local_candidates = find_backbone_candidates(cube); + b.collect_backbone_candidates(m_l2g, local_candidates); + if (!m.inc()) + return; + } lbool r = check_cube(cube); if (b.lease_canceled(lease)) { - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": lease canceled\n"); + LOG_WORKER(1, " abandoning canceled lease\n"); lease = {}; m.limit().dec_cancel(); continue; @@ -623,24 +1141,24 @@ class parallel_solver { switch (r) { case l_undef: { - update_max_conflicts(); - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": undef – attempting split\n"); + update_max_thread_conflicts(); + LOG_WORKER(1, " found undef cube\n"); + if (m_config.m_max_cube_depth <= cube.size()) + goto check_cube_start; expr_ref atom = get_split_atom(cube); if (atom) { b.try_split(m_l2g, id, lease, atom.get(), m_config.m_threads_max_conflicts); + lease = {}; } else { - b.release_lease(id, lease); + goto check_cube_start; } - if (m_config.m_share_units) share_units(); break; } case l_true: { - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": SAT\n"); + LOG_WORKER(1, " found sat cube\n"); model_ref mdl; s->get_model(mdl); if (mdl) @@ -649,49 +1167,43 @@ class parallel_solver { } case l_false: { - IF_VERBOSE(1, verbose_stream() << "par2 worker " << id - << ": UNSAT cube\n"); - expr_ref_vector core(m); - s->get_unsat_core(core); + expr_ref_vector unsat_core(m); + s->get_unsat_core(unsat_core); + LOG_WORKER(2, " unsat core:\n"; + for (auto c : unsat_core) verbose_stream() << mk_bounded_pp(c, m, 3) << "\n"); - /* Filter to only cube literals (exclude base assumptions). */ - expr_ref_vector cube_core(m); - for (expr* c : core) { - if (cube.contains(c)) - cube_core.push_back(c); - } - - /* If core contains none of the cube lits, the whole - * problem is UNSAT independent of the cube path. */ - if (cube_core.empty()) { - b.set_unsat(m_l2g, core); + if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) { + LOG_WORKER(1, " determined formula unsat\n"); + b.set_unsat(m_l2g, unsat_core); return; } - b.backtrack(m_l2g, id, cube_core, lease); + LOG_WORKER(1, " found unsat cube\n"); + auto* source = lease.leased_node; + b.backtrack(m_l2g, id, unsat_core, lease); - if (m_config.m_share_conflicts) { - /* Share the negation of the cube-core conjunction - * as a learned clause: ¬(c₁ ∧ … ∧ cₙ) ≡ ¬c₁ ∨ … ∨ ¬cₙ */ - expr_ref_vector neg_lits(m); - for (expr* c : cube_core) - neg_lits.push_back(mk_not(expr_ref(c, m))); - expr_ref clause(mk_or(neg_lits), m); - b.collect_clause(m_l2g, id, clause.get()); - } - if (m_config.m_share_units) share_units(); + if (m_config.m_core_minimize) + b.enqueue_core_minimization(m_l2g, source, unsat_core); + lease = {}; + + if (m_config.m_share_conflicts) + b.collect_clause(m_l2g, id, mk_not(mk_and(unsat_core))); break; } - } // switch - } // while - } // run() + } + if (m_config.m_share_units) + share_units(); + } + } void cancel() { + LOG_WORKER(1, " canceling\n"); m.limit().cancel(); } void cancel_lease() { + LOG_WORKER(1, " canceling lease\n"); m.limit().inc_cancel(); } @@ -700,16 +1212,596 @@ class parallel_solver { } reslimit& limit() { return m.limit(); } - }; // class worker + }; + + class backbones_worker { + private: + struct stats { + unsigned m_batches_total = 0; + unsigned m_candidates_total = 0; + unsigned m_singleton_backbones = 0; + unsigned m_backbones_detected = 0; + unsigned m_internal_backbones_found = 0; + unsigned m_retry_backbones_found = 0; + unsigned m_bb_retries = 0; + unsigned m_fallback_singleton_checks = 0; + unsigned m_fallback_reason_chunk_exhausted = 0; + unsigned m_fallback_reason_undef = 0; + unsigned m_core_refinement_rounds = 0; + unsigned m_lits_removed_by_core = 0; + unsigned m_num_chunk_increases = 0; + }; + + unsigned id; + batch_manager& b; + ast_manager m; + ref s; + expr_ref_vector asms; + ast_translation m_g2l, m_l2g; + unsigned m_bb_chunk_size = 20; + unsigned m_bb_conflicts_per_chunk = 1000; + unsigned m_shared_clause_limit = 0; + stats m_stats; + unsigned m_shared_units_prefix = 0; + unsigned m_num_initial_atoms = 0; + bool m_positive_mode = false; + + void collect_shared_clauses() { + expr_ref_vector nc = b.return_shared_clauses(m_g2l, m_shared_clause_limit, UINT_MAX); + for (expr* e : nc) { + s->assert_expr(e); + LOG_BB_WORKER(4, " asserting shared clause: " << mk_bounded_pp(e, m, 3) << "\n"); + } + } + + bool try_get_unit_backbone(expr* candidate, expr_ref& backbone) { + expr_ref_vector trail = s->get_assigned_literals(); + expr* atom = candidate; + m.is_not(candidate, atom); + for (expr* e : trail) { + if (s->get_assign_level(e) > 0) + continue; + expr* trail_atom = e; + m.is_not(e, trail_atom); + if (trail_atom != atom) + continue; + backbone = expr_ref(e, m); + return true; + } + return false; + } + + lbool probe_literal(expr* e, bool is_retry) { + lbool r = l_undef; + try { + asms.push_back(e); + r = s->check_sat(asms); + asms.pop_back(); + } + catch (z3_error& err) { + asms.pop_back(); + if (!m.limit().is_canceled()) + b.set_exception(err.error_code()); + } + catch (z3_exception& ex) { + asms.pop_back(); + if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what())) + b.set_exception(ex.what()); + } + + if (r == l_false) { + expr_ref_vector core(m); + s->get_unsat_core(core); + if (!core.contains(e)) { + b.set_unsat(m_l2g, core); + return l_false; + } + expr_ref bb(mk_not(m, e), m); + ++m_stats.m_backbones_detected; + if (b.collect_global_backbone(m_l2g, bb)) { + ++m_stats.m_internal_backbones_found; + if (is_retry) + ++m_stats.m_retry_backbones_found; + } + s->assert_expr(bb.get()); + return l_undef; + } + if (r == l_true) { + model_ref mdl; + s->get_model(mdl); + if (mdl) + b.set_sat(m_l2g, *mdl); + } + return r; + } + + void run_batch_mode() { + bb_candidates curr_batch; + + while (m.inc()) { + if (!b.wait_for_backbone_job(id, m_g2l, curr_batch, m.limit())) { + LOG_BB_WORKER(1, " BACKBONES WORKER cancelling\n"); + return; + } + + if (curr_batch.empty()) + continue; + + LOG_BB_WORKER(1, " received batch of " << curr_batch.size() << " candidates\n"); + collect_shared_clauses(); + + unsigned local_cancel_epoch = b.get_cancel_epoch(); + auto canceled = [&] { return local_cancel_epoch != b.get_cancel_epoch(); }; + unsigned bb_candidate_epoch = b.get_bb_candidate_epoch(); + + auto fallback_failed_literal_probe = + [&](expr_ref_vector const& chunk_lits, expr_ref_vector& bb_candidate_lits, bool is_retry = false) { + if (is_retry) + ++m_stats.m_bb_retries; + else + ++m_stats.m_fallback_singleton_checks; + + unsigned old_max_conflicts = s->get_max_conflicts(); + s->set_max_conflicts(10); + + for (expr* lit : chunk_lits) { + if (is_retry && b.has_new_backbone_candidates(bb_candidate_epoch)) { + s->set_max_conflicts(old_max_conflicts); + return; + } + if (!m.inc() || canceled()) { + s->set_max_conflicts(old_max_conflicts); + return; + } + if (!bb_candidate_lits.contains(lit)) + continue; + + expr_ref bb_ref(lit, m); + if (m_positive_mode) + bb_ref = mk_not(m, bb_ref); + + if (!b.is_global_backbone_or_negation(m_l2g, bb_ref.get())) { + expr_ref backbone(m); + if (try_get_unit_backbone(bb_ref.get(), backbone)) { + ++m_stats.m_backbones_detected; + if (b.collect_global_backbone(m_l2g, backbone)) { + ++m_stats.m_internal_backbones_found; + if (is_retry) + ++m_stats.m_retry_backbones_found; + } + LOG_BB_WORKER(1, " fallback found unit backbone: " << mk_bounded_pp(backbone.get(), m, 3) << "\n"); + } + else { + expr* atom = bb_ref.get(); + m.is_not(bb_ref.get(), atom); + if (s->get_bool_var(atom) != UINT_MAX) { + lbool terminal_result = probe_literal(mk_not(m, bb_ref), is_retry); + LOG_BB_WORKER(1, " RESULT: " << terminal_result << " FOR CANDIDATE: " << mk_bounded_pp(bb_ref.get(), m, 3) << "\n"); + if (terminal_result != l_undef) { + s->set_max_conflicts(old_max_conflicts); + return; + } + } + } + } + bb_candidate_lits.erase(lit); + } + + s->set_max_conflicts(old_max_conflicts); + }; + + ++m_stats.m_batches_total; + m_stats.m_candidates_total += curr_batch.size(); + + expr_ref_vector bb_candidate_lits(m); + for (auto const& c : curr_batch) + bb_candidate_lits.push_back(c.lit); + + unsigned chunk_delta = 1; + + while (!bb_candidate_lits.empty() && !canceled() && m.inc()) { + { + unsigned j = 0; + for (expr* lit : bb_candidate_lits) { + if (!b.is_global_backbone_or_negation(m_l2g, lit)) + bb_candidate_lits[j++] = lit; + } + bb_candidate_lits.shrink(j); + } + + { + unsigned j = 0; + for (expr* lit : bb_candidate_lits) { + expr_ref backbone(m); + if (try_get_unit_backbone(lit, backbone)) { + if (b.collect_global_backbone(m_l2g, backbone)) + ++m_stats.m_internal_backbones_found; + ++m_stats.m_backbones_detected; + continue; + } + bb_candidate_lits[j++] = lit; + } + bb_candidate_lits.shrink(j); + } + + unsigned chunk_size = std::min(m_bb_chunk_size * chunk_delta, bb_candidate_lits.size()); + expr_ref_vector chunk_lits(m); + expr_ref_vector negated_chunk_lits(m); + expr_mark chunk_atoms; + + for (unsigned i = 0; i < bb_candidate_lits.size() && chunk_lits.size() < chunk_size; ++i) { + expr* lit = bb_candidate_lits.get(i); + expr* atom = lit; + m.is_not(lit, atom); + if (chunk_atoms.is_marked(atom)) + continue; + chunk_atoms.mark(atom); + chunk_lits.push_back(lit); + negated_chunk_lits.push_back(mk_not(m, lit)); + } + + expr_ref_vector bb_asms(m); + if (!m_positive_mode) + bb_asms.append(negated_chunk_lits); + else + bb_asms.append(chunk_lits); + + collect_shared_clauses(); + + while (true) { + if (!m.inc()) + return; + if (canceled()) + break; + + ++m_stats.m_core_refinement_rounds; + unsigned base_asms_sz = asms.size(); + for (expr* a : bb_asms) + asms.push_back(a); + + s->set_max_conflicts(m_bb_conflicts_per_chunk); + lbool r = l_undef; + try { + r = s->check_sat(asms); + } + catch (z3_error& err) { + if (!m.limit().is_canceled()) + b.set_exception(err.error_code()); + } + catch (z3_exception& ex) { + if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what())) + b.set_exception(ex.what()); + } + asms.shrink(base_asms_sz); + + if (!m.inc() || canceled()) + break; + + if (r == l_undef) { + LOG_BB_WORKER(1, " UNDEF at chunk_size=" << chunk_size << "\n"); + if (chunk_size < bb_candidate_lits.size()) { + ++chunk_delta; + ++m_stats.m_num_chunk_increases; + break; + } + + LOG_BB_WORKER(1, " UNDEF and max chunk -> fallback\n"); + fallback_failed_literal_probe(chunk_lits, bb_candidate_lits); + ++m_stats.m_fallback_reason_undef; + chunk_delta = 1; + break; + } + + if (r == l_true) { + LOG_BB_WORKER(1, " batch check returned SAT, thus entire formula is SAT\n"); + model_ref mdl; + s->get_model(mdl); + if (mdl) + b.set_sat(m_l2g, *mdl); + curr_batch.reset(); + return; + } + + expr_ref_vector bb_asms_in_core(m); + expr_ref_vector unsat_core(m); + s->get_unsat_core(unsat_core); + + for (expr* a : unsat_core) + if (bb_asms.contains(a)) + bb_asms_in_core.push_back(a); + + if (bb_asms_in_core.empty()) { + b.set_unsat(m_l2g, unsat_core); + return; + } + + if (bb_asms_in_core.size() == 1) { + expr* a = bb_asms_in_core.back(); + expr_ref backbone_lit(mk_not(m, a), m); + + ++m_stats.m_singleton_backbones; + ++m_stats.m_backbones_detected; + + if (b.collect_global_backbone(m_l2g, backbone_lit)) { + ++m_stats.m_internal_backbones_found; + s->assert_expr(backbone_lit.get()); + } + + expr* candidate_to_remove = + (!m_positive_mode) ? backbone_lit.get() : a; + bb_candidate_lits.erase(candidate_to_remove); + } + + unsigned sz_before = bb_asms.size(); + for (expr* a : bb_asms_in_core) + bb_asms.erase(a); + m_stats.m_lits_removed_by_core += sz_before - bb_asms.size(); + chunk_delta = 1; + + if (bb_asms.empty()) { + LOG_BB_WORKER(1, " no more negated chunk literals, fallback to individual checks\n"); + fallback_failed_literal_probe(chunk_lits, bb_candidate_lits); + ++m_stats.m_fallback_reason_chunk_exhausted; + break; + } + } + } + + while (!b.has_new_backbone_candidates(bb_candidate_epoch) && !canceled() && m.inc()) { + collect_shared_clauses(); + unsigned found_before = m_stats.m_internal_backbones_found; + + expr_ref_vector bb_snapshot = b.get_global_backbones_snapshot(m_g2l); + expr_mark bb_mark; + for (expr* e : bb_snapshot) { + bb_mark.mark(e); + bb_mark.mark(mk_not(m, e)); + } + bb_candidate_lits.reset(); + for (auto const& c : curr_batch) + if (!bb_mark.is_marked(c.lit.get())) + bb_candidate_lits.push_back(c.lit); + + if (bb_candidate_lits.empty()) + break; + + fallback_failed_literal_probe(bb_candidate_lits, bb_candidate_lits, true); + + if (m_stats.m_internal_backbones_found == found_before) + break; + } + + if (!canceled()) + b.cancel_current_backbone_batch(); + + curr_batch.reset(); + } + } + + public: + backbones_worker(unsigned id, parallel_solver& p, solver& src, params_ref const& params, + expr_ref_vector const& src_asms) + : id(id), b(p.m_batch_manager), + asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { + s = src.translate(m, params); + s->set_max_conflicts(m_bb_conflicts_per_chunk); + s->pop_to_base_level(); + for (expr* a : src_asms) + asms.push_back(m_g2l(a)); + m_positive_mode = id != 0; + m_shared_units_prefix = s->get_assigned_literals().size(); + m_num_initial_atoms = s->get_num_bool_vars(); + IF_VERBOSE(1, verbose_stream() << "Initialized backbones thread " << id << "\n"); + } + + void run() { run_batch_mode(); } + + void cancel() { + LOG_BB_WORKER(1, " BACKBONES WORKER cancelling\n"); + m.limit().cancel(); + } + + void collect_statistics(statistics& st) const { + st.update("bb-batches-total", m_stats.m_batches_total); + st.update("bb-candidates-total", m_stats.m_candidates_total); + st.update("bb-backbones-detected", m_stats.m_backbones_detected); + st.update("bb-internal-backbones-found", m_stats.m_internal_backbones_found); + st.update("bb-retry-backbones-found", m_stats.m_retry_backbones_found); + st.update("bb-retries", m_stats.m_bb_retries); + st.update("bb-core-refinement-rounds", m_stats.m_core_refinement_rounds); + st.update("bb-singleton-backbones", m_stats.m_singleton_backbones); + st.update("bb-fallback-singleton-checks", m_stats.m_fallback_singleton_checks); + st.update("bb-fallback-chunk-exhausted", m_stats.m_fallback_reason_chunk_exhausted); + st.update("bb-fallback-undef", m_stats.m_fallback_reason_undef); + st.update("bb-literals-removed-by-core", m_stats.m_lits_removed_by_core); + st.update("bb-num-chunk-increases", m_stats.m_num_chunk_increases); + + auto safe_ratio = [](double num, double den) -> double { + return den > 0 ? num / den : 0.0; + }; + + st.update("bb-backbone-yield-pct", + 100.0 * safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_candidates_total)); + st.update("bb-avg-backbones-per-batch", + safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_batches_total)); + st.update("bb-core-refinement-rounds-per-batch", + safe_ratio(m_stats.m_core_refinement_rounds, m_stats.m_batches_total)); + st.update("bb-core-effectiveness-lit-removed-per-round", + safe_ratio(m_stats.m_lits_removed_by_core, m_stats.m_core_refinement_rounds)); + } + + reslimit& limit() { return m.limit(); } + }; + + class core_minimizer_worker { + batch_manager& b; + ast_manager m; + ref s; + expr_ref_vector asms; + ast_translation m_g2l, m_l2g; + unsigned m_num_core_minimize_calls = 0; + unsigned m_num_core_minimize_undef = 0; + unsigned m_num_core_minimize_refined = 0; + unsigned m_num_core_minimize_lits_removed = 0; + unsigned m_num_core_minimize_found_sat = 0; + unsigned m_core_minimize_conflict_budget = 5000; + unsigned m_shared_clause_limit = 0; + + void collect_shared_clauses() { + expr_ref_vector nc = b.return_shared_clauses(m_g2l, m_shared_clause_limit, UINT_MAX); + for (expr* e : nc) { + s->assert_expr(e); + IF_VERBOSE(4, verbose_stream() << "Core minimizer asserting shared clause: " + << mk_bounded_pp(e, m, 3) << "\n";); + } + } + + void minimize_unsat_core(expr_ref_vector& core) { + expr_ref_vector unknown(core), mus(m), trial(m); + unsigned original_size = core.size(); + ++m_num_core_minimize_calls; + + while (!unknown.empty()) { + if (!m.inc()) { + core.reset(); + core.append(mus); + core.append(unknown); + return; + } + + expr* lit = unknown.back(); + unknown.pop_back(); + expr_ref not_lit(mk_not(m, lit), m); + + trial.reset(); + trial.append(mus); + trial.append(unknown); + trial.push_back(not_lit); + + lbool r = l_undef; + try { + s->set_max_conflicts(m_core_minimize_conflict_budget); + r = s->check_sat(trial); + } + catch (z3_error&) { + r = l_undef; + } + catch (z3_exception&) { + r = l_undef; + } + + switch (r) { + case l_undef: + ++m_num_core_minimize_undef; + mus.push_back(lit); + break; + case l_true: { + if (!asms.empty()) { + mus.push_back(lit); + break; + } + ++m_num_core_minimize_found_sat; + model_ref mdl; + s->get_model(mdl); + if (mdl) + b.set_sat(m_l2g, *mdl); + return; + } + case l_false: { + expr_ref_vector unsat_core(m); + s->get_unsat_core(unsat_core); + if (!unsat_core.contains(not_lit)) { + ++m_num_core_minimize_refined; + unknown.reset(); + expr_ref_vector new_mus(m); + for (expr* c : unsat_core) { + if (mus.contains(c)) + new_mus.push_back(c); + else + unknown.push_back(c); + } + mus.reset(); + mus.append(new_mus); + } + break; + } + default: + UNREACHABLE(); + } + } + + core.reset(); + core.append(mus); + core.append(unknown); + if (core.size() < original_size) + m_num_core_minimize_lits_removed += original_size - core.size(); + } + + public: + core_minimizer_worker(parallel_solver& p, solver& src, params_ref const& params, + expr_ref_vector const& src_asms) + : b(p.m_batch_manager), + asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { + s = src.translate(m, params); + s->pop_to_base_level(); + // avoid preprocessing lemmas that are exchanged + s->set_preprocess(false); + for (expr* a : src_asms) + asms.push_back(m_g2l(a)); + IF_VERBOSE(1, verbose_stream() << "Initialized core minimizer thread\n"); + } + + void run() { + while (m.inc()) { + search_tree::node* source = nullptr; + expr_ref_vector core(m); + if (!b.wait_for_core_min_job(m_g2l, source, core, m.limit())) + return; + + unsigned original_size = core.size(); + if (original_size <= 1) + continue; + + collect_shared_clauses(); + + expr_ref_vector minimized(m); + minimized.append(core); + + if (minimized.size() <= 1) + continue; + + minimize_unsat_core(minimized); + + if (minimized.size() < original_size) + b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); + } + } + + void cancel() { + IF_VERBOSE(1, verbose_stream() << "Core minimizer cancelling\n"); + m.limit().cancel(); + } + + void collect_statistics(statistics& st) const { + st.update("parallel-core-minimize-calls", m_num_core_minimize_calls); + st.update("parallel-core-minimize-undef", m_num_core_minimize_undef); + st.update("parallel-core-minimize-refined", m_num_core_minimize_refined); + st.update("parallel-core-minimize-lits-removed", m_num_core_minimize_lits_removed); + st.update("parallel-core-minimize-found-sat", m_num_core_minimize_found_sat); + } + + reslimit& limit() { return m.limit(); } + }; /* ---- members ---- */ ref m_solver; ast_manager& m_manager; params_ref m_params; scoped_ptr_vector m_workers; + scoped_ptr m_core_minimizer_worker; + scoped_ptr_vector m_global_backbones_workers; batch_manager m_batch_manager; statistics m_stats; - public: parallel_solver(solver* s, params_ref const& p) @@ -718,6 +1810,16 @@ public: m_params(p), m_batch_manager(s->get_manager(), *this) {} + params_ref mk_worker_params(unsigned seed_offset) const { + params_ref p(m_params); + // Match smt_parallel's per-worker m_smt_params.m_random_seed += id. + // Generic solver workers receive the seed through translate params. + unsigned base_seed = m_params.get_uint("random_seed", 0); + p.set_uint("random_seed", base_seed + seed_offset); + p.set_uint("threads", 1); + return p; + } + /* Run the portfolio. Returns sat/unsat/undef. * * On sat: *mdl is populated (translated into m_manager). @@ -731,10 +1833,13 @@ public: unsigned num_threads = std::min( static_cast(std::thread::hardware_concurrency()), pp.threads_max()); - if (num_threads < 2) num_threads = 2; + bool core_minimize = pp.core_minimize(); + unsigned num_bb_threads = pp.num_bb_threads(); + if (num_bb_threads > 2) + throw default_exception("parallel.num_bb_threads must be 0, 1, or 2"); + unsigned total_threads = num_threads + (core_minimize ? 1 : 0) + num_bb_threads; - IF_VERBOSE(1, verbose_stream() << "par2: launching " << num_threads - << " threads\n"); + IF_VERBOSE(1, verbose_stream() << "Parallel tactical2 with " << total_threads << " threads\n";); if (m_manager.has_trace_stream()) throw default_exception( @@ -743,29 +1848,73 @@ public: /* Build workers – each gets a translated solver copy. */ m_workers.reset(); scoped_limits sl(m_manager.limit()); - params_ref worker_params(m_params); - worker_params.set_bool("override_incremental", true); + + // Set up the source before translating workers. SMT context copies + // then run initial internalization/preprocessing before workers disable + // preprocessing for exchanged lemmas. + m_solver->setup_for_parallel(); for (unsigned i = 0; i < num_threads; ++i) { + params_ref worker_params = mk_worker_params(i); auto* w = alloc(worker, i, *this, *m_solver, worker_params, asms); m_workers.push_back(w); sl.push_child(&(w->limit())); } - m_batch_manager.initialize(num_threads); + m_core_minimizer_worker = nullptr; + if (core_minimize) { + params_ref core_min_params = mk_worker_params(num_threads); + m_core_minimizer_worker = alloc(core_minimizer_worker, *this, *m_solver, core_min_params, asms); + sl.push_child(&(m_core_minimizer_worker->limit())); + } + m_global_backbones_workers.reset(); + for (unsigned i = 0; i < num_bb_threads; ++i) { + params_ref bb_params = mk_worker_params(num_threads + (core_minimize ? 1 : 0) + i); + auto* w = alloc(backbones_worker, i, *this, *m_solver, bb_params, asms); + m_global_backbones_workers.push_back(w); + sl.push_child(&(w->limit())); + } + IF_VERBOSE(1, verbose_stream() << "Launched " << m_workers.size() << " CDCL threads, " + << 0 << " SLS threads, " + << (m_core_minimizer_worker ? 1 : 0) << " core minimizer threads, " + << m_global_backbones_workers.size() << " global backbone threads.\n";); + + m_batch_manager.initialize(num_bb_threads); /* Launch threads. */ vector threads; for (auto* w : m_workers) threads.push_back(std::thread([w]() { w->run(); })); + if (m_core_minimizer_worker) + threads.push_back(std::thread([this]() { m_core_minimizer_worker->run(); })); + for (auto* w : m_global_backbones_workers) + threads.push_back(std::thread([w]() { w->run(); })); for (auto& t : threads) t.join(); - /* Collect per-worker statistics. */ - for (auto* w : m_workers) - w->collect_statistics(m_stats); - m_batch_manager.collect_statistics(m_stats); + m_solver->reset_parallel_statistics(); + statistics aux; + for (auto* w : m_workers) { + aux.reset(); + w->collect_statistics(aux); + m_solver->add_parallel_statistics(aux); + } + aux.reset(); + m_batch_manager.collect_statistics(aux); + m_solver->add_parallel_statistics(aux); + if (m_core_minimizer_worker) { + aux.reset(); + m_core_minimizer_worker->collect_statistics(aux); + m_solver->add_parallel_statistics(aux); + } + for (auto* w : m_global_backbones_workers) { + aux.reset(); + w->collect_statistics(aux); + m_solver->add_parallel_statistics(aux); + } + m_stats.reset(); + m_solver->collect_parallel_statistics(m_stats); m_manager.limit().reset_cancel(); @@ -779,7 +1928,10 @@ public: core.push_back(c); } + sl.reset(); m_workers.reset(); + m_core_minimizer_worker = nullptr; + m_global_backbones_workers.reset(); return result; } @@ -790,7 +1942,7 @@ public: void reset_statistics() { m_stats.reset(); } -}; // class parallel_solver +}; /* ------------------------------------------------------------------ */ /* parallel_tactic2 – wraps parallel_solver as a tactic */ @@ -824,8 +1976,7 @@ public: ptr_vector assumptions_raw; obj_map bool2dep; ref fmc; - extract_clauses_and_dependencies(g, clauses, assumptions_raw, - bool2dep, fmc); + extract_clauses_and_dependencies(g, clauses, assumptions_raw, bool2dep, fmc); for (expr* cl : clauses) s->assert_expr(cl); @@ -841,15 +1992,16 @@ public: ps.collect_statistics(m_stats); switch (is_sat) { - case l_true: - g->reset(); + case l_true: { if (g->models_enabled() && mdl) { - if (fmc) - g->add(concat(fmc.get(), model2model_converter(mdl.get()))); - else - g->add(model2model_converter(mdl.get())); + model_converter_ref mc = model2model_converter(mdl.get()); + mc = concat(fmc.get(), mc.get()); + mc = concat(s->mc0(), mc.get()); + g->add(mc.get()); } + g->reset(); break; + } case l_false: { SASSERT(!g->proofs_enabled()); @@ -875,9 +2027,7 @@ public: result.push_back(g.get()); } - void cleanup() override { - m_stats.reset(); - } + void cleanup() override {} tactic* translate(ast_manager& m) override { solver* s = m_solver->translate(m, m_params); @@ -895,10 +2045,10 @@ public: void reset_statistics() override { m_stats.reset(); } -}; // class parallel_tactic2 +}; tactic* mk_parallel_tactic2(solver* s, params_ref const& p) { return alloc(parallel_tactic2, s, p); } -#endif /* !SINGLE_THREAD */ +#endif diff --git a/src/solver/solver.h b/src/solver/solver.h index b45f4f347..d4118c4c2 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -57,7 +57,15 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p, symbol const& logic class solver : public check_sat_result, public user_propagator::core { params_ref m_params; symbol m_cancel_backup_file; + statistics m_parallel_stats; public: + struct scored_literal { + expr_ref lit; + double score = 0.0; + scored_literal(ast_manager& m, expr* e, double s): lit(e, m), score(s) {} + scored_literal(expr_ref const& e, double s): lit(e), score(s) {} + }; + solver(ast_manager& m): check_sat_result(m) {} /** @@ -298,9 +306,47 @@ public: expr_ref_vector get_non_units(); virtual expr_ref_vector get_trail(unsigned max_level) = 0; // { return expr_ref_vector(get_manager()); } + virtual expr_ref_vector get_assigned_literals() { return get_trail(UINT_MAX); } + virtual unsigned get_assign_level(expr* e) const { return UINT_MAX; } + virtual bool is_relevant(expr* e) const { return true; } + virtual unsigned get_num_bool_vars() const { return UINT_MAX; } + virtual unsigned get_bool_var(expr* e) const { return UINT_MAX; } + virtual expr* bool_var2expr(unsigned) const { return nullptr; } + virtual lbool get_assignment(unsigned) const { return l_undef; } + virtual double get_activity(unsigned) const { return 0.0; } + virtual bool was_eliminated(unsigned) const { return false; } + + virtual void pop_to_base_level() {} + + virtual void setup_for_parallel() {} + + virtual void set_preprocess(bool) {} + + virtual void set_max_conflicts(unsigned max_conflicts) { + params_ref p; + p.set_uint("max_conflicts", max_conflicts); + updt_params(p); + } + + virtual unsigned get_max_conflicts() const { return UINT_MAX; } + + virtual void reset_parallel_statistics() { + m_parallel_stats.reset(); + } + + virtual void add_parallel_statistics(statistics const& st) { + m_parallel_stats.copy(st); + } + + virtual void collect_parallel_statistics(statistics& st) const { + st.copy(m_parallel_stats); + collect_statistics(st); + } virtual void get_levels(ptr_vector const& vars, unsigned_vector& depth) = 0; + virtual void get_backbone_candidates(vector&, unsigned) {} + class scoped_push { solver& s; bool m_nopop; diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 3cf97ce3b..1463eecf8 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -127,6 +127,10 @@ public: m_base->get_levels(vars, depth); } + void get_backbone_candidates(vector& candidates, unsigned max_num) override { + m_base->get_backbone_candidates(candidates, max_num); + } + expr_ref_vector get_trail(unsigned max_level) override { return m_base->get_trail(max_level); } diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 85294d550..701c2fe8d 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -68,9 +68,17 @@ namespace search_tree { literal const &get_literal() const { return m_literal; } + bool path_contains_atom(literal const& l) const { + for (node const* n = this; n; n = n->parent()) + if (!Config::literal_is_null(n->get_literal()) && Config::same_atom(n->get_literal(), l)) + return true; + return false; + } void split(literal const &a, literal const &b) { SASSERT(!Config::literal_is_null(a)); SASSERT(!Config::literal_is_null(b)); + VERIFY(!path_contains_atom(a)); + VERIFY(!path_contains_atom(b)); if (m_status != status::active) return; SASSERT(!m_left); From e06ca1489e010b40547092a94ab78bda94a54c10 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 14:51:28 -0700 Subject: [PATCH 02/34] remove parallal_stats --- src/smt/smt_solver.cpp | 12 ------------ src/solver/parallel_tactical2.cpp | 12 ++++++------ src/solver/solver.h | 13 ------------- 3 files changed, 6 insertions(+), 31 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 81391cb34..6d075ebcd 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -279,18 +279,6 @@ namespace { return const_cast(m_context).get_context().get_fparams().m_max_conflicts; } - void reset_parallel_statistics() override { - m_context.reset_aux_statistics(); - } - - void add_parallel_statistics(statistics const& st) override { - m_context.add_aux_statistics(st); - } - - void collect_parallel_statistics(statistics& st) const override { - m_context.collect_statistics(st); - } - void get_backbone_candidates(vector& candidates, unsigned max_num) override { ast_manager& m = get_manager(); auto& ctx = m_context.get_context(); diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ae5b739f4..dcd844b09 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1893,28 +1893,28 @@ public: for (auto& t : threads) t.join(); - m_solver->reset_parallel_statistics(); + m_solver->reset_statistics(); statistics aux; for (auto* w : m_workers) { aux.reset(); w->collect_statistics(aux); - m_solver->add_parallel_statistics(aux); + m_solver->add_statistics(aux); } aux.reset(); m_batch_manager.collect_statistics(aux); - m_solver->add_parallel_statistics(aux); + m_solver->add_statistics(aux); if (m_core_minimizer_worker) { aux.reset(); m_core_minimizer_worker->collect_statistics(aux); - m_solver->add_parallel_statistics(aux); + m_solver->add_statistics(aux); } for (auto* w : m_global_backbones_workers) { aux.reset(); w->collect_statistics(aux); - m_solver->add_parallel_statistics(aux); + m_solver->add_statistics(aux); } m_stats.reset(); - m_solver->collect_parallel_statistics(m_stats); + m_solver->collect_statistics(m_stats); m_manager.limit().reset_cancel(); diff --git a/src/solver/solver.h b/src/solver/solver.h index d4118c4c2..f1de41880 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -57,7 +57,6 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p, symbol const& logic class solver : public check_sat_result, public user_propagator::core { params_ref m_params; symbol m_cancel_backup_file; - statistics m_parallel_stats; public: struct scored_literal { expr_ref lit; @@ -330,18 +329,6 @@ public: virtual unsigned get_max_conflicts() const { return UINT_MAX; } - virtual void reset_parallel_statistics() { - m_parallel_stats.reset(); - } - - virtual void add_parallel_statistics(statistics const& st) { - m_parallel_stats.copy(st); - } - - virtual void collect_parallel_statistics(statistics& st) const { - st.copy(m_parallel_stats); - collect_statistics(st); - } virtual void get_levels(ptr_vector const& vars, unsigned_vector& depth) = 0; From 5aa06b6333f9da2fdb82118dec55510f3bb72649 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 15:28:48 -0700 Subject: [PATCH 03/34] refactor phase update --- src/sat/sat_solver.cpp | 72 +++++++++++++++--------------------------- src/sat/sat_solver.h | 1 + 2 files changed, 26 insertions(+), 47 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index cd4793416..a90840d3b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -657,11 +657,16 @@ namespace sat { if (l.var() >= num_vars()) return; bool value = !l.sign(); - if (m_phase[l.var()] != value) - m_phase_birthdate[l.var()] = m_stats.m_conflicts; + set_phase(l.var(), value); if (m_best_phase[l.var()] != value) m_best_phase_birthdate[l.var()] = m_stats.m_conflicts; - m_best_phase[l.var()] = m_phase[l.var()] = value; + m_best_phase[l.var()] = value; + } + + void solver::set_phase(bool_var v, bool value) { + if (m_phase[v] != value) + m_phase_birthdate[v] = m_stats.m_conflicts; + m_phase[v] = value; } struct solver::cmp_activity { @@ -915,9 +920,7 @@ namespace sat { m_assignment[(~l).index()] = l_false; bool_var v = l.var(); m_justification[v] = j; - if (m_phase[v] != !l.sign()) - m_phase_birthdate[v] = m_stats.m_conflicts; - m_phase[v] = !l.sign(); + set_phase(v, !l.sign()); m_assigned_since_gc[v] = true; m_trail.push_back(l); @@ -2197,11 +2200,9 @@ namespace sat { if (!was_eliminated(v)) { m_model[v] = value(v); bool is_true = value(v) == l_true; - if (m_phase[v] != is_true) - m_phase_birthdate[v] = m_stats.m_conflicts; + set_phase(v, is_true); if (m_best_phase[v] != is_true) m_best_phase_birthdate[v] = m_stats.m_conflicts; - m_phase[v] = is_true; m_best_phase[v] = is_true; } } @@ -2972,9 +2973,7 @@ namespace sat { bool_var v = m_trail[i].var(); TRACE(forget_phase, tout << "forgetting phase of v" << v << "\n";); bool value = m_rand() % 2 == 0; - if (m_phase[v] != value) - m_phase_birthdate[v] = m_stats.m_conflicts; - m_phase[v] = value; + set_phase(v, value); } if (is_sat_phase() && head >= m_best_phase_size) { m_best_phase_size = head; @@ -3032,18 +3031,12 @@ namespace sat { void solver::do_rephase() { switch (m_config.m_phase) { case PS_ALWAYS_TRUE: - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (!m_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = true; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, true); break; case PS_ALWAYS_FALSE: - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (m_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = false; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, false); break; case PS_FROZEN: break; @@ -3052,23 +3045,16 @@ namespace sat { case 0: for (unsigned i = 0; i < m_phase.size(); ++i) { bool value = (m_rand() % 2) == 0; - if (m_phase[i] != value) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = value; + set_phase(i, value); } break; case 1: - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (m_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = false; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, false); break; case 2: - for (unsigned i = 0; i < m_phase.size(); ++i) { - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = !m_phase[i]; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, !m_phase[i]); break; default: break; @@ -3076,29 +3062,21 @@ namespace sat { break; case PS_SAT_CACHING: if (m_search_state == s_sat) - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (m_phase[i] != m_best_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = m_best_phase[i]; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, m_best_phase[i]); break; case PS_RANDOM: for (unsigned i = 0; i < m_phase.size(); ++i) { bool value = (m_rand() % 2) == 0; - if (m_phase[i] != value) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = value; + set_phase(i, value); } break; case PS_LOCAL_SEARCH: if (m_search_state == s_sat) { if (m_rand() % 2 == 0) bounded_local_search(); - for (unsigned i = 0; i < m_phase.size(); ++i) { - if (m_phase[i] != m_best_phase[i]) - m_phase_birthdate[i] = m_stats.m_conflicts; - m_phase[i] = m_best_phase[i]; - } + for (unsigned i = 0; i < m_phase.size(); ++i) + set_phase(i, m_best_phase[i]); } break; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index d50ee9461..5581668ef 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -376,6 +376,7 @@ namespace sat { void set_eliminated(bool_var v, bool f) override; bool was_eliminated(literal l) const { return was_eliminated(l.var()); } void set_phase(literal l) override; + void set_phase(bool_var v, bool value); bool get_phase(bool_var b) { return m_phase.get(b, false); } bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); } uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); } From de028f33a226153cc10367adc94c3d09418dfebc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 15:40:11 -0700 Subject: [PATCH 04/34] Update inc_sat_solver.cpp --- src/sat/sat_solver/inc_sat_solver.cpp | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e8cd6d3fd..f5a5eed75 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -406,16 +406,14 @@ public: } unsigned get_assign_level(expr* e) const override { - expr* atom = e; - m.is_not(e, atom); - sat::bool_var bv = m_map.to_bool_var(atom); + m.is_not(e, e); + sat::bool_var bv = m_map.to_bool_var(e); return bv == sat::null_bool_var ? UINT_MAX : m_solver.lvl(bv); } bool is_relevant(expr* e) const override { - expr* atom = e; - m.is_not(e, atom); - sat::bool_var bv = m_map.to_bool_var(atom); + m.is_not(e, e); + sat::bool_var bv = m_map.to_bool_var(e); if (bv == sat::null_bool_var) return true; auto* ext = dynamic_cast(m_solver.get_extension()); @@ -427,9 +425,8 @@ public: } unsigned get_bool_var(expr* e) const override { - expr* atom = e; - m.is_not(e, atom); - sat::bool_var bv = m_map.to_bool_var(atom); + m.is_not(e, e); + auto bv = m_map.to_bool_var(atom); return bv == sat::null_bool_var ? UINT_MAX : bv; } From 49d725f477cf1956259b93404f50e19c06bb2d40 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 15:40:38 -0700 Subject: [PATCH 05/34] refactor --- src/sat/sat_solver.cpp | 22 ++++++++++------------ src/sat/sat_solver.h | 1 + src/smt/smt_kernel.cpp | 8 -------- src/smt/smt_kernel.h | 4 ---- 4 files changed, 11 insertions(+), 24 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index a90840d3b..9cda41b50 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -658,9 +658,7 @@ namespace sat { return; bool value = !l.sign(); set_phase(l.var(), value); - if (m_best_phase[l.var()] != value) - m_best_phase_birthdate[l.var()] = m_stats.m_conflicts; - m_best_phase[l.var()] = value; + set_best_phase(l.var(), value); } void solver::set_phase(bool_var v, bool value) { @@ -669,6 +667,12 @@ namespace sat { m_phase[v] = value; } + void solver::set_best_phase(bool_var v, bool value) { + if (m_best_phase[v] != value) + m_best_phase_birthdate[v] = m_stats.m_conflicts; + m_best_phase[v] = value; + } + struct solver::cmp_activity { solver& s; cmp_activity(solver& s):s(s) {} @@ -1404,9 +1408,7 @@ namespace sat { if (mdl.size() == m_best_phase.size()) { for (unsigned i = 0; i < m_best_phase.size(); ++i) { bool is_true = l_true == mdl[i]; - if (m_best_phase[i] != is_true) - m_best_phase_birthdate[i] = m_stats.m_conflicts; - m_best_phase[i] = is_true; + set_best_phase(i, is_true); } if (r == l_true) { @@ -2201,9 +2203,7 @@ namespace sat { m_model[v] = value(v); bool is_true = value(v) == l_true; set_phase(v, is_true); - if (m_best_phase[v] != is_true) - m_best_phase_birthdate[v] = m_stats.m_conflicts; - m_best_phase[v] = is_true; + set_best_phase(v, is_true); } } TRACE(sat_mc_bug, m_mc.display(tout);); @@ -2980,9 +2980,7 @@ namespace sat { IF_VERBOSE(12, verbose_stream() << "sticky trail: " << head << "\n"); for (unsigned i = 0; i < head; ++i) { bool_var v = m_trail[i].var(); - if (m_best_phase[v] != m_phase[v]) - m_best_phase_birthdate[v] = m_stats.m_conflicts; - m_best_phase[v] = m_phase[v]; + set_best_phase(v, m_phase[v]); } set_has_new_best_phase(true); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 5581668ef..622e551bb 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -377,6 +377,7 @@ namespace sat { bool was_eliminated(literal l) const { return was_eliminated(l.var()); } void set_phase(literal l) override; void set_phase(bool_var v, bool value); + void set_best_phase(bool_var v, bool value); bool get_phase(bool_var b) { return m_phase.get(b, false); } bool get_best_phase(bool_var b) { return m_best_phase.get(b, false); } uint64_t get_phase_birthdate(bool_var b) const { return m_phase_birthdate.get(b, 0); } diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index fc2c87f5a..034c34d79 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -288,14 +288,6 @@ namespace smt { m_imp->m_kernel.get_fparams().m_preprocess = f; } - void kernel::reset_aux_statistics() { - m_imp->m_kernel.m_aux_stats.reset(); - } - - void kernel::add_aux_statistics(::statistics const& st) { - m_imp->m_kernel.m_aux_stats.copy(st); - } - context & kernel::get_context() { return m_imp->m_kernel; } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index a1b2bfc18..9c4395cf8 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -304,10 +304,6 @@ namespace smt { void set_preprocess(bool f); - void reset_aux_statistics(); - - void add_aux_statistics(::statistics const& st); - void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause); /** From deb9fe42408cdcd944df350fdbb26019a21940a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 15:53:44 -0700 Subject: [PATCH 06/34] use bool_var instead of unsigned --- src/smt/smt_solver.cpp | 10 +++++----- src/solver/solver.h | 11 ++++++----- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 6d075ebcd..7409b5851 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -251,11 +251,11 @@ namespace { return const_cast(m_context).get_context().get_num_bool_vars(); } - unsigned get_bool_var(expr* e) const override { + sat::bool_var get_bool_var(expr* e) const override { auto& ctx = const_cast(m_context).get_context(); expr* atom = e; get_manager().is_not(e, atom); - return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : UINT_MAX; + return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : sat::null_bool_var; } void pop_to_base_level() override { @@ -450,9 +450,9 @@ namespace { ast_manager& m = get_manager(); if (!get_params().get_bool("cube.lookahead", false)) { auto& ctx = m_context.get_context(); - obj_hashtable selected_vars; + expr_mark selected_vars; for (expr* v : vars) - selected_vars.insert(v); + selected_vars.mark(v); expr_ref_vector candidates(m); expr_ref result(m); double score = 0.0; @@ -465,7 +465,7 @@ namespace { expr* e = ctx.bool_var2expr(v); if (!e) continue; - if (!selected_vars.empty() && !selected_vars.contains(e)) + if (!vars.empty() && !selected_vars.is_marked(e)) continue; candidates.push_back(e); double new_score = ctx.get_activity(v); diff --git a/src/solver/solver.h b/src/solver/solver.h index f1de41880..73a83a6dd 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -22,6 +22,7 @@ Notes: #include "solver/check_sat_result.h" #include "solver/progress_callback.h" #include "util/params.h" +#include "util/sat_literal.h" class solver; class model_converter; @@ -309,11 +310,11 @@ public: virtual unsigned get_assign_level(expr* e) const { return UINT_MAX; } virtual bool is_relevant(expr* e) const { return true; } virtual unsigned get_num_bool_vars() const { return UINT_MAX; } - virtual unsigned get_bool_var(expr* e) const { return UINT_MAX; } - virtual expr* bool_var2expr(unsigned) const { return nullptr; } - virtual lbool get_assignment(unsigned) const { return l_undef; } - virtual double get_activity(unsigned) const { return 0.0; } - virtual bool was_eliminated(unsigned) const { return false; } + virtual sat::bool_var get_bool_var(expr* e) const { return sat::null_bool_var; } + virtual expr* bool_var2expr(sat::bool_var) const { return nullptr; } + virtual lbool get_assignment(sat::bool_var) const { return l_undef; } + virtual double get_activity(sat::bool_var) const { return 0.0; } + virtual bool was_eliminated(sat::bool_var) const { return false; } virtual void pop_to_base_level() {} From 9485e964167447b336ef49e450e1716e0cf0a898 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 15:59:08 -0700 Subject: [PATCH 07/34] signatrue update --- src/sat/sat_solver/inc_sat_solver.cpp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index f5a5eed75..229462a0e 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -424,25 +424,24 @@ public: return m_solver.num_vars(); } - unsigned get_bool_var(expr* e) const override { + sat::bool_var get_bool_var(expr* e) const override { m.is_not(e, e); - auto bv = m_map.to_bool_var(atom); - return bv == sat::null_bool_var ? UINT_MAX : bv; + return m_map.to_bool_var(e); } - expr* bool_var2expr(unsigned v) const override { + expr* bool_var2expr(sat::bool_var v) const override { return v < m_solver.num_vars() ? m_map.bool_var2expr(v) : nullptr; } - lbool get_assignment(unsigned v) const override { + lbool get_assignment(sat::bool_var v) const override { return v < m_solver.num_vars() ? m_solver.value(v) : l_undef; } - double get_activity(unsigned v) const override { + double get_activity(sat::bool_var v) const override { return v < m_solver.num_vars() ? static_cast(m_solver.get_activity(v)) : 0.0; } - bool was_eliminated(unsigned v) const override { + bool was_eliminated(sat::bool_var v) const override { return v < m_solver.num_vars() && m_solver.was_eliminated(v); } From 96ac8bfd774c4831f85370611d4b4680aaeb823b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 16:49:36 -0700 Subject: [PATCH 08/34] redo priority selection --- src/sat/sat_solver/inc_sat_solver.cpp | 45 ++++++++++++++++----------- src/solver/solver_pool.cpp | 4 --- 2 files changed, 27 insertions(+), 22 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 229462a0e..e03ae8c07 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -493,29 +493,38 @@ public: sat::literal_vector lits; expr_ref_vector fmls(m); if (!m_params.get_bool("cube.lookahead", false)) { - sat::bool_var best = sat::null_bool_var; - double best_activity = 0.0; - unsigned n = 0; + sat::bool_var_vector candidates; + unsigned search_lvl = m_solver.search_lvl(); for (sat::bool_var v : vars) { - if (get_assignment(v) != l_undef || was_eliminated(v)) + if (was_eliminated(v)) continue; - double activity = get_activity(v); - if (best == sat::null_bool_var || activity > best_activity || (activity == best_activity && m_solver.rand()(++n) == 0)) { - best = v; - best_activity = activity; - } + if (get_assignment(v) != l_undef && m_solver.lvl(v) <= search_lvl) + continue; + candidates.push_back(v); } - if (best == sat::null_bool_var) + std::sort(candidates.begin(), candidates.end(), [&](sat::bool_var a, sat::bool_var b) { + return get_activity(a) > get_activity(b); + }); + // shuffle sub-sequences with equal activity + unsigned i = 0; + while (i < candidates.size()) { + unsigned j = i + 1; + double act = get_activity(candidates[i]); + while (j < candidates.size() && get_activity(candidates[j]) == act) + ++j; + if (j - i > 1) + shuffle(j - i, candidates.data() + i, m_solver.rand()); + i = j; + } + if (candidates.empty()) return expr_ref_vector(m); - expr* e = bool_var2expr(best); - SASSERT(e); - if (e) - fmls.push_back(e); vs.reset(); - for (sat::bool_var v : vars) { - expr* x = bool_var2expr(v); - if (x) - vs.push_back(x); + for (sat::bool_var v : candidates) { + expr* e = bool_var2expr(v); + if (e) { + fmls.push_back(e); + vs.push_back(e); + } } return fmls; } diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp index 1463eecf8..3cf97ce3b 100644 --- a/src/solver/solver_pool.cpp +++ b/src/solver/solver_pool.cpp @@ -127,10 +127,6 @@ public: m_base->get_levels(vars, depth); } - void get_backbone_candidates(vector& candidates, unsigned max_num) override { - m_base->get_backbone_candidates(candidates, max_num); - } - expr_ref_vector get_trail(unsigned max_level) override { return m_base->get_trail(max_level); } From a3f07ba9ab8f74969e3ce5ae51be47cdbc2841c2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2026 22:47:32 -0700 Subject: [PATCH 09/34] Update atom2bool_var.cpp --- src/sat/smt/atom2bool_var.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/atom2bool_var.cpp b/src/sat/smt/atom2bool_var.cpp index b6760c943..4d074f772 100644 --- a/src/sat/smt/atom2bool_var.cpp +++ b/src/sat/smt/atom2bool_var.cpp @@ -1,4 +1,4 @@ -/*++ +add a smart constructor to seq_util to create the simplified range given two characters. It would create either the empty regex, the singleton string or a range expression./*++ Copyright (c) 2011 Microsoft Corporation Module Name: @@ -50,9 +50,9 @@ sat::bool_var atom2bool_var::to_bool_var(expr * n) const { } expr* atom2bool_var::bool_var2expr(sat::bool_var v) const { - for (auto const& kv : m_mapping) - if (kv.m_value == v) - return kv.m_key; + for (auto const& [key, val] : m_mapping) + if (val == v) + return key; return nullptr; } From 4b7e4cf08a5c7ce80b3c2bd97ce7a9b0b2cc0e19 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 12 Jun 2026 06:15:29 +0000 Subject: [PATCH 10/34] Remove const_cast from smt_solver context access --- src/smt/smt_context.h | 5 ++++- src/smt/smt_kernel.cpp | 4 ++++ src/smt/smt_kernel.h | 2 +- src/smt/smt_solver.cpp | 17 ++++++++--------- 4 files changed, 17 insertions(+), 11 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 193ef7705..1aaecf736 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -294,6 +294,10 @@ namespace smt { return m_fparams; } + smt_params const& get_fparams() const { + return m_fparams; + } + params_ref const & get_params() { return m_params; } @@ -1921,4 +1925,3 @@ namespace smt { std::ostream& operator<<(std::ostream& out, enode_pp const& p); }; - diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 034c34d79..1e49a8d3c 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -292,6 +292,10 @@ namespace smt { return m_imp->m_kernel; } + context const& kernel::get_context() const { + return m_imp->m_kernel; + } + void kernel::get_levels(ptr_vector const& vars, unsigned_vector& depth) { m_imp->m_kernel.get_levels(vars, depth); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 9c4395cf8..0a6faaa09 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -344,6 +344,6 @@ namespace smt { \warning This method should not be used in new code. */ context & get_context(); + context const& get_context() const; }; }; - diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 7409b5851..e3e15ea9a 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -221,7 +221,7 @@ namespace { expr_ref_vector get_assigned_literals() override { expr_ref_vector result(m); - auto& ctx = const_cast(m_context).get_context(); + auto const& ctx = m_context.get_context(); for (auto lit : ctx.assigned_literals()) { expr* atom = ctx.bool_var2expr(lit.var()); if (!atom) @@ -232,7 +232,7 @@ namespace { } unsigned get_assign_level(expr* e) const override { - auto& ctx = const_cast(m_context).get_context(); + auto const& ctx = m_context.get_context(); expr* atom = e; get_manager().is_not(e, atom); if (!ctx.b_internalized(atom)) @@ -241,18 +241,18 @@ namespace { } bool is_relevant(expr* e) const override { - auto& ctx = const_cast(m_context).get_context(); + auto const& ctx = m_context.get_context(); expr* atom = e; get_manager().is_not(e, atom); return ctx.b_internalized(atom) && ctx.is_relevant(atom); } unsigned get_num_bool_vars() const override { - return const_cast(m_context).get_context().get_num_bool_vars(); + return m_context.get_context().get_num_bool_vars(); } sat::bool_var get_bool_var(expr* e) const override { - auto& ctx = const_cast(m_context).get_context(); + auto const& ctx = m_context.get_context(); expr* atom = e; get_manager().is_not(e, atom); return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : sat::null_bool_var; @@ -263,7 +263,7 @@ namespace { } void setup_for_parallel() override { - const_cast(m_context).get_context().setup_for_parallel(); + m_context.get_context().setup_for_parallel(); } void set_preprocess(bool f) override { @@ -271,12 +271,12 @@ namespace { } void set_max_conflicts(unsigned max_conflicts) override { - auto& ctx = const_cast(m_context).get_context(); + auto& ctx = m_context.get_context(); ctx.get_fparams().m_max_conflicts = max_conflicts; } unsigned get_max_conflicts() const override { - return const_cast(m_context).get_context().get_fparams().m_max_conflicts; + return m_context.get_context().get_fparams().m_max_conflicts; } void get_backbone_candidates(vector& candidates, unsigned max_num) override { @@ -676,4 +676,3 @@ public: solver_factory * mk_smt_solver_factory() { return alloc(smt_solver_factory); } - From af5bbb45661d03c8b0055925d6a9b547ff8e5e6f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 12 Jun 2026 06:37:48 +0000 Subject: [PATCH 11/34] Restore atom2bool_var.cpp to fix CI build break --- src/sat/smt/atom2bool_var.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/atom2bool_var.cpp b/src/sat/smt/atom2bool_var.cpp index 4d074f772..b6760c943 100644 --- a/src/sat/smt/atom2bool_var.cpp +++ b/src/sat/smt/atom2bool_var.cpp @@ -1,4 +1,4 @@ -add a smart constructor to seq_util to create the simplified range given two characters. It would create either the empty regex, the singleton string or a range expression./*++ +/*++ Copyright (c) 2011 Microsoft Corporation Module Name: @@ -50,9 +50,9 @@ sat::bool_var atom2bool_var::to_bool_var(expr * n) const { } expr* atom2bool_var::bool_var2expr(sat::bool_var v) const { - for (auto const& [key, val] : m_mapping) - if (val == v) - return key; + for (auto const& kv : m_mapping) + if (kv.m_value == v) + return kv.m_key; return nullptr; } From 502309f246c5cd28fc5b8739fa8e147be7d67a5e Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 12 Jun 2026 17:26:55 +0000 Subject: [PATCH 12/34] Sort cube candidates by activity with tie shuffling --- src/smt/smt_solver.cpp | 37 ++++++++++++++++++++++--------------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index e3e15ea9a..aa575a336 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -453,10 +453,11 @@ namespace { expr_mark selected_vars; for (expr* v : vars) selected_vars.mark(v); - expr_ref_vector candidates(m); - expr_ref result(m); - double score = 0.0; - unsigned n = 0; + struct candidate { + expr* e; + double score; + }; + vector candidates; ctx.pop_to_search_level(); for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) { @@ -467,22 +468,28 @@ namespace { continue; if (!vars.empty() && !selected_vars.is_marked(e)) continue; - candidates.push_back(e); - double new_score = ctx.get_activity(v); - // Match smt_parallel: cube split tie-breaking is independent - // of the per-worker SMT search seed. - if (new_score > score || !result || (new_score == score && m_rand(++n) == 0)) { - score = new_score; - result = e; - } + candidates.push_back({ e, ctx.get_activity(v) }); + } + + std::stable_sort(candidates.begin(), candidates.end(), + [](candidate const& a, candidate const& b) { + return a.score > b.score; + }); + for (unsigned i = 0, j = 0; i < candidates.size(); i = j) { + j = i + 1; + while (j < candidates.size() && candidates[i].score == candidates[j].score) + ++j; + if (j > i + 1) + shuffle(j - i, candidates.data() + i, m_rand); } vars.reset(); - vars.append(candidates); + for (auto const& c : candidates) + vars.push_back(c.e); expr_ref_vector lits(m); - if (result) - lits.push_back(result); + if (!candidates.empty()) + lits.push_back(candidates[0].e); return lits; } From 7f1e74c0da681c467997fbaf1900f0fdde977ac9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jun 2026 10:49:05 -0700 Subject: [PATCH 13/34] remove atom Signed-off-by: Nikolaj Bjorner --- src/smt/smt_solver.cpp | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index aa575a336..69e63d1f2 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -233,18 +233,16 @@ namespace { unsigned get_assign_level(expr* e) const override { auto const& ctx = m_context.get_context(); - expr* atom = e; - get_manager().is_not(e, atom); - if (!ctx.b_internalized(atom)) + get_manager().is_not(e, e); + if (!ctx.b_internalized(e)) return UINT_MAX; - return ctx.get_assign_level(ctx.get_bool_var(atom)); + return ctx.get_assign_level(ctx.get_bool_var(e)); } bool is_relevant(expr* e) const override { auto const& ctx = m_context.get_context(); - expr* atom = e; - get_manager().is_not(e, atom); - return ctx.b_internalized(atom) && ctx.is_relevant(atom); + get_manager().is_not(e, e); + return ctx.b_internalized(e) && ctx.is_relevant(e); } unsigned get_num_bool_vars() const override { @@ -253,9 +251,8 @@ namespace { sat::bool_var get_bool_var(expr* e) const override { auto const& ctx = m_context.get_context(); - expr* atom = e; - get_manager().is_not(e, atom); - return ctx.b_internalized(atom) ? ctx.get_bool_var(atom) : sat::null_bool_var; + get_manager().is_not(e, e); + return ctx.b_internalized(e) ? ctx.get_bool_var(e) : sat::null_bool_var; } void pop_to_base_level() override { From 81af0cc2303b6edeec8f5016fc510e0946d2a81f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jun 2026 10:58:11 -0700 Subject: [PATCH 14/34] remove atom Signed-off-by: Nikolaj Bjorner --- src/smt/smt_solver.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 69e63d1f2..f691dfa05 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -88,13 +88,13 @@ namespace { updt_params(p); } - solver * translate(ast_manager & m, params_ref const & p) override { - ast_translation translator(get_manager(), m); + solver * translate(ast_manager & target, params_ref const & p) override { + ast_translation translator(get_manager(), target); params_ref init; init.copy(get_params()); init.copy(p); - smt_solver* result = alloc(smt_solver, m, init, m_logic); + smt_solver* result = alloc(smt_solver, target, init, m_logic); smt::kernel::copy(m_context, result->m_context, true); if (mc0()) @@ -481,12 +481,12 @@ namespace { } vars.reset(); - for (auto const& c : candidates) - vars.push_back(c.e); - expr_ref_vector lits(m); - if (!candidates.empty()) - lits.push_back(candidates[0].e); + for (auto const &c : candidates) { + vars.push_back(c.e); + lits.push_back(c.e); + } + return lits; } From 864c6a3f345c1f17c0fd754d0c447975be4316b9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jun 2026 18:34:08 -0700 Subject: [PATCH 15/34] remove get/set max conflicts from solver, handle it using updt_params and get_params. Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 6 ++++++ src/smt/smt_solver.cpp | 9 --------- src/solver/parallel_tactical2.cpp | 26 ++++++++++++++++---------- src/solver/solver.h | 9 --------- 4 files changed, 22 insertions(+), 28 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f95b77b2d..6b6728e07 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -118,6 +118,12 @@ namespace smt { if (!m_setup.already_configured()) { m_fparams.updt_params(p); } + else { + // selected parameters are safe to update after initialization + params_ref new_p; + new_p.set_uint("max_conflicts", p.get_uint("max_conflicts", UINT_MAX)); + m_fparams.updt_params(new_p); + } for (auto th : m_theory_set) if (th) th->updt_params(); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index f691dfa05..3687f1194 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -267,15 +267,6 @@ namespace { m_context.set_preprocess(f); } - void set_max_conflicts(unsigned max_conflicts) override { - auto& ctx = m_context.get_context(); - ctx.get_fparams().m_max_conflicts = max_conflicts; - } - - unsigned get_max_conflicts() const override { - return m_context.get_context().get_fparams().m_max_conflicts; - } - void get_backbone_candidates(vector& candidates, unsigned max_num) override { ast_manager& m = get_manager(); auto& ctx = m_context.get_context(); diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index dcd844b09..c6f7891bc 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -106,6 +106,12 @@ static bool is_cancellation_exception(char const* msg) { return msg && (strstr(msg, "canceled") != nullptr || strstr(msg, "cancelled") != nullptr); } +static void set_max_conflicts(solver_ref& s, unsigned max_conflicts) { + params_ref p; + p.set_uint("max_conflicts", max_conflicts); + s->updt_params(p); +} + /* ------------------------------------------------------------------ */ /* parallel_solver – the core portfolio engine */ /* ------------------------------------------------------------------ */ @@ -950,7 +956,7 @@ class parallel_solver { } lbool check_cube(expr_ref_vector const& cube) { - s->set_max_conflicts(std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts)); + set_max_conflicts(s, std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts)); expr_ref_vector combined(m); combined.append(asms); @@ -1341,16 +1347,16 @@ class parallel_solver { else ++m_stats.m_fallback_singleton_checks; - unsigned old_max_conflicts = s->get_max_conflicts(); - s->set_max_conflicts(10); + unsigned old_max_conflicts = s->get_params().get_uint("max_conflicts", UINT_MAX); + set_max_conflicts(s, 10); for (expr* lit : chunk_lits) { if (is_retry && b.has_new_backbone_candidates(bb_candidate_epoch)) { - s->set_max_conflicts(old_max_conflicts); + set_max_conflicts(s, old_max_conflicts); return; } if (!m.inc() || canceled()) { - s->set_max_conflicts(old_max_conflicts); + set_max_conflicts(s, old_max_conflicts); return; } if (!bb_candidate_lits.contains(lit)) @@ -1378,7 +1384,7 @@ class parallel_solver { lbool terminal_result = probe_literal(mk_not(m, bb_ref), is_retry); LOG_BB_WORKER(1, " RESULT: " << terminal_result << " FOR CANDIDATE: " << mk_bounded_pp(bb_ref.get(), m, 3) << "\n"); if (terminal_result != l_undef) { - s->set_max_conflicts(old_max_conflicts); + set_max_conflicts(s,old_max_conflicts); return; } } @@ -1387,7 +1393,7 @@ class parallel_solver { bb_candidate_lits.erase(lit); } - s->set_max_conflicts(old_max_conflicts); + set_max_conflicts(s, old_max_conflicts); }; ++m_stats.m_batches_total; @@ -1459,7 +1465,7 @@ class parallel_solver { for (expr* a : bb_asms) asms.push_back(a); - s->set_max_conflicts(m_bb_conflicts_per_chunk); + set_max_conflicts(s,m_bb_conflicts_per_chunk); lbool r = l_undef; try { r = s->check_sat(asms); @@ -1584,7 +1590,7 @@ class parallel_solver { : id(id), b(p.m_batch_manager), asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { s = src.translate(m, params); - s->set_max_conflicts(m_bb_conflicts_per_chunk); + set_max_conflicts(s, m_bb_conflicts_per_chunk); s->pop_to_base_level(); for (expr* a : src_asms) asms.push_back(m_g2l(a)); @@ -1680,7 +1686,7 @@ class parallel_solver { lbool r = l_undef; try { - s->set_max_conflicts(m_core_minimize_conflict_budget); + set_max_conflicts(s, m_core_minimize_conflict_budget); r = s->check_sat(trial); } catch (z3_error&) { diff --git a/src/solver/solver.h b/src/solver/solver.h index 73a83a6dd..45a3a28a9 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -321,15 +321,6 @@ public: virtual void setup_for_parallel() {} virtual void set_preprocess(bool) {} - - virtual void set_max_conflicts(unsigned max_conflicts) { - params_ref p; - p.set_uint("max_conflicts", max_conflicts); - updt_params(p); - } - - virtual unsigned get_max_conflicts() const { return UINT_MAX; } - virtual void get_levels(ptr_vector const& vars, unsigned_vector& depth) = 0; From bcbfeec6c0f0fad6cc1d0d67f8cec5722e5c9c2b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jun 2026 08:32:34 -0700 Subject: [PATCH 16/34] address deadlock in cancellation path Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index c6f7891bc..a31b6db2d 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -480,6 +480,11 @@ class parallel_solver { cancel_workers_unlocked(); } + void set_cancel() { + std::scoped_lock lock(mux); + cancel_workers_unlocked(); + } + void set_unsat(ast_translation& l2g, expr_ref_vector const& core) { std::scoped_lock lock(mux); @@ -1130,8 +1135,10 @@ class parallel_solver { if (m_config.m_global_backbones) { bb_candidates local_candidates = find_backbone_candidates(cube); b.collect_backbone_candidates(m_l2g, local_candidates); - if (!m.inc()) + if (!m.inc()) { + b.set_cancel(); return; + } } lbool r = check_cube(cube); @@ -1142,7 +1149,10 @@ class parallel_solver { continue; } - if (!m.inc()) return; + if (!m.inc()) { + b.set_cancel(); + return; + } switch (r) { From 491d990ed1b1f9d84bd2880c63171a62fb471626 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jun 2026 08:38:58 -0700 Subject: [PATCH 17/34] use structured parameters Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 3 ++- src/smt/smt_solver.cpp | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e03ae8c07..ae5cef768 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -492,7 +492,8 @@ public: } sat::literal_vector lits; expr_ref_vector fmls(m); - if (!m_params.get_bool("cube.lookahead", false)) { + parallel_params pp(m_params); + if (!pp.cube_lookahead()) { sat::bool_var_vector candidates; unsigned search_lvl = m_solver.search_lvl(); for (sat::bool_var v : vars) { diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 3687f1194..dd03c3a6c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -27,6 +27,7 @@ Notes: #include "params/smt_params.h" #include "params/smt_params_helper.hpp" #include "solver/solver_na2as.h" +#include "solver/parallel_params.hpp" #include "solver/mus.h" #include @@ -436,7 +437,8 @@ namespace { expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override { ast_manager& m = get_manager(); - if (!get_params().get_bool("cube.lookahead", false)) { + parallel_params pp(get_params()); + if (!pp.cube_lookahead()) { auto& ctx = m_context.get_context(); expr_mark selected_vars; for (expr* v : vars) From f2d5d6fecf32bb34de3cf83cc62db3ac68a7ac06 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jun 2026 16:13:47 -0700 Subject: [PATCH 18/34] add set_canceled to smt_parallel to avoid deadlock Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 28 ++++++++++++++++++++++------ src/smt/smt_parallel.h | 1 + 2 files changed, 23 insertions(+), 6 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index a7a1acf8a..695588fb5 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -78,8 +78,10 @@ namespace smt { lbool res = l_undef; try { - if (!m.inc()) + if (!m.inc()) { + b.set_canceled(); return; + } res = m_sls->check(); } catch (z3_exception &ex) { // Cancellation is normal in portfolio mode @@ -180,8 +182,9 @@ namespace smt { for (expr* lit : bb_candidate_lits) { if (is_retry && b.has_new_backbone_candidates(bb_candidate_epoch)) break; - if (!m.inc() || canceled()) + if (!m.inc() || canceled()) break; + expr* atom = lit; m.is_not(lit, atom); @@ -218,11 +221,13 @@ namespace smt { } if (!m.inc()) - return; + break; if (!canceled()) b.cancel_current_backbone_batch(); bb_candidates.reset(); } + if (!m.inc()) + b.set_canceled(); } lbool parallel::backbones_worker::probe_literal(bool_var v, expr *e, bool is_retry) { @@ -290,6 +295,7 @@ namespace smt { } if (!m.inc() || canceled()) { ctx->get_fparams().m_max_conflicts = old_max_conflicts; + b.set_canceled(); return; } if (!bb_candidate_lits.contains(lit)) // already handled in singleton core → backbone case below @@ -391,7 +397,7 @@ namespace smt { while (true) { if (!m.inc()) - return; + break; if (canceled()) break; @@ -515,6 +521,8 @@ namespace smt { bb_curr_batch_candidates.reset(); } + if (!m.inc()) + b.set_canceled(); } void parallel::backbones_worker::cancel() { @@ -655,6 +663,7 @@ namespace smt { core.reset(); core.append(mus); core.append(unknown); + b.set_canceled(); return; } @@ -764,7 +773,7 @@ namespace smt { bb_candidates local_candidates = find_backbone_candidates(); b.collect_backbone_candidates(m_l2g, local_candidates); if (!m.inc()) - return; + break; } lbool r = check_cube(cube); @@ -777,7 +786,7 @@ namespace smt { } if (!m.inc()) - return; + break; switch (r) { case l_undef: { @@ -836,6 +845,8 @@ namespace smt { if (m_config.m_share_units) share_units(); } + if (!m.inc()) + b.set_canceled(); } parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms) @@ -1684,6 +1695,11 @@ namespace smt { cancel_background_threads(); } + void parallel::batch_manager::set_canceled() { + std::scoped_lock lock(mux); + cancel_background_threads(); + } + void parallel::batch_manager::set_exception(unsigned error_code) { std::scoped_lock lock(mux); IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n"); diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index b98870e0c..79b326889 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -196,6 +196,7 @@ namespace smt { void set_sat(ast_translation& l2g, model& m); void set_exception(std::string const& msg); void set_exception(unsigned error_code); + void set_canceled(); void collect_statistics(::statistics& st) const; void collect_backbone_candidates(ast_translation& l2g, bb_candidates& bb_candidates); From f2270d46545d998b715b73ee5e76119aca425bbc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jun 2026 17:01:09 -0700 Subject: [PATCH 19/34] make sure split atoms are not already used on the path Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 3 ++- src/smt/smt_solver.cpp | 3 ++- src/solver/parallel_tactical2.cpp | 21 ++++++++++++++++++--- 3 files changed, 22 insertions(+), 5 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index ae5cef768..08e17039f 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -523,7 +523,8 @@ public: for (sat::bool_var v : candidates) { expr* e = bool_var2expr(v); if (e) { - fmls.push_back(e); + if (fmls.size() < backtrack_level) + fmls.push_back(e); vs.push_back(e); } } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index dd03c3a6c..fac58e1c2 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -477,7 +477,8 @@ namespace { expr_ref_vector lits(m); for (auto const &c : candidates) { vars.push_back(c.e); - lits.push_back(c.e); + if (lits.size() < cutoff) + lits.push_back(c.e); } return lits; diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index a31b6db2d..13a5aa18d 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -675,6 +675,19 @@ class parallel_solver { } } + bool path_contains_atom(ast_translation& l2g, node_lease const& lease, expr* atom) { + std::scoped_lock lock(mux); + if (!lease.leased_node) + return false; + if (m_state != state::is_running) + return false; + if (m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch)) + return false; + + expr_ref _atom(l2g(atom), m); + return lease.leased_node->path_contains_atom(_atom); + } + void try_split(ast_translation& l2g, unsigned worker_id, node_lease const& lease, expr* atom, unsigned effort) { @@ -1038,20 +1051,22 @@ class parallel_solver { m_shared_units_prefix = prefix_sz; } - expr_ref get_split_atom(expr_ref_vector const& cube) { + expr_ref get_split_atom(node_lease const& lease, expr_ref_vector const& cube) { if (cube.size() >= m_config.m_max_cube_depth) return expr_ref(nullptr, m); expr_ref_vector vars(m); obj_hashtable rejected_atoms; while (true) { - expr_ref_vector cands = s->cube(vars, 1); + expr_ref_vector cands = s->cube(vars, 10); bool rejected = false; for (expr* lit : cands) { if (!lit) continue; if (m.is_true(lit) || m.is_false(lit)) continue; + if (b.path_contains_atom(m_l2g, lease, lit)) + continue; if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) { expr* atom = lit; m.is_not(lit, atom); @@ -1161,7 +1176,7 @@ class parallel_solver { LOG_WORKER(1, " found undef cube\n"); if (m_config.m_max_cube_depth <= cube.size()) goto check_cube_start; - expr_ref atom = get_split_atom(cube); + expr_ref atom = get_split_atom(lease, cube); if (atom) { b.try_split(m_l2g, id, lease, atom.get(), m_config.m_threads_max_conflicts); From 96092b196c7350444365f85216f576aca077e6a8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 13:46:29 -0700 Subject: [PATCH 20/34] add exception handling in case run method throws Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 5 +---- src/solver/parallel_tactical2.cpp | 28 +++++++++++++++++++++++----- 2 files changed, 24 insertions(+), 9 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6b6728e07..0e8062e88 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -120,9 +120,7 @@ namespace smt { } else { // selected parameters are safe to update after initialization - params_ref new_p; - new_p.set_uint("max_conflicts", p.get_uint("max_conflicts", UINT_MAX)); - m_fparams.updt_params(new_p); + m_fparams.m_max_conflicts = p.get_uint("max_conflicts", m_fparams.m_max_conflicts); } for (auto th : m_theory_set) if (th) @@ -4685,7 +4683,6 @@ namespace smt { theory_id th_id = l->get_id(); for (enode * parent : enode::parents(n)) { - auto p = parent->get_expr(); family_id fid = parent->get_family_id(); if (fid != th_id && fid != m.get_basic_family_id()) { if (is_beta_redex(parent, n)) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 13a5aa18d..2d73046bd 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -883,7 +883,7 @@ class parallel_solver { if (lim.is_canceled() || m_state != state::is_running) return false; - if (m_bb_last_batch_processed[bb_thread_id] == m_bb_batch_id) { + if (m_bb_last_batch_processed[bb_thread_id] == m_bb_batch_id) { unsigned n = std::min(m_bb_batch_size, m_bb_candidates.size()); m_bb_current_batch.reset(); for (unsigned i = 0; i < n; ++i) { @@ -1912,14 +1912,32 @@ public: m_batch_manager.initialize(num_bb_threads); + auto safe_run = [&](std::function run_fn, reslimit& lim) { + try { + run_fn(); + } catch (z3_error &err) { + if (!lim.is_canceled()) + m_batch_manager.set_exception(err.error_code()); + } catch (z3_exception &ex) { + if (!lim.is_canceled() && !is_cancellation_exception(ex.what())) + m_batch_manager.set_exception(ex.what()); + } + }; /* Launch threads. */ vector threads; - for (auto* w : m_workers) - threads.push_back(std::thread([w]() { w->run(); })); + for (auto *w : m_workers) + threads.push_back(std::thread([&]() { + safe_run([w]() -> void { w->run(); }, w->limit()); + })); if (m_core_minimizer_worker) - threads.push_back(std::thread([this]() { m_core_minimizer_worker->run(); })); + threads.push_back(std::thread([&]() { + safe_run([this]() -> void { m_core_minimizer_worker->run(); }, m_core_minimizer_worker->limit()); + })); for (auto* w : m_global_backbones_workers) - threads.push_back(std::thread([w]() { w->run(); })); + threads.push_back(std::thread([&]() { + safe_run([w]() -> void { + w->run(); }, w->limit()); + })); for (auto& t : threads) t.join(); From 84a3c8789fb2f9222d0006cbefa8a671700b4e82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 14:06:48 -0700 Subject: [PATCH 21/34] fix scoping for functions Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 2d73046bd..36c17d5ce 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1926,18 +1926,17 @@ public: /* Launch threads. */ vector threads; for (auto *w : m_workers) - threads.push_back(std::thread([&]() { - safe_run([w]() -> void { w->run(); }, w->limit()); + threads.push_back(std::thread([w, &safe_run]() { + safe_run([w]() { w->run(); }, w->limit()); })); if (m_core_minimizer_worker) - threads.push_back(std::thread([&]() { - safe_run([this]() -> void { m_core_minimizer_worker->run(); }, m_core_minimizer_worker->limit()); + threads.push_back(std::thread([this, &safe_run]() { + safe_run([this]() { m_core_minimizer_worker->run(); }, m_core_minimizer_worker->limit()); })); for (auto* w : m_global_backbones_workers) - threads.push_back(std::thread([&]() { - safe_run([w]() -> void { - w->run(); }, w->limit()); - })); + threads.push_back(std::thread([w, &safe_run]() { + safe_run([w]() { w->run(); }, w->limit()); + })); for (auto& t : threads) t.join(); From fc3892486c843dae74b535b7858eaec8872f0cd5 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Sun, 14 Jun 2026 19:55:28 -0700 Subject: [PATCH 22/34] fix cancel bugs and remove smt_parallel_params --- src/params/CMakeLists.txt | 1 - src/params/smt_parallel_params.pyg | 12 ------ src/smt/smt_parallel.cpp | 65 +++++++++++++++++------------- src/solver/parallel_tactical2.cpp | 12 +++++- 4 files changed, 48 insertions(+), 42 deletions(-) delete mode 100644 src/params/smt_parallel_params.pyg diff --git a/src/params/CMakeLists.txt b/src/params/CMakeLists.txt index 732430fe3..9aea5b918 100644 --- a/src/params/CMakeLists.txt +++ b/src/params/CMakeLists.txt @@ -28,7 +28,6 @@ z3_add_component(params seq_rewriter_params.pyg sls_params.pyg smt_params_helper.pyg - smt_parallel_params.pyg solver_params.pyg tactic_params.pyg EXTRA_REGISTER_MODULE_HEADERS diff --git a/src/params/smt_parallel_params.pyg b/src/params/smt_parallel_params.pyg deleted file mode 100644 index 315d3d029..000000000 --- a/src/params/smt_parallel_params.pyg +++ /dev/null @@ -1,12 +0,0 @@ -def_module_params('smt_parallel', - export=True, - description='Experimental parameters for parallel solving', - params=( - ('inprocessing', BOOL, False, 'integrate in-processing as a heuristic simplification'), - ('sls', BOOL, False, 'add sls-tactic as a separate worker thread outside the search tree parallelism'), - ('num_global_bb_fl_threads', UINT, 0, 'run failed-literal backbone worker threads; default is 0 (off), supported values are 1 (negative mode only) or 2 (negative and positive mode)'), - ('num_global_bb_batch_threads', UINT, 2, 'run Janota-style chunking backbone worker threads; default is 2 (negative and positive mode), supported values are 0 (off), 1 (negative mode only) or 2 (negative and positive mode)'), - ('local_backbones', BOOL, False, 'enable local backbones experiment within the search tree parallelism'), - ('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'), - ('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'), - )) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 695588fb5..9ce35eaf4 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -25,7 +25,6 @@ Author: #include "smt/smt_parallel.h" #include "smt/smt_lookahead.h" #include "solver/solver_preprocess.h" -#include "params/smt_parallel_params.hpp" #include #include @@ -751,6 +750,7 @@ namespace smt { if (minimized.size() < original_size) b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); } + b.set_canceled(); } void parallel::worker::run() { @@ -865,12 +865,11 @@ namespace smt { m_num_initial_atoms = ctx->get_num_bool_vars(); ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged - smt_parallel_params pp(p.ctx.m_params); - m_config.m_inprocessing = pp.inprocessing(); - m_config.m_global_backbones = pp.num_global_bb_batch_threads() > 0 || pp.num_global_bb_fl_threads() > 0; - m_config.m_local_backbones = pp.local_backbones(); - m_config.m_core_minimize = pp.core_minimize(); - m_config.m_ablate_backtracking = pp.ablate_backtracking(); + m_config.m_inprocessing = false; + m_config.m_global_backbones = true; + m_config.m_local_backbones = false; + m_config.m_core_minimize = true; + m_config.m_ablate_backtracking = false; // When ablating backtracking, disable core minimization since we're using the full cube path if (m_config.m_ablate_backtracking) { @@ -899,9 +898,7 @@ namespace smt { m_shared_units_prefix = ctx->assigned_literals().size(); m_num_initial_atoms = ctx->get_num_bool_vars(); ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged - - smt_parallel_params pp(p.ctx.m_params); - m_use_failed_literal_test = pp.num_global_bb_fl_threads() > 0; + m_use_failed_literal_test = false; // true failed literal mode, false for Janota chunking algorithm } parallel::bb_candidates parallel::worker::find_backbone_candidates(unsigned k) { @@ -1796,8 +1793,7 @@ namespace smt { m_worker_leases.reset(); m_worker_leases.resize(p.m_workers.size()); - smt_parallel_params pp(p.ctx.m_params); - m_ablate_backtracking = pp.ablate_backtracking(); + m_ablate_backtracking = false; } void parallel::batch_manager::collect_statistics(::statistics &st) const { @@ -1811,18 +1807,11 @@ namespace smt { } lbool parallel::operator()(expr_ref_vector const &asms) { - smt_parallel_params pp(ctx.m_params); - unsigned num_global_bb_batch_threads = pp.num_global_bb_batch_threads(); - if (num_global_bb_batch_threads > 2) - throw default_exception("smt_parallel.num_global_bb_batch_threads must be 0, 1, or 2"); + unsigned num_global_bb_batch_threads = 2; unsigned num_workers = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads); - unsigned num_sls_threads = (pp.sls() ? 1 : 0); - unsigned num_core_min_threads = (pp.core_minimize() ? 1 : 0); - unsigned num_global_bb_fl_threads = pp.num_global_bb_fl_threads(); - if (num_global_bb_fl_threads > 2) - throw default_exception("smt_parallel.num_global_bb_fl_threads must be 0, 1, or 2"); - if (num_global_bb_fl_threads > 0 && num_global_bb_batch_threads > 0) - throw default_exception("smt_parallel.num_global_bb_fl_threads and smt_parallel.num_global_bb_batch_threads cannot both be enabled"); + unsigned num_sls_threads = 0; + unsigned num_core_min_threads = 1; + unsigned num_global_bb_fl_threads = 0; unsigned num_global_bb_threads = num_global_bb_fl_threads > 0 ? num_global_bb_fl_threads : num_global_bb_batch_threads; unsigned total_threads = num_workers + num_sls_threads + num_core_min_threads + num_global_bb_threads; @@ -1858,7 +1847,7 @@ namespace smt { m_sls_worker = alloc(sls_worker, *this); sl.push_child(&(m_sls_worker->limit())); } - if (pp.core_minimize()) { + if (num_core_min_threads == 1) { m_core_minimizer_worker = alloc(core_minimizer_worker, *this, asms); sl.push_child(&(m_core_minimizer_worker->limit())); } @@ -1874,17 +1863,37 @@ namespace smt { m_batch_manager.initialize(num_global_bb_threads); + auto safe_run = [&](auto* w) { + try { + w->run(); + if (w->limit().is_canceled()) + m_batch_manager.set_canceled(); + } + catch (z3_error& err) { + if (!w->limit().is_canceled()) + m_batch_manager.set_exception(err.error_code()); + else + m_batch_manager.set_canceled(); + } + catch (z3_exception& ex) { + if (!w->limit().is_canceled() && !is_cancellation_exception(ex.what())) + m_batch_manager.set_exception(ex.what()); + else + m_batch_manager.set_canceled(); + } + }; + // Launch threads vector threads(total_threads); unsigned thread_idx = 0; for (auto* w : m_workers) - threads[thread_idx++] = std::thread([&, w]() { w->run(); }); + threads[thread_idx++] = std::thread([&, w]() { safe_run(w); }); if (m_sls_worker) - threads[thread_idx++] = std::thread([&]() { m_sls_worker->run(); }); + threads[thread_idx++] = std::thread([&]() { safe_run(m_sls_worker.get()); }); if (m_core_minimizer_worker) - threads[thread_idx++] = std::thread([&]() { m_core_minimizer_worker->run(); }); + threads[thread_idx++] = std::thread([&]() { safe_run(m_core_minimizer_worker.get()); }); for (auto* w : m_global_backbones_workers) - threads[thread_idx++] = std::thread([&, w]() { w->run(); }); + threads[thread_idx++] = std::thread([&, w]() { safe_run(w); }); // Wait for all threads to finish diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 36c17d5ce..8f1045c5e 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1480,8 +1480,10 @@ class parallel_solver { collect_shared_clauses(); while (true) { - if (!m.inc()) + if (!m.inc()) { + b.set_cancel(); return; + } if (canceled()) break; @@ -1607,6 +1609,7 @@ class parallel_solver { curr_batch.reset(); } + b.set_cancel(); } public: @@ -1806,6 +1809,7 @@ class parallel_solver { if (minimized.size() < original_size) b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); } + b.set_cancel(); } void cancel() { @@ -1915,12 +1919,18 @@ public: auto safe_run = [&](std::function run_fn, reslimit& lim) { try { run_fn(); + if (lim.is_canceled()) + m_batch_manager.set_cancel(); } catch (z3_error &err) { if (!lim.is_canceled()) m_batch_manager.set_exception(err.error_code()); + else + m_batch_manager.set_cancel(); } catch (z3_exception &ex) { if (!lim.is_canceled() && !is_cancellation_exception(ex.what())) m_batch_manager.set_exception(ex.what()); + else + m_batch_manager.set_cancel(); } }; /* Launch threads. */ From 5b307545e6975023b41b4b7c71386f69cf3869f1 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Sun, 14 Jun 2026 22:02:00 -0700 Subject: [PATCH 23/34] change scheduling in old smt_parallel code to keep it updated --- src/smt/smt_parallel.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 9ce35eaf4..2e893360b 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -294,7 +294,6 @@ namespace smt { } if (!m.inc() || canceled()) { ctx->get_fparams().m_max_conflicts = old_max_conflicts; - b.set_canceled(); return; } if (!bb_candidate_lits.contains(lit)) // already handled in singleton core → backbone case below @@ -395,8 +394,10 @@ namespace smt { while (true) { - if (!m.inc()) - break; + if (!m.inc()) { + b.set_canceled(); + return; + } if (canceled()) break; @@ -662,7 +663,6 @@ namespace smt { core.reset(); core.append(mus); core.append(unknown); - b.set_canceled(); return; } From 38a8644ae3f6354022cff4f86b82c8d2bf320085 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 22:24:02 -0700 Subject: [PATCH 24/34] avoid double cancel Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 8f1045c5e..921e6dcf6 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -482,6 +482,8 @@ class parallel_solver { void set_cancel() { std::scoped_lock lock(mux); + if (m_state != state::is_running) + return; cancel_workers_unlocked(); } From 26f7ce23b6d97dde43214ce6b682b9d61b8264a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 22:29:33 -0700 Subject: [PATCH 25/34] lipstick Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 921e6dcf6..3966732e6 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -928,9 +928,9 @@ class parallel_solver { expr_ref_vector const& get_unsat_core() const { return m_unsat_core; } void collect_statistics(statistics& st) const { - st.update("parallel-num_cubes", m_stats.m_num_cubes); + st.update("parallel-num-cubes", m_stats.m_num_cubes); st.update("parallel-max-cube-size", m_stats.m_max_cube_depth); - st.update("bb-backbones-found", m_stats.m_backbones_found); + st.update("parallel-backbones-found", m_stats.m_backbones_found); st.update("parallel-core-min-jobs-enqueued", m_stats.m_core_min_jobs_enqueued); st.update("parallel-core-min-jobs-published", m_stats.m_core_min_jobs_published); st.update("parallel-core-min-jobs-skipped", m_stats.m_core_min_jobs_skipped); @@ -1638,19 +1638,19 @@ class parallel_solver { } void collect_statistics(statistics& st) const { - st.update("bb-batches-total", m_stats.m_batches_total); - st.update("bb-candidates-total", m_stats.m_candidates_total); - st.update("bb-backbones-detected", m_stats.m_backbones_detected); - st.update("bb-internal-backbones-found", m_stats.m_internal_backbones_found); - st.update("bb-retry-backbones-found", m_stats.m_retry_backbones_found); - st.update("bb-retries", m_stats.m_bb_retries); - st.update("bb-core-refinement-rounds", m_stats.m_core_refinement_rounds); - st.update("bb-singleton-backbones", m_stats.m_singleton_backbones); - st.update("bb-fallback-singleton-checks", m_stats.m_fallback_singleton_checks); - st.update("bb-fallback-chunk-exhausted", m_stats.m_fallback_reason_chunk_exhausted); - st.update("bb-fallback-undef", m_stats.m_fallback_reason_undef); - st.update("bb-literals-removed-by-core", m_stats.m_lits_removed_by_core); - st.update("bb-num-chunk-increases", m_stats.m_num_chunk_increases); + st.update("parallel-bb-batches-total", m_stats.m_batches_total); + st.update("parallel-bb-candidates-total", m_stats.m_candidates_total); + st.update("parallel-bb-backbones-detected", m_stats.m_backbones_detected); + st.update("parallel-bb-internal-backbones-found", m_stats.m_internal_backbones_found); + st.update("parallel-bb-retry-backbones-found", m_stats.m_retry_backbones_found); + st.update("parallel-bb-retries", m_stats.m_bb_retries); + st.update("parallel-bb-core-refinement-rounds", m_stats.m_core_refinement_rounds); + st.update("parallel-bb-singleton-backbones", m_stats.m_singleton_backbones); + st.update("parallel-bb-fallback-singleton-checks", m_stats.m_fallback_singleton_checks); + st.update("parallel-bb-fallback-chunk-exhausted", m_stats.m_fallback_reason_chunk_exhausted); + st.update("parallel-bb-fallback-undef", m_stats.m_fallback_reason_undef); + st.update("parallel-bb-literals-removed-by-core", m_stats.m_lits_removed_by_core); + st.update("parallel-bb-num-chunk-increases", m_stats.m_num_chunk_increases); auto safe_ratio = [](double num, double den) -> double { return den > 0 ? num / den : 0.0; From e95f9757c92185e5c8a9cd2795ee7a8ec7b3d95b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 22:38:40 -0700 Subject: [PATCH 26/34] lipstick Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 3966732e6..5b0902751 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1656,13 +1656,13 @@ class parallel_solver { return den > 0 ? num / den : 0.0; }; - st.update("bb-backbone-yield-pct", + st.update("parallel-bb-backbone-yield-pct", 100.0 * safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_candidates_total)); - st.update("bb-avg-backbones-per-batch", + st.update("parallel-bb-avg-backbones-per-batch", safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_batches_total)); - st.update("bb-core-refinement-rounds-per-batch", + st.update("parallel-bb-core-refinement-rounds-per-batch", safe_ratio(m_stats.m_core_refinement_rounds, m_stats.m_batches_total)); - st.update("bb-core-effectiveness-lit-removed-per-round", + st.update("parallel-bb-core-effectiveness-lit-removed-per-round", safe_ratio(m_stats.m_lits_removed_by_core, m_stats.m_core_refinement_rounds)); } From dba826039d457d5b29ef418179d7f42a68ec10b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 23:31:37 -0700 Subject: [PATCH 27/34] avoid spurious cancel Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 2e893360b..ac0193169 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -1694,6 +1694,8 @@ namespace smt { void parallel::batch_manager::set_canceled() { std::scoped_lock lock(mux); + if (m_state != state::is_running) + return; cancel_background_threads(); } From be1b2f6e1545c3ddc4ff4ea9b1e01814de2d5557 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Sun, 14 Jun 2026 23:31:47 -0700 Subject: [PATCH 28/34] normalize parallel params --- src/smt/smt_parallel.cpp | 22 ++++++++++++++++------ src/solver/parallel_params.pyg | 1 + src/solver/parallel_tactical2.cpp | 9 ++++++++- 3 files changed, 25 insertions(+), 7 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 2e893360b..d9badd2b1 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -25,6 +25,7 @@ Author: #include "smt/smt_parallel.h" #include "smt/smt_lookahead.h" #include "solver/solver_preprocess.h" +#include "solver/parallel_params.hpp" #include #include @@ -865,11 +866,12 @@ namespace smt { m_num_initial_atoms = ctx->get_num_bool_vars(); ctx->get_fparams().m_preprocess = false; // avoid preprocessing lemmas that are exchanged + parallel_params pp(p.ctx.get_params()); m_config.m_inprocessing = false; - m_config.m_global_backbones = true; + m_config.m_global_backbones = pp.num_bb_threads() > 0; m_config.m_local_backbones = false; - m_config.m_core_minimize = true; - m_config.m_ablate_backtracking = false; + m_config.m_core_minimize = pp.core_minimize(); + m_config.m_ablate_backtracking = pp.ablate_backtracking(); // When ablating backtracking, disable core minimization since we're using the full cube path if (m_config.m_ablate_backtracking) { @@ -1793,7 +1795,8 @@ namespace smt { m_worker_leases.reset(); m_worker_leases.resize(p.m_workers.size()); - m_ablate_backtracking = false; + parallel_params pp(p.ctx.get_params()); + m_ablate_backtracking = pp.ablate_backtracking(); } void parallel::batch_manager::collect_statistics(::statistics &st) const { @@ -1807,10 +1810,17 @@ namespace smt { } lbool parallel::operator()(expr_ref_vector const &asms) { - unsigned num_global_bb_batch_threads = 2; + params_ref const& params = ctx.get_params(); + parallel_params pp(params); + unsigned num_global_bb_batch_threads = pp.num_bb_threads(); + if (num_global_bb_batch_threads > 2) + throw default_exception("parallel.num_bb_threads must be 0, 1, or 2"); unsigned num_workers = std::min((unsigned)std::thread::hardware_concurrency(), ctx.get_fparams().m_threads); unsigned num_sls_threads = 0; - unsigned num_core_min_threads = 1; + bool core_minimize = pp.core_minimize(); + if (pp.ablate_backtracking()) + core_minimize = false; + unsigned num_core_min_threads = (core_minimize ? 1 : 0); unsigned num_global_bb_fl_threads = 0; unsigned num_global_bb_threads = num_global_bb_fl_threads > 0 ? num_global_bb_fl_threads : num_global_bb_batch_threads; unsigned total_threads = num_workers + num_sls_threads + num_core_min_threads + num_global_bb_threads; diff --git a/src/solver/parallel_params.pyg b/src/solver/parallel_params.pyg index e577c58e8..222d4a8fd 100644 --- a/src/solver/parallel_params.pyg +++ b/src/solver/parallel_params.pyg @@ -8,6 +8,7 @@ def_module_params('parallel', ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'), ('num_bb_threads', UINT, 2, 'run Janota-style chunking backbone worker threads; default is 2 (negative and positive mode), supported values are 0 (off), 1 (negative mode only) or 2 (negative and positive mode)'), ('core_minimize', BOOL, True, 'minimize unsat cores used for parallel cube backtracking'), + ('ablate_backtracking', BOOL, False, 'ablation: pass entire cube as core instead of unsat core during backtracking'), ('cube.lookahead', BOOL, False, 'use lookahead cubing in the parallel solver; when false, use VSIDS activity to select one split literal'), ('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'), ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'), diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 8f1045c5e..8d341b665 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -953,6 +953,7 @@ class parallel_solver { bool m_share_units_initial_only = true; bool m_core_minimize = false; bool m_global_backbones = false; + bool m_ablate_backtracking = false; unsigned m_max_cube_depth = 20; }; @@ -1117,7 +1118,10 @@ class parallel_solver { : id(id), b(p.m_batch_manager), asms(m), m_g2l(src.get_manager(), m), m_l2g(m, src.get_manager()) { parallel_params pp(params); m_config.m_core_minimize = pp.core_minimize(); + m_config.m_ablate_backtracking = pp.ablate_backtracking(); m_config.m_global_backbones = pp.num_bb_threads() > 0; + if (m_config.m_ablate_backtracking) + m_config.m_core_minimize = false; s = src.translate(m, params); // don't share initial units @@ -1211,7 +1215,8 @@ class parallel_solver { LOG_WORKER(1, " found unsat cube\n"); auto* source = lease.leased_node; - b.backtrack(m_l2g, id, unsat_core, lease); + expr_ref_vector const& core_to_use = m_config.m_ablate_backtracking ? cube : unsat_core; + b.backtrack(m_l2g, id, core_to_use, lease); if (m_config.m_core_minimize) b.enqueue_core_minimization(m_l2g, source, unsat_core); @@ -1869,6 +1874,8 @@ public: static_cast(std::thread::hardware_concurrency()), pp.threads_max()); bool core_minimize = pp.core_minimize(); + if (pp.ablate_backtracking()) + core_minimize = false; unsigned num_bb_threads = pp.num_bb_threads(); if (num_bb_threads > 2) throw default_exception("parallel.num_bb_threads must be 0, 1, or 2"); From 4dbd592137ed099895ffc0e74eea5b1545a61106 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 23:54:28 -0700 Subject: [PATCH 29/34] guard cancelation behind !m.inc() Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 96d9e1c32..d19116e24 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1616,7 +1616,8 @@ class parallel_solver { curr_batch.reset(); } - b.set_cancel(); + if (!m.inc()) + b.set_cancel(); } public: @@ -1816,7 +1817,8 @@ class parallel_solver { if (minimized.size() < original_size) b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); } - b.set_cancel(); + if (!m.inc()) + b.set_cancel(); } void cancel() { From 4237f9d86b2cc804a68f620f3de846f9ebfc2077 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Jun 2026 10:03:46 -0700 Subject: [PATCH 30/34] log exceptions Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index d19116e24..677cb0e36 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -861,7 +861,7 @@ class parallel_solver { if (changed && !m_bb_candidates.empty()) { m_bb_candidate_epoch.fetch_add(1, std::memory_order_release); - std::sort( + std::stable_sort( m_bb_candidates.begin(), m_bb_candidates.end(), [&](bb_candidate const& a, bb_candidate const& b) { @@ -1933,11 +1933,13 @@ public: if (lim.is_canceled()) m_batch_manager.set_cancel(); } catch (z3_error &err) { + IF_VERBOSE(0, verbose_stream() << "Exception in parallel solver: " << err.what() << "\n"); if (!lim.is_canceled()) m_batch_manager.set_exception(err.error_code()); else m_batch_manager.set_cancel(); } catch (z3_exception &ex) { + IF_VERBOSE(0, verbose_stream() << "Exception in parallel solver: " << ex.what() << "\n"); if (!lim.is_canceled() && !is_cancellation_exception(ex.what())) m_batch_manager.set_exception(ex.what()); else From 2b9b9a96237b9e1518a6f6329d4da1faf97ea038 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Jun 2026 10:28:52 -0700 Subject: [PATCH 31/34] log exceptions Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 677cb0e36..d0e370669 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -598,14 +598,13 @@ class parallel_solver { unsigned best_idx = select_best_core_min_job_unlocked(); m_core_min_jobs.swap(best_idx, m_core_min_jobs.size() - 1); - core_min_job* job = m_core_min_jobs.detach_back(); + scoped_ptr job = m_core_min_jobs.detach_back(); m_core_min_jobs.pop_back(); SASSERT(job); source = job->source; core.reset(); for (expr* c : job->core) core.push_back(g2l(c)); - dealloc(job); return source != nullptr; } @@ -999,6 +998,10 @@ class parallel_solver { catch (z3_exception& ex) { if (!m.limit().is_canceled() && !is_cancellation_exception(ex.what())) b.set_exception(ex.what()); + } + catch (...) { + IF_VERBOSE(0, verbose_stream() << "Unknown exception in check_cube\n";); + throw; } LOG_WORKER(1, " DONE checking cube " << r << "\n";); return r; From 48ae786c4c1bc6fee87c3de42c6bb1f07e4690c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Jun 2026 14:02:43 -0600 Subject: [PATCH 32/34] catch exceptions from cube and backbone calls. They can throw Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 46 +++++++++++++++++++------------ 1 file changed, 29 insertions(+), 17 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index d0e370669..ab69b713c 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1064,23 +1064,30 @@ class parallel_solver { expr_ref_vector vars(m); obj_hashtable rejected_atoms; while (true) { - expr_ref_vector cands = s->cube(vars, 10); bool rejected = false; - for (expr* lit : cands) { - if (!lit) - continue; - if (m.is_true(lit) || m.is_false(lit)) - continue; - if (b.path_contains_atom(m_l2g, lease, lit)) - continue; - if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) { - expr* atom = lit; - m.is_not(lit, atom); - rejected_atoms.insert(atom); - rejected = true; - continue; + try { + expr_ref_vector cands = s->cube(vars, 10); + for (expr *lit : cands) { + if (!lit) + continue; + if (m.is_true(lit) || m.is_false(lit)) + continue; + if (b.path_contains_atom(m_l2g, lease, lit)) + continue; + if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) { + expr *atom = lit; + m.is_not(lit, atom); + rejected_atoms.insert(atom); + rejected = true; + continue; + } + return expr_ref(lit, m); } - return expr_ref(lit, m); + } + catch (...) { + if (!m.inc()) + return expr_ref(nullptr, m); + throw; } if (!rejected || vars.empty()) @@ -1103,8 +1110,13 @@ class parallel_solver { bb_candidates find_backbone_candidates(expr_ref_vector const& cube, unsigned k = 10) { bb_candidates result; vector cands; - s->get_backbone_candidates(cands, s->get_num_bool_vars()); - + try { + s->get_backbone_candidates(cands, s->get_num_bool_vars()); + } catch (z3_exception &ex) { + if (!m.inc()) + return result; + throw; + } for (auto const& cand : cands) { expr* lit = cand.lit.get(); if (m_config.m_global_backbones && From fc5e4d7557d4dda0e31e06689551e27f36d1ec8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Jun 2026 16:00:26 -0600 Subject: [PATCH 33/34] check for lease expiration before checking for m.inc() Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ab69b713c..ec27f176f 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1171,10 +1171,6 @@ class parallel_solver { if (m_config.m_global_backbones) { bb_candidates local_candidates = find_backbone_candidates(cube); b.collect_backbone_candidates(m_l2g, local_candidates); - if (!m.inc()) { - b.set_cancel(); - return; - } } lbool r = check_cube(cube); @@ -1185,11 +1181,14 @@ class parallel_solver { continue; } + // NSB - at this point it shouldn't be possible to call inc_cancel. + // Is this ensured? I am not sure. if (!m.inc()) { b.set_cancel(); return; } + switch (r) { case l_undef: { From ab523fce54d941515734e27f994f6605eb6eef78 Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Mon, 15 Jun 2026 23:14:53 -0700 Subject: [PATCH 34/34] attempt at lease policy patch --- src/smt/smt_parallel.cpp | 79 ++++++++++++------- src/smt/smt_parallel.h | 9 +-- src/solver/parallel_tactical2.cpp | 124 +++++++++++++----------------- src/util/search_tree.h | 16 +--- 4 files changed, 113 insertions(+), 115 deletions(-) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 8a3910590..5497d7ec0 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -80,6 +80,7 @@ namespace smt { try { if (!m.inc()) { b.set_canceled(); + // b.notify_cv_waiters; return; } res = m_sls->check(); @@ -227,7 +228,8 @@ namespace smt { bb_candidates.reset(); } if (!m.inc()) - b.set_canceled(); + b.set_canceled(); + // b.notify_cv_waiters; } lbool parallel::backbones_worker::probe_literal(bool_var v, expr *e, bool is_retry) { @@ -397,6 +399,7 @@ namespace smt { if (!m.inc()) { b.set_canceled(); + // b.notify_cv_waiters; return; } if (canceled()) @@ -524,6 +527,7 @@ namespace smt { } if (!m.inc()) b.set_canceled(); + // b.notify_cv_waiters; } void parallel::backbones_worker::cancel() { @@ -559,7 +563,7 @@ namespace smt { if (m_ablate_backtracking) { // Ablation: for each target, pass the entire path from root to that node for (auto const& target : targets) { - if (m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch)) + if (m_search_tree.is_lease_canceled(target.leased_node)) continue; // Reconstruct the full path from root to this target node @@ -752,6 +756,7 @@ namespace smt { b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); } b.set_canceled(); + // b.notify_cv_waiters; } void parallel::worker::run() { @@ -773,21 +778,29 @@ namespace smt { if (m_config.m_global_backbones) { bb_candidates local_candidates = find_backbone_candidates(); b.collect_backbone_candidates(m_l2g, local_candidates); - if (!m.inc()) + if (!m.inc()) { + b.set_canceled(); + // b.notify_cv_waiters; break; + } } lbool r = check_cube(cube); - if (b.lease_canceled(lease)) { + bool cancel_signaled = false; + if (b.release_canceled_lease(id, lease, cancel_signaled)) { LOG_WORKER(1, " abandoning canceled lease\n"); lease = {}; - m.limit().dec_cancel(); + if (cancel_signaled) + m.limit().dec_cancel(); continue; } - if (!m.inc()) + if (!m.inc()) { + b.set_canceled(); + // b.notify_cv_waiters; break; + } switch (r) { case l_undef: { @@ -846,8 +859,11 @@ namespace smt { if (m_config.m_share_units) share_units(); } - if (!m.inc()) + if (!m.inc()) { b.set_canceled(); + // b.notify_cv_waiters; + return; + } } parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms) @@ -1135,7 +1151,7 @@ namespace smt { // only cancel workers that currently hold a lease, whose lease is canceled, // and haven't already been signaled (prevents multiple inc_cancel() for same lease) - if (lease.leased_node && !lease.cancel_signaled && m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch)) { + if (lease.leased_node && !lease.cancel_signaled && m_search_tree.is_lease_canceled(lease.leased_node)) { p.m_workers[worker_id]->cancel_lease(); m_worker_leases[worker_id].cancel_signaled = true; } @@ -1190,14 +1206,13 @@ namespace smt { unsigned best_idx = select_best_core_min_job_unlocked(); m_core_min_jobs.swap(best_idx, m_core_min_jobs.size() - 1); - core_min_job* job = m_core_min_jobs.detach_back(); + scoped_ptr job = m_core_min_jobs.detach_back(); m_core_min_jobs.pop_back(); SASSERT(job); source = job->source; core.reset(); for (expr* c : job->core) core.push_back(g2l(c)); - dealloc(job); return source != nullptr; } @@ -1288,7 +1303,7 @@ namespace smt { if (!g_core.empty()) { collect_matching_targets_unlocked(source, g_core[0].get(), g_core, targets); for (auto const& target : targets) { - if (!m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch)) + if (!m_search_tree.is_lease_canceled(target.leased_node)) m_search_tree.backtrack(target.leased_node, g_core); } } @@ -1342,7 +1357,7 @@ namespace smt { for (node* t : matches) { if (!t || t == source) continue; - if (m_search_tree.is_lease_canceled(t, t->get_cancel_epoch())) + if (m_search_tree.is_lease_canceled(t)) continue; // When source is provided, keep only external matches. Nodes in the @@ -1369,7 +1384,7 @@ namespace smt { if (!is_highest_ancestor) continue; - targets.push_back({ t, t->get_cancel_epoch() }); + targets.push_back({ t }); } } @@ -1385,7 +1400,7 @@ namespace smt { SASSERT(lease != nullptr || targets != nullptr); bool did_backtrack = false; - if (lease && !m_search_tree.is_lease_canceled(lease->leased_node, lease->cancel_epoch)) { + if (lease && !m_search_tree.is_lease_canceled(lease->leased_node)) { // we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled // i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack did_backtrack = true; @@ -1395,7 +1410,7 @@ namespace smt { } if (targets) { for (auto const& target : *targets) { - if (m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch)) + if (m_search_tree.is_lease_canceled(target.leased_node)) continue; did_backtrack = true; @@ -1427,13 +1442,13 @@ namespace smt { if (m_state != state::is_running) return; - if (m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch)) + if (m_search_tree.is_lease_canceled(lease.leased_node)) return; expr_ref lit(m), nlit(m); lit = l2g(atom); nlit = mk_not(m, lit); - bool did_split = m_search_tree.try_split(lease.leased_node, lease.cancel_epoch, lit, nlit, effort); + bool did_split = m_search_tree.try_split(lease.leased_node, lit, nlit, effort); release_lease_unlocked(worker_id, lease.leased_node); @@ -1449,9 +1464,22 @@ namespace smt { release_lease_unlocked(worker_id, lease.leased_node); } - bool parallel::batch_manager::lease_canceled(node_lease const &lease) { + bool parallel::batch_manager::release_canceled_lease(unsigned worker_id, node_lease const &lease, bool& cancel_signaled) { std::scoped_lock lock(mux); - return m_state == state::is_running && m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch); + cancel_signaled = false; + if (m_state != state::is_running || !lease.leased_node || worker_id >= m_worker_leases.size()) + return false; + + auto& stored = m_worker_leases[worker_id]; + if (stored.leased_node != lease.leased_node) + return false; + + if (!m_search_tree.is_lease_canceled(stored.leased_node)) + return false; + + cancel_signaled = stored.cancel_signaled; + release_lease_unlocked(worker_id, stored.leased_node); + return true; } void parallel::batch_manager::collect_clause(ast_translation &l2g, unsigned source_worker_id, expr *clause) { @@ -1701,6 +1729,12 @@ namespace smt { cancel_background_threads(); } + // void parallel::batch_manager::notify_cv_waiters { + // std::scoped_lock lock(mux); + // m_bb_cv.notify_all(); + // m_core_min_cv.notify_all(); + // } + void parallel::batch_manager::set_exception(unsigned error_code) { std::scoped_lock lock(mux); IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n"); @@ -1763,7 +1797,6 @@ namespace smt { IF_VERBOSE(2, m_search_tree.display(verbose_stream()); verbose_stream() << "\n";); lease.leased_node = t; - lease.cancel_epoch = t->get_cancel_epoch(); if (id >= m_worker_leases.size()) m_worker_leases.resize(id + 1); m_worker_leases[id] = lease; @@ -1878,20 +1911,14 @@ namespace smt { auto safe_run = [&](auto* w) { try { w->run(); - if (w->limit().is_canceled()) - m_batch_manager.set_canceled(); } catch (z3_error& err) { if (!w->limit().is_canceled()) m_batch_manager.set_exception(err.error_code()); - else - m_batch_manager.set_canceled(); } catch (z3_exception& ex) { if (!w->limit().is_canceled() && !is_cancellation_exception(ex.what())) m_batch_manager.set_exception(ex.what()); - else - m_batch_manager.set_canceled(); } }; diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 79b326889..2e0632aed 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -64,12 +64,6 @@ namespace smt { struct node_lease { node* leased_node = nullptr; - // Cancellation generation counter for this node/subtree. - // Incremented when the node is closed; used to signal that all - // workers holding leases on this node (or its descendants) - // must abandon work immediately. - unsigned cancel_epoch = 0; - // Guards against multiple inc_cancel() calls for the same lease. // Set when cancel_lease() is signaled; cleared when a new lease is assigned. bool cancel_signaled = false; @@ -197,6 +191,7 @@ namespace smt { void set_exception(std::string const& msg); void set_exception(unsigned error_code); void set_canceled(); + void notify_cv_waiters(); void collect_statistics(::statistics& st) const; void collect_backbone_candidates(ast_translation& l2g, bb_candidates& bb_candidates); @@ -226,7 +221,7 @@ namespace smt { unsigned original_core_size, expr_ref_vector const& minimized_core); void try_split(ast_translation& l2g, unsigned worker_id, node_lease const& lease, expr* atom, unsigned effort); void release_lease(unsigned worker_id, node_lease const& lease); - bool lease_canceled(node_lease const& lease); + bool release_canceled_lease(unsigned worker_id, node_lease const& lease, bool& cancel_signaled); 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); diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ec27f176f..601f8f476 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -127,12 +127,6 @@ class parallel_solver { struct node_lease { search_tree::node* leased_node = nullptr; - // Cancellation generation counter for this node/subtree. - // Incremented when the node is closed; used to signal that all - // workers holding leases on this node (or its descendants) - // must abandon work immediately. - unsigned cancel_epoch = 0; - // Guards against multiple inc_cancel() calls for the same lease. // Set when cancel_lease() is signaled; cleared when a new lease is assigned. bool cancel_signaled = false; @@ -218,7 +212,7 @@ class parallel_solver { expr_ref_vector m_unsat_core; // called from batch manager to cancel other workers if we've reached a verdict - void cancel_workers_unlocked() { + void cancel_background_threads() { IF_VERBOSE(1, verbose_stream() << "Canceling workers\n"); for (auto* w : p.m_workers) w->cancel(); @@ -248,7 +242,7 @@ class parallel_solver { if (id == source_worker_id) continue; auto const& lease = m_worker_leases[id]; if (lease.leased_node && !lease.cancel_signaled && - m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch)) { + m_search_tree.is_lease_canceled(lease.leased_node)) { p.m_workers[id]->cancel_lease(); m_worker_leases[id].cancel_signaled = true; } @@ -316,7 +310,7 @@ class parallel_solver { for (auto* t : matches) { if (!t || t == source) continue; - if (m_search_tree.is_lease_canceled(t, t->get_cancel_epoch())) + if (m_search_tree.is_lease_canceled(t)) continue; // When source is provided, keep only external matches. Nodes in the @@ -343,7 +337,7 @@ class parallel_solver { if (!is_highest_ancestor) continue; - targets.push_back({ t, t->get_cancel_epoch() }); + targets.push_back({ t }); } } @@ -405,7 +399,7 @@ class parallel_solver { SASSERT(lease != nullptr || targets != nullptr); bool did_backtrack = false; - if (lease && !m_search_tree.is_lease_canceled(lease->leased_node, lease->cancel_epoch)) { + if (lease && !m_search_tree.is_lease_canceled(lease->leased_node)) { // we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled // i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack did_backtrack = true; @@ -414,7 +408,7 @@ class parallel_solver { } if (targets) { for (auto const& target : *targets) { - if (m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch)) + if (m_search_tree.is_lease_canceled(target.leased_node)) continue; did_backtrack = true; m_search_tree.backtrack(target.leased_node, g_core); @@ -438,7 +432,7 @@ class parallel_solver { SASSERT(m_unsat_core.empty()); for (auto& e : m_search_tree.get_core_from_root()) m_unsat_core.push_back(e.get()); - cancel_workers_unlocked(); + cancel_background_threads(); } } @@ -477,16 +471,23 @@ class parallel_solver { if (m_state != state::is_running) return; m_state = state::is_sat; m_model = mdl.translate(l2g); - cancel_workers_unlocked(); + cancel_background_threads(); } - void set_cancel() { + void set_canceled() { std::scoped_lock lock(mux); if (m_state != state::is_running) return; - cancel_workers_unlocked(); + cancel_background_threads(); } + // CODE IS LOCKED WHEN WE ADD THIS FUNCTION -- NEED TO FIX + // void notify_cv_waiters() { + // std::scoped_lock lock(mux); + // m_bb_cv.notify_all(); + // m_core_min_cv.notify_all(); + // } + void set_unsat(ast_translation& l2g, expr_ref_vector const& core) { std::scoped_lock lock(mux); @@ -496,7 +497,7 @@ class parallel_solver { SASSERT(m_unsat_core.empty()); for (expr* c : core) m_unsat_core.push_back(l2g(c)); - cancel_workers_unlocked(); + cancel_background_threads(); } void set_exception(std::string const& msg) { @@ -505,7 +506,7 @@ class parallel_solver { if (m_state != state::is_running) return; m_state = state::is_exception_msg; m_exception_msg = msg; - cancel_workers_unlocked(); + cancel_background_threads(); } void set_exception(unsigned error_code) { @@ -514,7 +515,7 @@ class parallel_solver { if (m_state != state::is_running) return; m_state = state::is_exception_code; m_exception_code = error_code; - cancel_workers_unlocked(); + cancel_background_threads(); } bool get_cube(ast_translation& g2l, unsigned id, @@ -531,7 +532,6 @@ class parallel_solver { if (!t) return false; lease.leased_node = t; - lease.cancel_epoch = t->get_cancel_epoch(); if (id >= m_worker_leases.size()) m_worker_leases.resize(id + 1); m_worker_leases[id] = lease; @@ -638,7 +638,7 @@ class parallel_solver { m_unsat_core.push_back(l2g(e)); ++m_stats.m_core_min_jobs_published; ++m_stats.m_core_min_global_unsat; - cancel_workers_unlocked(); + cancel_background_threads(); return; } @@ -651,7 +651,7 @@ class parallel_solver { if (!g_core.empty()) { collect_matching_targets_unlocked(source, g_core[0].get(), g_core, targets); for (auto const& target : targets) { - if (!m_search_tree.is_lease_canceled(target.leased_node, target.cancel_epoch)) + if (!m_search_tree.is_lease_canceled(target.leased_node)) m_search_tree.backtrack(target.leased_node, g_core); } } @@ -672,7 +672,7 @@ class parallel_solver { SASSERT(m_unsat_core.empty()); for (auto& e : m_search_tree.get_core_from_root()) m_unsat_core.push_back(e.get()); - cancel_workers_unlocked(); + cancel_background_threads(); } } @@ -682,7 +682,7 @@ class parallel_solver { return false; if (m_state != state::is_running) return false; - if (m_search_tree.is_lease_canceled(lease.leased_node, lease.cancel_epoch)) + if (m_search_tree.is_lease_canceled(lease.leased_node)) return false; expr_ref _atom(l2g(atom), m); @@ -694,8 +694,7 @@ class parallel_solver { expr* atom, unsigned effort) { std::scoped_lock lock(mux); if (m_state != state::is_running) return; - if (m_search_tree.is_lease_canceled( - lease.leased_node, lease.cancel_epoch)) return; + if (m_search_tree.is_lease_canceled(lease.leased_node)) return; expr_ref lit(m), nlit(m); lit = l2g(atom); @@ -704,8 +703,7 @@ class parallel_solver { VERIFY(!lease.leased_node->path_contains_atom(nlit)); bool did_split = m_search_tree.try_split( - lease.leased_node, lease.cancel_epoch, - lit, nlit, effort); + lease.leased_node, lit, nlit, effort); release_lease_unlocked(worker_id, lease.leased_node); @@ -723,11 +721,22 @@ class parallel_solver { release_lease_unlocked(worker_id, lease.leased_node); } - bool lease_canceled(node_lease const& lease) { + bool release_canceled_lease(unsigned worker_id, node_lease const& lease, bool& cancel_signaled) { std::scoped_lock lock(mux); - return m_state == state::is_running && - m_search_tree.is_lease_canceled( - lease.leased_node, lease.cancel_epoch); + cancel_signaled = false; + if (m_state != state::is_running || !lease.leased_node || worker_id >= m_worker_leases.size()) + return false; + + auto& stored = m_worker_leases[worker_id]; + if (stored.leased_node != lease.leased_node) + return false; + + if (!m_search_tree.is_lease_canceled(stored.leased_node)) + return false; + + cancel_signaled = stored.cancel_signaled; + release_lease_unlocked(worker_id, stored.leased_node); + return true; } void collect_clause(ast_translation& l2g, @@ -1174,17 +1183,20 @@ class parallel_solver { } lbool r = check_cube(cube); - if (b.lease_canceled(lease)) { + bool cancel_signaled = false; + if (b.release_canceled_lease(id, lease, cancel_signaled)) { LOG_WORKER(1, " abandoning canceled lease\n"); lease = {}; - m.limit().dec_cancel(); + if (cancel_signaled) + m.limit().dec_cancel(); continue; } // NSB - at this point it shouldn't be possible to call inc_cancel. // Is this ensured? I am not sure. if (!m.inc()) { - b.set_cancel(); + b.set_canceled(); + // b.notify_cv_waiters(); return; } @@ -1502,7 +1514,8 @@ class parallel_solver { while (true) { if (!m.inc()) { - b.set_cancel(); + b.set_canceled(); + // b.notify_cv_waiters(); return; } if (canceled()) @@ -1630,8 +1643,6 @@ class parallel_solver { curr_batch.reset(); } - if (!m.inc()) - b.set_cancel(); } public: @@ -1831,8 +1842,8 @@ class parallel_solver { if (minimized.size() < original_size) b.publish_minimized_core(m_l2g, asms, source, original_size, minimized); } - if (!m.inc()) - b.set_cancel(); + b.set_canceled(); + // b.notify_cv_waiters(); } void cancel() { @@ -1892,8 +1903,6 @@ public: static_cast(std::thread::hardware_concurrency()), pp.threads_max()); bool core_minimize = pp.core_minimize(); - if (pp.ablate_backtracking()) - core_minimize = false; unsigned num_bb_threads = pp.num_bb_threads(); if (num_bb_threads > 2) throw default_exception("parallel.num_bb_threads must be 0, 1, or 2"); @@ -1941,39 +1950,14 @@ public: m_batch_manager.initialize(num_bb_threads); - auto safe_run = [&](std::function run_fn, reslimit& lim) { - try { - run_fn(); - if (lim.is_canceled()) - m_batch_manager.set_cancel(); - } catch (z3_error &err) { - IF_VERBOSE(0, verbose_stream() << "Exception in parallel solver: " << err.what() << "\n"); - if (!lim.is_canceled()) - m_batch_manager.set_exception(err.error_code()); - else - m_batch_manager.set_cancel(); - } catch (z3_exception &ex) { - IF_VERBOSE(0, verbose_stream() << "Exception in parallel solver: " << ex.what() << "\n"); - if (!lim.is_canceled() && !is_cancellation_exception(ex.what())) - m_batch_manager.set_exception(ex.what()); - else - m_batch_manager.set_cancel(); - } - }; /* Launch threads. */ vector threads; for (auto *w : m_workers) - threads.push_back(std::thread([w, &safe_run]() { - safe_run([w]() { w->run(); }, w->limit()); - })); + threads.push_back(std::thread([w]() { w->run(); })); if (m_core_minimizer_worker) - threads.push_back(std::thread([this, &safe_run]() { - safe_run([this]() { m_core_minimizer_worker->run(); }, m_core_minimizer_worker->limit()); - })); + threads.push_back(std::thread([this]() { m_core_minimizer_worker->run(); })); for (auto* w : m_global_backbones_workers) - threads.push_back(std::thread([w, &safe_run]() { - safe_run([w]() { w->run(); }, w->limit()); - })); + threads.push_back(std::thread([w]() { w->run(); })); for (auto& t : threads) t.join(); diff --git a/src/util/search_tree.h b/src/util/search_tree.h index 701c2fe8d..9b9f15064 100644 --- a/src/util/search_tree.h +++ b/src/util/search_tree.h @@ -50,7 +50,6 @@ namespace search_tree { unsigned m_effort_spent = 0; unsigned m_round_max_effort = 0; unsigned m_active_workers = 0; - unsigned m_cancel_epoch = 0; public: node(literal const &l, node *parent) : m_literal(l), m_parent(parent), m_status(status::open) {} @@ -156,12 +155,6 @@ namespace search_tree { m_round_max_effort = effort; m_effort_spent += m_round_max_effort; } - unsigned get_cancel_epoch() const { - return m_cancel_epoch; - } - void inc_cancel_epoch() { - ++m_cancel_epoch; - } }; template class tree { @@ -348,7 +341,6 @@ namespace search_tree { void close(node *n, vector const &C) { if (!n || n->get_status() == status::closed) return; - n->inc_cancel_epoch(); n->set_status(status::closed); n->set_core(C); close(n->left(), C); @@ -452,8 +444,8 @@ namespace search_tree { // On timeout, either expand the current leaf or reopen the node for a // later revisit, depending on the tree-expansion heuristic. - bool try_split(node *n, unsigned cancel_epoch, literal const &a, literal const &b, unsigned effort) { - if (is_lease_canceled(n, cancel_epoch)) + bool try_split(node *n, literal const &a, literal const &b, unsigned effort) { + if (is_lease_canceled(n)) return false; // Record at most one effort contribution per concurrent round on this node. @@ -552,8 +544,8 @@ namespace search_tree { n->dec_active_workers(); } - bool is_lease_canceled(node* n, unsigned cancel_epoch) const { - return !n || n->get_status() == status::closed || n->get_cancel_epoch() != cancel_epoch; + bool is_lease_canceled(node* n) const { + return !n || n->get_status() == status::closed; } vector const &get_core_from_root() const {