mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

address code review: cap conflict growth, clarify cube/split comments, use mk_or for conflict clause

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/8b3749c7-5957-41aa-85b5-2d76d4780d61

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-13 00:01:08 +00:00 • committed by GitHub
parent 7313174b6a
commit 2894808dea
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/solver/parallel_tactical2.cpp
View file

@ -475,6 +475,9 @@ class parallel_solver {
void update_max_conflicts() {
m_config.m_threads_max_conflicts = static_cast<unsigned>(
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).
@ -562,6 +565,11 @@ class parallel_solver {
s->pop(1);
/* 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);
@ -665,7 +673,12 @@ class parallel_solver {
b.backtrack(m_l2g, id, cube_core, lease);
if (m_config.m_share_conflicts) {
expr_ref clause(mk_not(mk_and(cube_core)), m);
/* 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();