Join proof steps with the same premises.
(
con: problem.Dependency,
con2prems: dict[tuple[str, ...], list[problem.Dependency]],
expanded: set[tuple[str, ...]],
)
| 315 | |
| 316 | |
| 317 | def join_prems( |
| 318 | con: problem.Dependency, |
| 319 | con2prems: dict[tuple[str, ...], list[problem.Dependency]], |
| 320 | expanded: set[tuple[str, ...]], |
| 321 | ) -> list[problem.Dependency]: |
| 322 | """Join proof steps with the same premises.""" |
| 323 | h = con.hashed() |
| 324 | if h in expanded or h not in con2prems: |
| 325 | return [con] |
| 326 | |
| 327 | result = [] |
| 328 | for p in con2prems[h]: |
| 329 | result += join_prems(p, con2prems, expanded) |
| 330 | return result |
| 331 | |
| 332 | |
| 333 | def shorten_proof( |