From: Michael Schroeder <mls@suse.de>
Date: Thu, 1 Dec 2022 10:01:43 +0000 (+0100)
Subject: proof generation: Try not to end with a SOLVER_RULE_RPM_SAME_NAME rule
X-Git-Tag: 0.7.23~30
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=6da047059ab0298038234651b408b0c2a5b0a1c2;p=thirdparty%2Flibsolv.git

proof generation: Try not to end with a SOLVER_RULE_RPM_SAME_NAME rule

They usually get not shown to the user, so it is nicer to have
something else as unsolvable rule.

Also fix sorting and start with negative assertions.
---

diff --git a/src/problems.c b/src/problems.c
index b525e0f6..7c777e26 100644
--- a/src/problems.c
+++ b/src/problems.c
@@ -1495,6 +1495,15 @@ proofsort(const void *va, const void *vb, void *vd)
   return 0;
 }
 
+/* move a decison from position "from" to a smaller position "to" */
+static inline void
+move_decision(Queue *q, int to, int from)
+{
+  queue_insertn(q, to, 6, 0);
+  memmove(q->elements + to, q->elements + from + 6, 6 * sizeof(Id));
+  queue_deleten(q, from + 6, 6); 
+}
+
 void
 solver_get_proof(Solver *solv, Id id, int islearnt, Queue *q)
 {
@@ -1573,6 +1582,21 @@ solver_get_proof(Solver *solv, Id id, int islearnt, Queue *q)
     }
   queue_deleten(q, 0, cnt);
 
+  /* switch last two decisions if the unsolvable rule is of type SOLVER_RULE_RPM_SAME_NAME */
+  if (q->count >= 12 && q->elements[q->count - 6 + 2] == SOLVER_RULE_RPM_SAME_NAME && q->elements[q->count - 12] > 0)
+    {
+      Rule *r = solv->rules + q->elements[q->count - 6 + 1];
+      /* make sure that the rule is a binary conflict and it matches the installed element */
+      if (r->p < 0 && (r->d == 0 || r->d == -1) && r->w2 < 0
+	 && (q->elements[q->count - 12] == -r->p || q->elements[q->count - 12] -r->w2))
+	{
+	  /* looks good! swap decisions and fixup truelit entries */
+	  move_decision(q, q->count - 12, q->count - 6);
+	  q->elements[q->count - 12] = -q->elements[q->count - 6];
+	  q->elements[q->count - 6] = 0;
+	}
+    }
+
   /* put learnt rule premises in front */
   MAPZERO(&seen);
   i = 0;
@@ -1598,7 +1622,7 @@ solver_get_proof(Solver *solv, Id id, int islearnt, Queue *q)
    *   if a package is installed, move conflicts right after
    *   if a package is conflicted, move requires right after
    */
-  doing = 0;
+  doing = 1;
   while (i < q->count - 6)
     {
       doing ^= 1;
@@ -1615,13 +1639,8 @@ solver_get_proof(Solver *solv, Id id, int islearnt, Queue *q)
 	      break;
 	  if (p)
 	    continue;	/* not unit yet */
-	  if (k > j)
-	    {
-	      /* move from j to k */
-	      queue_insertn(q, k, 6, 0);
-	      memmove(q->elements + k, q->elements + j + 6, 6 * sizeof(Id));
-	      queue_deleten(q, j + 6, 6); 
-	    }
+	  if (j > k)
+	    move_decision(q, k, j);
 	  k += 6;
 	}
       if (k == i)