From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sun, 17 Jun 2012 22:33:31 +0000 (+0000)
Subject: fixing a problem due to lemmas produced while backtracking
X-Git-Tag: cvc5-1.0.0~7982
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ac3a5f6bcab217186afb8a8143d342209fc273c;p=cvc5.git

fixing a problem due to lemmas produced while backtracking
---

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index dcf60e8f1..4c5743c7c 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1526,7 +1526,7 @@ bool Solver::flipDecision() {
 
 CRef Solver::updateLemmas() {
 
-  Debug("minisat::lemmas") << "Solver::updateLemmas()" << std::endl;
+  Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
   CRef conflict = CRef_Undef;
 
@@ -1537,36 +1537,40 @@ CRef Solver::updateLemmas() {
   lemma_lt lt(*this);
 
   // Check for propagation and level to backtrack to
-  for (int i = 0; i < lemmas.size(); ++ i)
-  {
-    // The current lemma
-    vec<Lit>& lemma = lemmas[i];
-    // If it's an empty lemma, we have a conflict at zero level
-    if (lemma.size() == 0) {
-      conflict = CRef_Lazy;
-      backtrackLevel = 0;
-      Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
-      continue;
-    }
-    // Sort the lemma to be able to attach
-    sort(lemma, lt);
-    // See if the lemma propagates something
-    if (lemma.size() == 1 || value(lemma[1]) == l_False) {
-      Debug("minisat::lemmas") << "found unit " << lemma.size() << std::endl;
-      // This lemma propagates, see which level we need to backtrack to
-      int currentBacktrackLevel = lemma.size() == 1 ? 0 : level(var(lemma[1]));
-      // Even if the first literal is true, we should propagate it at this level (unless it's set at a lower level)
-      if (value(lemma[0]) != l_True || level(var(lemma[0])) > currentBacktrackLevel) {
-        if (currentBacktrackLevel < backtrackLevel) {
-          backtrackLevel = currentBacktrackLevel;
+  int i = 0;
+  while (i < lemmas.size()) {
+    // We need this loop as when we backtrack, due to registration more lemmas could be added
+    for (; i < lemmas.size(); ++ i)
+    {
+      // The current lemma
+      vec<Lit>& lemma = lemmas[i];
+      // If it's an empty lemma, we have a conflict at zero level
+      if (lemma.size() == 0) {
+        conflict = CRef_Lazy;
+        backtrackLevel = 0;
+        Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
+        continue;
+      }
+      // Sort the lemma to be able to attach
+      sort(lemma, lt);
+      // See if the lemma propagates something
+      if (lemma.size() == 1 || value(lemma[1]) == l_False) {
+        Debug("minisat::lemmas") << "found unit " << lemma.size() << std::endl;
+        // This lemma propagates, see which level we need to backtrack to
+        int currentBacktrackLevel = lemma.size() == 1 ? 0 : level(var(lemma[1]));
+        // Even if the first literal is true, we should propagate it at this level (unless it's set at a lower level)
+        if (value(lemma[0]) != l_True || level(var(lemma[0])) > currentBacktrackLevel) {
+          if (currentBacktrackLevel < backtrackLevel) {
+            backtrackLevel = currentBacktrackLevel;
+          }
         }
       }
     }
-  }
 
-  // Pop so that propagation would be current
-  Debug("minisat::lemmas") << "Solver::updateLemmas(): backtracking to " << backtrackLevel << " from " << decisionLevel() << std::endl;
-  cancelUntil(backtrackLevel);
+    // Pop so that propagation would be current
+    Debug("minisat::lemmas") << "Solver::updateLemmas(): backtracking to " << backtrackLevel << " from " << decisionLevel() << std::endl;
+    cancelUntil(backtrackLevel);
+  }
 
   // Last index in the trail
   int backtrack_index = trail.size();
@@ -1624,5 +1628,7 @@ CRef Solver::updateLemmas() {
     theoryConflict = true;
   }
 
+  Debug("minisat::lemmas") << "Solver::updateLemmas() end" << std::endl;
+
   return conflict;
 }