Term encoding: rebuild via correlated OR - #2
Draft
oflatt-claude wants to merge 2 commits into
Draft
Conversation
Applies the disjunction feature to the egglog subtree: a rule query may contain (OR (branch) (branch) ...), where each branch is a conjunction of facts; the rule matches when any branch matches, and only variables common to every branch (or bound by the surrounding conjunction) may be used outside the OR. Correlated branches are supported and compile to a fused, deduplicating, seminaive/delta-driven union node in the core-relations free-join engine. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Changes the term encoding's generated rebuild rule (non-proof mode) to the correlated OR form, so rebuilding is delta-driven and deduplicated per row. Proof mode keeps the existing rule. Measured ~1.20x faster than the previous rebuild on math-microbenchmark, with identical results. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
Draft. Changes the term encoding's generated rebuild rule (non-proof mode) to the correlated
ORform, so rebuilding is delta-driven and per-row deduplicated. Proof mode keeps the existing rule. ~1.20× faster than the previous rebuild onmath-microbenchmark, with byte-identical results. Changes confined to theegglog/subtree.Stacked on the "Add OR" PR. GitHub can't base a PR on a fork branch across repos, so this PR's diff also contains the OR feature commit; the net-new change here is the single commit "Term encoding: rebuild via correlated OR" (5 files under
egglog/). Review/merge the feature PR first.Rebuild dispatch (
egglog/src/proofs/proof_encoding.rs):ORover stale eq-sort columns (≥2 cols) or a plain delta-driven rule (1 col); 0 eq-sort cols → no rule.Verified on the underlying egglog tree: full
.eggharness 747/747 (term-encoding treatment now exercises the OR rebuild; proofs use the old rule), 17/17 disjunction,make nitsclean. Exactly one program-text snapshot changed (rule form only); no output/print-sizesnapshots changed, confirming identical results.🤖 Generated with Claude Code