From: Dejan Jovanović Date: Tue, 15 Mar 2011 22:08:46 +0000 (+0000) Subject: real fix for bug 245, previous one was faulty X-Git-Tag: cvc5-1.0.0~8655 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4ee5a74967c9cd273ca3449b948ac8a12834991c;p=cvc5.git real fix for bug 245, previous one was faulty --- diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 3e4c9d8a2..6703a44be 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -312,7 +312,7 @@ bool Solver::satisfied(const Clause& c) const { // Revert to the state at given level (keeping all assignment at 'level' but not beyond). // -void Solver::cancelUntil(int level) { +void Solver::cancelUntil(int level, bool re_propagate) { if (decisionLevel() > level){ // Pop the SMT context for (int l = trail_lim.size() - level; l > 0; --l) @@ -327,31 +327,50 @@ void Solver::cancelUntil(int level) { trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); - // Propagate the lemma literals - int i, j; - for (i = j = propagating_lemmas_lim[level]; i < propagating_lemmas.size(); ++ i) { - Clause& lemma = ca[propagating_lemmas[i]]; - bool propagating = value(var(lemma[0])) == l_Undef;; - for(int lit = 1; lit < lemma.size() && propagating; ++ lit) { - if (value(var(lemma[lit])) != l_False) { - propagating = false; - break; - } - } - if (propagating) { - // Propagate - uncheckedEnqueue(lemma[0], propagating_lemmas[i]); - // Remember the lemma - propagating_lemmas[j++] = propagating_lemmas[i]; - } + // Re-Propagate the lemmas if asked + if (re_propagate) { + rePropagate(level); } - Assert(i >= j); - propagating_lemmas.shrink(propagating_lemmas.size() - j); - Assert(propagating_lemmas_lim.size() >= level); - propagating_lemmas_lim.shrink(propagating_lemmas_lim.size() - level); } } +CRef Solver::rePropagate(int level) { + // Propagate the lemma literals + int i, j; + for (i = j = propagating_lemmas_lim[level]; i < propagating_lemmas.size(); ++ i) { + Clause& lemma = ca[propagating_lemmas[i]]; + bool propagating = value(var(lemma[0])) == l_Undef;; + for(int lit = 1; lit < lemma.size() && propagating; ++ lit) { + if (value(var(lemma[lit])) != l_False) { + propagating = false; + break; + } + } + if (propagating) { + if (value(lemma[0]) != l_Undef) { + if (value(lemma[0]) == l_False) { + // Conflict + return propagating_lemmas[i]; + } else { + // Already there + continue; + } + } + // Propagate + uncheckedEnqueue(lemma[0], propagating_lemmas[i]); + // Remember the lemma + propagating_lemmas[j++] = propagating_lemmas[i]; + } + } + Assert(i >= j); + propagating_lemmas.shrink(propagating_lemmas.size() - j); + Assert(propagating_lemmas_lim.size() >= level); + propagating_lemmas_lim.shrink(propagating_lemmas_lim.size() - level); + + // No conflict + return CRef_Undef; +} + void Solver::popTrail() { // If we're not incremental, just pop until level 0 if (!enable_incremental) { @@ -938,28 +957,29 @@ lbool Solver::search(int nof_conflicts) lemma_propagated_reasons.clear(); // CONFLICT - int max_level = 0; - do { + while (confl != CRef_Undef) { conflicts++; conflictC++; if (decisionLevel() == 0) return l_False; - - 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); + // Analyze the conflict + learnt_clause.clear(); + int max_level = analyze(confl, learnt_clause, backtrack_level); + cancelUntil(backtrack_level, false); + + // Assert the conflict clause and the asserting literal + if (learnt_clause.size() == 1){ + uncheckedEnqueue(learnt_clause[0]); + }else{ + CRef cr = ca.alloc(max_level, learnt_clause, true); + learnts.push(cr); + attachClause(cr); + claBumpActivity(ca[cr]); + uncheckedEnqueue(learnt_clause[0], cr); + } - if (learnt_clause.size() == 1){ - uncheckedEnqueue(learnt_clause[0]); - }else{ - CRef cr = ca.alloc(max_level, learnt_clause, true); - learnts.push(cr); - attachClause(cr); - claBumpActivity(ca[cr]); - uncheckedEnqueue(learnt_clause[0], cr); - } + // We repropagate lemmas + confl = rePropagate(backtrack_level); + }; varDecayActivity(); claDecayActivity(); diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 5c0f0f9a3..1eb407c62 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -299,7 +299,8 @@ protected: CRef propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause. bool propagateTheory (); // Perform Theory propagation. Return true if any literals were asserted. CRef theoryCheck (CVC4::theory::Theory::Effort effort); // Perform a theory satisfiability check. Returns possibly conflicting clause. - void cancelUntil (int level); // Backtrack until a certain level. + void cancelUntil (int level, bool re_propagate = true); // Backtrack until a certain level. + CRef rePropagate (int level); // Re-propagate on lemmas, returns a concflict clause if it introduces a conflict void popTrail (); // Backtrack the trail to the previous push position int analyze (CRef confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?