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 c0cf4adc37a108a01b46ba6e262babf5b2d38aaf..b73a59e67a65111a6e8e2a3f4da246e373cdc00e 100644 (file)
--- 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;
            }
        }
     }