From: Michael Schroeder <mls@suse.de>
Date: Tue, 9 Apr 2024 09:26:39 +0000 (+0200)
Subject: getdecisionlist: keep track of all literals from a unit rule
X-Git-Tag: 0.7.29~9
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=29ebc283f819dc4c24534fa50a62931e262a5c32;p=thirdparty%2Flibsolv.git

getdecisionlist: keep track of all literals from a unit rule

Otherwise, sort_unit_decisions() may not find a unit rule and
go into and endless loop. Before this commit, we left out
conflicted packages to make the decisionlist shorter.

An alternative would be to track those left out literals.

Fixes #558.
---

diff --git a/src/decision.c b/src/decision.c
index c0cf4adc..b73a59e6 100644
--- a/src/decision.c
+++ b/src/decision.c
@@ -487,7 +487,7 @@ solver_get_proof(Solver *solv, Id id, int flags, Queue *q)
       /* sort premise block */
       if (i > 8)
 	solv_sort(q->elements, i / 8, 8 * sizeof(Id), decisionsort_cmp, solv);
-      sort_unit_decisions(solv, q, i, q->count - 8, &seen);
+      sort_unit_decisions(solv, q, i, q->count - i, &seen);
     }
 
   map_free(&seen);
@@ -675,7 +675,7 @@ getdecisionlist(Solver *solv, Map *dm, int flags, Queue *decisionlistq)
 	      Id p2 = iq.elements[i];
 	      if (p2 < 0)
 		MAPSET(dm, -p2);
-	      else if (solv->decisionmap[p2] > 0)
+	      else if (reason == SOLVER_REASON_UNIT_RULE || solv->decisionmap[p2] > 0)
 		MAPSET(dm, p2);
 	    }
 	  break;
@@ -703,6 +703,7 @@ getdecisionlist(Solver *solv, Map *dm, int flags, Queue *decisionlistq)
 		if (decisionlistq->elements[j + 1] != SOLVER_REASON_UNIT_RULE)
 		  break;
 	      sort_unit_decisions(solv, decisionlistq, i, j, dm);
+	      i = j - 8;
 	    }
 	}
     }