Solve-pipeline refactor (integration branch — do not merge yet)

[ciaranm]

Long-lived integration branch for the solve-pipeline refactor. Plan and rationale in dev_docs/preprocessor-refactor.md.

Not for merging phase-by-phase. Phases accumulate as commits here; the branch merges to master only once the refactor (or a meaningful chunk) is complete. Kept as a draft PR so CI runs on every push (the workflow only triggers on PRs to master). Head 6a5d7a4, all 6 CI lanes green.

Motivation (the three problems this targets)

1. The "before search" preprocessor generated huge proofs unnecessarily.
2. It was dumber than it could be — work done up front that the search didn't need.
3. New features were hard to add — the model and proof code were tangled.

Status — the canonical phases are complete

• Phase 0 — proof-size measurement harness (proof_metrics).
• Phase 1 — extract the SolveStep pipeline; search becomes the terminal step.
• Phase 1b — unify SolveState (model + root domains + nogood store carried through the pipeline).
• Phase 2 — one ShapeGraphSpec plan as the single source of truth for the supplemental graphs.
• Phase 3 — proof layering + file split (3a ProcessedGraphsData; 3b HomomorphismProofs middle layer; 3c clique-size split; 3d OPB emission into the middle layer). homomorphism_model.cc ~1300 → ~830 lines.
• Phase 4 — supplemental constraint-level subsumption (S2a). Graph-level inert/duplicate elimination was shelved as unsound — measurement showed the supplemental adjacency derivations are ~92–100% never explicitly cited yet stay RUP-load-bearing in search, so dropping whole graphs is unsound. What is sound and instance-independent is constraint subsumption: the adjacency constraints nest (distance3 ⊇ exact-path-1 ⊇ exact-path-2 …, same head), so emit only the strongest per head; a degree/NDS check that needs an elided one re-derives it as a one-step weakening of the kept constraint and deletes it again. Hidden --no-proof-supplemental-subsumption restores full emission. ~25–39% PBP shrink on preprocessing-heavy configs, counts unchanged.
• Phase 5 — cost ordering (S2b). The loop-cancelled adjacency derivations (loop_fix_adjacencies) were emitted at the head of emit_model, so even a trivial refutation carried them. Deferred to the start of the search step, after the cheap concluding steps. Byte-identical for any instance that reaches search; an early conclusion now emits none (e.g. induced c3 → trident PBP 2439 → 9).
• Phase 6 — staged solving (S3, --staged). A cheap first round (original graph only: degree + Hall, no NDS, no supplementals); only if a bounded search round does not conclude does it build the supplementals + NDS, re-filter the domains, and continue unbounded. Full proof support — the supplementals are derived mid-proof at the level-0 restart boundary. Sequential; decision and (see below) counting.

Follow-on work, also on this branch

• Staged counting (without proof). Initially rejected because the Stage-1 → Stage-2 transition restart double-counted. The root cause was narrow: might_have_watches() was keyed on the user's restart schedule, so under the --restarts none that counting defaults to, the transition's resumption nogoods were never posted and Stage 2 re-explored the tree. One-line fix (params.staged || …), validated against the brute-force oracle over the random sweep. Under proof it is still gated (logging an enumeration across a restart — the same restriction as counting with restarts).
• Lean the bottom Proof API (Phase 3 Option 2). The middle layer used to marshal vector<NamedVertex> to call hom-specific Proof methods. Proof now exposes generic emit primitives (emit_proof_line / emit_proof_directive, emit_model_constraint / emit_model_comment, variable_name, injectivity/at-most-one label and dedup-cache accessors) plus a shared AdjacencyProofLines cache, and every homomorphism-exclusive derivation (adjacency, exact-path, distance-3, extra-shape, loop-fix, transient weaken/forget) is emitted from HomomorphismProofs using plain indices. create_adjacency_constraint / start_adjacency_constraints_for are kept in Proof for the common-subgraph and clique solvers, which still use them; the homomorphism solver drives its own clean path.

Deferred / not done (a reviewer's map of the edges)

• Staged counting under proof — needs the enumeration proof to survive a restart; blocked on the upstream VeriPB core id monotonicity bug (the same blocker as re-adding solution-blocking-nogood deletion, issue Enumeration proofs are linear in #solutions; re-add blocking-constraint deletion once upstream VeriPB bug is fixed #59).
• Threaded staging; making --staged the default (wants budget tuning first).
• The model-driven filter proofs (incompatible_by_degrees/_nds, emit_hall) and the clique-size proof still use the old Proof API — the latter is entangled with the shared clique-solver proof path (its translation state lives in Proof because the clique solver's own proof methods read it), so it is left on the old API deliberately.

Guardrail

Phases 1–3 are byte-identical (verified by the random correctness + proof sweeps, the cake gss → veripb → cake pipeline, and the proof_metrics matrix — 274 emitted .opb/.pbp files). Phases 4–6 change proofs deliberately, verified by re-running the sweeps under VeriPB with solution counts unchanged. Each Phase-3-Option-2 step is again byte-identical — it moves where a proof line is emitted, not what. Every push is green on all 6 CI lanes (ubuntu 24.04 / 26.04, macOS 15 / 26, Sanitize, Proof coverage).

🤖 Generated with Claude Code

[ciaranm]

@ArthurGontierPro Give this branch a go, in particular using the "--staged" command line option. It restructures some of how we do the preprocessing and seems to produce less noisy proofs.