From d7554865a91733a39dd658e2003ca072e8e2ed4b Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Tue, 15 Mar 2011 20:48:57 +0000 Subject: [PATCH] fix for bug 254, lemmas were propagating at lower levels, and the conflict clauses asserting literal would overwrite the propagated literal let's see if i break the build again --- src/prop/minisat/core/Solver.cc | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 80d6b116e..3e4c9d8a2 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -933,17 +933,23 @@ lbool Solver::search(int nof_conflicts) CRef confl = propagate(check_type); if (confl != CRef_Undef){ - // CONFLICT - conflicts++; conflictC++; - if (decisionLevel() == 0) return l_False; - - // Clear the propagated literals + // Clear the propagated literals lemma_propagated_literals.clear(); lemma_propagated_reasons.clear(); + + // CONFLICT + int max_level = 0; + do { + conflicts++; conflictC++; + if (decisionLevel() == 0) return l_False; - learnt_clause.clear(); - int max_level = analyze(confl, learnt_clause, backtrack_level); - cancelUntil(backtrack_level); + learnt_clause.clear(); + max_level = std::max(max_level, analyze(confl, learnt_clause, backtrack_level)); + cancelUntil(backtrack_level); + + // It might have happened that we have repropagated a literal that is actually learnt_clause[0] + // so we must go into conflict resolition again + } while (value(learnt_clause[0]) != l_Undef); if (learnt_clause.size() == 1){ uncheckedEnqueue(learnt_clause[0]); -- 2.30.2