Skip to content

Commit

Permalink
getdecisionlist: keep track of all literals from a unit rule
Browse files Browse the repository at this point in the history
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.
mlschroe committed Apr 9, 2024
1 parent 709092e commit 29ebc28
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions src/decision.c
Original file line number Diff line number Diff line change
@@ -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;
}
}
}

0 comments on commit 29ebc28

Please sign in to comment.