Fix panic in add_pending_forbid_clauses during conflict detection

[dralley]

Forbid-multiple clauses (which enforce "at most one version of a package") are created lazily as solvables become reachable. When run_sat() decides a solvable true and then encodes its dependencies, add_pending_forbid_clauses may discover that another solvable for the same package name was already decided true — but the forbid clause between them didn't exist yet to prevent it.

The old code hit unreachable!() in this case. Handle it as a normal conflict instead, so the solver can backtrack and try alternatives.

This is triggered by soft_requirements: the hard solve installs version A, then run_sat for a soft requirement decides version B true. During encoding of B, the forbid clause between A and B is finally created, at which point both are already true.

Assisted-By: Claude Opus 4.6 noreply@anthropic.com

[dralley]

I am not certain about this one - it was mentioned here prefix-dev/resolvo-rpm#2 (comment) that

I think you can totally implement recommends, obsoletes and suggests, although I believe it's implemented as extra "loops" in libsolv where you first add all recommends, and then remove accordingly. For obsoletes, I think there is probably another trick (maybe add a next version of the old package that has a a dependency on the new package?).

So it would make sense that backtracking w/ soft requirements would be needed, but I'm not sure if this is a complete fix. IDK if something more needs to happen with soft requirements or maybe with how add_pending_forbid_clauses is called.

[dralley]

Here's the full description from claude which has a little bit more detail.

1. The hard solve installs version A of package P (decided true)
2. The soft requirements list includes a solvable for version B of package P (because collect_soft_dep_solvables finds ALL versions matching a recommended/suggested capability)
3. run_sat(B) decides B true at its starting level
4. During encoding of B's dependencies, add_pending_forbid_clauses tries to create the "at most one of {A, B}" clause — but both are already true

The key point is: B is decided true before the forbid clause exists to prevent it. The solver would normally backtrack, but the old code panicked instead of reporting the conflict.

It's possible my implementation of collect_soft_dep_solvables is also a bit too brute force, although obviously a panic! is still probably wrong.

[dralley]

Also, a question:

While I haven't gotten around to needing to deal with this part yet, I know that DNF can whitelist certain packages to have multiple versions installed in parallel - e.g. multiple different versions of the kernel package (for emergency boot into an older kernel)

I presume then that this codepath would need to be turned off in that case? Is there an equivalent to libsolv's SOLVER_MULTIVERSION? (I think that's what it's called, I did some work with libsolv in the past but it was years ago)

[baszalmstra]

Do you think you can add a regression test for this case?

The fix look good to me.

[baszalmstra]

I presume then that this codepath would need to be turned off in that case? Is there an equivalent to libsolv's SOLVER_MULTIVERSION? (I think that's what it's called, I did some work with libsolv in the past but it was years ago)

I wonder how this is implemented in libsolv. I can also imagine that you can implement this using a "virtual name" maybe? But I would have to dive into libsolv to see how this works. Would be a very interesting case to support!

[dralley]

@baszalmstra regression test added - I verified that it fails w/o the patch present.

[baszalmstra]

Perfect thanks!