From 7ea6e9bed48e1e5fa2ed928def0bc03db830702f Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Thu, 14 May 2026 05:35:11 +0000 Subject: [PATCH] simplify parallel_tactical2: use std::min and consistent mk_not - Replace manual conflict cap with std::min in update_max_conflicts() - Use mk_not(m, c) instead of mk_not(expr_ref(c, m)) for consistency with the existing call pattern at line 349 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/solver/parallel_tactical2.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ebae4cb57..eb62069d0 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -471,11 +471,9 @@ class parallel_solver { unsigned m_shared_clause_limit = 0; void update_max_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; + m_config.m_threads_max_conflicts = std::min( + static_cast(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts), + m_config.m_max_conflicts); } /* Check the current cube (passed as additional assumptions). @@ -675,7 +673,7 @@ class parallel_solver { * 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))); + neg_lits.push_back(mk_not(m, c)); expr_ref clause(mk_or(neg_lits), m); b.collect_clause(m_l2g, id, clause.get()); }