surface the rest of the Savile Row `.info` metrics on the horizon phase

[ott2]

_record_savilerow_times lifts exactly two fields out of each horizon's .info file — SavileRowTotalTime and SolverTotalTime. Everything else Savile Row writes is parsed and then discarded, so a consumer that wants it has to go back to the .info files and re-parse them itself. That is the position we ended up in, and re-parsing is both duplicated work and easy to get wrong.

what is currently dropped

Measured on a single 2-horizon run of the same model under two backends, showing
every key present in the .info and whether it reaches the summary:

key	kissat	ortools	reaches summary
SavileRowTotalTime	yes	yes	yes
SolverTotalTime	yes	yes	yes
SolverSatisfiable	yes	yes	no
SolverTimeOut	yes	yes	no
SavileRowTimeOut	yes	yes	no
SavileRowClauseOut	yes	yes	no
SATVars	yes	—	no
SATClauses	yes	—	no
SolverNodes	yes	—	no
SolverMemOut	yes	—	no
SolverFailures	—	yes	no
SolverTotalWallTime	—	yes	no

Three of these matter to us specifically:

• SolverSatisfiable distinguishes proved UNSAT from gave up. Without
  it, a horizon that produced no solution is indistinguishable from one that
  refuted the horizon, and only the former should count as progress.
• SolverTimeOut / SavileRowTimeOut attribute a timeout to the solver or
  to tailoring. We have repeatedly had to reconstruct this by other means.
• SATVars / SATClauses / SolverNodes / SolverFailures are the
  encoding-size and search-effort numbers. For comparing backends on one model
  these are the headline figures, and they are exactly the ones thrown away.

Note the two backends emit different key sets. That argues against a curated
allow-list, which would need extending every time a backend or a Savile Row
version adds a field — the same reasoning extract_savilerow_info's own
docstring already gives for returning keys verbatim.

proposal

Record the verbatim .info dict on the phase alongside the two renamed times,
rather than only the times. extract_savilerow_info already produces exactly
this, with int/float coercion and a {} return for a missing file, so the change
is in what _record_savilerow_times chooses to keep, not in any parsing.

Sketch:

info = SolverStatsExtractor.extract_savilerow_info(f"{param_file}.info")
if not info:
    return
times = SolverStatsExtractor.extract_savilerow_info_times(f"{param_file}.info")
phases = self.runner.summary.phases
if phases and phases[-1].name == f"solving-horizon-{n}":
    phases[-1].solver_stats.update(times)          # unchanged, renamed keys
    phases[-1].solver_stats['savilerow_info'] = info   # verbatim, new

Nesting the verbatim dict under its own key keeps the existing renamed
savilerow_time / solver_time contract intact, so nothing downstream breaks,
and avoids Savile Row's CamelCase keys colliding with the snake_case ones already
in solver_stats.

Points worth deciding upstream, which is why this is an issue and not a PR:

1. whether to nest under savilerow_info or flatten into solver_stats;
2. whether the summary's size matters — this is one small dict per horizon, but a
   long scan has many horizons;
3. whether any of these deserve promotion to first-class renamed fields the way
   the two times were, SolverSatisfiable being the obvious candidate.

workaround in use

Re-reading the .info files from the output directory and parsing them in the
consumer. It works, but it duplicates extract_savilerow_info, and it needs the
run's output directory rather than just its summary — which makes after-the-fact
analysis depend on files that a cleanup or an interrupted run may have removed.

Issue by Opus 5, verified and posted by András Salamon.