[pavelzw]

Summary

Unsat reports for a conflict involving a package with many versions ran to hundreds of lines, and the lines that did the explaining did not say which versions were at odds. This makes the conflict report readable.

• simplify no longer refuses to merge candidates that share a "forbid multiple instances" edge, so a package's versions collapse into one line (node 1 | 2 | 3 | ... | 8).
• Candidates are expanded once per branch that requires them instead of being silently skipped after the first, so every branch can be read on its own; a cycle guard and a cap on repeats keep that bounded (see unsat_repeated_subtrees_are_cut_off).
• "forbid multiple instances" messages are emitted on both sides of the conflict, skip candidates that are installable, and name the conflicting requirements that hold on the same path rather than every version of the package in the report.
• Every requirement line that a conflict message points at gets an (A)-style label, listed in the order the report prints them, so the reader can find the line a message refers to. Line paths are keyed on one node per merge group, since only one member of a group is printed.

Example

Before (unsat_pubgrub_article):

└─ menu * cannot be installed because there are no viable options:
   ├─ menu 15 would require
   │  └─ dropdown >=2, <3, which cannot be installed because there are no viable options:
   │     └─ dropdown 2 would require
   │        └─ icons >=2, <3, which cannot be installed because there are no viable options:
   │           └─ icons 2, which conflicts with the versions reported above.

After:

├─ (A) icons >=1, <2 can be installed with any of the following options:
│  └─ icons 1
...
└─ menu * cannot be installed because there are no viable options:
   ├─ menu 15 would require
   │  └─ dropdown >=2, <3, which cannot be installed because there are no viable options:
   │     └─ dropdown 2 would require
   │        └─ icons >=2, <3, which cannot be installed because there are no viable options:
   │           └─ icons 2, which conflicts with icons >=1, <2 (A)

Many conflicting versions now collapse and name the requirement they conflict with (unsat_many_conflicting_versions_name_the_requirement):

   ├─ app 3 would require
   │  ├─ helper *, which cannot be installed because there are no viable options:
   │  │  └─ helper 1 would require
   │  │     └─ (A) node >=1, <9, which cannot be installed because there are no viable options:
   │  │        └─ node 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8, which conflicts with node >=12, <13 (B)
   │  └─ (B) node >=12, <13, which cannot be installed because there are no viable options:
   │     └─ node 12, which conflicts with node >=1, <9 (A)

Context

conda/rattler#2870 currently pins this branch via [patch.crates-io] to produce the new reports; that patch is dropped once this lands and is released.

Test plan

• Existing conflict snapshots updated; new snapshots cover the collapsed candidate list, per-branch expansion with the repeat cap, and requirement labelling.
• Rebase on main (branch is currently 11 commits behind).

[richinsley]

Thanks for this PR. While porting resolvo to Go (goomba) and fuzzing it differentially against resolvo, we hit the unbounded explanation rendering that this PR fixes, and we wrote two regression tests for it. They may be useful to include here.

On main (f8a5147, v0.12.2):

• Cyclic conflict graph: in the first test, a requires b, b requires a and c, and c forbids a. display_user_friendly(..).to_string() never terminates and allocates until the process aborts. With the address space capped at 3 GB, it ends after about 3 s with memory allocation of 64928 bytes failed. The cause is that fmt_graph only records candidates of merged groups in reported, so other candidates are expanded again every time they are reached.
• Layered acyclic graph: each layer has x{i} and y{i}, each requiring x{i+1} | y{i+1}. For 2..=12 layers the explanation is exactly 2^(n+2) - 3 lines: [13, 29, 61, 125, 253, 509, 1021, 2045, 4093, 8189, 16381].

On this PR's head (9c793e5) both tests pass. The cyclic case terminates, and the layered case is linear: [13, 29, 53, 77, 101, 125, 149, 173, 197, 221, 245], 24 lines per layer.

Both tests render through a fmt::Write sink capped at a fixed size, so a regression fails fast instead of exhausting memory. They use the existing BundleBoxProvider helpers in tests/solver:

Regression tests

/// A `fmt::Write` sink that refuses to grow beyond `limit` bytes, so a
/// runaway explanation fails fast instead of exhausting memory.
struct BoundedWriter {
    buf: String,
    limit: usize,
}

impl std::fmt::Write for BoundedWriter {
    fn write_str(&mut self, s: &str) -> std::fmt::Result {
        if self.buf.len() + s.len() > self.limit {
            return Err(std::fmt::Error);
        }
        self.buf.push_str(s);
        Ok(())
    }
}

/// Solves an unsat problem and renders the explanation into a writer capped
/// at `limit` bytes. `Err` holds what was written before the cap was hit.
fn render_unsat_bounded(
    mut provider: BundleBoxProvider,
    specs: &[&str],
    limit: usize,
) -> Result<String, String> {
    use std::fmt::Write as _;
    let requirements = provider.requirements(specs);
    let mut solver = Solver::new(provider);
    let problem = Problem::new().requirements(requirements);
    let Err(UnsolvableOrCancelled::Unsolvable(conflict)) = solver.solve(problem) else {
        panic!("expected the problem to be unsolvable");
    };
    let mut out = BoundedWriter {
        buf: String::new(),
        limit,
    };
    match write!(out, "{}", conflict.display_user_friendly(&solver)) {
        Ok(()) => Ok(out.buf),
        Err(_) => Err(out.buf),
    }
}

/// `a` requires `b`, `b` requires `a` and `c`, and `c` forbids `a`, so the
/// conflict graph contains the cycle a -> b -> a. Rendering the explanation
/// never terminates.
#[test]
fn test_explanation_of_cyclic_conflict_graph_terminates() {
    let mut provider = BundleBoxProvider::new();
    provider.add_package("a", 2.into(), &["b"], &[]);
    provider.add_package("b", 4.into(), &["c", "a"], &[]);
    provider.add_package("c", 4.into(), &[], &["a 0..1"]);

    if let Err(prefix) = render_unsat_bounded(provider, &["a | b"], 1 << 20) {
        let head = prefix.lines().take(14).collect::<Vec<_>>().join("\n");
        panic!("the explanation exceeded 1 MiB; it starts with:\n{head}");
    }
}

/// Layers of packages `x{i}` and `y{i}`, each requiring `x{i+1} | y{i+1}`;
/// the last layer requires a package that does not exist. Every candidate is
/// expanded again each time the tree reaches it, so the explanation doubles
/// with every layer.
#[test]
fn test_explanation_of_layered_conflict_graph_is_not_exponential() {
    let explanation_lines = |layers: usize| {
        let mut provider = BundleBoxProvider::new();
        for i in 0..layers {
            let dep = if i + 1 == layers {
                "missing".to_string()
            } else {
                format!("x{} | y{}", i + 1, i + 1)
            };
            provider.add_package(&format!("x{i}"), 1.into(), &[dep.as_str()], &[]);
            provider.add_package(&format!("y{i}"), 1.into(), &[dep.as_str()], &[]);
        }
        match render_unsat_bounded(provider, &["x0 | y0"], 1 << 26) {
            Ok(s) => s.lines().count(),
            Err(_) => usize::MAX,
        }
    };

    let lines: Vec<usize> = (2..=12).map(explanation_lines).collect();
    // 2 candidates and 4 requirement edges per layer: a bounded number of
    // lines per layer is expected.
    assert!(
        lines.iter().zip(2..).all(|(&n, layers)| n <= 40 * layers),
        "explanation lines for 2..=12 layers: {lines:?}"
    );
}

Separately, we filed #315, #316 and #317 for solver-side issues found by the same fuzzing.