//! The minimal-unsat-core search: which named constructs / facts are jointly
//! responsible for an unsatisfiable system, via SAT under assumptions.
use crate::cnf::{build_cnf, clause_lit, fact_lit, rule_consequent_clause};
use crate::report::{
    CoreItem, Fix, FixKind, Hence, ProveOutcome, Proved, Tried, TryOutcome, label,
};
use crate::sat;
use alloc::string::String;
use alloc::vec;
use alloc::vec::Vec;
use elenchus_compiler::{Compiled, Lit, Origin, StepRef, Value};

/// The minimal set of `ASSUME` hypotheses to retract so an
/// otherwise-consistent program stops contradicting itself.
///
/// Returns empty unless **all three** hold: there is at least one soft fact; the
/// hard program (facts + premises + rules, no assumptions) is satisfiable on its
/// own; and the full program (with assumptions) is unsatisfiable. In that case
/// the assumptions are the cause, and we deletion-minimize **over the soft facts
/// only** — every hard construct stays active, so a `FACT`/`PREMISE` can never be
/// blamed. What survives is an irreducible set of assumptions that cannot all
/// hold together; dropping any one restores consistency.
///
/// Reuses the same CNF / SAT machinery as [`minimal_unsat_core`]
/// ([`constructs`], [`subset_is_sat`]); the only difference is that hard
/// constructs are pinned active. Labels carry polarity (`NOT …`) so a small
/// model sees exactly what it assumed.
pub(crate) fn retract_assumptions(
    c: &Compiled,
    budget: Option<&sat::Budget>,
) -> Result<Vec<CoreItem>, sat::BudgetExhausted> {
    if !c.facts.iter().any(|f| f.soft) {
        return Ok(Vec::new());
    }
    let all = constructs(c);
    // The first `c.facts.len()` constructs mirror `c.facts` 1:1 (see `constructs`).
    let is_soft: Vec<bool> = (0..all.len())
        .map(|i| i < c.facts.len() && c.facts[i].soft)
        .collect();

    // One shared incremental solver answers every satisfiability question below.
    // All of them are verdict-only, so heuristics are on from the start.
    let mut cs = ConstructSolver::new(c.atoms.len(), &all, budget);
    cs.enable_turbo();

    // The hard program (drop every soft construct) must be consistent on its own,
    // else the facts/premises are to blame and we must not point at assumptions.
    let hard_only: Vec<bool> = is_soft.iter().map(|&s| !s).collect();
    if !cs.subset_is_sat(&hard_only)? {
        return Ok(Vec::new());
    }
    // The full program must actually be UNSAT for there to be anything to drop.
    let mut active = vec![true; all.len()];
    if cs.subset_is_sat(&active)? {
        return Ok(Vec::new());
    }
    // Deletion-minimize over the soft constructs only; hard ones stay pinned.
    for i in 0..all.len() {
        if active[i] && is_soft[i] {
            active[i] = false;
            if cs.subset_is_sat(&active)? {
                active[i] = true; // still needed for the contradiction
            }
        }
    }
    let mut core: Vec<CoreItem> = Vec::new();
    for i in (0..all.len()).filter(|&i| active[i] && is_soft[i]) {
        let f = &c.facts[i];
        // Show the assumed polarity so `ASSUME NOT x` reads as `NOT x`.
        let label = if matches!(f.value, Value::False) {
            alloc::format!("NOT {}", label(c, f.atom))
        } else {
            label(c, f.atom)
        };
        let fixes = fixes_for(c, &mut cs, &all, &active, i, &label)?;
        core.push(CoreItem {
            origin: f.origin.clone(),
            label,
            fixes,
        });
    }
    core.sort_by_key(|it| key(&it.origin));
    Ok(core)
}

// --- near-duplicate atom detection (advisory typo hints) -------------------

/// A removable source construct (one fact, one premise, or one rule) and the CNF
/// clauses it contributes — the unit of an unsat-core explanation.
pub(crate) struct Construct {
    origin: Origin,
    label: String,
    clauses: Vec<Vec<sat::SatLit>>,
}

/// Two origins refer to the same source construct.
pub(crate) fn same_origin(a: &Origin, b: &Origin) -> bool {
    a.source == b.source && a.line == b.line && a.premise == b.premise && a.kind == b.kind
}

/// Split the program into removable constructs. A premise that desugared into
/// several clauses (e.g. an `EXCLUSIVE` over n atoms) is grouped back into one
/// construct by origin, so the core blames whole premises, not clause shards.
pub(crate) fn constructs(c: &Compiled) -> Vec<Construct> {
    let mut out: Vec<Construct> = Vec::new();

    for f in &c.facts {
        out.push(Construct {
            origin: f.origin.clone(),
            label: label(c, f.atom),
            clauses: vec![vec![fact_lit(f)]],
        });
    }

    let mut premises: Vec<Construct> = Vec::new();
    for clause in &c.clauses {
        let lits: Vec<sat::SatLit> = clause.lits.iter().map(clause_lit).collect();
        match premises
            .iter_mut()
            .find(|k| same_origin(&k.origin, &clause.origin))
        {
            Some(k) => k.clauses.push(lits),
            None => premises.push(Construct {
                label: clause.origin.premise.clone().unwrap_or_default(),
                origin: clause.origin.clone(),
                clauses: vec![lits],
            }),
        }
    }
    out.extend(premises);

    for r in &c.rules {
        let clauses = r
            .consequent
            .iter()
            .map(|cons| rule_consequent_clause(r, cons))
            .collect();
        out.push(Construct {
            label: r.origin.premise.clone().unwrap_or_default(),
            origin: r.origin.clone(),
            clauses,
        });
    }
    out
}

/// A persistent selector-guarded solver over the program's constructs — the shared
/// engine of every minimization loop. Construct `k`'s clauses are loaded once as
/// `(¬s_k ∨ clause)`; a query *assumes* `s_k` for each active construct. A selector
/// that is not assumed is free, and since selectors occur only negatively, a free
/// selector lets the solver switch that construct off — so each query is
/// equisatisfiable with the formula containing exactly the active constructs.
///
/// Incremental on purpose: a deletion-minimization loop asks O(n) closely related
/// SAT/UNSAT questions over one formula; sharing the clause database lets learned
/// clauses answer later queries instead of being re-derived from scratch each time.
/// Only *verdicts* are consumed by the loops (semantically unique, so the reported
/// cores/fixes are byte-identical to the scratch-per-query implementation this
/// replaces); the one query whose *contents* feed the report — the initial core
/// candidate — is the solver's first, which on a fresh database is the exact same
/// computation as a standalone `solve_assuming`.
pub(crate) struct ConstructSolver {
    inc: sat::Incremental,
    /// Selector variables start here (== the program's atom count).
    base: usize,
}

impl ConstructSolver {
    /// Load every construct's clauses, guarded by one selector each. `budget`
    /// (a clone of the run-wide pool, if any) caps the total conflicts every
    /// query on this solver may analyze.
    pub(crate) fn new(num_vars: usize, all: &[Construct], budget: Option<&sat::Budget>) -> Self {
        let mut cnf = sat::Cnf::new(num_vars + all.len());
        for (i, k) in all.iter().enumerate() {
            let s_neg = sat::SatLit::negative((num_vars + i) as sat::Var);
            for cl in &k.clauses {
                let mut lits = Vec::with_capacity(cl.len() + 1);
                lits.push(s_neg);
                lits.extend_from_slice(cl);
                cnf.add_clause(lits);
            }
        }
        let mut inc = sat::Incremental::new(&cnf);
        inc.set_budget(budget.cloned());
        ConstructSolver {
            inc,
            base: num_vars,
        }
    }

    /// The selector literal enabling construct `i`.
    fn selector(&self, i: usize) -> sat::SatLit {
        sat::SatLit::positive((self.base + i) as sat::Var)
    }

    /// Turn search heuristics on for the queries that follow. Sound only once no
    /// remaining query's *contents* reach the report — i.e. after the core
    /// candidate (whose literals do) has been solved on the reference profile;
    /// the deletion/flip queries consume bare SAT/UNSAT verdicts, which
    /// heuristics cannot change.
    fn enable_turbo(&mut self) {
        self.inc.set_config(sat::SolverConfig::TURBO);
    }

    /// Is the program satisfiable using only the constructs marked active?
    pub(crate) fn subset_is_sat(&mut self, active: &[bool]) -> Result<bool, sat::BudgetExhausted> {
        let asm: Vec<sat::SatLit> = active
            .iter()
            .enumerate()
            .filter(|&(_, &a)| a)
            .map(|(i, _)| self.selector(i))
            .collect();
        Ok(matches!(self.inc.solve(&asm)?, sat::Solved::Sat(_)))
    }

    /// Like [`ConstructSolver::subset_is_sat`], but construct `i` is replaced by
    /// asserting the single literal `flipped` (its selector stays free = off).
    fn flip_is_sat(
        &mut self,
        active: &[bool],
        i: usize,
        flipped: sat::SatLit,
    ) -> Result<bool, sat::BudgetExhausted> {
        let mut asm: Vec<sat::SatLit> = active
            .iter()
            .enumerate()
            .filter(|&(k, &a)| a && k != i)
            .map(|(k, _)| self.selector(k))
            .collect();
        asm.push(flipped);
        Ok(matches!(self.inc.solve(&asm)?, sat::Solved::Sat(_)))
    }
}

/// Would *flipping* construct `i` (a single-unit `FACT`/`ASSUME`) — keeping every
/// currently-active construct as-is, but asserting the opposite value for `i` —
/// restore satisfiability? Only unit constructs can be flipped; a premise/rule has
/// no single polarity to reverse, so this returns `false` for them (their only fix
/// is `Drop`). Tested against the same `active` mask the drop-minimization used, so
/// the flip advice shares the drop advice's frame of reference.
pub(crate) fn flip_restores_sat(
    cs: &mut ConstructSolver,
    all: &[Construct],
    active: &[bool],
    i: usize,
) -> Result<bool, sat::BudgetExhausted> {
    // A flippable construct is exactly one unit clause holding one literal.
    if all[i].clauses.len() != 1 || all[i].clauses[0].len() != 1 {
        return Ok(false);
    }
    cs.flip_is_sat(active, i, all[i].clauses[0][0].negate())
}

/// The engine-verified repairs for a retained construct `i`: always `Drop` (its
/// removal restores SAT — that is what put it in the minimal set), plus `Flip` **only
/// when** re-solving with the fact flipped is actually consistent. `Flip` is offered
/// only for a `FACT`/`ASSUME` (`i < c.facts.len()`, the 1:1 prefix in [`constructs`]);
/// its target is the literal the flip would assert (opposite of the fact's value).
pub(crate) fn fixes_for(
    c: &Compiled,
    cs: &mut ConstructSolver,
    all: &[Construct],
    active: &[bool],
    i: usize,
    drop_target: &str,
) -> Result<Vec<Fix>, sat::BudgetExhausted> {
    let mut fixes = vec![Fix {
        kind: FixKind::Drop,
        target: String::from(drop_target),
    }];
    if i < c.facts.len() && flip_restores_sat(cs, all, active, i)? {
        let f = &c.facts[i];
        // The flip asserts the opposite of the fact's current value.
        let target = if matches!(f.value, Value::True) {
            alloc::format!("NOT {}", label(c, f.atom))
        } else {
            label(c, f.atom)
        };
        fixes.push(Fix {
            kind: FixKind::Flip,
            target,
        });
    }
    Ok(fixes)
}

/// A fast sufficient core via one assumption-solve: solve asserting every selector
/// true; the SAT core (a subset of the selectors) names a sufficient set of
/// constructs in a single solve — versus O(n) deletion solves. Returns an `active`
/// mask over the constructs.
///
/// Must be the **first** query on `cs`: on a fresh clause database this is the
/// exact same computation as a standalone `solve_assuming` over the same CNF, so
/// the returned candidate — whose contents shape the reported core — is identical
/// to the pre-incremental implementation's.
pub(crate) fn candidate_via_assumptions(
    cs: &mut ConstructSolver,
    count: usize,
) -> Result<Vec<bool>, sat::BudgetExhausted> {
    let assumptions: Vec<sat::SatLit> = (0..count).map(|i| cs.selector(i)).collect();
    let base = cs.base;
    let mut active = vec![false; count];
    match cs.inc.solve(&assumptions)? {
        sat::Solved::Unsat(core) => {
            for lit in core {
                let v = lit.var() as usize;
                if v >= base {
                    active[v - base] = true;
                }
            }
        }
        // The caller only calls this when the system is UNSAT, so this is
        // unreachable; fall back to all-active so the deletion pass below is still
        // correct (just slower).
        sat::Solved::Sat(_) => active.iter_mut().for_each(|a| *a = true),
    }
    Ok(active)
}

/// A 1-minimal unsat core. First an assumption-solve narrows the program to a
/// sufficient candidate ([`candidate_via_assumptions`]); then deletion-based
/// minimization over *that candidate only* drops each construct in turn — if the
/// rest is still unsatisfiable it was not needed — leaving an irreducible set
/// jointly to blame. Called only when the full system is UNSAT.
pub(crate) fn minimal_unsat_core(
    c: &Compiled,
    budget: Option<&sat::Budget>,
) -> Result<Vec<CoreItem>, sat::BudgetExhausted> {
    let all = constructs(c);
    // One incremental solver serves the candidate solve, the deletion loop, and
    // the flip checks; the candidate must come first (see its docs).
    let mut cs = ConstructSolver::new(c.atoms.len(), &all, budget);
    let mut active = candidate_via_assumptions(&mut cs, all.len())?;
    // The content-bearing candidate query is done; everything after is verdict-only.
    cs.enable_turbo();
    for i in 0..all.len() {
        if active[i] {
            active[i] = false;
            if cs.subset_is_sat(&active)? {
                active[i] = true; // removing it restored SAT → it is part of the core
            }
        }
    }
    let mut core: Vec<CoreItem> = Vec::new();
    for (i, k) in all.iter().enumerate().filter(|&(i, _)| active[i]) {
        let fixes = fixes_for(c, &mut cs, &all, &active, i, &k.label)?;
        core.push(CoreItem {
            origin: k.origin.clone(),
            label: k.label.clone(),
            fixes,
        });
    }
    core.sort_by_key(|it| key(&it.origin));
    Ok(core)
}

/// Sort key giving conflicts/warnings a stable, source-then-line order.
pub(crate) fn key(o: &Origin) -> (String, u32) {
    (o.source.clone(), o.line)
}

/// The entailment (⊨) side-check: for each `PROVE <literal>` goal, ask
/// refutationally whether the theory entails it. `theory ∧ ¬goal` unsatisfiable →
/// [`ProveOutcome::Proved`]; `theory ∧ goal` unsatisfiable →
/// [`ProveOutcome::Refuted`]; both satisfiable → [`ProveOutcome::Open`] (the honest
/// three-valued answer); both unsatisfiable → [`ProveOutcome::Vacuous`] (the theory
/// itself is inconsistent, so it entails everything). Purely advisory — the goal is
/// never committed; cost is exactly two bounded solves per *written* goal, and the
/// engine never picks goals itself (Law 5).
pub(crate) fn prove_goals(
    c: &Compiled,
    budget: Option<&sat::Budget>,
) -> Result<Vec<Proved>, sat::BudgetExhausted> {
    if c.goals.is_empty() {
        return Ok(Vec::new());
    }
    let (cnf, _) = build_cnf(c);
    // Every query below is verdict-only (no model contents reach the report), so
    // the turbo profile is sound from the first solve. One incremental solver
    // answers both refutation questions for every goal.
    let mut inc = sat::Incremental::with_config(&cnf, sat::SolverConfig::TURBO);
    inc.set_budget(budget.cloned());
    let mut out = Vec::with_capacity(c.goals.len());
    for g in &c.goals {
        // The goal literal as written (positive unless `PROVE NOT …`).
        let lit = sat::SatLit::new(g.lit.atom, !g.lit.negated);
        let neg_unsat = matches!(inc.solve(&[lit.negate()])?, sat::Solved::Unsat(_));
        let pos_unsat = matches!(inc.solve(&[lit])?, sat::Solved::Unsat(_));
        let outcome = match (neg_unsat, pos_unsat) {
            (true, false) => ProveOutcome::Proved,
            (false, true) => ProveOutcome::Refuted,
            (false, false) => ProveOutcome::Open,
            (true, true) => ProveOutcome::Vacuous,
        };
        let name = label(c, g.lit.atom);
        let text = if g.lit.negated {
            alloc::format!("NOT {name}")
        } else {
            name
        };
        out.push(Proved {
            origin: g.origin.clone(),
            label: text,
            outcome,
        });
    }
    Ok(out)
}

/// A literal rendered with its surface polarity (`NOT …` when negated) — the
/// shared spelling for HENCE conclusions and references.
fn lit_label(c: &Compiled, l: &Lit) -> String {
    let name = label(c, l.atom);
    if l.negated {
        alloc::format!("NOT {name}")
    } else {
        name
    }
}

/// The checked-derivation (proof kernel) pass: verify each `HENCE <conclusion>
/// FROM <refs>` step separately — do the clauses of the *cited* references alone
/// entail the conclusion? One refutation solve per step over a CNF containing
/// exactly: every clause of each cited `PREMISE`/`RULE` (a defeasible rule keeps
/// its `UNLESS` escapes), one unit per cited fact, one unit per cited earlier
/// conclusion (each step is checked *locally* — a broken earlier step is visible
/// on its own line, and citing its conclusion does not silently re-break later
/// steps), plus the negated conclusion. UNSAT → the step holds; SAT → the gap is
/// here. Purely advisory — no step is committed, the main solve is untouched, and
/// cost is O(steps written) × one bounded solve (Law 5: the engine never completes
/// a proof or picks premises).
pub(crate) fn check_derivations(
    c: &Compiled,
    budget: Option<&sat::Budget>,
) -> Result<Vec<Hence>, sat::BudgetExhausted> {
    if c.derivations.is_empty() {
        return Ok(Vec::new());
    }
    let mut out: Vec<Hence> = Vec::with_capacity(c.derivations.len());
    for d in &c.derivations {
        let mut cnf = sat::Cnf::new(c.atoms.len());
        let mut from = Vec::with_capacity(d.refs.len());
        for r in &d.refs {
            match r {
                StepRef::Construct { source, name } => {
                    for cl in c.clauses.iter().filter(|cl| {
                        cl.origin.source == *source && cl.origin.premise.as_deref() == Some(name)
                    }) {
                        cnf.add_clause(cl.lits.iter().map(clause_lit).collect());
                    }
                    for rl in c.rules.iter().filter(|rl| {
                        rl.origin.source == *source && rl.origin.premise.as_deref() == Some(name)
                    }) {
                        for cons in &rl.consequent {
                            cnf.add_clause(rule_consequent_clause(rl, cons));
                        }
                    }
                    from.push(name.clone());
                }
                StepRef::Fact(l) => {
                    cnf.add_clause(vec![sat::SatLit::new(l.atom, !l.negated)]);
                    from.push(lit_label(c, l));
                }
                StepRef::Earlier(i) => {
                    let concl = &c.derivations[*i as usize].conclusion;
                    cnf.add_clause(vec![sat::SatLit::new(concl.atom, !concl.negated)]);
                    from.push(lit_label(c, concl));
                }
            }
        }
        // The refutation target: assert the conclusion's negation.
        cnf.add_clause(vec![sat::SatLit::new(
            d.conclusion.atom,
            d.conclusion.negated,
        )]);
        // Verdict-only (UNSAT = the step holds), so the turbo profile is sound.
        let mut inc = sat::Incremental::with_config(&cnf, sat::SolverConfig::TURBO);
        inc.set_budget(budget.cloned());
        let holds = matches!(inc.solve(&[])?, sat::Solved::Unsat(_));
        out.push(Hence {
            origin: d.origin.clone(),
            conclusion: lit_label(c, &d.conclusion),
            from,
            holds,
        });
    }
    Ok(out)
}

/// The abduction (L5) side-check: for each `TRY <literal>` hypothesis, judge whether
/// asserting the supplied candidate would resolve the program's open model. Purely
/// advisory — the candidate is **never committed**; each verdict is one bounded
/// side-solve (the program CNF plus the single candidate literal), so cost grows with
/// the number of `TRY` lines, never with any search the engine invents (Law 5).
///
/// The base program's model multiplicity (counted up to two) sets the baseline; adding
/// the candidate either drops it to a unique model ([`TryOutcome::Closes`] — it pins the
/// gap), makes the program unsatisfiable ([`TryOutcome::Conflicts`] — it clashes with
/// what is established), or leaves more than one model ([`TryOutcome::StillOpen`] — it
/// does not pin it). On an already-unsatisfiable program every hypothesis reads as
/// `Conflicts` (adding a clause never clears a conflict — that is L4's job).
pub(crate) fn tried_hypotheses(
    c: &Compiled,
    budget: Option<&sat::Budget>,
) -> Result<Vec<Tried>, sat::BudgetExhausted> {
    if c.hypotheses.is_empty() {
        return Ok(Vec::new());
    }
    let (cnf, project) = build_cnf(c);
    // One incremental solver counts models for the base program AND every
    // hypothesis, instead of cloning + re-solving the CNF per hypothesis. Each
    // counting session mints its own **guard variable** on entry: its blocking
    // clause is `(¬guard ∨ ¬model-projection)`, active only while that session
    // assumes its guard — so blocked models never leak into another hypothesis's
    // count. Counts (up to 2, distinct on `project`) are semantic — independent
    // of enumeration order — so the reported outcomes are identical to the
    // clone-per-hypothesis implementation this replaces.
    //
    // Counts are heuristic-invariant, so the turbo profile is sound throughout.
    let mut inc = sat::Incremental::with_config(&cnf, sat::SolverConfig::TURBO);
    inc.set_budget(budget.cloned());
    // Count the models of (program ∧ assumptions) projected on `project`, up to 2.
    // The guard lives exactly as long as its session: minted on entry (a future
    // session's guard does not exist yet, so it is never branched on) and
    // **retired** on exit with a root unit `¬guard` (a past session's blocking
    // clause is satisfied at level 0 forever, its guard assigned and never
    // branched on again). Without both ends every solve would branch over
    // O(#hypotheses) idle guards — quadratic over a long TRY list.
    let count2 = |inc: &mut sat::Incremental,
                  assume: &[sat::SatLit]|
     -> Result<usize, sat::BudgetExhausted> {
        let guard = inc.add_var();
        let count = match inc.solve(assume)? {
            sat::Solved::Unsat(_) => 0,
            sat::Solved::Sat(model) => {
                let mut block = Vec::with_capacity(project.len() + 1);
                block.push(sat::SatLit::negative(guard));
                block.extend(project.iter().map(|&v| {
                    if model[v as usize] {
                        sat::SatLit::negative(v)
                    } else {
                        sat::SatLit::positive(v)
                    }
                }));
                inc.add_clause(&block);
                let mut asm = Vec::with_capacity(assume.len() + 1);
                asm.extend_from_slice(assume);
                asm.push(sat::SatLit::positive(guard));
                match inc.solve(&asm)? {
                    sat::Solved::Sat(_) => 2,
                    sat::Solved::Unsat(_) => 1,
                }
            }
        };
        inc.add_clause(&[sat::SatLit::negative(guard)]);
        Ok(count)
    };
    // A single base model over the constrained atoms means the program is already
    // pinned; two means it is open (the same measure the backward pass uses).
    let base_unique = count2(&mut inc, &[])? == 1;
    let mut tried = Vec::with_capacity(c.hypotheses.len());
    for h in &c.hypotheses {
        // Assume the candidate literal (positive unless written `TRY NOT …`).
        let lit = sat::SatLit::new(h.lit.atom, !h.lit.negated);
        let outcome = match &h.goal {
            // Plain TRY (L5 abduction): count models under the candidate.
            None => match count2(&mut inc, &[lit])? {
                0 => TryOutcome::Conflicts,
                1 if !base_unique => TryOutcome::Closes,
                _ => TryOutcome::StillOpen,
            },
            // `TRY H FOR G` (targeted abduction): the textbook pair of checks —
            // (a) theory + H must stay consistent, (b) theory + H ⊨ G, decided
            // refutationally (theory + H + ¬G unsatisfiable). Both are plain
            // verdict-only solves; a past session's retired guard cannot affect
            // them (its blocking clause is satisfied at level 0 forever).
            Some(g) => match inc.solve(&[lit])? {
                sat::Solved::Unsat(_) => TryOutcome::Conflicts,
                sat::Solved::Sat(_) => {
                    let goal = sat::SatLit::new(g.atom, !g.negated);
                    match inc.solve(&[lit, goal.negate()])? {
                        sat::Solved::Unsat(_) => TryOutcome::Explains,
                        sat::Solved::Sat(_) => TryOutcome::NotExplaining,
                    }
                }
            },
        };
        let name = label(c, h.lit.atom);
        let text = if h.lit.negated {
            alloc::format!("NOT {name}")
        } else {
            name
        };
        let goal_text = h.goal.as_ref().map(|g| lit_label(c, g));
        tried.push(Tried {
            origin: h.origin.clone(),
            label: text,
            goal: goal_text,
            outcome,
        });
    }
    Ok(tried)
}
