Add OR (disjunction) to rule bodies by oflatt-claude · Pull Request #7 · oflatt-claude/egglog

oflatt-claude · 2026-07-02T16:53:53Z

Builds on #6 (Strategy C's fused union node) and adds the two things the rebuilding use case needs: correlated branches and a seminaive / delta-driven union.

What's new over C (#6)

Correlated disjunction. Branches may reference variables bound by the surrounding query (not just self-contained sub-queries). The interface rule is relaxed to: a variable is usable outside the OR if it's bound by the surrounding conjunction or common to every branch; branch-locals are renamed and may not escape.
Seminaive through the union (the crux). The union is no longer naive. Using seminaive(⋁ᵢ (O ∧ Bᵢ)) = ⋃ᵢ seminaive(O ∧ Bᵢ), add_rules_from_cached (egglog-bridge) is now union-aware: for each disjunct it emits the standard per-atom delta variants over that disjunct's atoms only (never across branches), and each variant's branch delta is carried as extra JoinHeaders reprocessed onto that branch's sub-plan (core-relations). All variants feed the one deduping materialization + single shared action.

Net: a new tuple in a branch atom index-probes only the affected rows (no re-scan), and dedup on the output row keeps a row changed in multiple columns to a single action firing.

The motivating rule (efficient e-graph rebuilding)

(relation stale_Math (Math Math))
(rule ((UF_Math t l) (!= t l)) ((stale_Math t l)) :ruleset rebuilding)

(rule ((MulView c0 c1 c2)
       (OR ((stale_Math c0 l0)) ((stale_Math c1 l1)) ((stale_Math c2 l2))))
      ((set (MulView (UF_Mathf c0) (UF_Mathf c1) (UF_Mathf c2)) ())
       (delete (MulView c0 c1 c2)))
       :ruleset rebuilding :unsafe-seminaive)

Verification

tests/disjunction.rs: 17/17, including:
- or_correlated_dedup_single_rebuild — a row stale in two columns fires the action once (dedup semijoin).
- or_correlated_seminaive_delta_driven — after fixpoint nfire=1 (not re-fired per iteration ⇒ not naive); adding one new stale edge takes nfire 1→3, i.e. only the two newly-affected rows, independent of table size ⇒ delta-driven index probe, not O(N).
full .egg harness: 747/747; make nits clean.

Restrictions (documented)

Independent ORs (branches share no outer var) still run naive; only correlated ORs are delta-driven so far.
Branch atoms must be tables (a branch != is rejected with a clean error; use a staleness relation, as above).
Shape B (each branch binds the row and pins an outer var into a different column) is not supported; the prepended-conjunction layout covers the rebuild use case.
OR works under term encoding but is rejected under full proof mode.

Performance

A four-way benchmark (current vs split vs fused-OR) on math-microbenchmark under term encoding is running; I'll post the numbers here. Hypothesis: fused-OR matches split's delta-driven win and cuts split's redundant rebuilds of multi-stale rows (fewer action firings).

🤖 Generated with Claude Code

…(Strategy C) Add `(OR (branch) (branch) ...)` to rule bodies, compiled to a single backend rule with a fused union node in the core-relations free-join engine — the surrounding conjunction is scanned once and the branches are enumerated additively (no rule-splitting / no cartesian product of rules). Backend: a new `JoinStage::Union { branches }` (core-relations/src/free_join/plan.rs, executed in execute.rs) forms block 0 of a DecomposedPlan; each branch is a self-contained sub-plan projecting onto the OR's common variables, written into one materialization keyed on those variables (deduplicated in memory). The result block is the surrounding conjunction, planned via the existing tree-decomposition message-passing (`FusedIntersectMat`) so it joins that materialization by index and fires the action. `Query.union` / `QueryBuilder::set_union` carry the union; `egglog-bridge` `RuleBuilder::set_union_branches` bridges it. Frontend: `OR` is a real AST fact (`GenericFact::Or`); typechecking resolves each branch (branch-local vars renamed to fresh names), enforces that only variables common to every branch cross the OR boundary, and binds those common variables for the actions. Restrictions: OR rules run in naive mode (no seminaive delta through a union); branch atoms must be tables (primitives allowed in the surrounding conjunction); OR is rejected under proofs / term encoding. - egglog-ast, src/ast/parse.rs: `GenericFact::Or` + parsing - src/typechecking.rs, src/core.rs, src/lib.rs: typecheck + wire OR to the backend - core-relations: `JoinStage::Union`, `plan_union`, execution - egglog-bridge: union plumbing - tests/disjunction.rs (14 tests), docs/disjunction-design.md, CHANGELOG.md Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Extend the OR disjunction implementation (Strategy C's fused union node) to support correlated branches and seminaive evaluation: - Typecheck: relax the interface rule so a branch may reference variables bound by the surrounding conjunction (correlated branches); only true branch-locals are renamed/rejected. - Parser: accept the uppercase OR spelling and bare-fact disjuncts (e.g. (OR (= a d) ...)) in addition to C's list-of-facts branches. - add_or_rule: dispatch to Strategy C's fused union node for naive, self-groundable branches, or to a new splitting path (one ordinary backend rule per disjunct, sharing the action) for correlated or seminaive ORs. Split rules are plain conjunctive rules, so per-disjunct canonicalization turns a correlated equality into a shared-variable index-probe join (no cartesian product), and seminaive / :unsafe-seminaive work natively. - Term encoding: allow OR without proofs (proof_form recurses into branches; instrument_fact rewrites branch atoms to view lookups and re-emits an or fact); still rejected with proofs enabled. - Tests: add a rebuild-shaped correlated :unsafe-seminaive test (with a (!= d e) primitive beside the OR and a function lookup in the action) and a correlated naive test; C's 14 independent-union tests still pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Replace the rule-splitting compilation of correlated/seminaive OR with C's fused, deduplicating union node, so a row matched via several branches is processed exactly once (disjunctive-semijoin single-rebuild), not once per matching branch. - add_or_rule now always compiles to one backend rule with the fused union node. A correlated OR (a disjunct references a surrounding-conjunction var not common to all disjuncts, e.g. (v a b c) outside and (stale a al) inside) prepends the conjunction into every branch, so branches bind and deduplicate on the shared output row; an independent OR keeps the conjunction as a scanned-once continuation. Output/dedup vars exclude Unit-sorted vars (fixes a term-encoding view-lookup unit result leaking into the dedup key). - Removes the split path (add_or_rule_split / branch_self_groundable). - Runs naive: the seminaive delta machinery can't reach union branch atoms; correct at a fixpoint (a rebuild that deletes the stale row converges), but not incremental. Documented as future work. - Tests: or_correlated_dedup_single_rebuild asserts a row stale in TWO columns fires the action exactly once (dedup); or_correlated_rebuild_to_fixpoint runs the full delete+rebuild with a leader-function lookup to a fixpoint. C's 14 independent-union tests unchanged. Correlated OR also verified under term encoding. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

A correlated OR now runs seminaive instead of naive: a new tuple in a branch atom drives an index probe of the row, not an O(N) per-iteration re-scan, while the deduplicating materialization keeps the shared action firing once per row. Semi-naive of a union of conjunctions is the union of the per-disjunct expansions: seminaive(OR_i B_i) = union_i seminaive(B_i). Because a correlated OR prepends the surrounding conjunction into every branch, each branch B_i holds all of O union B_i, so its delta expansion is self-contained (constraints never cross branch boundaries). - egglog-bridge add_rules_from_cached: union-aware. For each branch, generate the standard per-atom focus/old timestamp variants over that branch's atoms only, and call the new RuleSetBuilder::add_union_rule_from_cached. - core-relations add_union_rule_from_cached: builds one variant of the cached union plan whose JoinStage::Union holds one variant-branch per variant (the cached branch narrowed by the variant's ts constraints, applied as extra JoinHeaders via reprocess_union_branch). All variant-branches feed the single dedup materialization + shared action. The branch delta constraint reaches the branch sub-plan as a header the execute Union handler already intersects in. - src/lib.rs: correlated OR rules build the backend rule with seminaive=true; independent OR rules keep the scanned-once continuation and run naive. Test: or_correlated_seminaive_delta_driven proves it — the fixpoint fires once per stale row (=1, which naive re-firing would blow past), and adding ONE new stale edge then running one step fires only for the two newly-affected rows (1 -> 3), independent of table size. 17 disjunction + 747 file tests pass; nits clean; correlated OR still works under term encoding. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

oflatt-claude · 2026-07-02T17:24:29Z

Benchmark: fused-OR rebuild wins

math-microbenchmark.egg under term encoding, one binary with an EGGLOG_REBUILD_MODE switch, pinned to core 0, -j1, 2 warmup + 10 interleaved rounds (median).

rebuild rule	median (s)	speedup vs current
current (all-column lookup + guard)	17.120	1.00×
split (per-column delta-driven, N rules)	15.362	1.11×
fused-OR (D: correlated + seminaive + dedup)	14.226	1.20×

Fused is 1.08× / 7.4% faster than split, and 20% faster than current (vs split's 11%). σ ≤ 0.07s.

The win over split is the multi-stale-row dedup: a row whose args both changed is rebuilt once, not once per column. Rebuild-ruleset search time drops 8.66s → 5.51s (~36%); the added stale_* maintenance rule is cheap (~0.18s).

Correctness: current / split / fused all produce a byte-identical print-size fingerprint (sha 17811bd1…; Add=641743, Mul=345075, Diff=13504, Integral=32434, Sub=15123, …).

Benchmark harness + env-gated generator modes are on branch payoff-fused-or (not for merge; the OR rebuild rule it generates is the correlated form documented above).

oflatt-claude · 2026-07-02T17:25:46Z

Why fused beats split — rebuild-action firing counts (deterministic)

mode	rebuild firings	#rebuild rules	@Rebuilding search
current	1,445,004	13	~9.0s
split	1,720,779 (+19.5%)	31	~7.0s
fused (D)	1,439,965	13	~5.5s

Split does 19.5% more rebuild firings than fused: a row stale in k columns rebuilds k times under split, once under fused (dedup on the row). Fused's firing count matches current's (both per-row), but fused is delta-driven, so it has the lowest rebuild-search time of the three. The staleness-maintenance rule costs ~1.05M monotone inserts (+slightly higher merge), more than offset by the search savings.

So fused's win decomposes cleanly: delta-driven (like split) gets it from current's ~9s to ~7s of rebuild search; per-row dedup (unlike split) gets it the rest of the way to ~5.5s and removes split's extra 275k firings. Full four-way report and harness on branch payoff-fused-or (commit 3c3a7faf).

oflatt and others added 4 commits July 2, 2026 00:14

oflatt-claude changed the title ~~Disjunction (OR): Strategy D — correlated + seminaive union node~~ Add OR (disjunction) to rule bodies Jul 2, 2026

Navigation Menu

Add OR (disjunction) to rule bodies - #7

Add OR (disjunction) to rule bodies#7
oflatt-claude wants to merge 4 commits into
mainfrom
disjunction-seminaive-union

oflatt-claude commented Jul 2, 2026

Uh oh!

oflatt-claude commented Jul 2, 2026

Uh oh!

oflatt-claude commented Jul 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

oflatt-claude commented Jul 2, 2026

What's new over C (#6)

The motivating rule (efficient e-graph rebuilding)

Verification

Restrictions (documented)

Performance

Uh oh!

oflatt-claude commented Jul 2, 2026

Benchmark: fused-OR rebuild wins

Uh oh!

oflatt-claude commented Jul 2, 2026

Why fused beats split — rebuild-action firing counts (deterministic)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants