Term-encoding congruence via native :merge (proof mode, ~15% faster)#2
Closed
oflatt-claude wants to merge 4 commits into
Closed
Term-encoding congruence via native :merge (proof mode, ~15% faster)#2oflatt-claude wants to merge 4 commits into
oflatt-claude wants to merge 4 commits into
Conversation
…/Construct/IfEq)
Add a general "run arbitrary actions" capability to the bridge merge language,
following egglog PR #933: MergeFn::{TableInsert, Seq, Construct, IfEq} plus
TableAction::lookup_or_insert_multi, wired through fill_deps/resolve/run. These
let a function's :merge stage a row into another table, build a value-tuple
constructor term, sequence effects, and branch — enough to express term-encoding
congruence (union edge + proof composition) as a native merge instead of a rule.
Dormant: no encoder emits these yet. Workspace builds clean.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add EGraph::native_congruence_merge, which builds the term-encoding congruence merge for a proof-mode constructor view `(children) -> (eclass, proof)` using the general merge-action variants: on an FD conflict it keeps the old (eclass, proof) and stages `(@UF_S new_eclass old_eclass) = (Trans new_proof (Sym old_proof))` into the per-sort UF table — the exact edge/proof the rule-encoded congruence produces. declare_function calls it, falling back to the ordinary merge lowering. Inert until the encoder emits 2-output views (next commit): the guard requires a term-constructor view with two outputs, which nothing produces yet. Builds clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
In proof mode each constructor's view becomes a functional-dependency tuple `(children) -> (eclass, proof)` whose native :merge resolves congruence, instead of the rule-encoded self-join. On an FD conflict the merge stages the congruence edge `(@UF_S new old) = (Trans new_pf (Sym old_pf))` into the per-sort UF table (built from the general merge-action variants) and keeps the current row; the existing UF/path-compression/rebuild machinery is unchanged. The `@congruence_rule` is dropped for constructors — the rebuild's re-`set` at canonical children triggers the merge, subsuming it. Encoder (proof_encoding.rs): FD view declaration, `update_fd_view`/`query_fd_view`, FD-aware `add_term_and_view`, `rebuilding_rules_fd`, fact-reader destructuring, and FD delete/subsume rules. Backend: `native_congruence_merge` builds the merge in declare_function; serialization, extraction helpers, the delete-arity check, the typecheck tuple-output/0-input carve-outs, and multi-output `subsume` all updated to handle the tuple view. Verified: all `proofs`, `proof_testing`, `term_encoding`, and normal file treatments pass, plus the proof unit/extraction/regression suites. KNOWN LIMITATION: the 7 `desugar_proof_testing` round-trip tests fail — the merge is built from proof_state, so a dumped-and-re-run encoded program (fresh egraph, no proof_state) loses the Trans/Sym/UF bindings and congruence degrades. Fix is to carry those names in a view annotation so the program is self-contained. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Port PR #927's annotation mechanism so a desugared proof program re-parses self-contained. The Proof sort now carries :internal-proof-names <congr> <trans> <sym>; declaring it repopulates proof_state.proof_names, and native_congruence_merge is detected purely by view shape (term-constructor + eq-sort first output + a second proof output) rather than a live proof_state flag. Together with the existing :internal-uf -> uf_parent round-trip, a dumped encoded program rebuilds the congruence merge in a fresh egraph. Threads a proof_ctors field through the Sort command (parse/Display/desugar/ typecheck/declare), mirroring uf/proof_func. Fixes the 7 desugar_proof_testing failures. Full files suite: 747/747 across all treatments (normal, term_encoding, proofs, proof_testing, desugar). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Owner
Author
|
Reopening against saulshanabrook/egglog-encoding (stacked on saulshanabrook#3). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on saulshanabrook#3 (tuple-output functions) — review/merge that first; this PR's diff is against
port-tuple-outputs.Ports the proof-mode speedup from
oflatt/egglog-duckdb: term-encoding congruence closure now runs as a native:mergeinstead of a generated self-join rule. Contained to the encoding + a general, reusable merge mechanism — no--native-uf, no--fast-rebuild, no dataflow backends, no backend-trait layer, noDefaultVal::Identity, and the union-find stays the existing keyed@UF_S (S S) -> Prooftable (path-compression/single-parent rules unchanged).Result
Proofs on
tests/math-microbenchmark.egg((run 11), release):@rebuildingsearch:mergecongruence)≈15% faster (1.18×); the win is the congruence self-join disappearing from rebuild. Output is equivalent (only a cosmetic fresh-variable name differs). Full
tests/files.rssuite: 747/747 across all treatments (normal, term_encoding, proofs, proof_testing, desugar), plus the proof unit/extraction/regression suites.How it works
egglog-bridge). NewMergeFn::{Seq, TableInsert, Construct, IfEq}+TableAction::lookup_or_insert_multi(following egglog PR #933): a:mergecan now sequence effects, insert a row into another table, mint a value-tuple constructor, and branch. This is the only bridge addition — no proof-specific variants.(children) -> (eclass, proof). On an FD conflict (two congruent terms share canonical children) its:mergestages the congruence edge(@UF_S new old) = (Trans new_pf (Sym old_pf))— the exact edge/proof the rule produced — and keeps the current row. The rebuild's re-setat canonical children is what triggers the merge, so the@congruence_ruleis dropped entirely.Proofsort carries:internal-proof-names <congr> <trans> <sym>; re-declaring it repopulates the proof-constructor names, and the congruence merge is detected purely by view shape. So a dumped/desugared program rebuilds its own merge in a fresh egraph (fixes thedesugar_proof_testinground-trip).Touch points beyond the above: multi-output-aware
serialize, extraction eclass-column helpers,constraint.rsdelete arity, typecheck tuple-output/0-input carve-outs for the encoder-minted view, and multi-outputsubsume.Not included / follow-ups
Commits
egglog-bridge: general merge-actionMergeFnvariants:mergebuilder (inert):merge(FD tuple view):internal-proof-names(round-trip fix)🤖 Generated with Claude Code