Make custom schedulers compose with the term/proof encoding

[oflatt-claude]

Problem

Custom schedulers — e.g. egglog-experimental's backoff scheduler — drive a ruleset through EGraph::step_rules_with_scheduler. Under the term/proof encoding, the e-graph's invariants (canonical representatives, congruence closure, deferred deletion) are maintained by generated maintenance rulesets rather than the backend union-find, and those rulesets must be run to fixpoint between steps. step_rules_with_scheduler never ran them, so a scheduled step queried stale, un-canonicalized view tables — schedulers and term/proof mode did not compose.

Approach

Record the maintenance schedule in the program itself via a new internal command (internal-rebuild-schedule <schedule>), emitted once by the term-encoding pass. step_rules and step_rules_with_scheduler then run that schedule to fixpoint after each step. Runs are no longer wrapped with an inline rebuild in the desugared schedule; non-run commands keep their existing per-command rebuild.

Because the schedule travels with the desugared program (as data), the desugared output stays self-contained — it still runs correctly when replayed on a plain e-graph without term encoding (the desugar test mode), which is why the schedule is carried in the program rather than gated on a runtime flag.

Only the user's ruleset is scheduled; maintenance always runs unscheduled. The command is named internal-rebuild-schedule to signal it is not for direct use.

Tests

• term encoding + scheduler runs maintenance (single step)
• proof mode + scheduler preserves proofs (extract + check a derived equality's proof)
• real backoff algorithm (ported from egglog-experimental) reaches the same saturated e-graph as an unscheduled run on an AC-rewrite benchmark, asserting it actually bans
• a fractional (partial-selection) scheduler reaches the same result — residual matches held across rebuilds are re-applied idempotently (sound, since term-encoding terms are immutable)
• choose_all saturation-equivalence

Full .egg suite (744, across term-encoding / proofs / proof-testing / desugar modes) and lib tests pass; make nits clean.

Follow-up

The per-command rebuild for non-run commands is still injected into the desugared program. Moving it to a lazy rebuild-before-observe runtime model (mutations mark the e-graph dirty; maintenance runs only before check/extract/print/queries) would remove that injection too. An eager "rebuild after each mutating command" does not work: a single user set on a :merge function desugars into multiple commands that must rebuild as a unit, and the flat desugared list has lost those boundaries — so this needs the lazy model, left as follow-up.

🤖 Generated with Claude Code