Single self-referential UF for the encoding (proofs ~1.8x faster)#7
Closed
oflatt-claude wants to merge 9 commits into
Closed
Single self-referential UF for the encoding (proofs ~1.8x faster)#7oflatt-claude wants to merge 9 commits into
oflatt-claude wants to merge 9 commits into
Conversation
Ports egraphs-good/egglog#938 ("Add tuple-output functions") into the vendored egglog/ subtree. A function may declare more than one output sort, stored as separate value columns (no boxing); outputs are destructured in queries, written in actions, and merged per column with a (values ...) clause. Restricted to plain functions and unsupported by the term/proof encoding. The upstream diff applied cleanly except for one context conflict in src/proofs/proof_encoding_helpers.rs (this fork carries an extra NaiveEqSortPrimitiveFact reason); the TupleOutputFunction variant and guard were reapplied by hand. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…/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>
In the merge_simple fast path, pre-seed the merging table's own write-buffer so a :merge can stage a row back into the very table it is resolving. This is what a self-referential union-find merge needs (redirect the losing edge into @UF_S during @UF_S's own merge). Non-self-referential merges get an empty, unused buffer; the strata path already handled this via write-deps. Foundation for the single-table self-referential UF (no effect on its own). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add EGraph::peek_next_function_id and reorder add_table to reserve the table id and push the new FunctionInfo BEFORE building the merge callback. This lets a merge reference the very table it defines (e.g. the single-table UF whose :merge does a TableInsert into itself), since merge resolution reads self.funcs[self_id].table. Non-self-referential merges are unaffected — the new ordering is a strict superset. Foundation for the self-referential UF (inert). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replace the two-table UF (@UF_S relation + @UF_Sf index) with one self-referential function @uf : (S) -> S per sort, on the non-proof term-encoding path (proof mode unchanged). - Union writes a single-key edge `(set (@uf (ordering-max a b)) (ordering-min a b))`. - @uf's :merge is native self-referential (build_uf_self_merge, from the committed Seq/TableInsert/IfEq actions + peek_next_function_id + core-relations self-write): keep min, and TableInsert the losing edge into its own table. - Keep only path_compress; drop single_parent, uf_function_index, the @UF_Sf index, the per-term self-loop seed, and their schedule steps. - Rebuild fans out to one rule per eq-sort view column (root columns don't fire, so no self-loop / default lookup / Pair needed). - Extraction find_canonical chases the single-key @uf to a fixpoint (miss = self). Validates the self-referential-merge mechanism end-to-end. Full files suite 747/747 across all treatments (normal, term_encoding, proofs, proof_testing, desugar); proof unit tests pass; make nits clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replace the two-table proof UF (@UF_S (S S)->Proof relation + @UF_Sf (S)->Pair index) with one self-referential native-tuple function @uf : (S) -> (S, Proof) per sort, mirroring the term path. - Union writes `(set (@uf larger) (values smaller proof))`. - @uf's :merge is native, proof-composing self-referential (build_uf_self_merge proof branch): keep min eclass + its proof, and TableInsert the displaced edge `(@uf max) = (values min (Trans (Sym max_pf) min_pf))` into its own table. - The constructor view's congruence merge (native_congruence_merge) now orients max->min and stages `(@uf max) = (values min (Trans max_vp (Sym min_vp)))` into the single @uf (was an unoriented edge into the relation; orientation is required since there is no single_parent rule to normalize). - path_compress composes proofs `(Trans pb pc)`; single_parent, uf_function_index, the @UF_Sf pair index, self-loops, and their schedule steps are dropped. - Rebuild reads the single @uf via `(= (values leader proof) (@uf ci))`, fanned out per eq-sort column. Extraction chases the 1-key @uf (unchanged). - Sort re-registers its :internal-uf name in self_merge_uf_functions so a re-parsed desugared program reattaches the self-merge (self-contained). Full files suite 747/747 across all treatments (proofs/proof_testing run the proof checker); proof unit tests pass; make nits clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Author
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 #6 (congruence via native
:merge), which is stacked on #3 (tuple outputs). Until those merge, the diff below includes their commits; the self-referential-UF work is the last 4 commits.Replaces the term/proof encoding's two-table union-find (
@UF_S (S S)->Proofedge relation +@UF_Sf (S)->Pairindex) with one self-referential native-tuple function@UF : (S) -> S(term) /(S) -> (S, Proof)(proof) per sort. This is where egglog-duckdb's encoding converged ("single fast term-encoding").Result
Proofs on
tests/math-microbenchmark.egg((run 11), release):@rebuildingsearch:mergecongruence, 2-table UF)≈1.83× faster than the original baseline, ≈1.55× faster than #6. Output is equivalent; full
tests/files.rssuite 747/747 across all treatments (theproofs/proof_testingtreatments run the proof checker), proof unit tests pass,make nitsclean.How it works
(set (@UF (ordering-max a b)) (values (ordering-min a b) proof)).@UF's:mergeis a native self-referential merge (built from theSeq/TableInsert/IfEq/Constructactions +peek_next_function_id+ a core-relations self-write): on an FD conflict it keepsminandTableInserts the displaced edge back into its own table, composing the transitivity proof. Single-parent is now automatic (the UF is keyed by the node), so thesingle_parentanduf_function_indexrulesets and the@UF_Sfindex are gone; only a proof-composingpath_compressremains.:merge, from Faster proof encoding: congruence via :merge + single self-referential UF (~1.8x) #6) is retargeted to orientmax→minand stage into the single@UF.@UFwith a native(= (values leader proof) (@UF ci))and is fanned out to one rule per eq-sort column — a canonical (root) column has no@UFrow, so its rule simply doesn't fire. That's what lets us drop the self-loop rows, thePairindex, and any default-on-miss lookup: nothing needsfind(root)to hit.@UF; the encoding stays self-contained (:internal-ufre-registers the self-merge on a desugar re-parse).Engine additions (small, general)
core-relations: pre-seed a merging table's own write-buffer so a:mergecan stage into its own table (~16 lines).egglog-bridge:peek_next_function_id+add_tablereserves the table id / registersFunctionInfobefore building the merge (so a merge can name its own table). NoDefaultVal::Identityneeded.Commits (self-ref-UF portion)
🤖 Generated with Claude Code