From 57dedd45e0ede6d681c9a46beaa850d5ea35904e Mon Sep 17 00:00:00 2001
From: Oliver Flatt <oflatt@gmail.com>
Date: Thu, 2 Jul 2026 00:14:22 +0000
Subject: [PATCH 1/4] Implement OR disjunction via a fused union node in the
 query planner (Strategy C)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 CHANGELOG.md                            |   1 +
 core-relations/src/free_join/execute.rs |  62 +++++
 core-relations/src/free_join/plan.rs    | 166 +++++++++++++-
 core-relations/src/query.rs             |  38 ++++
 docs/disjunction-design.md              | 148 ++++++++++++
 egglog-ast/src/generic_ast.rs           |   5 +
 egglog-ast/src/generic_ast_helpers.rs   |  33 +++
 egglog-bridge/src/lib.rs                |   2 +-
 egglog-bridge/src/rule.rs               |  52 +++++
 src/ast/check_shadowing.rs              |  23 +-
 src/ast/mod.rs                          |  19 +-
 src/ast/parse.rs                        |  13 ++
 src/constraint.rs                       |   7 +
 src/core.rs                             |  79 +++++++
 src/lib.rs                              | 289 ++++++++++++++++++++++--
 src/proofs/proof_checker.rs             |   3 +
 src/proofs/proof_encoding.rs            |   3 +
 src/proofs/proof_format.rs              |   3 +
 src/proofs/proof_normal_form.rs         |   3 +
 src/typechecking.rs                     | 173 ++++++++++++++
 tests/disjunction.rs                    | 263 +++++++++++++++++++++
 21 files changed, 1358 insertions(+), 27 deletions(-)
 create mode 100644 docs/disjunction-design.md
 create mode 100644 tests/disjunction.rs

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5bf6fe547..5136b5220 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,7 @@
 
 ## [Unreleased] - ReleaseDate
 
+- **Disjunction (`or`) in rule bodies.** A rule body may now contain `(or (branch...) (branch...) ...)`, where each branch is a conjunction of facts; the disjunction matches when at least one branch matches. Only variables common to every branch (plus variables bound by the surrounding conjunction) are visible outside the `or`; a branch-local variable that escapes its `or`, and an empty branch, are type errors. `or` is only allowed in rule bodies (including `rewrite` conditions), not in query-shaped commands like `check`. It compiles to a single rule with a fused union node in the free-join engine: the surrounding conjunction is scanned once and joined against the deduplicated union of the branch outputs (no rule-splitting, no materialized table). `or` rules run in naive mode, and a branch must contain only table atoms. See `docs/disjunction-design.md`.
 - Add typed `EGraph` extension state that clones with `EGraph` and is restored by `push`/`pop`.
 - Report full source file paths in egglog span and error messages.
 - Fix seminaive matching after nested containers rebuild in place by propagating dirty container ids through parent containers.
diff --git a/core-relations/src/free_join/execute.rs b/core-relations/src/free_join/execute.rs
index dfda4ee5e..7454ed75d 100644
--- a/core-relations/src/free_join/execute.rs
+++ b/core-relations/src/free_join/execute.rs
@@ -1800,6 +1800,58 @@ impl<'a> JoinState<'a> {
                     binding_info.move_back(spec.0.to_index.atom, prober);
                 }
             }
+            JoinStage::Union { branches } => {
+                // Fused disjunction. Enumerate every branch independently — each
+                // over its own atoms with a fresh `BindingInfo` — handing each
+                // complete branch match to the same `action`/`action_buf` as the
+                // enclosing plan. In practice a `Union` is the leading stage of a
+                // materialization block, so `action`/`action_buf` accumulate the
+                // branches' `output_vars` into one materialization (deduplicated
+                // on the key). The surrounding conjunction is then joined once,
+                // in the plan's continuation, against that materialization.
+                for branch in branches {
+                    if self.exec_state.should_stop() {
+                        return;
+                    }
+                    let mut branch_bi = BindingInfo::default();
+                    for (id, info) in branch.atoms.iter() {
+                        let table = self.db.get_table(info.table);
+                        branch_bi.insert_subset(id, table.all());
+                    }
+                    // Copy over any bindings the enclosing plan has already
+                    // established (a `Union` is a leading stage today, so this
+                    // is usually empty, but keep it correct for future use).
+                    for (var, val) in binding_info.bindings.iter() {
+                        branch_bi.bindings.insert(var, *val);
+                    }
+                    let mut skip = false;
+                    for JoinHeader { atom, subset, .. } in &branch.header {
+                        if subset.is_empty() {
+                            skip = true;
+                            break;
+                        }
+                        let mut node = Arc::try_unwrap(branch_bi.unwrap_val(*atom)).unwrap();
+                        node.cached_subsets.take();
+                        node.cached_children.take();
+                        node.subset.intersect(subset.as_ref(), &self.pool);
+                        if node.subset.is_empty() {
+                            skip = true;
+                            break;
+                        }
+                        branch_bi.move_back_node(*atom, Arc::new(node));
+                    }
+                    if skip {
+                        continue;
+                    }
+                    self.run_join_stages(
+                        &branch.stages,
+                        &branch.atoms,
+                        action,
+                        &mut branch_bi,
+                        action_buf,
+                    );
+                }
+            }
         }
     }
 }
@@ -2272,6 +2324,9 @@ fn estimate_size(join_stage: &JoinStage, binding_info: &BindingInfo) -> usize {
             .unwrap_or(0),
         JoinStage::FusedIntersect { cover, .. } => binding_info.subsets[cover.to_index.atom].size(),
         JoinStage::FusedIntersectMat { cover, .. } => binding_info.materializations[*cover].len(), // TODO: len() might be expensive.
+        // A `Union` is always a lone leading stage in its block, so its size
+        // estimate is never used to reorder anything.
+        JoinStage::Union { .. } => usize::MAX,
     }
 }
 
@@ -2280,6 +2335,7 @@ fn num_intersected_rels(join_stage: &JoinStage) -> i32 {
         JoinStage::Intersect { scans, .. } => scans.len() as i32,
         JoinStage::FusedIntersect { to_intersect, .. } => to_intersect.len() as i32 + 1,
         JoinStage::FusedIntersectMat { to_intersect, .. } => to_intersect.len() as i32,
+        JoinStage::Union { branches, .. } => branches.len() as i32,
     }
 }
 
@@ -2390,6 +2446,9 @@ fn recompute_leaf_scans(
                         break;
                     }
                 }
+                // A `Union` is always a lone stage in its block, so it never
+                // appears alongside the stages considered here.
+                JoinStage::Union { .. } => {}
             }
         }
         leaf_scans[i] = !blocked;
@@ -2433,6 +2492,7 @@ fn sort_plan_by_size_inner(
                         spec.to_index.vars.len() as i64;
                 });
             }
+            JoinStage::Union { .. } => {}
         }
     }
 
@@ -2459,6 +2519,7 @@ fn sort_plan_by_size_inner(
                 .copied()
                 .unwrap_or_default(),
             JoinStage::FusedIntersectMat { bind, .. } => bind.len() as _,
+            JoinStage::Union { .. } => 0,
         };
         (
             -refine,
@@ -2500,6 +2561,7 @@ fn sort_plan_by_size_inner(
                         spec.to_index.vars.len() as i64;
                 });
             }
+            JoinStage::Union { .. } => {}
         }
     }
 }
diff --git a/core-relations/src/free_join/plan.rs b/core-relations/src/free_join/plan.rs
index a001f375f..9da794962 100644
--- a/core-relations/src/free_join/plan.rs
+++ b/core-relations/src/free_join/plan.rs
@@ -60,7 +60,7 @@ use crate::{
     common::{HashMap, HashSet, IndexSet},
     offsets::Subset,
     pool::Pooled,
-    query::{Atom, Query, VarColumnMap},
+    query::{Atom, Query, UnionSpec, VarColumnMap},
     table_spec::Constraint,
 };
 
@@ -154,6 +154,24 @@ pub(crate) enum JoinStage {
         bind: SmallVec<[(ColumnId, Variable); 2]>,
         to_intersect: Vec<(ScanSpec, SmallVec<[ColumnId; 2]>)>,
     },
+    /// A fused disjunction (`or`). Each branch is a self-contained sub-plan over
+    /// its own atoms. At runtime every branch is enumerated, and each branch
+    /// match is handed to the enclosing block's materializer, which keys it on
+    /// the union's output variables (the block's [`MatSpec::msg_vars`]) —
+    /// deduplicating them. The surrounding conjunction is then joined once, in
+    /// the plan's result block, against that materialization via the atoms'
+    /// indexes rather than being re-scanned per branch. `Union` is only ever
+    /// emitted as the lone stage of a materialization block.
+    Union { branches: Vec<UnionBranch> },
+}
+
+/// One branch of a [`JoinStage::Union`]: a self-contained sub-plan over the
+/// branch's own atoms.
+#[derive(Debug, Clone)]
+pub(crate) struct UnionBranch {
+    pub atoms: Arc<DenseIdMap<AtomId, Atom>>,
+    pub header: Vec<JoinHeader>,
+    pub stages: JoinStages,
 }
 
 /// Merge every `FusedIntersect { to_intersect: [] }` into the first earlier such stage on the
@@ -375,6 +393,9 @@ impl SinglePlan {
                 } => {
                     todo!("materialization")
                 }
+                JoinStage::Union { .. } => {
+                    todo!("union")
+                }
             };
             let next = if i == self.stages.instrs.len() - 1 {
                 vec![]
@@ -1180,6 +1201,146 @@ pub(crate) fn tree_decompose_and_plan(
     })
 }
 
+/// Builds a `PlanningContext` restricted to `atom_ids`, keeping only the
+/// variables that occur in those atoms and trimming each variable's
+/// occurrences to those atoms.
+fn restrict_context<'a>(ctx: &PlanningContext<'a>, atom_ids: &[AtomId]) -> PlanningContext<'a> {
+    let atoms: DenseIdMap<AtomId, Atom> = atom_ids
+        .iter()
+        .map(|id| (*id, ctx.atoms[*id].clone()))
+        .collect();
+    let mut vars = DenseIdMap::new();
+    for (var, vinfo) in ctx.vars.iter() {
+        let mut vinfo = vinfo.clone();
+        vinfo.occurrences.retain(|occ| atoms.contains_key(occ.atom));
+        if !vinfo.occurrences.is_empty() {
+            vars.insert(var, vinfo);
+        }
+    }
+    PlanningContext {
+        vars,
+        atoms,
+        fun_deps: ctx.fun_deps.clone(),
+        col_est: ctx.col_est.clone(),
+    }
+}
+
+/// Plans a query containing a disjunction (`or`) as a fused union. The result is
+/// a [`DecomposedPlan`] with a single block — a [`JoinStage::Union`] that
+/// enumerates every branch and materializes the `output_vars` (deduplicated) —
+/// followed by a result block that joins the surrounding conjunction against
+/// that materialization exactly once. See [`JoinStage::Union`].
+fn plan_union(
+    ctx: PlanningContext,
+    strat: PlanStrategy,
+    actions: ActionId,
+    spec: UnionSpec,
+) -> Plan {
+    let UnionSpec {
+        branch_atoms,
+        output_vars,
+    } = spec;
+
+    // Plan each branch over its own atoms. Every output variable must be bound
+    // by the branch (so it can be materialized), even if the branch itself does
+    // not otherwise use it, so mark them as used.
+    let branches: Vec<UnionBranch> = branch_atoms
+        .iter()
+        .map(|atom_ids| {
+            let mut branch_ctx = restrict_context(&ctx, atom_ids);
+            for var in output_vars.iter() {
+                if let Some(vinfo) = branch_ctx.vars.get_mut(*var) {
+                    vinfo.used_in_rhs = true;
+                }
+            }
+            let (header, instrs) = plan_stages(&branch_ctx, strat);
+            UnionBranch {
+                atoms: Arc::new(branch_ctx.atoms),
+                header,
+                stages: JoinStages {
+                    instrs: Arc::new(instrs),
+                },
+            }
+        })
+        .collect();
+
+    let output_vars: SmallVec<[Variable; 8]> = output_vars.into_iter().collect();
+
+    // Block 0 is the union: a lone `Union` stage whose "action" (when run as a
+    // materialization block) keys the branch outputs on `output_vars`.
+    let union_stages = JoinStages {
+        instrs: Arc::new(vec![JoinStage::Union { branches }]),
+    };
+    let union_spec = MatSpec {
+        msg_vars: output_vars.iter().copied().collect(),
+        val_vars: smallvec![],
+    };
+    let blocks = vec![(union_stages, union_spec)];
+
+    // The continuation joins the atoms not in any branch, receiving
+    // `output_vars` as message variables from block 0. `plan_single_bag`
+    // produces exactly this: a prologue that scans the materialization and
+    // probes the continuation atoms by `output_vars`, followed by the join of
+    // the remaining continuation variables. Running those stages as the result
+    // block (with the rule's action) fires the action per match.
+    let cont_atom_ids: Vec<AtomId> = ctx
+        .atoms
+        .iter()
+        .map(|(id, _)| id)
+        .filter(|id| !branch_atoms.iter().any(|b| b.contains(id)))
+        .collect();
+    let mut cont_ctx = restrict_context(&ctx, &cont_atom_ids);
+    // The continuation must know about `output_vars` so the message-var prologue
+    // can match, even for output vars that appear only in the branches.
+    for var in output_vars.iter() {
+        if !cont_ctx.vars.contains_key(*var) {
+            cont_ctx.vars.insert(
+                *var,
+                VarInfo {
+                    occurrences: Default::default(),
+                    used_in_rhs: true,
+                    defined_in_rhs: false,
+                    name: None,
+                },
+            );
+        }
+    }
+
+    let mut n_used_in_bag = count_variable_usage_per_bag(std::slice::from_ref(&cont_ctx));
+    // Bump usage for output vars so `plan_single_bag` treats them as coming from
+    // the (single) prior block rather than pruning them.
+    for var in output_vars.iter() {
+        let count = n_used_in_bag.get_or_default(*var);
+        *count += 1;
+    }
+    let mut has_block_contributed = vec![false];
+    let (cont_header, result_block, _cont_spec) = plan_single_bag(
+        &mut cont_ctx,
+        &blocks,
+        &mut has_block_contributed,
+        &mut n_used_in_bag,
+        strat,
+    );
+
+    let blocks = blocks
+        .into_iter()
+        .map(|(stages, mat_spec)| (loop_lifting(stages), mat_spec))
+        .collect::<Vec<_>>();
+    let result_block = loop_lifting(result_block);
+
+    // The plan's atom set is the continuation atoms only; each branch carries
+    // its own atoms inside the `Union` stage. This keeps the execution-time
+    // `BindingInfo` (seeded from these atoms) free of branch atoms, so an empty
+    // branch relation does not abort the whole rule.
+    Plan::DecomposedPlan(DecomposedPlan {
+        atoms: Arc::new(cont_ctx.atoms),
+        header: cont_header,
+        stages: JoinStageBlocks { blocks },
+        result_block,
+        actions,
+    })
+}
+
 pub(crate) fn plan_query<'a>(query: Query, col_est: ColumnCardEst<'a>) -> Plan {
     let atoms = query.atoms;
     let ctx = PlanningContext {
@@ -1188,6 +1349,9 @@ pub(crate) fn plan_query<'a>(query: Query, col_est: ColumnCardEst<'a>) -> Plan {
         fun_deps: Arc::new(query.fun_deps),
         col_est,
     };
+    if let Some(union) = query.union {
+        return plan_union(ctx, query.plan_strategy, query.action, union);
+    }
     tree_decompose_and_plan(ctx, query.plan_strategy, query.action, query.no_decomp)
 }
 
diff --git a/core-relations/src/query.rs b/core-relations/src/query.rs
index 090263962..2e48d11ef 100644
--- a/core-relations/src/query.rs
+++ b/core-relations/src/query.rs
@@ -126,6 +126,7 @@ impl<'outer> RuleSetBuilder<'outer> {
                 plan_strategy: Default::default(),
                 fun_deps: Default::default(),
                 no_decomp: false,
+                union: None,
             },
         }
     }
@@ -306,6 +307,24 @@ impl<'outer, 'a> QueryBuilder<'outer, 'a> {
         self.query.no_decomp = no_decomp;
     }
 
+    /// Mark this query as a fused disjunction (`or`). `branch_atoms[i]` are the
+    /// [`AtomId`]s (as returned by [`add_atom`](Self::add_atom)) belonging to
+    /// branch `i`; every atom not listed in any branch is a "continuation"
+    /// atom, joined once against each branch output. `output_vars` are the
+    /// variables the branches bind that the continuation and action may read
+    /// (the variables common to every branch).
+    ///
+    /// A union query is always planned as a single bag (tree-decomposition is
+    /// skipped), and is intended to be run in naive mode (seminaive delta
+    /// through a union is not supported).
+    pub fn set_union(&mut self, branch_atoms: Vec<Vec<AtomId>>, output_vars: Vec<Variable>) {
+        self.query.no_decomp = true;
+        self.query.union = Some(UnionSpec {
+            branch_atoms,
+            output_vars,
+        });
+    }
+
     /// Create a new variable of the given type.
     pub fn new_var(&mut self) -> Variable {
         self.query.var_info.push(VarInfo {
@@ -1048,4 +1067,23 @@ pub(crate) struct Query {
     /// [`crate::free_join::plan::tree_decompose_and_plan`]. Set via
     /// [`QueryBuilder::set_no_decomp`].
     pub(crate) no_decomp: bool,
+    /// A disjunction (`or`) in the query, if present. See [`UnionSpec`] and
+    /// [`QueryBuilder::set_union`]. When set, the query is planned as a fused
+    /// union: each branch is planned over its own atoms and enumerated at
+    /// runtime to produce the `output_vars`, and the remaining
+    /// ("continuation") atoms are joined against those bindings exactly once.
+    pub(crate) union: Option<UnionSpec>,
+}
+
+/// Describes a disjunction (`or`) embedded in a query. The atoms of each branch
+/// and the "continuation" atoms (everything not in a branch) share one atom /
+/// variable namespace. `output_vars` are the variables a branch binds that the
+/// continuation and action may use — the variables common to every branch.
+#[derive(Debug, Clone)]
+pub(crate) struct UnionSpec {
+    /// The atoms belonging to each branch of the disjunction.
+    pub(crate) branch_atoms: Vec<Vec<AtomId>>,
+    /// The variables produced by the union (common to every branch) that flow
+    /// into the continuation and the action.
+    pub(crate) output_vars: Vec<Variable>,
 }
diff --git a/docs/disjunction-design.md b/docs/disjunction-design.md
new file mode 100644
index 000000000..849423e40
--- /dev/null
+++ b/docs/disjunction-design.md
@@ -0,0 +1,148 @@
+# Disjunction (`or`) in rule bodies
+
+## Surface syntax
+
+A rule body may contain a disjunction fact:
+
+```
+(rule (C
+       (or (branch-1-fact ...)
+           (branch-2-fact ...)
+           ...))
+      (action ...))
+```
+
+Each branch is a parenthesized *list of facts* (a conjunction). The body
+`C ∧ (D₁ ∨ … ∨ Dₙ)` matches when the surrounding conjunction `C` holds and at
+least one branch `Dᵢ` holds.
+
+## Semantics
+
+- **Common variables.** `V = ⋂ᵢ vars(Dᵢ)` — the variables that appear in every
+  branch. Only `V`, together with the variables bound by the surrounding
+  conjunction `C`, are visible in the action and elsewhere outside the `or`.
+- **Branch-local variables.** A variable that appears in some branch but is not
+  in `V` is *branch-local*. Branch-locals in different branches are independent:
+  during typechecking they are renamed to fresh names so their sorts are not
+  conflated. A branch-local variable that is used outside its `or` is a type
+  error (`TypeError::OrBranchLocalEscapes`).
+- **Empty branch.** A branch with no facts is a type error
+  (`TypeError::EmptyOrBranch`).
+- **Scope.** `or` is only supported inside rule bodies (including the `:when`
+  conditions of a `rewrite`, which desugar to rules). It is rejected in
+  query-shaped commands like `check` and `query`
+  (`TypeError::OrOutsideRule`).
+
+## Frontend pipeline
+
+1. **AST** — `egglog-ast/src/generic_ast.rs`: `GenericFact::Or(Span,
+   Vec<Vec<GenericFact<Head, Leaf>>>)`. `Display`, `visit_exprs`, `map_exprs`,
+   and `map_symbols` recurse into the branches
+   (`egglog-ast/src/generic_ast_helpers.rs`).
+2. **Parsing** — `src/ast/parse.rs`: `parse_fact` recognises the `OR_HEAD`
+   (`"or"`) head and parses each argument as a list of facts.
+3. **Typechecking** — `src/typechecking.rs` `typecheck_rule`:
+   - `rename_or_locals` renames each branch's branch-local variables to fresh
+     names (independently per branch) and enforces the interface rule
+     (branch-locals may not escape their `or`). `outside_vars` is the set of
+     variables visible outside every `or`: conjunctive-fact variables, action
+     variables, and each `or`'s common variables.
+   - `Facts::to_query` (`src/ast/mod.rs`) flattens every branch's atoms into one
+     shared constraint `Query` so the constraint solver assigns a sort to every
+     variable — common variables (whose sort is thereby unified across branches
+     and with `C`) and the already-renamed branch-locals.
+   - `Assignment::annotate_fact` (`src/constraint.rs`) reconstructs a
+     `ResolvedFact::Or` with the resolved branches.
+   - `src/ast/check_shadowing.rs` recurses into `or` branches when collecting
+     pattern variable names.
+
+## Backend compilation: Strategy C — a fused union node in the free-join engine
+
+An `or`-containing rule compiles to **one** backend rule with a fused union node
+in the free-join engine. The surrounding conjunction `C` is scanned **once**;
+the branches are enumerated additively (never a `∏` of separate rules).
+
+### egglog crate (`src/lib.rs`, `add_or_rule`)
+
+`add_rule` dispatches `or`-containing rules to `add_or_rule`, which:
+
+1. Splits the body into the conjunction `C` (non-`or` facts) and the `or`s, and
+   forms the union's **branches** as the cartesian product of every `or`'s
+   disjuncts (`expand_or_branch` expands nested `or`s the same way). One `or`
+   gives one branch per disjunct; multiple/nested `or`s give `∏` *branches* (but
+   still one rule, and `C` is still scanned once).
+2. Computes the union's **output variables** (`common_branch_vars`): the
+   variables common to every branch — exactly the variables an `or` shares
+   across its disjuncts, which are the only branch variables visible to `C` and
+   the action.
+3. Compiles `C`'s query and the rule's actions together
+   (`to_canonicalized_core_rule_extra_binding`) so their flattened
+   (fresh-`gensym`) variables agree, adding the output variables to the action
+   binding (they are bound by the union at runtime, not by `C`'s atoms).
+4. Compiles each branch's query on its own
+   (`to_canonicalized_core_rule_ungrounded`; the grounded check is skipped since
+   a branch variable may be grounded by `C`).
+5. Builds one backend rule: adds `C`'s atoms (`BackendRule::query`), then each
+   branch's atoms (`query_union_branch`, recording their `AtomId`s), calls
+   `set_union_branches`, and adds the actions. The rule is compiled in **naive**
+   mode (seminaive delta through a union is unsupported). Branch atoms must be
+   table atoms; a primitive inside a branch is rejected.
+
+### Bridge (`egglog-bridge/src/rule.rs`)
+
+`RuleBuilder::set_union_branches(branch_atoms, output_vars)` records the branch
+atom groups and output variables on the bridge `Query`. `Query::build_cached_plan`
+translates the high-level atom indices / variable ids into the core-relations
+`AtomId`s / `Variable`s allocated when the atoms were added, and calls
+`QueryBuilder::set_union`.
+
+### core-relations (`query.rs`, `free_join/plan.rs`, `free_join/execute.rs`)
+
+- `Query` gains an optional `union: Option<UnionSpec>` (`branch_atoms`,
+  `output_vars`), set by `QueryBuilder::set_union` (which also forces
+  single-bag planning).
+- `plan.rs` adds `JoinStage::Union { branches: Vec<UnionBranch> }`, where each
+  `UnionBranch` is a self-contained sub-plan (its own atoms, header, and
+  stages). `plan_union` produces a **`DecomposedPlan`**:
+  - **Block 0** is the lone `Union` stage. `plan_union` plans each branch over
+    its own atoms (`restrict_context` + `plan_stages`), marking the output
+    variables `used_in_rhs` so the branch binds them. The block's `MatSpec`
+    keys on the output variables.
+  - The **result block** is the continuation: the atoms of `C`, planned with
+    `plan_single_bag` treating the output variables as message variables coming
+    from block 0. This reuses the tree-decomposition message-passing machinery:
+    a `FusedIntersectMat { mode: KeyOnly }` prologue iterates the distinct
+    output tuples and probes `C`'s atoms by them via their indexes, then the
+    rest of `C` is joined and the action fires.
+  - The plan's `atoms` are `C`'s atoms only; each branch carries its own atoms,
+    so an empty branch relation cannot abort the whole rule.
+- `execute.rs` handles `JoinStage::Union` in `run_plan`: for each branch it
+  seeds a fresh `BindingInfo` from the branch's atoms, applies the branch
+  header, and runs the branch's stages via `run_join_stages` with the enclosing
+  block's `action`/`action_buf`. Because block 0 runs with the block's
+  `InPlaceMaterializer`, each branch match is written into one materialization
+  keyed on the output variables — **deduplicated on the key**, in memory, with
+  no temporary database table. The result block then joins `C` once against
+  that materialization.
+
+This shares `C`: it is evaluated a single time in the result block, joined by
+index against the deduplicated union of the branch outputs — never re-scanned per
+branch and never producing `∏` separate rules.
+
+### Tradeoffs / restrictions
+
+- **Naive evaluation.** `or` rules match the whole database each iteration
+  (seminaive delta through a union is not supported).
+- **Primitives in branches** are rejected (a branch must be a conjunction of
+  table atoms). Primitives in the surrounding conjunction `C` are fine.
+- **`∏` branches for multiple/nested `or`s.** `k` disjunctions produce `∏`
+  union *branches* (enumerated additively into one materialization), but still a
+  single rule with `C` scanned once — unlike rule-splitting, which would create
+  `∏` rules each re-scanning `C`. A single `or` (the common case) is linear.
+- **No cross-branch dedup of firings beyond the output key.** The union
+  deduplicates output tuples; like every egglog rule, the action still fires per
+  full match otherwise. This matches egglog's normal non-dedup semantics and is
+  invisible for idempotent actions.
+- **Proofs.** `or` is not supported with the proof / term encoding; the proof
+  passes panic if they ever see an `or` fact (they never do, because proof mode
+  compiles only proof-instrumented rules).
diff --git a/egglog-ast/src/generic_ast.rs b/egglog-ast/src/generic_ast.rs
index cf8a29c00..3117ca671 100644
--- a/egglog-ast/src/generic_ast.rs
+++ b/egglog-ast/src/generic_ast.rs
@@ -35,6 +35,11 @@ pub enum GenericExpr<Head, Leaf> {
 pub enum GenericFact<Head, Leaf> {
     Eq(Span, GenericExpr<Head, Leaf>, GenericExpr<Head, Leaf>),
     Fact(GenericExpr<Head, Leaf>),
+    /// A disjunction `(or (branch...) (branch...) ...)`. Each branch is a
+    /// conjunction (list) of facts. The disjunction matches when at least one
+    /// branch matches. Only variables common to every branch (plus variables
+    /// bound by the surrounding conjunction) are visible outside the `or`.
+    Or(Span, Vec<Vec<GenericFact<Head, Leaf>>>),
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
diff --git a/egglog-ast/src/generic_ast_helpers.rs b/egglog-ast/src/generic_ast_helpers.rs
index e3b0b84fc..d70d756b6 100644
--- a/egglog-ast/src/generic_ast_helpers.rs
+++ b/egglog-ast/src/generic_ast_helpers.rs
@@ -98,6 +98,13 @@ impl<Head: Display, Leaf: Display> Display for GenericFact<Head, Leaf> {
         match self {
             GenericFact::Eq(_, e1, e2) => write!(f, "(= {e1} {e2})"),
             GenericFact::Fact(expr) => write!(f, "{expr}"),
+            GenericFact::Or(_, branches) => {
+                write!(f, "(or")?;
+                for branch in branches {
+                    write!(f, " ({})", ListDisplay(branch, " "))?;
+                }
+                write!(f, ")")
+            }
         }
     }
 }
@@ -533,6 +540,13 @@ where
                 GenericFact::Eq(span, e1.visit_exprs(f), e2.visit_exprs(f))
             }
             GenericFact::Fact(expr) => GenericFact::Fact(expr.visit_exprs(f)),
+            GenericFact::Or(span, branches) => GenericFact::Or(
+                span,
+                branches
+                    .into_iter()
+                    .map(|branch| branch.into_iter().map(|fact| fact.visit_exprs(f)).collect())
+                    .collect(),
+            ),
         }
     }
 
@@ -543,6 +557,13 @@ where
         match self {
             GenericFact::Eq(span, e1, e2) => GenericFact::Eq(span.clone(), f(e1), f(e2)),
             GenericFact::Fact(expr) => GenericFact::Fact(f(expr)),
+            GenericFact::Or(span, branches) => GenericFact::Or(
+                span.clone(),
+                branches
+                    .iter()
+                    .map(|branch| branch.iter().map(|fact| fact.map_exprs(f)).collect())
+                    .collect(),
+            ),
         }
     }
 
@@ -575,6 +596,18 @@ where
                 GenericFact::Eq(span, e1.map_symbols(head, leaf), e2.map_symbols(head, leaf))
             }
             GenericFact::Fact(expr) => GenericFact::Fact(expr.map_symbols(head, leaf)),
+            GenericFact::Or(span, branches) => GenericFact::Or(
+                span,
+                branches
+                    .into_iter()
+                    .map(|branch| {
+                        branch
+                            .into_iter()
+                            .map(|fact| fact.map_symbols(head, leaf))
+                            .collect()
+                    })
+                    .collect(),
+            ),
         }
     }
 
diff --git a/egglog-bridge/src/lib.rs b/egglog-bridge/src/lib.rs
index ed427216c..a5468e4a1 100644
--- a/egglog-bridge/src/lib.rs
+++ b/egglog-bridge/src/lib.rs
@@ -38,7 +38,7 @@ pub(crate) mod rule;
 #[cfg(test)]
 mod tests;
 
-pub use rule::{Function, QueryEntry, RuleBuilder};
+pub use rule::{AtomId, Function, QueryEntry, RuleBuilder, Variable};
 use thiserror::Error;
 
 /// A live registry of action handles for use by typed primitives.
diff --git a/egglog-bridge/src/rule.rs b/egglog-bridge/src/rule.rs
index 8a4a7da12..415858d75 100644
--- a/egglog-bridge/src/rule.rs
+++ b/egglog-bridge/src/rule.rs
@@ -120,6 +120,14 @@ pub(crate) struct Query {
     /// If `true`, skip tree-decomposition during query planning. See
     /// [`core_relations::QueryBuilder::set_no_decomp`].
     no_decomp: bool,
+    /// A disjunction (`or`) in this rule's query, if any. Each element of
+    /// `branch_atoms` lists the [`AtomId`]s (returned by `query_table` /
+    /// `query_prim`-style atom builders) that belong to one branch; every atom
+    /// not listed is a "continuation" atom of the surrounding conjunction.
+    /// `output_vars` are the variables the branches bind that flow into the
+    /// continuation and the action (the variables common to every branch). See
+    /// [`core_relations::QueryBuilder::set_union`].
+    union: Option<(Vec<Vec<AtomId>>, Vec<VariableId>)>,
 }
 
 pub struct RuleBuilder<'a> {
@@ -151,6 +159,7 @@ impl EGraph {
                 add_rule: Default::default(),
                 plan_strategy: Default::default(),
                 no_decomp: false,
+                union: None,
             },
         }
     }
@@ -194,6 +203,26 @@ impl RuleBuilder<'_> {
         self.query.no_decomp = no_decomp;
     }
 
+    /// Mark this rule's query as a fused disjunction (`or`). `branch_atoms[i]`
+    /// are the [`AtomId`]s belonging to branch `i` (as returned by the atom
+    /// builders such as `query_table`); every atom not listed is a
+    /// "continuation" atom of the surrounding conjunction. `output_vars` are the
+    /// variables the branches bind that the continuation and the action may read
+    /// (the variables common to every branch). See
+    /// [`core_relations::QueryBuilder::set_union`].
+    ///
+    /// A union rule is run in naive mode (seminaive delta through a union is not
+    /// supported), so callers should construct it via
+    /// `new_rule(desc, /* seminaive */ false)`.
+    pub fn set_union_branches(
+        &mut self,
+        branch_atoms: Vec<Vec<AtomId>>,
+        output_vars: Vec<Variable>,
+    ) {
+        let output_var_ids = output_vars.into_iter().map(|v| v.id).collect();
+        self.query.union = Some((branch_atoms, output_var_ids));
+    }
+
     /// Get the canonical value of an id in the union-find. An internal-only
     /// routine used to implement rebuilding.
     ///
@@ -764,6 +793,29 @@ impl Query {
         for (table, entries, _schema_info) in &self.atoms {
             atom_mapping.push(add_atom(&mut qb, *table, entries, &[], &mut inner)?);
         }
+        if let Some((branch_atoms, output_var_ids)) = &self.union {
+            // Translate the high-level atom indices / variable ids into the
+            // core-relations atom ids / variables allocated above.
+            let core_branches: Vec<Vec<core_relations::AtomId>> = branch_atoms
+                .iter()
+                .map(|branch| {
+                    branch
+                        .iter()
+                        .map(|atom| atom_mapping[atom.index()])
+                        .collect()
+                })
+                .collect();
+            let core_output_vars: Vec<core_relations::Variable> = output_var_ids
+                .iter()
+                .map(|id| match inner.mapping[*id] {
+                    DstVar::Var(v) => v,
+                    DstVar::Const(_) => {
+                        panic!("union output variable must be a query variable, not a constant")
+                    }
+                })
+                .collect();
+            qb.set_union(core_branches, core_output_vars);
+        }
         let rule_id = self.run_rules_and_build(qb, inner, desc)?;
         let rs = rsb.build();
         let plan = Arc::new(rs.build_cached_plan(rule_id));
diff --git a/src/ast/check_shadowing.rs b/src/ast/check_shadowing.rs
index 7e808dff7..7f2f15504 100644
--- a/src/ast/check_shadowing.rs
+++ b/src/ast/check_shadowing.rs
@@ -103,18 +103,29 @@ impl Names {
             }
         }
 
-        let mut collected = HashMap::default();
-
-        for fact in query {
+        fn collect_fact_names(fact: &ResolvedFact, out: &mut HashMap<String, Span>) {
             match fact {
                 ResolvedFact::Eq(_span, e1, e2) => {
-                    collect_expr_names(e1, &mut collected);
-                    collect_expr_names(e2, &mut collected);
+                    collect_expr_names(e1, out);
+                    collect_expr_names(e2, out);
+                }
+                ResolvedFact::Fact(e) => collect_expr_names(e, out),
+                ResolvedFact::Or(_span, branches) => {
+                    for branch in branches {
+                        for fact in branch {
+                            collect_fact_names(fact, out);
+                        }
+                    }
                 }
-                ResolvedFact::Fact(e) => collect_expr_names(e, &mut collected),
             }
         }
 
+        let mut collected = HashMap::default();
+
+        for fact in query {
+            collect_fact_names(fact, &mut collected);
+        }
+
         for (name, span) in collected {
             self.check_pattern_name(&name, &span)?;
         }
diff --git a/src/ast/mod.rs b/src/ast/mod.rs
index 4d1126dce..6aa6a08cb 100644
--- a/src/ast/mod.rs
+++ b/src/ast/mod.rs
@@ -23,7 +23,9 @@ pub use parse::*;
 #[derive(Clone, Debug)]
 /// The egglog internal representation of already compiled rules
 pub(crate) enum Ruleset {
-    /// Represents a ruleset with a set of rules.
+    /// Represents a ruleset with a set of rules. Each named rule compiles to a
+    /// single backend rule (a rule whose body contains `or` uses a fused union
+    /// node, still a single backend rule).
     Rules(IndexMap<String, (ResolvedCoreRule, egglog_bridge::RuleId)>),
     /// A combined ruleset may contain other rulesets.
     Combined(Vec<String>),
@@ -1427,6 +1429,21 @@ where
                     atoms.extend(child_atoms);
                     new_body.push(GenericFact::Fact(expr));
                 }
+                GenericFact::Or(span, branches) => {
+                    // Flatten each branch into atoms of the shared query so the
+                    // constraint solver infers a sort for every variable
+                    // (common vars and the already-renamed branch-locals).
+                    // Branch-local renaming happens upstream in
+                    // `typecheck_rule` before `to_query` is called.
+                    let mut mapped_branches = Vec::with_capacity(branches.len());
+                    for branch in branches {
+                        let (branch_query, mapped_branch) =
+                            Facts(branch.clone()).to_query(typeinfo, fresh_gen);
+                        atoms.extend(branch_query.atoms);
+                        mapped_branches.push(mapped_branch);
+                    }
+                    new_body.push(GenericFact::Or(span.clone(), mapped_branches));
+                }
             }
         }
         (Query { atoms }, new_body)
diff --git a/src/ast/parse.rs b/src/ast/parse.rs
index 4d0aebb5e..83da9d500 100644
--- a/src/ast/parse.rs
+++ b/src/ast/parse.rs
@@ -23,6 +23,9 @@ macro_rules! span {
 // differently to different parse errors. The benefit of this is that
 // error messages are defined in the same place that they are created,
 // making it easier to improve errors over time.
+/// The head symbol for a disjunction fact `(or (branch...) ...)`.
+pub const OR_HEAD: &str = "or";
+
 #[derive(Debug, Error)]
 pub struct ParseError(pub Span, pub String);
 
@@ -906,6 +909,16 @@ impl Parser {
                 [e1, e2] => Fact::Eq(span, self.parse_expr(e1)?, self.parse_expr(e2)?),
                 _ => return error!(span, "usage: (= <expr> <expr>)"),
             },
+            OR_HEAD => {
+                // `(or (branch...) (branch...) ...)`: each branch is a
+                // parenthesized list of facts.
+                let mut branches = Vec::with_capacity(tail.len());
+                for branch_sexp in tail {
+                    let facts = branch_sexp.expect_list("or branch (a list of facts)")?;
+                    branches.push(map_fallible(facts, self, Self::parse_fact)?);
+                }
+                Fact::Or(span, branches)
+            }
             _ => Fact::Fact(self.parse_expr(sexp)?),
         })
     }
diff --git a/src/constraint.rs b/src/constraint.rs
index 3267a58be..d0895bcd0 100644
--- a/src/constraint.rs
+++ b/src/constraint.rs
@@ -570,6 +570,13 @@ impl Assignment<AtomTerm, ArcSort> {
                 self.annotate_expr(e2, typeinfo, ctx),
             ),
             GenericFact::Fact(expr) => ResolvedFact::Fact(self.annotate_expr(expr, typeinfo, ctx)),
+            GenericFact::Or(span, branches) => ResolvedFact::Or(
+                span.clone(),
+                branches
+                    .iter()
+                    .map(|branch| self.annotate_facts(branch, typeinfo, ctx))
+                    .collect(),
+            ),
         }
     }
 
diff --git a/src/core.rs b/src/core.rs
index d0dd46dfd..3a44d2092 100644
--- a/src/core.rs
+++ b/src/core.rs
@@ -1128,6 +1128,31 @@ pub(crate) trait ResolvedRuleExt {
         fresh_gen: &mut SymbolGen,
         union_to_set_optimization: bool,
     ) -> Result<ResolvedCoreRule, TypeError>;
+
+    /// Like [`Self::to_canonicalized_core_rule`] but skips the groundedness
+    /// check. Used to flatten a single branch of an `or` in isolation, where a
+    /// variable may be grounded by the surrounding conjunction rather than by
+    /// the branch itself.
+    fn to_canonicalized_core_rule_ungrounded(
+        &self,
+        typeinfo: &TypeInfo,
+        fresh_gen: &mut SymbolGen,
+        union_to_set_optimization: bool,
+    ) -> Result<ResolvedCoreRule, TypeError>;
+
+    /// Like [`Self::to_canonicalized_core_rule_ungrounded`] but treats the given
+    /// variable names as already bound when lowering the actions (in addition to
+    /// the query's own variables). Used for the surrounding conjunction of an
+    /// `or`: the `or`'s output variables are bound by the fused union at
+    /// runtime, so the actions may reference them even though they do not appear
+    /// in the conjunction's own atoms.
+    fn to_canonicalized_core_rule_extra_binding(
+        &self,
+        typeinfo: &TypeInfo,
+        fresh_gen: &mut SymbolGen,
+        union_to_set_optimization: bool,
+        extra_binding: &[ResolvedVar],
+    ) -> Result<ResolvedCoreRule, TypeError>;
 }
 
 impl ResolvedRuleExt for ResolvedRule {
@@ -1159,6 +1184,60 @@ impl ResolvedRuleExt for ResolvedRule {
 
         Ok(rule)
     }
+
+    fn to_canonicalized_core_rule_ungrounded(
+        &self,
+        typeinfo: &TypeInfo,
+        fresh_gen: &mut SymbolGen,
+        union_to_set_optimization: bool,
+    ) -> Result<ResolvedCoreRule, TypeError> {
+        let value_eq = &typeinfo.get_prims("value-eq").unwrap()[0];
+        let value_eq = |at1: &ResolvedAtomTerm, at2: &ResolvedAtomTerm| {
+            ResolvedCall::Primitive(SpecializedPrimitive {
+                prim_with_id: value_eq.clone(),
+                input: vec![at1.output(), at2.output()],
+                output: UnitSort.to_arcsort(),
+            })
+        };
+        let rule = self.to_core_rule(typeinfo, fresh_gen, union_to_set_optimization)?;
+        let rule = rule.canonicalize(&value_eq);
+        let rule = rule.remove_dup_vars(value_eq);
+        Ok(rule)
+    }
+
+    fn to_canonicalized_core_rule_extra_binding(
+        &self,
+        typeinfo: &TypeInfo,
+        fresh_gen: &mut SymbolGen,
+        union_to_set_optimization: bool,
+        extra_binding: &[ResolvedVar],
+    ) -> Result<ResolvedCoreRule, TypeError> {
+        let value_eq = &typeinfo.get_prims("value-eq").unwrap()[0];
+        let value_eq = |at1: &ResolvedAtomTerm, at2: &ResolvedAtomTerm| {
+            ResolvedCall::Primitive(SpecializedPrimitive {
+                prim_with_id: value_eq.clone(),
+                input: vec![at1.output(), at2.output()],
+                output: UnitSort.to_arcsort(),
+            })
+        };
+
+        let (body, _correspondence) = Facts(self.body.clone()).to_query(typeinfo, fresh_gen);
+        let mut binding = body.get_vars();
+        for var in extra_binding {
+            binding.insert(var.clone());
+        }
+        let mut ctx =
+            CoreActionContext::new(typeinfo, &mut binding, fresh_gen, union_to_set_optimization);
+        let (head, _correspondence) = self.head.to_core_actions(&mut ctx)?;
+        let rule = GenericCoreRule {
+            span: self.span.clone(),
+            body,
+            head,
+        };
+        let rule = rule.canonicalize(&value_eq);
+        let rule = rule.remove_dup_vars(value_eq);
+        Ok(rule)
+    }
 }
 
 #[cfg(test)]
diff --git a/src/lib.rs b/src/lib.rs
index 1fe33855e..ab9594db8 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1134,15 +1134,6 @@ impl EGraph {
     }
 
     fn add_rule(&mut self, rule: ast::ResolvedRule) -> Result<String, Error> {
-        // Disable union_to_set optimization in proof or term encoding mode, since
-        // it expects only `union` on constructors (not set).
-        let core_rule = rule.to_canonicalized_core_rule(
-            &self.type_info,
-            &mut self.parser.symbol_gen,
-            self.proof_state.original_typechecking.is_none(),
-        )?;
-        let (query, actions) = (&core_rule.body, &core_rule.head);
-
         // The `:naive` rule option opts a single rule out of seminaive
         // evaluation. This widens primitive-context selection from
         // Pure/Write to Read/Full, so primitives that read or write the
@@ -1158,14 +1149,40 @@ impl EGraph {
                 RuleEvalMode::Naive | RuleEvalMode::UnsafeSeminaive
             );
 
-        let rule_id = {
-            let mut rb = self.backend.new_rule(&rule.name, seminaive);
-            rb.set_no_decomp(no_decomp);
-            let mut translator =
-                BackendRule::new(rb, &self.functions, &self.type_info, requires_read_context);
-            translator.query(query, rule.include_subsumed);
-            translator.actions(actions)?;
-            translator.build()
+        // Disable union_to_set optimization in proof or term encoding mode, since
+        // it expects only `union` on constructors (not set).
+        let union_to_set = self.proof_state.original_typechecking.is_none();
+
+        let has_or = rule
+            .body
+            .iter()
+            .any(|f| matches!(f, ast::ResolvedFact::Or(..)));
+
+        let (stored_core_rule, rule_id) = if has_or {
+            self.add_or_rule(
+                &rule,
+                union_to_set,
+                seminaive,
+                no_decomp,
+                requires_read_context,
+            )?
+        } else {
+            let core_rule = rule.to_canonicalized_core_rule(
+                &self.type_info,
+                &mut self.parser.symbol_gen,
+                union_to_set,
+            )?;
+            let (query, actions) = (&core_rule.body, &core_rule.head);
+            let rule_id = {
+                let mut rb = self.backend.new_rule(&rule.name, seminaive);
+                rb.set_no_decomp(no_decomp);
+                let mut translator =
+                    BackendRule::new(rb, &self.functions, &self.type_info, requires_read_context);
+                translator.query(query, rule.include_subsumed);
+                translator.actions(actions)?;
+                translator.build()
+            };
+            (core_rule, rule_id)
         };
 
         if let Some(rules) = self.rulesets.get_mut(&rule.ruleset) {
@@ -1176,7 +1193,7 @@ impl EGraph {
                             let name = rule.name;
                             panic!("Rule '{name}' was already present")
                         }
-                        indexmap::map::Entry::Vacant(e) => e.insert((core_rule, rule_id)),
+                        indexmap::map::Entry::Vacant(e) => e.insert((stored_core_rule, rule_id)),
                     };
                     Ok(rule.name)
                 }
@@ -1187,6 +1204,129 @@ impl EGraph {
         }
     }
 
+    /// Compiles a rule whose body contains one or more `or` facts into a single
+    /// backend rule using a fused union in the free-join engine. The surrounding
+    /// conjunction is joined once against the deduplicated union of the branch
+    /// outputs (see [`egglog_bridge::RuleBuilder::set_union_branches`] and
+    /// `core_relations::QueryBuilder::set_union`). Runs in naive mode.
+    fn add_or_rule(
+        &mut self,
+        rule: &ast::ResolvedRule,
+        union_to_set: bool,
+        _seminaive: bool,
+        no_decomp: bool,
+        requires_read_context: bool,
+    ) -> Result<(core::ResolvedCoreRule, egglog_bridge::RuleId), Error> {
+        // Split the body into the surrounding conjunction and the `or`s, then
+        // form the union's branches as the cartesian product of every `or`'s
+        // branches (each combined branch is a conjunction, with nested `or`s
+        // expanded the same way). A single `or` gives one branch per disjunct.
+        let mut conj_facts: Vec<ast::ResolvedFact> = Vec::new();
+        let mut combined_branches: Vec<Vec<ast::ResolvedFact>> = vec![vec![]];
+        for fact in &rule.body {
+            match fact {
+                ast::ResolvedFact::Or(_, branches) => {
+                    let branch_expansions: Vec<Vec<ast::ResolvedFact>> =
+                        branches.iter().flat_map(|b| expand_or_branch(b)).collect();
+                    let mut next =
+                        Vec::with_capacity(combined_branches.len() * branch_expansions.len());
+                    for combo in &combined_branches {
+                        for expansion in &branch_expansions {
+                            let mut new_combo = combo.clone();
+                            new_combo.extend(expansion.iter().cloned());
+                            next.push(new_combo);
+                        }
+                    }
+                    combined_branches = next;
+                }
+                other => conj_facts.push(other.clone()),
+            }
+        }
+
+        // The variables visible outside the `or`s (shared with the surrounding
+        // conjunction and the action) are the union's output variables: the
+        // variables that appear in every branch of an `or`. We take, for each
+        // combined branch, the intersection of variable sets across all combined
+        // branches — a variable common to every combined branch is exactly a
+        // variable common to every disjunct of every `or`.
+        let output_resolved_vars = common_branch_vars(&combined_branches);
+
+        // Compile the surrounding conjunction's query and the rule's actions
+        // together, so their flattened (fresh) variables are consistent. The
+        // `or`'s output variables are added to the action binding: they are not
+        // in the conjunction's atoms but are bound by the fused union at
+        // runtime, and the actions may read them.
+        let conj_rule = ast::ResolvedRule {
+            span: rule.span.clone(),
+            head: rule.head.clone(),
+            body: conj_facts.clone(),
+            name: rule.name.clone(),
+            ruleset: rule.ruleset.clone(),
+            eval_mode: rule.eval_mode,
+            no_decomp: rule.no_decomp,
+            include_subsumed: rule.include_subsumed,
+        };
+        let core_conj = conj_rule.to_canonicalized_core_rule_extra_binding(
+            &self.type_info,
+            &mut self.parser.symbol_gen,
+            union_to_set,
+            &output_resolved_vars,
+        )?;
+
+        // Flatten each combined branch into a canonicalized core query. The
+        // grounded check is skipped: a branch variable may be grounded by the
+        // surrounding conjunction rather than the branch.
+        let mut branch_queries: Vec<core::Query<ResolvedCall, ResolvedVar>> =
+            Vec::with_capacity(combined_branches.len());
+        for branch in &combined_branches {
+            let branch_rule = ast::ResolvedRule {
+                span: rule.span.clone(),
+                head: Default::default(),
+                body: branch.clone(),
+                name: rule.name.clone(),
+                ruleset: rule.ruleset.clone(),
+                eval_mode: rule.eval_mode,
+                no_decomp: rule.no_decomp,
+                include_subsumed: rule.include_subsumed,
+            };
+            let core_branch = branch_rule.to_canonicalized_core_rule_ungrounded(
+                &self.type_info,
+                &mut self.parser.symbol_gen,
+                union_to_set,
+            )?;
+            branch_queries.push(core_branch.body);
+        }
+
+        // Build the backend rule. Union rules run in naive mode (seminaive
+        // delta through a union is unsupported).
+        let rule_id = {
+            let mut rb = self.backend.new_rule(&rule.name, false);
+            rb.set_no_decomp(no_decomp);
+            let mut translator =
+                BackendRule::new(rb, &self.functions, &self.type_info, requires_read_context);
+            // Continuation (surrounding conjunction) atoms.
+            translator.query(&core_conj.body, rule.include_subsumed);
+            // Branch atoms, recording which backend AtomIds belong to each branch.
+            let mut branch_atom_ids = Vec::with_capacity(branch_queries.len());
+            for branch_query in &branch_queries {
+                let ids = translator.query_union_branch(branch_query, rule.include_subsumed)?;
+                branch_atom_ids.push(ids);
+            }
+            // The output variables, as backend query variables.
+            let output_vars = output_resolved_vars
+                .iter()
+                .map(|v| translator.union_output_var(v, rule.span.clone()))
+                .collect::<Result<Vec<_>, _>>()?;
+            translator
+                .rb
+                .set_union_branches(branch_atom_ids, output_vars);
+            translator.actions(&core_conj.head)?;
+            translator.build()
+        };
+
+        Ok((core_conj, rule_id))
+    }
+
     fn eval_actions(&mut self, actions: &ResolvedActions) -> Result<(), Error> {
         let mut binding = IndexSet::default();
         let mut ctx = CoreActionContext::new(
@@ -2688,6 +2828,56 @@ impl<'a> BackendRule<'a> {
         }
     }
 
+    /// Adds the atoms of one `or` branch, returning their backend [`AtomId`]s so
+    /// the caller can register them as a union branch. All atoms in a branch
+    /// must be table (function/relation) atoms; primitives inside a branch are
+    /// not supported by the fused union.
+    fn query_union_branch(
+        &mut self,
+        query: &core::Query<ResolvedCall, ResolvedVar>,
+        include_subsumed: bool,
+    ) -> Result<Vec<egglog_bridge::AtomId>, Error> {
+        let mut atom_ids = Vec::with_capacity(query.atoms.len());
+        for atom in &query.atoms {
+            match &atom.head {
+                ResolvedCall::Func(f) => {
+                    let f = self.func(f);
+                    let args = self.args(&atom.args);
+                    let is_subsumed = match include_subsumed {
+                        true => None,
+                        false => Some(false),
+                    };
+                    atom_ids.push(self.rb.query_table(f, &args, is_subsumed).unwrap());
+                }
+                ResolvedCall::Primitive(p) => {
+                    return Err(Error::BackendError(format!(
+                        "primitive `{}` is not supported inside an `or` branch",
+                        p.name()
+                    )));
+                }
+            }
+        }
+        Ok(atom_ids)
+    }
+
+    /// Resolves an `or` output variable (a variable common to every branch) to
+    /// its backend [`egglog_bridge::Variable`]. The variable must already have
+    /// been introduced by a branch atom.
+    fn union_output_var(
+        &mut self,
+        var: &ResolvedVar,
+        span: Span,
+    ) -> Result<egglog_bridge::Variable, Error> {
+        let term = core::GenericAtomTerm::Var(span.clone(), var.clone());
+        match self.entry(&term) {
+            QueryEntry::Var(v) => Ok(v),
+            QueryEntry::Const { .. } => Err(Error::BackendError(format!(
+                "{span}: `or` output variable `{}` did not resolve to a query variable",
+                var.name
+            ))),
+        }
+    }
+
     fn actions(&mut self, actions: &core::ResolvedCoreActions) -> Result<(), Error> {
         for action in &actions.0 {
             match action {
@@ -2760,6 +2950,69 @@ impl<'a> BackendRule<'a> {
     }
 }
 
+/// Expands one `or` branch (a conjunction of facts that may itself contain
+/// nested `or`s) into a list of purely-conjunctive fact lists — one per
+/// combination of the nested disjuncts. A branch with no nested `or` yields a
+/// single fact list equal to itself.
+fn expand_or_branch(branch: &[ast::ResolvedFact]) -> Vec<Vec<ast::ResolvedFact>> {
+    let mut combos: Vec<Vec<ast::ResolvedFact>> = vec![vec![]];
+    for fact in branch {
+        match fact {
+            ast::ResolvedFact::Or(_, nested) => {
+                let nested_expansions: Vec<Vec<ast::ResolvedFact>> =
+                    nested.iter().flat_map(|b| expand_or_branch(b)).collect();
+                let mut next = Vec::with_capacity(combos.len() * nested_expansions.len());
+                for combo in &combos {
+                    for expansion in &nested_expansions {
+                        let mut new_combo = combo.clone();
+                        new_combo.extend(expansion.iter().cloned());
+                        next.push(new_combo);
+                    }
+                }
+                combos = next;
+            }
+            other => {
+                for combo in &mut combos {
+                    combo.push(other.clone());
+                }
+            }
+        }
+    }
+    combos
+}
+
+/// Collects the (non-global) variables appearing in a list of resolved facts,
+/// keyed by name.
+fn collect_resolved_fact_vars(
+    facts: &[ast::ResolvedFact],
+    out: &mut IndexMap<String, ResolvedVar>,
+) {
+    for fact in facts {
+        fact.visit_vars(&mut |_, v| {
+            if !v.is_global_ref {
+                out.entry(v.name.clone()).or_insert_with(|| v.clone());
+            }
+        });
+    }
+}
+
+/// The variables common to every combined branch: exactly the variables that
+/// each `or` shares across all its disjuncts (its "output" variables), in a
+/// stable order. Returns an empty set if there are no branches.
+fn common_branch_vars(branches: &[Vec<ast::ResolvedFact>]) -> Vec<ResolvedVar> {
+    let Some((first, rest)) = branches.split_first() else {
+        return Vec::new();
+    };
+    let mut common: IndexMap<String, ResolvedVar> = IndexMap::default();
+    collect_resolved_fact_vars(first, &mut common);
+    for branch in rest {
+        let mut branch_vars = IndexMap::default();
+        collect_resolved_fact_vars(branch, &mut branch_vars);
+        common.retain(|name, _| branch_vars.contains_key(name));
+    }
+    common.into_values().collect()
+}
+
 fn literal_to_entry(egraph: &egglog_bridge::EGraph, l: &Literal) -> QueryEntry {
     match l {
         Literal::Int(x) => egraph.base_value_constant::<i64>(*x),
diff --git a/src/proofs/proof_checker.rs b/src/proofs/proof_checker.rs
index 8938026ed..e55f7a572 100644
--- a/src/proofs/proof_checker.rs
+++ b/src/proofs/proof_checker.rs
@@ -970,6 +970,9 @@ impl ProofStore {
 
                 Ok(())
             }
+            ResolvedFact::Or(..) => {
+                panic!("`or` facts are not supported with proofs")
+            }
         }
     }
 
diff --git a/src/proofs/proof_encoding.rs b/src/proofs/proof_encoding.rs
index a51701e55..b95a3ca0f 100644
--- a/src/proofs/proof_encoding.rs
+++ b/src/proofs/proof_encoding.rs
@@ -794,6 +794,9 @@ impl<'a> ProofInstrumentor<'a> {
                 let (_, proof) = self.instrument_fact_expr(generic_expr, res, action_lookups);
                 proof
             }
+            ResolvedFact::Or(..) => {
+                panic!("`or` facts are not supported with proofs")
+            }
         }
     }
 
diff --git a/src/proofs/proof_format.rs b/src/proofs/proof_format.rs
index 027e2dfbd..547ba57fe 100644
--- a/src/proofs/proof_format.rs
+++ b/src/proofs/proof_format.rs
@@ -544,6 +544,9 @@ impl ProofStore {
             ResolvedFact::Fact(expr) => {
                 self.unify_expr(expr, proof.rhs(), subst);
             }
+            ResolvedFact::Or(..) => {
+                panic!("`or` facts are not supported with proofs")
+            }
         }
     }
 
diff --git a/src/proofs/proof_normal_form.rs b/src/proofs/proof_normal_form.rs
index 795546893..461b39fce 100644
--- a/src/proofs/proof_normal_form.rs
+++ b/src/proofs/proof_normal_form.rs
@@ -68,6 +68,9 @@ fn proof_form_fact(
         GenericFact::Fact(generic_expr) => {
             GenericFact::Fact(proof_form_expr(generic_expr, res, fresh))
         }
+        GenericFact::Or(..) => {
+            panic!("`or` facts are not supported with proofs")
+        }
     }
 }
 
diff --git a/src/typechecking.rs b/src/typechecking.rs
index 53cf2b405..c30cdaf81 100644
--- a/src/typechecking.rs
+++ b/src/typechecking.rs
@@ -825,6 +825,115 @@ impl TypeInfo {
         Result::Ok(schedule)
     }
 
+    /// Collects the set of non-global variable names that appear anywhere in
+    /// `facts` (recursing into `or` branches).
+    fn collect_fact_vars(&self, facts: &[Fact], out: &mut HashSet<String>) {
+        for fact in facts {
+            match fact {
+                GenericFact::Eq(..) | GenericFact::Fact(..) => {
+                    fact.visit_vars(&mut |_, v| {
+                        if !self.is_global(v) {
+                            out.insert(v.clone());
+                        }
+                    });
+                }
+                GenericFact::Or(_, branches) => {
+                    for branch in branches {
+                        self.collect_fact_vars(branch, out);
+                    }
+                }
+            }
+        }
+    }
+
+    /// Rewrites the rule body so that every top-level `or`'s branch-local
+    /// variables are renamed to fresh names (independently per branch), and
+    /// enforces the interface rule: a branch-local variable must not be used
+    /// outside its `or`.
+    ///
+    /// Returns the rewritten body. `outside_vars` must be the set of variable
+    /// names visible outside every `or` in this rule (conjunctive-fact vars,
+    /// action vars, and other `or`s' common vars).
+    fn rename_or_locals(
+        &self,
+        body: &[Fact],
+        outside_vars: &HashSet<String>,
+        symbol_gen: &mut SymbolGen,
+    ) -> Result<Vec<Fact>, TypeError> {
+        let mut new_body = Vec::with_capacity(body.len());
+        for fact in body {
+            match fact {
+                GenericFact::Or(span, branches) => {
+                    if branches.iter().any(|b| b.is_empty()) {
+                        return Err(TypeError::EmptyOrBranch(span.clone()));
+                    }
+                    // Common variables: appear (non-global) in every branch.
+                    let per_branch_vars: Vec<HashSet<String>> = branches
+                        .iter()
+                        .map(|branch| {
+                            let mut set = HashSet::default();
+                            self.collect_fact_vars(branch, &mut set);
+                            set
+                        })
+                        .collect();
+                    let mut common: HashSet<String> = per_branch_vars[0].clone();
+                    for set in &per_branch_vars[1..] {
+                        common.retain(|v| set.contains(v));
+                    }
+
+                    let mut new_branches = Vec::with_capacity(branches.len());
+                    for (branch, branch_vars) in branches.iter().zip(&per_branch_vars) {
+                        // Branch-locals are this branch's non-common,
+                        // non-global vars. If any is used outside the `or`,
+                        // that's an interface violation.
+                        let mut subst: HashMap<String, GenericExpr<String, String>> =
+                            HashMap::default();
+                        for v in branch_vars {
+                            if common.contains(v) {
+                                continue;
+                            }
+                            if outside_vars.contains(v) {
+                                return Err(TypeError::OrBranchLocalEscapes(
+                                    v.clone(),
+                                    span.clone(),
+                                ));
+                            }
+                            let fresh = symbol_gen.fresh(v);
+                            subst.insert(v.clone(), GenericExpr::Var(span.clone(), fresh));
+                        }
+                        let renamed: Vec<Fact> = branch
+                            .iter()
+                            .map(|f| {
+                                f.subst(
+                                    &mut |fspan, leaf| {
+                                        subst.get(leaf).cloned().unwrap_or_else(|| {
+                                            GenericExpr::Var(fspan.clone(), leaf.clone())
+                                        })
+                                    },
+                                    &mut |h| h.clone(),
+                                )
+                            })
+                            .collect();
+                        // Recurse to rename locals in nested `or`s within
+                        // this branch. Nested-or vars common to the nested
+                        // branches remain visible within the enclosing branch.
+                        let mut branch_outside = outside_vars.clone();
+                        branch_outside.extend(common.iter().cloned());
+                        for other_set in &per_branch_vars {
+                            branch_outside.extend(other_set.iter().cloned());
+                        }
+                        let renamed =
+                            self.rename_or_locals(&renamed, &branch_outside, symbol_gen)?;
+                        new_branches.push(renamed);
+                    }
+                    new_body.push(GenericFact::Or(span.clone(), new_branches));
+                }
+                other => new_body.push(other.clone()),
+            }
+        }
+        Ok(new_body)
+    }
+
     fn typecheck_rule(
         &self,
         symbol_gen: &mut SymbolGen,
@@ -841,6 +950,52 @@ impl TypeInfo {
             no_decomp,
             include_subsumed,
         } = rule;
+
+        // Preprocess `or` facts: rename branch-local variables to fresh names
+        // and enforce the interface rule (branch-locals may not escape the
+        // `or`). `outside_vars` is the set of variables visible outside any
+        // `or`: variables in conjunctive facts, action variables, and the
+        // common variables shared by every branch of an `or`.
+        let has_or = body.iter().any(|f| matches!(f, GenericFact::Or(..)));
+        let body: Vec<Fact> = if has_or {
+            let mut outside_vars = HashSet::default();
+            for fact in body {
+                match fact {
+                    GenericFact::Or(_, branches) => {
+                        // Only common vars of the `or` are visible outside it.
+                        let per_branch: Vec<HashSet<String>> = branches
+                            .iter()
+                            .map(|branch| {
+                                let mut set = HashSet::default();
+                                self.collect_fact_vars(branch, &mut set);
+                                set
+                            })
+                            .collect();
+                        if let Some((first, rest)) = per_branch.split_first() {
+                            let mut common = first.clone();
+                            for set in rest {
+                                common.retain(|v| set.contains(v));
+                            }
+                            outside_vars.extend(common);
+                        }
+                    }
+                    other => {
+                        let mut set = HashSet::default();
+                        self.collect_fact_vars(std::slice::from_ref(other), &mut set);
+                        outside_vars.extend(set);
+                    }
+                }
+            }
+            head.visit_vars(&mut |_, v| {
+                if !self.is_global(v) {
+                    outside_vars.insert(v.clone());
+                }
+            });
+            self.rename_or_locals(body, &outside_vars, symbol_gen)?
+        } else {
+            body.clone()
+        };
+        let body = &body;
         let mut constraints = vec![];
 
         // Compile with the permissive Read/Full primitive contexts (so the RHS
@@ -949,6 +1104,14 @@ impl TypeInfo {
         symbol_gen: &mut SymbolGen,
         facts: &[Fact],
     ) -> Result<Vec<ResolvedFact>, TypeError> {
+        // `or` is only supported inside rule bodies, where it can be lowered to
+        // a disjunction of matches. Query-shaped commands like `check` and
+        // `query` evaluate a single conjunctive pattern.
+        if let Some(GenericFact::Or(span, _)) =
+            facts.iter().find(|f| matches!(f, GenericFact::Or(..)))
+        {
+            return Err(TypeError::OrOutsideRule(span.clone()));
+        }
         let (query, mapped_facts) = Facts(facts.to_vec()).to_query(self, symbol_gen);
         let mut problem = Problem::default();
         // Top-level query-shaped commands (e.g. `check`) are read-only:
@@ -1197,6 +1360,16 @@ pub enum TypeError {
         crate::GLOBAL_NAME_PREFIX
     )]
     GlobalMissingPrefix { name: String, span: Span },
+    #[error(
+        "{1}\nVariable `{0}` is local to one branch of an `or` but is used outside it. Only variables common to every branch are visible outside the `or`."
+    )]
+    OrBranchLocalEscapes(String, Span),
+    #[error("{0}\nAn `or` branch is empty; each branch must contain at least one fact.")]
+    EmptyOrBranch(Span),
+    #[error(
+        "{0}\n`or` is only supported inside rule bodies, not in query-shaped commands like `check` or `query`."
+    )]
+    OrOutsideRule(Span),
 }
 
 #[cfg(test)]
diff --git a/tests/disjunction.rs b/tests/disjunction.rs
new file mode 100644
index 000000000..74e0ac529
--- /dev/null
+++ b/tests/disjunction.rs
@@ -0,0 +1,263 @@
+//! Behavioral tests for disjunction (`or`) in rule bodies.
+//!
+//! A body `C ∧ (D₁ ∨ … ∨ Dₙ)` matches when `C` holds and at least one branch
+//! `Dᵢ` holds. Only the variables common to every branch (plus variables bound
+//! by the surrounding conjunction) are visible outside the `or`. Branch-local
+//! variables that escape their `or`, and empty branches, are type errors.
+//!
+//! Each test runs rules to a fixpoint and asserts on the resulting database via
+//! `check` / `fail`.
+
+use egglog::{EGraph, Error};
+
+/// Runs a program, returning any error.
+fn run(program: &str) -> Result<(), Error> {
+    let mut egraph = EGraph::default();
+    egraph.parse_and_run_program(None, program)?;
+    Ok(())
+}
+
+/// A two-branch `or` over relations behaves as set union.
+#[test]
+fn or_basic_union() -> Result<(), Error> {
+    run("
+(relation A (i64))
+(relation B (i64))
+(relation R (i64))
+(A 1) (A 2)
+(B 2) (B 3)
+(rule ((or ((A x)) ((B x)))) ((R x)))
+(run 5)
+(check (R 1))
+(check (R 2))
+(check (R 3))
+(fail (check (R 4)))
+")
+}
+
+/// An `or` conjoined with a surrounding fact `C` matches only when `C` holds and
+/// at least one branch holds.
+#[test]
+fn or_with_conjunction() -> Result<(), Error> {
+    run("
+(relation C (i64))
+(relation A (i64))
+(relation B (i64))
+(relation R (i64))
+(C 1) (C 2) (C 3)
+(A 1) (A 2)
+(B 2) (B 3)
+(rule ((C x) (or ((A x)) ((B x)))) ((R x)))
+(run 5)
+(check (R 1))
+(check (R 2))
+(check (R 3))
+(fail (check (R 4)))
+")
+}
+
+/// A `C` value that satisfies neither branch does not fire.
+#[test]
+fn or_conjunction_requires_a_branch() -> Result<(), Error> {
+    run("
+(relation C (i64))
+(relation A (i64))
+(relation R (i64))
+(C 5)
+(rule ((C x) (or ((A x)) ((A x)))) ((R x)))
+(run 5)
+(fail (check (R 5)))
+")
+}
+
+/// A variable common to every branch may be used in the action; a branch-local
+/// variable (`y`) stays inside its branch.
+#[test]
+fn or_common_variable() -> Result<(), Error> {
+    run("
+(relation P (i64 i64))
+(relation Q (i64 i64))
+(relation Out (i64))
+(P 1 10)
+(Q 1 20)
+(P 2 30)
+(rule ((or ((P x y)) ((Q x y)))) ((Out x)))
+(run 5)
+(check (Out 1))
+(check (Out 2))
+(fail (check (Out 3)))
+")
+}
+
+/// Three-branch `or`.
+#[test]
+fn or_three_branches() -> Result<(), Error> {
+    run("
+(relation A (i64))
+(relation B (i64))
+(relation C (i64))
+(relation R (i64))
+(A 1) (B 2) (C 3)
+(rule ((or ((A x)) ((B x)) ((C x)))) ((R x)))
+(run 5)
+(check (R 1))
+(check (R 2))
+(check (R 3))
+(fail (check (R 4)))
+")
+}
+
+/// A branch may itself be a conjunction of several facts.
+#[test]
+fn or_branch_is_a_conjunction() -> Result<(), Error> {
+    run("
+(relation A (i64))
+(relation B (i64))
+(relation C (i64))
+(relation R (i64))
+(A 1) (B 1)
+(A 2)
+(C 3)
+(rule ((or ((A x) (B x)) ((C x)))) ((R x)))
+(run 5)
+(check (R 1))
+(fail (check (R 2)))
+(check (R 3))
+")
+}
+
+/// Two `or`s in one body distribute as a cartesian product of branch choices.
+#[test]
+fn or_two_disjunctions() -> Result<(), Error> {
+    run("
+(relation A (i64))
+(relation B (i64))
+(relation C (i64))
+(relation D (i64))
+(relation R (i64))
+(A 1) (C 1)
+(B 2) (D 2)
+(A 3) (D 3)
+(rule ((or ((A x)) ((B x))) (or ((C x)) ((D x)))) ((R x)))
+(run 5)
+(check (R 1))
+(check (R 2))
+(check (R 3))
+(fail (check (R 4)))
+")
+}
+
+/// A branch may join several atoms internally on a branch-local variable, with
+/// only the common variable escaping.
+#[test]
+fn or_branch_internal_join() -> Result<(), Error> {
+    run("
+(relation A (i64 i64))
+(relation B (i64 i64))
+(relation C (i64 i64))
+(relation Res (i64))
+(A 1 9) (B 9 1)
+(C 2 2)
+(rule ((or ((A x t) (B t x)) ((C x x)))) ((Res x)))
+(run 3)
+(check (Res 1))
+(check (Res 2))
+(fail (check (Res 9)))
+")
+}
+
+/// An `or` nested inside a branch of another `or` flattens correctly.
+#[test]
+fn or_nested() -> Result<(), Error> {
+    run("
+(relation A (i64))
+(relation B (i64))
+(relation C (i64))
+(relation R (i64))
+(A 1) (B 2) (C 3)
+(rule ((or ((A x)) ((or ((B x)) ((C x)))))) ((R x)))
+(run 5)
+(check (R 1))
+(check (R 2))
+(check (R 3))
+(fail (check (R 4)))
+")
+}
+
+/// `or` works with an equality (`union`) action over an eq-sort.
+#[test]
+fn or_with_union_action() -> Result<(), Error> {
+    run("
+(datatype Math (Num i64))
+(relation A (Math))
+(relation B (Math))
+(A (Num 1))
+(B (Num 2))
+(rule ((or ((A x)) ((B x)))) ((union x (Num 0))))
+(run 5)
+(check (= (Num 0) (Num 1)))
+(check (= (Num 0) (Num 2)))
+")
+}
+
+/// A branch-local variable used outside its `or` is a type error.
+#[test]
+fn or_branch_local_escapes_errors() {
+    let err = run("
+(relation P (i64 i64))
+(relation Q (i64 i64))
+(relation Out (i64))
+(rule ((or ((P x y)) ((Q x z)))) ((Out y)))
+")
+    .unwrap_err()
+    .to_string();
+    assert!(
+        err.contains("local to one branch") && err.contains('y'),
+        "unexpected error: {err}"
+    );
+}
+
+/// An empty `or` branch is a type error.
+#[test]
+fn or_empty_branch_errors() {
+    let err = run("
+(relation A (i64))
+(relation R (i64))
+(rule ((or ((A x)) ())) ((R x)))
+")
+    .unwrap_err()
+    .to_string();
+    assert!(err.contains("empty"), "unexpected error: {err}");
+}
+
+/// `or` is rejected in query-shaped commands like `check`.
+#[test]
+fn or_outside_rule_errors() {
+    let err = run("
+(relation A (i64))
+(relation B (i64))
+(A 1)
+(check (or ((A 1)) ((B 1))))
+")
+    .unwrap_err()
+    .to_string();
+    assert!(
+        err.contains("only supported inside rule bodies"),
+        "unexpected error: {err}"
+    );
+}
+
+/// `or` works in a `rewrite`'s `:when` condition (which desugars to a rule).
+#[test]
+fn or_in_rewrite_condition() -> Result<(), Error> {
+    run("
+(datatype Math (Num i64) (Add Math Math))
+(relation Good (Math))
+(relation Alt (Math))
+(Good (Num 1))
+(rewrite (Add x y) (Add y x) :when ((or ((Good x)) ((Alt x)))))
+(Add (Num 1) (Num 2))
+(run 3)
+(check (= (Add (Num 1) (Num 2)) (Add (Num 2) (Num 1))))
+")
+}

From 1a8641c64fb0c9c372c3cfe4ff137018a1337f9b Mon Sep 17 00:00:00 2001
From: Oliver Flatt <oflatt@gmail.com>
Date: Thu, 2 Jul 2026 03:51:00 +0000
Subject: [PATCH 2/4] Strategy D: correlated streaming disjunction with
 seminaive support

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>
---
 CHANGELOG.md                    |   2 +-
 docs/disjunction-design.md      | 133 ++++++++++++++++++++------
 src/ast/parse.rs                |  27 ++++--
 src/lib.rs                      | 163 ++++++++++++++++++++++++++++----
 src/proofs/proof_encoding.rs    |  20 +++-
 src/proofs/proof_normal_form.rs |  17 +++-
 src/typechecking.rs             |  54 +++++++----
 tests/disjunction.rs            |  58 ++++++++++++
 8 files changed, 400 insertions(+), 74 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5136b5220..8ee1302e4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,7 +2,7 @@
 
 ## [Unreleased] - ReleaseDate
 
-- **Disjunction (`or`) in rule bodies.** A rule body may now contain `(or (branch...) (branch...) ...)`, where each branch is a conjunction of facts; the disjunction matches when at least one branch matches. Only variables common to every branch (plus variables bound by the surrounding conjunction) are visible outside the `or`; a branch-local variable that escapes its `or`, and an empty branch, are type errors. `or` is only allowed in rule bodies (including `rewrite` conditions), not in query-shaped commands like `check`. It compiles to a single rule with a fused union node in the free-join engine: the surrounding conjunction is scanned once and joined against the deduplicated union of the branch outputs (no rule-splitting, no materialized table). `or` rules run in naive mode, and a branch must contain only table atoms. See `docs/disjunction-design.md`.
+- **Disjunction (`or`) in rule bodies.** A rule body may now contain `(or (branch...) (branch...) ...)` (either spelling `or`/`OR`), where each branch is a conjunction of facts (or a single bare fact, e.g. `(= a d)`); the disjunction matches when at least one branch matches. A branch may be *correlated*: it may reference variables bound by the surrounding conjunction (as in `(= col d)`). Variables usable outside the `or` are those bound by the surrounding conjunction plus those common to every branch; a branch-local variable that escapes its `or`, and an empty branch, are type errors. `or` is only allowed in rule bodies (including `rewrite` conditions), not in query-shaped commands like `check`, and is allowed under the term encoding (without proofs). Compilation uses one of two strategies: a naive rule whose branches each bind their own variables compiles to a single **fused union node** in the free-join engine (the surrounding conjunction is scanned once and joined against the deduplicated union of the branch outputs); a correlated or seminaive `or` (e.g. `:unsafe-seminaive`) compiles by **splitting** into one ordinary backend rule per disjunct, so seminaive evaluation and index-probe joins work normally (a delta on an outer atom drives an index probe of a correlated atom, with no cartesian product). See `docs/disjunction-design.md`.
 - Add typed `EGraph` extension state that clones with `EGraph` and is restored by `push`/`pop`.
 - Report full source file paths in egglog span and error messages.
 - Fix seminaive matching after nested containers rebuild in place by propagating dirty container ids through parent containers.
diff --git a/docs/disjunction-design.md b/docs/disjunction-design.md
index 849423e40..627be4928 100644
--- a/docs/disjunction-design.md
+++ b/docs/disjunction-design.md
@@ -12,26 +12,33 @@ A rule body may contain a disjunction fact:
       (action ...))
 ```
 
-Each branch is a parenthesized *list of facts* (a conjunction). The body
-`C ∧ (D₁ ∨ … ∨ Dₙ)` matches when the surrounding conjunction `C` holds and at
-least one branch `Dᵢ` holds.
+Each branch is either a parenthesized *list of facts* (a conjunction,
+`((A x) (B x))`) or a single bare fact (`(= a d)`, `(A x)`). Both the lowercase
+`or` and uppercase `OR` spellings are accepted. The body `C ∧ (D₁ ∨ … ∨ Dₙ)`
+matches when the surrounding conjunction `C` holds and at least one branch `Dᵢ`
+holds.
 
 ## Semantics
 
 - **Common variables.** `V = ⋂ᵢ vars(Dᵢ)` — the variables that appear in every
   branch. Only `V`, together with the variables bound by the surrounding
   conjunction `C`, are visible in the action and elsewhere outside the `or`.
-- **Branch-local variables.** A variable that appears in some branch but is not
-  in `V` is *branch-local*. Branch-locals in different branches are independent:
-  during typechecking they are renamed to fresh names so their sorts are not
-  conflated. A branch-local variable that is used outside its `or` is a type
-  error (`TypeError::OrBranchLocalEscapes`).
+- **Correlated branches.** A branch may reference a variable bound by the
+  surrounding conjunction `C` (even one not common to every branch), e.g.
+  `(= col d)` where `col` and `d` come from `C`. Such a reference is left
+  untouched during typechecking; it is *not* treated as branch-local.
+- **Branch-local variables.** A variable that appears in some branch but is
+  neither in `V` nor bound by `C` is *branch-local*. Branch-locals in different
+  branches are independent: during typechecking they are renamed to fresh names
+  so their sorts are not conflated. A branch-local variable that is used outside
+  its `or` is a type error (`TypeError::OrBranchLocalEscapes`).
 - **Empty branch.** A branch with no facts is a type error
   (`TypeError::EmptyOrBranch`).
 - **Scope.** `or` is only supported inside rule bodies (including the `:when`
   conditions of a `rewrite`, which desugar to rules). It is rejected in
   query-shaped commands like `check` and `query`
-  (`TypeError::OrOutsideRule`).
+  (`TypeError::OrOutsideRule`). It is allowed under the term encoding without
+  proofs; with proofs it is unsupported.
 
 ## Frontend pipeline
 
@@ -40,13 +47,17 @@ least one branch `Dᵢ` holds.
    and `map_symbols` recurse into the branches
    (`egglog-ast/src/generic_ast_helpers.rs`).
 2. **Parsing** — `src/ast/parse.rs`: `parse_fact` recognises the `OR_HEAD`
-   (`"or"`) head and parses each argument as a list of facts.
+   (`"or"`) / `OR_HEAD_UPPER` (`"OR"`) head. Each argument is parsed as a list
+   of facts if it is an empty list or its first element is itself a list;
+   otherwise it is a single bare fact.
 3. **Typechecking** — `src/typechecking.rs` `typecheck_rule`:
    - `rename_or_locals` renames each branch's branch-local variables to fresh
      names (independently per branch) and enforces the interface rule
-     (branch-locals may not escape their `or`). `outside_vars` is the set of
-     variables visible outside every `or`: conjunctive-fact variables, action
-     variables, and each `or`'s common variables.
+     (branch-locals may not escape their `or`). It takes both `outside_vars`
+     (all variables visible outside every `or`: conjunctive-fact variables,
+     action variables, and each `or`'s common variables) and `conj_vars` (the
+     subset bound by the surrounding conjunction); a branch reference to a
+     `conj_var` is a correlation and is left as-is rather than renamed.
    - `Facts::to_query` (`src/ast/mod.rs`) flattens every branch's atoms into one
      shared constraint `Query` so the constraint solver assigns a sort to every
      variable — common variables (whose sort is thereby unified across branches
@@ -56,15 +67,26 @@ least one branch `Dᵢ` holds.
    - `src/ast/check_shadowing.rs` recurses into `or` branches when collecting
      pattern variable names.
 
-## Backend compilation: Strategy C — a fused union node in the free-join engine
+## Backend compilation
 
-An `or`-containing rule compiles to **one** backend rule with a fused union node
-in the free-join engine. The surrounding conjunction `C` is scanned **once**;
-the branches are enumerated additively (never a `∏` of separate rules).
+`add_rule` dispatches `or`-containing rules to `add_or_rule`, which picks one of
+two strategies (returning one `(name, core rule, backend rule id)` per compiled
+backend rule):
 
-### egglog crate (`src/lib.rs`, `add_or_rule`)
+- **Strategy C — fused union node.** Used when the rule is naive *and* every
+  disjunct is *self-groundable* (`branch_self_groundable`: every non-global
+  variable the disjunct references is bound by one of its own table atoms). One
+  backend rule with a fused union node; `C` is scanned once.
+- **Strategy D — splitting.** Used otherwise — a *correlated* disjunct (which
+  references a `C`-bound variable it does not bind itself) or a seminaive rule.
+  See "Strategy D" below.
 
-`add_rule` dispatches `or`-containing rules to `add_or_rule`, which:
+## Strategy C — a fused union node in the free-join engine
+
+The `or`-containing rule compiles to **one** backend rule with a fused union
+node in the free-join engine. The surrounding conjunction `C` is scanned
+**once**; the branches are enumerated additively (never a `∏` of separate
+rules). `add_or_rule` (Strategy-C path):
 
 1. Splits the body into the conjunction `C` (non-`or` facts) and the `or`s, and
    forms the union's **branches** as the cartesian product of every `or`'s
@@ -129,20 +151,77 @@ This shares `C`: it is evaluated a single time in the result block, joined by
 index against the deduplicated union of the branch outputs — never re-scanned per
 branch and never producing `∏` separate rules.
 
-### Tradeoffs / restrictions
+### Strategy-C tradeoffs / restrictions
 
-- **Naive evaluation.** `or` rules match the whole database each iteration
-  (seminaive delta through a union is not supported).
+- **Naive only.** Strategy C runs in naive mode; a seminaive rule uses Strategy
+  D instead.
 - **Primitives in branches** are rejected (a branch must be a conjunction of
   table atoms). Primitives in the surrounding conjunction `C` are fine.
 - **`∏` branches for multiple/nested `or`s.** `k` disjunctions produce `∏`
   union *branches* (enumerated additively into one materialization), but still a
-  single rule with `C` scanned once — unlike rule-splitting, which would create
-  `∏` rules each re-scanning `C`. A single `or` (the common case) is linear.
+  single rule with `C` scanned once. A single `or` (the common case) is linear.
 - **No cross-branch dedup of firings beyond the output key.** The union
   deduplicates output tuples; like every egglog rule, the action still fires per
   full match otherwise. This matches egglog's normal non-dedup semantics and is
   invisible for idempotent actions.
-- **Proofs.** `or` is not supported with the proof / term encoding; the proof
-  passes panic if they ever see an `or` fact (they never do, because proof mode
-  compiles only proof-instrumented rules).
+
+## Strategy D — splitting (correlated / seminaive `or`s)
+
+Strategy C's fused union requires each branch to bind the union's output
+variables *itself* (its branches run first, materializing those variables), and
+it forces naive mode. Neither holds for a **correlated** `or` such as the
+e-graph rebuild pattern
+
+```
+(rule ((MulView c0 c1 c2) (UF_Math d e) (!= d e)
+       (OR (= c0 d) (= c1 d) (= c2 d)))
+      (...)
+      :ruleset rebuilding :unsafe-seminaive)
+```
+
+where each disjunct only *constrains* variables (`c0`/`d`) bound by the
+surrounding conjunction, and where per-disjunct variable merging (`c0 = d` in
+one branch, `c1 = d` in another) must propagate into the shared action.
+
+`add_or_rule` (via `add_or_rule_split` in `src/lib.rs`) therefore compiles a
+correlated or seminaive `or` by **splitting**: the disjuncts are expanded into
+the cartesian product of the `or`s (`expand_or_branch`), and for each combined
+disjunct one ordinary backend rule is emitted, with body `C ∧ disjunct` and the
+rule's shared action. Extra split rules get synthetic names `{name}__or{i}` so
+they coexist in the ruleset (`add_rule` inserts one ruleset entry per split).
+
+Each split rule is a plain conjunctive rule, so the existing machinery does the
+right thing with no changes to the free-join engine or seminaive evaluation:
+
+- **Per-disjunct canonicalization** merges each disjunct's equalities
+  independently. `(= c0 d)` substitutes `c0 → d`, so `MulView(c0,c1,c2)` becomes
+  `MulView(d,c1,c2)` sharing variable `d` with `UF_Math(d,e)`. A join on a
+  shared variable is an **index probe**, never a cartesian product — even in
+  naive mode. The merge propagates into the action, so a correlated variable
+  resolves correctly there too.
+- **Seminaive** (`:unsafe-seminaive`) runs normally per split rule. A delta on
+  the outer atom (`UF_Math`) drives an index probe of the correlated atom
+  (`MulView`) by the new key; a delta on `MulView` probes `UF_Math`. The
+  `Read`/`Full` RHS contexts of `:unsafe-seminaive` let the action perform
+  lookups (e.g. `(UF_Mathf c0)`).
+- **Primitives** in the surrounding conjunction (e.g. `(!= d e)`) are ordinary
+  RHS-context checks in each split rule.
+
+### Strategy-D tradeoffs / restrictions
+
+- **`k` backend rules per `or`.** A `k`-way `or` (or `∏` over several `or`s)
+  becomes `k` (or `∏`) backend rules. In seminaive mode this is cheap — each
+  processes only the delta and probes by index — so the cartesian-product
+  blow-up the fused union avoids does not reappear.
+- **Split rule names.** Extra disjuncts occupy synthetic `{name}__or{i}`
+  ruleset entries, which show up separately in run reports.
+
+## Proofs and the term encoding
+
+`or` is allowed under the term encoding **without** proofs: `proof_form`
+normalizes each branch independently, and `instrument_fact` rewrites each
+branch's atoms to view-table lookups and re-emits an `(or (branch...) ...)`
+fact, which is then compiled by the strategies above. With proofs enabled the
+instrumentation panics (`or` is unsupported with proofs). `:unsafe-seminaive`
+remains unsupported under the term encoding regardless (a pre-existing
+limitation, since it performs arbitrary live-database reads).
diff --git a/src/ast/parse.rs b/src/ast/parse.rs
index 83da9d500..6a266b96b 100644
--- a/src/ast/parse.rs
+++ b/src/ast/parse.rs
@@ -23,8 +23,10 @@ macro_rules! span {
 // differently to different parse errors. The benefit of this is that
 // error messages are defined in the same place that they are created,
 // making it easier to improve errors over time.
-/// The head symbol for a disjunction fact `(or (branch...) ...)`.
+/// The head symbols for a disjunction fact `(or (branch...) ...)`. Both the
+/// lowercase `or` and the uppercase `OR` spellings are accepted.
 pub const OR_HEAD: &str = "or";
+pub const OR_HEAD_UPPER: &str = "OR";
 
 #[derive(Debug, Error)]
 pub struct ParseError(pub Span, pub String);
@@ -909,13 +911,26 @@ impl Parser {
                 [e1, e2] => Fact::Eq(span, self.parse_expr(e1)?, self.parse_expr(e2)?),
                 _ => return error!(span, "usage: (= <expr> <expr>)"),
             },
-            OR_HEAD => {
-                // `(or (branch...) (branch...) ...)`: each branch is a
-                // parenthesized list of facts.
+            OR_HEAD | OR_HEAD_UPPER => {
+                // Each disjunct is either a parenthesized conjunction of facts
+                // `((A x) (B x))` or a single bare fact `(= a d)` / `(A x)`. A
+                // conjunction is recognized by being an empty list or a list
+                // whose first element is itself a list (a nested fact); anything
+                // else is a call with a symbol head, i.e. one fact.
                 let mut branches = Vec::with_capacity(tail.len());
                 for branch_sexp in tail {
-                    let facts = branch_sexp.expect_list("or branch (a list of facts)")?;
-                    branches.push(map_fallible(facts, self, Self::parse_fact)?);
+                    let is_conjunction = matches!(
+                        branch_sexp,
+                        Sexp::List(elems, _)
+                            if elems.is_empty() || matches!(elems.first(), Some(Sexp::List(..)))
+                    );
+                    let branch = if is_conjunction {
+                        let facts = branch_sexp.expect_list("or branch (a list of facts)")?;
+                        map_fallible(facts, self, Self::parse_fact)?
+                    } else {
+                        vec![self.parse_fact(branch_sexp)?]
+                    };
+                    branches.push(branch);
                 }
                 Fact::Or(span, branches)
             }
diff --git a/src/lib.rs b/src/lib.rs
index ab9594db8..646bc492c 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1158,7 +1158,11 @@ impl EGraph {
             .iter()
             .any(|f| matches!(f, ast::ResolvedFact::Or(..)));
 
-        let (stored_core_rule, rule_id) = if has_or {
+        // Each logical rule normally compiles to one backend rule, keyed by its
+        // name. A correlated / seminaive `or` compiles by *splitting* into one
+        // backend rule per disjunct (all sharing the action); those extra rules
+        // get synthetic names so they can coexist in the ruleset.
+        let compiled: Vec<(String, core::ResolvedCoreRule, egglog_bridge::RuleId)> = if has_or {
             self.add_or_rule(
                 &rule,
                 union_to_set,
@@ -1182,19 +1186,20 @@ impl EGraph {
                 translator.actions(actions)?;
                 translator.build()
             };
-            (core_rule, rule_id)
+            vec![(rule.name.clone(), core_rule, rule_id)]
         };
 
         if let Some(rules) = self.rulesets.get_mut(&rule.ruleset) {
             match rules {
                 Ruleset::Rules(rules) => {
-                    match rules.entry(rule.name.clone()) {
-                        indexmap::map::Entry::Occupied(_) => {
-                            let name = rule.name;
-                            panic!("Rule '{name}' was already present")
-                        }
-                        indexmap::map::Entry::Vacant(e) => e.insert((stored_core_rule, rule_id)),
-                    };
+                    for (name, core_rule, rule_id) in compiled {
+                        match rules.entry(name.clone()) {
+                            indexmap::map::Entry::Occupied(_) => {
+                                panic!("Rule '{name}' was already present")
+                            }
+                            indexmap::map::Entry::Vacant(e) => e.insert((core_rule, rule_id)),
+                        };
+                    }
                     Ok(rule.name)
                 }
                 Ruleset::Combined(_) => Err(Error::CombinedRulesetError(rule.ruleset, rule.span)),
@@ -1204,23 +1209,39 @@ impl EGraph {
         }
     }
 
-    /// Compiles a rule whose body contains one or more `or` facts into a single
-    /// backend rule using a fused union in the free-join engine. The surrounding
-    /// conjunction is joined once against the deduplicated union of the branch
-    /// outputs (see [`egglog_bridge::RuleBuilder::set_union_branches`] and
-    /// `core_relations::QueryBuilder::set_union`). Runs in naive mode.
+    /// Compiles a rule whose body contains one or more `or` facts.
+    ///
+    /// Two strategies:
+    /// - **Fused union (Strategy C).** When every disjunct is *self-groundable*
+    ///   (binds all its own variables with its own table atoms) and the rule is
+    ///   naive, the whole `or` compiles to a single backend rule with a fused
+    ///   union node: the surrounding conjunction is joined once against the
+    ///   deduplicated union of the branch outputs (see
+    ///   [`egglog_bridge::RuleBuilder::set_union_branches`] and
+    ///   `core_relations::QueryBuilder::set_union`).
+    /// - **Splitting (Strategy D).** Otherwise — a *correlated* branch (one that
+    ///   references a variable bound by the surrounding conjunction, e.g.
+    ///   `(= col d)`), or a seminaive rule — the `or` compiles to one backend
+    ///   rule per disjunct, each the surrounding conjunction conjoined with that
+    ///   disjunct and the shared action. Each split rule is an ordinary
+    ///   conjunctive rule, so seminaive evaluation and index-probe joins work
+    ///   normally: a delta on an outer atom drives an index probe of the atom a
+    ///   correlated equality constrains, with no cartesian product.
+    ///
+    /// Returns one `(name, core rule, backend rule id)` per compiled backend
+    /// rule (one for a fused union, one per disjunct when splitting).
     fn add_or_rule(
         &mut self,
         rule: &ast::ResolvedRule,
         union_to_set: bool,
-        _seminaive: bool,
+        seminaive: bool,
         no_decomp: bool,
         requires_read_context: bool,
-    ) -> Result<(core::ResolvedCoreRule, egglog_bridge::RuleId), Error> {
+    ) -> Result<Vec<(String, core::ResolvedCoreRule, egglog_bridge::RuleId)>, Error> {
         // Split the body into the surrounding conjunction and the `or`s, then
-        // form the union's branches as the cartesian product of every `or`'s
-        // branches (each combined branch is a conjunction, with nested `or`s
-        // expanded the same way). A single `or` gives one branch per disjunct.
+        // form the branches as the cartesian product of every `or`'s branches
+        // (each combined branch is a conjunction, with nested `or`s expanded the
+        // same way). A single `or` gives one branch per disjunct.
         let mut conj_facts: Vec<ast::ResolvedFact> = Vec::new();
         let mut combined_branches: Vec<Vec<ast::ResolvedFact>> = vec![vec![]];
         for fact in &rule.body {
@@ -1243,6 +1264,23 @@ impl EGraph {
             }
         }
 
+        // Correlated (non-self-groundable) branches and seminaive rules can't use
+        // C's fused union node (its branches must bind the union's output vars
+        // themselves, and it forces naive mode). Fall back to splitting.
+        let fused_union_ok =
+            !seminaive && combined_branches.iter().all(|b| branch_self_groundable(b));
+        if !fused_union_ok {
+            return self.add_or_rule_split(
+                rule,
+                &conj_facts,
+                &combined_branches,
+                union_to_set,
+                seminaive,
+                no_decomp,
+                requires_read_context,
+            );
+        }
+
         // The variables visible outside the `or`s (shared with the surrounding
         // conjunction and the action) are the union's output variables: the
         // variables that appear in every branch of an `or`. We take, for each
@@ -1324,7 +1362,63 @@ impl EGraph {
             translator.build()
         };
 
-        Ok((core_conj, rule_id))
+        Ok(vec![(rule.name.clone(), core_conj, rule_id)])
+    }
+
+    /// Strategy D: compile an `or` rule by splitting it into one ordinary
+    /// backend rule per disjunct, each conjoining the surrounding conjunction
+    /// with that disjunct and firing the shared action. See [`Self::add_or_rule`].
+    #[allow(clippy::too_many_arguments)]
+    fn add_or_rule_split(
+        &mut self,
+        rule: &ast::ResolvedRule,
+        conj_facts: &[ast::ResolvedFact],
+        combined_branches: &[Vec<ast::ResolvedFact>],
+        union_to_set: bool,
+        seminaive: bool,
+        no_decomp: bool,
+        requires_read_context: bool,
+    ) -> Result<Vec<(String, core::ResolvedCoreRule, egglog_bridge::RuleId)>, Error> {
+        let mut compiled = Vec::with_capacity(combined_branches.len());
+        for (i, branch) in combined_branches.iter().enumerate() {
+            // Each split rule is `conjunction ∧ branch => action`. Per-branch
+            // canonicalization merges each disjunct's equalities (e.g. `(= col
+            // d)`) independently, so a correlated variable resolves correctly in
+            // both the body and the shared action.
+            let mut body = conj_facts.to_vec();
+            body.extend(branch.iter().cloned());
+            let name = if i == 0 {
+                rule.name.clone()
+            } else {
+                format!("{}__or{i}", rule.name)
+            };
+            let split_rule = ast::ResolvedRule {
+                span: rule.span.clone(),
+                head: rule.head.clone(),
+                body,
+                name: name.clone(),
+                ruleset: rule.ruleset.clone(),
+                eval_mode: rule.eval_mode,
+                no_decomp: rule.no_decomp,
+                include_subsumed: rule.include_subsumed,
+            };
+            let core_rule = split_rule.to_canonicalized_core_rule(
+                &self.type_info,
+                &mut self.parser.symbol_gen,
+                union_to_set,
+            )?;
+            let rule_id = {
+                let mut rb = self.backend.new_rule(&name, seminaive);
+                rb.set_no_decomp(no_decomp);
+                let mut translator =
+                    BackendRule::new(rb, &self.functions, &self.type_info, requires_read_context);
+                translator.query(&core_rule.body, split_rule.include_subsumed);
+                translator.actions(&core_rule.head)?;
+                translator.build()
+            };
+            compiled.push((name, core_rule, rule_id));
+        }
+        Ok(compiled)
     }
 
     fn eval_actions(&mut self, actions: &ResolvedActions) -> Result<(), Error> {
@@ -2950,6 +3044,35 @@ impl<'a> BackendRule<'a> {
     }
 }
 
+/// Whether every non-global variable referenced by `branch` is bound by one of
+/// the branch's own table (function/relation) atoms. A self-groundable branch
+/// can be evaluated by C's fused union node, which requires each branch to bind
+/// the union's output variables itself. A branch that references a variable it
+/// does not bind — a *correlated* branch, e.g. `(= col d)` where `col` and `d`
+/// come from the surrounding conjunction — is not self-groundable and is
+/// compiled by splitting instead.
+fn branch_self_groundable(branch: &[ast::ResolvedFact]) -> bool {
+    let mut bound: IndexSet<String> = IndexSet::default();
+    for fact in branch {
+        if let ast::ResolvedFact::Fact(ResolvedExpr::Call(_, ResolvedCall::Func(_), _)) = fact {
+            fact.visit_vars(&mut |_, v| {
+                if !v.is_global_ref {
+                    bound.insert(v.name.clone());
+                }
+            });
+        }
+    }
+    let mut groundable = true;
+    for fact in branch {
+        fact.visit_vars(&mut |_, v| {
+            if !v.is_global_ref && !bound.contains(&v.name) {
+                groundable = false;
+            }
+        });
+    }
+    groundable
+}
+
 /// Expands one `or` branch (a conjunction of facts that may itself contain
 /// nested `or`s) into a list of purely-conjunctive fact lists — one per
 /// combination of the nested disjuncts. A branch with no nested `or` yields a
diff --git a/src/proofs/proof_encoding.rs b/src/proofs/proof_encoding.rs
index b95a3ca0f..5877ed525 100644
--- a/src/proofs/proof_encoding.rs
+++ b/src/proofs/proof_encoding.rs
@@ -794,8 +794,24 @@ impl<'a> ProofInstrumentor<'a> {
                 let (_, proof) = self.instrument_fact_expr(generic_expr, res, action_lookups);
                 proof
             }
-            ResolvedFact::Or(..) => {
-                panic!("`or` facts are not supported with proofs")
+            ResolvedFact::Or(_, branches) => {
+                // `or` is supported under the term encoding only without proofs:
+                // each branch's atoms are rewritten to view-table lookups and
+                // re-emitted as an `(or (branch...) ...)` fact. Proof tracking
+                // through a disjunction is not supported.
+                if self.egraph.proof_state.proofs_enabled {
+                    panic!("`or` facts are not supported with proofs")
+                }
+                let mut branch_strs = Vec::with_capacity(branches.len());
+                for branch in branches {
+                    let mut branch_res = vec![];
+                    for fact in branch {
+                        self.instrument_fact(fact, &mut branch_res, action_lookups);
+                    }
+                    branch_strs.push(format!("({})", ListDisplay(&branch_res, " ")));
+                }
+                res.push(format!("(or {})", ListDisplay(&branch_strs, " ")));
+                "()".to_string()
             }
         }
     }
diff --git a/src/proofs/proof_normal_form.rs b/src/proofs/proof_normal_form.rs
index 461b39fce..68b832084 100644
--- a/src/proofs/proof_normal_form.rs
+++ b/src/proofs/proof_normal_form.rs
@@ -68,8 +68,21 @@ fn proof_form_fact(
         GenericFact::Fact(generic_expr) => {
             GenericFact::Fact(proof_form_expr(generic_expr, res, fresh))
         }
-        GenericFact::Or(..) => {
-            panic!("`or` facts are not supported with proofs")
+        GenericFact::Or(span, branches) => {
+            // Normalize each branch independently, keeping any lifted helper
+            // facts inside their branch's conjunction.
+            let new_branches = branches
+                .into_iter()
+                .map(|branch| {
+                    let mut branch_res = vec![];
+                    for fact in branch {
+                        let rewritten = proof_form_fact(fact, &mut branch_res, fresh);
+                        branch_res.push(rewritten);
+                    }
+                    branch_res
+                })
+                .collect();
+            GenericFact::Or(span, new_branches)
         }
     }
 }
diff --git a/src/typechecking.rs b/src/typechecking.rs
index c30cdaf81..517082d63 100644
--- a/src/typechecking.rs
+++ b/src/typechecking.rs
@@ -848,16 +848,26 @@ impl TypeInfo {
 
     /// Rewrites the rule body so that every top-level `or`'s branch-local
     /// variables are renamed to fresh names (independently per branch), and
-    /// enforces the interface rule: a branch-local variable must not be used
-    /// outside its `or`.
+    /// enforces the interface rule.
     ///
-    /// Returns the rewritten body. `outside_vars` must be the set of variable
-    /// names visible outside every `or` in this rule (conjunctive-fact vars,
-    /// action vars, and other `or`s' common vars).
+    /// A variable referenced in a branch is classified as:
+    /// - **outer** if it is bound by the surrounding conjunction (`conj_vars`):
+    ///   the branch reference is a correlation to that outer variable, so it is
+    ///   left untouched (a *correlated* branch).
+    /// - **common** if it appears in every branch: visible outside the `or`,
+    ///   left untouched.
+    /// - **branch-local** otherwise: renamed to a fresh name per branch. If such
+    ///   a variable is also used outside the `or` (in the action or another
+    ///   `or`'s common vars) it is an interface violation.
+    ///
+    /// `outside_vars` is the set of variable names visible outside every `or`
+    /// in this rule (conjunctive-fact vars, action vars, and other `or`s' common
+    /// vars). `conj_vars` is the subset bound by the surrounding conjunction.
     fn rename_or_locals(
         &self,
         body: &[Fact],
         outside_vars: &HashSet<String>,
+        conj_vars: &HashSet<String>,
         symbol_gen: &mut SymbolGen,
     ) -> Result<Vec<Fact>, TypeError> {
         let mut new_body = Vec::with_capacity(body.len());
@@ -883,15 +893,15 @@ impl TypeInfo {
 
                     let mut new_branches = Vec::with_capacity(branches.len());
                     for (branch, branch_vars) in branches.iter().zip(&per_branch_vars) {
-                        // Branch-locals are this branch's non-common,
-                        // non-global vars. If any is used outside the `or`,
-                        // that's an interface violation.
                         let mut subst: HashMap<String, GenericExpr<String, String>> =
                             HashMap::default();
                         for v in branch_vars {
-                            if common.contains(v) {
+                            // Common vars and vars bound by the surrounding
+                            // conjunction (correlated branches) stay as-is.
+                            if common.contains(v) || conj_vars.contains(v) {
                                 continue;
                             }
+                            // A branch-local used outside its `or` is illegal.
                             if outside_vars.contains(v) {
                                 return Err(TypeError::OrBranchLocalEscapes(
                                     v.clone(),
@@ -914,16 +924,24 @@ impl TypeInfo {
                                 )
                             })
                             .collect();
-                        // Recurse to rename locals in nested `or`s within
-                        // this branch. Nested-or vars common to the nested
-                        // branches remain visible within the enclosing branch.
+                        // Recurse to rename locals in nested `or`s within this
+                        // branch. Common and sibling-branch vars, plus the
+                        // enclosing conjunction's vars, are all bound relative to
+                        // a nested `or`.
                         let mut branch_outside = outside_vars.clone();
                         branch_outside.extend(common.iter().cloned());
                         for other_set in &per_branch_vars {
                             branch_outside.extend(other_set.iter().cloned());
                         }
-                        let renamed =
-                            self.rename_or_locals(&renamed, &branch_outside, symbol_gen)?;
+                        let mut branch_conj = conj_vars.clone();
+                        branch_conj.extend(common.iter().cloned());
+                        branch_conj.extend(branch_vars.iter().cloned());
+                        let renamed = self.rename_or_locals(
+                            &renamed,
+                            &branch_outside,
+                            &branch_conj,
+                            symbol_gen,
+                        )?;
                         new_branches.push(renamed);
                     }
                     new_body.push(GenericFact::Or(span.clone(), new_branches));
@@ -959,6 +977,9 @@ impl TypeInfo {
         let has_or = body.iter().any(|f| matches!(f, GenericFact::Or(..)));
         let body: Vec<Fact> = if has_or {
             let mut outside_vars = HashSet::default();
+            // Variables bound by the surrounding conjunction (the non-`or`
+            // facts). A branch may correlate with these (e.g. `(= col d)`).
+            let mut conj_vars = HashSet::default();
             for fact in body {
                 match fact {
                     GenericFact::Or(_, branches) => {
@@ -982,7 +1003,8 @@ impl TypeInfo {
                     other => {
                         let mut set = HashSet::default();
                         self.collect_fact_vars(std::slice::from_ref(other), &mut set);
-                        outside_vars.extend(set);
+                        outside_vars.extend(set.iter().cloned());
+                        conj_vars.extend(set);
                     }
                 }
             }
@@ -991,7 +1013,7 @@ impl TypeInfo {
                     outside_vars.insert(v.clone());
                 }
             });
-            self.rename_or_locals(body, &outside_vars, symbol_gen)?
+            self.rename_or_locals(body, &outside_vars, &conj_vars, symbol_gen)?
         } else {
             body.clone()
         };
diff --git a/tests/disjunction.rs b/tests/disjunction.rs
index 74e0ac529..19a196722 100644
--- a/tests/disjunction.rs
+++ b/tests/disjunction.rs
@@ -261,3 +261,61 @@ fn or_in_rewrite_condition() -> Result<(), Error> {
 (check (= (Add (Num 1) (Num 2)) (Add (Num 2) (Num 1))))
 ")
 }
+
+/// A *correlated* `or` whose branches each equate an outer column with a
+/// variable bound elsewhere in the surrounding conjunction — the e-graph
+/// rebuild pattern. Every branch references the outer-bound `a`/`b`/`c` (from
+/// `v`) and `d` (from the seminaive delta atom `u`); a `(!= d e)` primitive
+/// sits in the conjunction beside the `or`. The action reads another table
+/// (`f`) by function lookup. Under `:unsafe-seminaive` this must fire exactly
+/// for `v`-rows that mention a `u`-key in some column (with `d != e`).
+#[test]
+fn or_correlated_seminaive_rebuild() -> Result<(), Error> {
+    run("
+(relation v (i64 i64 i64))
+(relation u (i64 i64))
+(function f (i64) i64 :merge (max old new))
+(relation hit (i64 i64 i64))
+
+(set (f 1) 10) (set (f 2) 20) (set (f 3) 30)
+(set (f 4) 40) (set (f 5) 50) (set (f 6) 60)
+(set (f 7) 70) (set (f 9) 90)
+
+(v 1 2 3)
+(v 4 5 6)
+(v 7 7 9)
+
+(u 2 8)   ; d=2, e=8: hits (v 1 2 3) via column b
+(u 9 8)   ; d=9, e=8: hits (v 7 7 9) via column c
+(u 5 5)   ; d=e=5: filtered out by (!= d e), so (v 4 5 6) is not hit
+
+(ruleset rr)
+(rule ((v a b c) (u d e) (!= d e) (OR (= a d) (= b d) (= c d)))
+      ((hit (f a) (f b) (f c)))
+      :ruleset rr :unsafe-seminaive)
+(run rr 10)
+
+(check (hit 10 20 30))
+(check (hit 70 70 90))
+(fail (check (hit 40 50 60)))
+")
+}
+
+/// The same correlated pattern in plain (naive) mode also compiles by splitting
+/// and produces the correct fixpoint.
+#[test]
+fn or_correlated_naive() -> Result<(), Error> {
+    run("
+(relation v (i64 i64 i64))
+(relation u (i64 i64))
+(relation hit (i64 i64 i64))
+(v 1 2 3)
+(v 4 5 6)
+(u 2 8)
+(rule ((v a b c) (u d e) (OR (= a d) (= b d) (= c d)))
+      ((hit a b c)))
+(run 5)
+(check (hit 1 2 3))
+(fail (check (hit 4 5 6)))
+")
+}

From 90c92342d5633c880d49459e32bde8254866a517 Mon Sep 17 00:00:00 2001
From: Oliver Flatt <oflatt@gmail.com>
Date: Thu, 2 Jul 2026 04:48:38 +0000
Subject: [PATCH 3/4] Correlated OR via C's deduplicating union node (no
 splitting)

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>
---
 CHANGELOG.md               |   2 +-
 docs/disjunction-design.md | 178 ++++++++++++---------------
 src/lib.rs                 | 241 ++++++++++++++-----------------------
 tests/disjunction.rs       |  93 ++++++++------
 4 files changed, 226 insertions(+), 288 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8ee1302e4..1268a91d3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,7 +2,7 @@
 
 ## [Unreleased] - ReleaseDate
 
-- **Disjunction (`or`) in rule bodies.** A rule body may now contain `(or (branch...) (branch...) ...)` (either spelling `or`/`OR`), where each branch is a conjunction of facts (or a single bare fact, e.g. `(= a d)`); the disjunction matches when at least one branch matches. A branch may be *correlated*: it may reference variables bound by the surrounding conjunction (as in `(= col d)`). Variables usable outside the `or` are those bound by the surrounding conjunction plus those common to every branch; a branch-local variable that escapes its `or`, and an empty branch, are type errors. `or` is only allowed in rule bodies (including `rewrite` conditions), not in query-shaped commands like `check`, and is allowed under the term encoding (without proofs). Compilation uses one of two strategies: a naive rule whose branches each bind their own variables compiles to a single **fused union node** in the free-join engine (the surrounding conjunction is scanned once and joined against the deduplicated union of the branch outputs); a correlated or seminaive `or` (e.g. `:unsafe-seminaive`) compiles by **splitting** into one ordinary backend rule per disjunct, so seminaive evaluation and index-probe joins work normally (a delta on an outer atom drives an index probe of a correlated atom, with no cartesian product). See `docs/disjunction-design.md`.
+- **Disjunction (`or`) in rule bodies.** A rule body may now contain `(or (branch...) (branch...) ...)` (either spelling `or`/`OR`), where each branch is a conjunction of facts (or a single bare fact); the disjunction matches when at least one branch matches. A branch may be *correlated*: it may reference variables bound by the surrounding conjunction (e.g. `(v a b c)` outside, `(stale a al)` inside a branch). Variables usable outside the `or` are those bound by the surrounding conjunction plus those common to every branch; a branch-local variable that escapes its `or`, and an empty branch, are type errors. `or` is only allowed in rule bodies (including `rewrite` conditions), not in query-shaped commands like `check`, and is allowed under the term encoding (without proofs). It compiles to a single backend rule with a fused, **deduplicating** union node in the free-join engine: every branch is enumerated additively and its output tuple is materialized and deduplicated on the union's output variables, so the shared action fires exactly once per distinct output tuple. For a correlated `or`, the surrounding conjunction is prepended into each branch so the branches bind and dedup on the shared row (disjunctive-semijoin single-rebuild: a row matched via several branches rebuilds once); for an independent `or`, the conjunction is scanned once as a continuation joined against the deduplicated branch outputs. `or` rules run in naive mode. See `docs/disjunction-design.md`.
 - Add typed `EGraph` extension state that clones with `EGraph` and is restored by `push`/`pop`.
 - Report full source file paths in egglog span and error messages.
 - Fix seminaive matching after nested containers rebuild in place by propagating dirty container ids through parent containers.
diff --git a/docs/disjunction-design.md b/docs/disjunction-design.md
index 627be4928..8931bba6c 100644
--- a/docs/disjunction-design.md
+++ b/docs/disjunction-design.md
@@ -67,48 +67,48 @@ holds.
    - `src/ast/check_shadowing.rs` recurses into `or` branches when collecting
      pattern variable names.
 
-## Backend compilation
+## Backend compilation: a fused, deduplicating union node
 
-`add_rule` dispatches `or`-containing rules to `add_or_rule`, which picks one of
-two strategies (returning one `(name, core rule, backend rule id)` per compiled
-backend rule):
+An `or`-containing rule compiles to **one** backend rule with a fused union node
+in the free-join engine (`src/lib.rs` `add_or_rule`). Every branch is enumerated
+additively; its output tuple is materialized and **deduplicated on the union's
+output variables**, and the shared action fires exactly once per distinct output
+tuple. Because branch-local variables are *not* output variables, a row matched
+via several branches (which differ only in branch-locals) is processed **once** —
+disjunctive-semijoin single-rebuild semantics.
 
-- **Strategy C — fused union node.** Used when the rule is naive *and* every
-  disjunct is *self-groundable* (`branch_self_groundable`: every non-global
-  variable the disjunct references is bound by one of its own table atoms). One
-  backend rule with a fused union node; `C` is scanned once.
-- **Strategy D — splitting.** Used otherwise — a *correlated* disjunct (which
-  references a `C`-bound variable it does not bind itself) or a seminaive rule.
-  See "Strategy D" below.
-
-## Strategy C — a fused union node in the free-join engine
-
-The `or`-containing rule compiles to **one** backend rule with a fused union
-node in the free-join engine. The surrounding conjunction `C` is scanned
-**once**; the branches are enumerated additively (never a `∏` of separate
-rules). `add_or_rule` (Strategy-C path):
+`add_or_rule`:
 
 1. Splits the body into the conjunction `C` (non-`or` facts) and the `or`s, and
-   forms the union's **branches** as the cartesian product of every `or`'s
-   disjuncts (`expand_or_branch` expands nested `or`s the same way). One `or`
-   gives one branch per disjunct; multiple/nested `or`s give `∏` *branches* (but
-   still one rule, and `C` is still scanned once).
-2. Computes the union's **output variables** (`common_branch_vars`): the
-   variables common to every branch — exactly the variables an `or` shares
-   across its disjuncts, which are the only branch variables visible to `C` and
-   the action.
-3. Compiles `C`'s query and the rule's actions together
+   forms the **disjuncts** as the cartesian product of every `or`'s branches
+   (`expand_or_branch` expands nested `or`s the same way).
+2. Chooses a branch layout by whether any disjunct is *correlated* — references a
+   `C`-bound variable that is not common to every disjunct (e.g. `(v a b c)`
+   outside, `(stale a al)` inside a branch, where `a` comes from `v`):
+   - **Independent** (no correlation): `C` is a **continuation** — scanned once
+     and joined against the deduplicated branch outputs. Branches are the
+     disjuncts; output variables are the variables common to every disjunct.
+   - **Correlated**: `C` is **prepended into every branch**, so each branch binds
+     the shared output tuple itself (typically the surrounding row) and probes
+     the disjunct's own atoms by the correlated columns. The continuation is
+     empty; output variables are the variables common to every prepended branch —
+     the surrounding row.
+3. Computes the union's **output variables** (`common_branch_vars`), excluding
+   `Unit`-sorted variables (they carry no dedup information and may be unbound at
+   runtime, e.g. the unit result of a term-encoding view lookup).
+4. Compiles the continuation's query and the rule's actions together
    (`to_canonicalized_core_rule_extra_binding`) so their flattened
    (fresh-`gensym`) variables agree, adding the output variables to the action
-   binding (they are bound by the union at runtime, not by `C`'s atoms).
-4. Compiles each branch's query on its own
+   binding (they are bound by the union at runtime).
+5. Compiles each branch's query on its own
    (`to_canonicalized_core_rule_ungrounded`; the grounded check is skipped since
-   a branch variable may be grounded by `C`).
-5. Builds one backend rule: adds `C`'s atoms (`BackendRule::query`), then each
-   branch's atoms (`query_union_branch`, recording their `AtomId`s), calls
-   `set_union_branches`, and adds the actions. The rule is compiled in **naive**
-   mode (seminaive delta through a union is unsupported). Branch atoms must be
-   table atoms; a primitive inside a branch is rejected.
+   a correlated branch variable is grounded by the prepended `C`).
+6. Builds one backend rule: adds the continuation's atoms (`BackendRule::query`),
+   then each branch's atoms (`query_union_branch`, recording their `AtomId`s),
+   calls `set_union_branches`, and adds the actions. The rule runs in **naive**
+   mode (see restrictions). Branch atoms must be table atoms; a primitive inside
+   a branch is rejected — a `!=` staleness filter is encoded as a relation (e.g.
+   `(stale term leader)` holding only non-canonical terms).
 
 ### Bridge (`egglog-bridge/src/rule.rs`)
 
@@ -144,77 +144,59 @@ translates the high-level atom indices / variable ids into the core-relations
   block's `action`/`action_buf`. Because block 0 runs with the block's
   `InPlaceMaterializer`, each branch match is written into one materialization
   keyed on the output variables — **deduplicated on the key**, in memory, with
-  no temporary database table. The result block then joins `C` once against
-  that materialization.
+  no temporary database table. The result block then iterates the distinct
+  output tuples (`FusedIntersectMat { mode: KeyOnly }`, joining the continuation
+  atoms if any) and fires the action **once per key**.
 
-This shares `C`: it is evaluated a single time in the result block, joined by
-index against the deduplicated union of the branch outputs — never re-scanned per
-branch and never producing `∏` separate rules.
+For an independent `or`, the continuation `C` is evaluated a single time in the
+result block, joined by index against the deduplicated union of the branch
+outputs. For a correlated `or`, the continuation is empty (it was prepended into
+every branch), so the result block simply enumerates the deduplicated output
+tuples and fires the action once each.
 
-### Strategy-C tradeoffs / restrictions
+### The correlated rebuild pattern
 
-- **Naive only.** Strategy C runs in naive mode; a seminaive rule uses Strategy
-  D instead.
-- **Primitives in branches** are rejected (a branch must be a conjunction of
-  table atoms). Primitives in the surrounding conjunction `C` are fine.
-- **`∏` branches for multiple/nested `or`s.** `k` disjunctions produce `∏`
-  union *branches* (enumerated additively into one materialization), but still a
-  single rule with `C` scanned once. A single `or` (the common case) is linear.
-- **No cross-branch dedup of firings beyond the output key.** The union
-  deduplicates output tuples; like every egglog rule, the action still fires per
-  full match otherwise. This matches egglog's normal non-dedup semantics and is
-  invisible for idempotent actions.
-
-## Strategy D — splitting (correlated / seminaive `or`s)
-
-Strategy C's fused union requires each branch to bind the union's output
-variables *itself* (its branches run first, materializing those variables), and
-it forces naive mode. Neither holds for a **correlated** `or` such as the
-e-graph rebuild pattern
+The motivating example is e-graph rebuild. With a view `AddView(a,b,c)` and a
+staleness relation `stale(term, leader)` (holding only non-canonical terms):
 
 ```
-(rule ((MulView c0 c1 c2) (UF_Math d e) (!= d e)
-       (OR (= c0 d) (= c1 d) (= c2 d)))
-      (...)
+(rule ((AddView a b c)
+       (OR ((stale a al)) ((stale b bl)) ((stale c cl))))
+      ((AddView (leader a) (leader b) (leader c))
+       (delete (AddView a b c)))
       :ruleset rebuilding :unsafe-seminaive)
 ```
 
-where each disjunct only *constrains* variables (`c0`/`d`) bound by the
-surrounding conjunction, and where per-disjunct variable merging (`c0 = d` in
-one branch, `c1 = d` in another) must propagate into the shared action.
-
-`add_or_rule` (via `add_or_rule_split` in `src/lib.rs`) therefore compiles a
-correlated or seminaive `or` by **splitting**: the disjuncts are expanded into
-the cartesian product of the `or`s (`expand_or_branch`), and for each combined
-disjunct one ordinary backend rule is emitted, with body `C ∧ disjunct` and the
-rule's shared action. Extra split rules get synthetic names `{name}__or{i}` so
-they coexist in the ruleset (`add_rule` inserts one ruleset entry per split).
-
-Each split rule is a plain conjunctive rule, so the existing machinery does the
-right thing with no changes to the free-join engine or seminaive evaluation:
-
-- **Per-disjunct canonicalization** merges each disjunct's equalities
-  independently. `(= c0 d)` substitutes `c0 → d`, so `MulView(c0,c1,c2)` becomes
-  `MulView(d,c1,c2)` sharing variable `d` with `UF_Math(d,e)`. A join on a
-  shared variable is an **index probe**, never a cartesian product — even in
-  naive mode. The merge propagates into the action, so a correlated variable
-  resolves correctly there too.
-- **Seminaive** (`:unsafe-seminaive`) runs normally per split rule. A delta on
-  the outer atom (`UF_Math`) drives an index probe of the correlated atom
-  (`MulView`) by the new key; a delta on `MulView` probes `UF_Math`. The
-  `Read`/`Full` RHS contexts of `:unsafe-seminaive` let the action perform
-  lookups (e.g. `(UF_Mathf c0)`).
-- **Primitives** in the surrounding conjunction (e.g. `(!= d e)`) are ordinary
-  RHS-context checks in each split rule.
-
-### Strategy-D tradeoffs / restrictions
-
-- **`k` backend rules per `or`.** A `k`-way `or` (or `∏` over several `or`s)
-  becomes `k` (or `∏`) backend rules. In seminaive mode this is cheap — each
-  processes only the delta and probes by index — so the cartesian-product
-  blow-up the fused union avoids does not reappear.
-- **Split rule names.** Extra disjuncts occupy synthetic `{name}__or{i}`
-  ruleset entries, which show up separately in run reports.
+Each branch references the outer row `a`/`b`/`c` and probes `stale` on one
+column, binding a branch-local leader. `AddView` is prepended into every branch,
+so the output/dedup variables are the row `(a b c)`. A row stale in two columns
+matches two branches but produces the same `(a b c)` tuple, so the shared action
+rebuilds it **exactly once**. `:unsafe-seminaive` supplies the `Read`/`Full` RHS
+context the action needs for the `leader` lookups.
+
+### Restrictions
+
+- **Naive evaluation.** The rule runs naive: the seminaive delta machinery
+  constrains atoms by their position in the top-level plan's atom list, but a
+  union's branch atoms live in per-branch sub-plans a delta focus can't reach.
+  This is correct at a fixpoint (a rebuild rule that deletes the stale row
+  converges), but not incremental. Making the delta drive an index probe of a
+  branch atom (the true seminaive rebuild) needs the delta machinery extended to
+  reach `JoinStage::Union` branches — future work.
+- **Primitives in branches** are rejected (a branch must be a conjunction of
+  table atoms). Primitives in the surrounding conjunction are fine; a `!=`
+  staleness filter is encoded as a staleness relation instead.
+- **`∏` branches for multiple/nested `or`s.** `k` disjunctions produce `∏` union
+  *branches* (enumerated additively into one deduplicated materialization), but
+  still a single rule. A single `or` (the common case) is linear.
+- **Dedup granularity.** Deduplication is on the (non-`Unit`) output tuple. For a
+  correlated rebuild the output is the surrounding row, giving single-rebuild.
+- **Branch-bound output (Shape B).** A layout where each branch *binds* the
+  output row itself and pins an outer variable into a different column per branch
+  (e.g. `((AddView a x1 x2)) ((AddView x0 a x2)) ...`) is not supported: aligning
+  the per-branch row columns onto shared output variables would need per-branch
+  output projections on the union node. The prepended-conjunction layout above
+  covers the same rebuild use case.
 
 ## Proofs and the term encoding
 
diff --git a/src/lib.rs b/src/lib.rs
index 646bc492c..3e468af53 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1209,27 +1209,29 @@ impl EGraph {
         }
     }
 
-    /// Compiles a rule whose body contains one or more `or` facts.
+    /// Compiles a rule whose body contains one or more `or` facts into a single
+    /// backend rule with a fused, **deduplicating** union node in the free-join
+    /// engine (see [`egglog_bridge::RuleBuilder::set_union_branches`] and
+    /// `core_relations::QueryBuilder::set_union`). Every branch is evaluated
+    /// additively, its output tuple is materialized and **deduplicated on the
+    /// union's output variables**, and the shared action fires exactly once per
+    /// distinct output tuple.
     ///
-    /// Two strategies:
-    /// - **Fused union (Strategy C).** When every disjunct is *self-groundable*
-    ///   (binds all its own variables with its own table atoms) and the rule is
-    ///   naive, the whole `or` compiles to a single backend rule with a fused
-    ///   union node: the surrounding conjunction is joined once against the
-    ///   deduplicated union of the branch outputs (see
-    ///   [`egglog_bridge::RuleBuilder::set_union_branches`] and
-    ///   `core_relations::QueryBuilder::set_union`).
-    /// - **Splitting (Strategy D).** Otherwise — a *correlated* branch (one that
-    ///   references a variable bound by the surrounding conjunction, e.g.
-    ///   `(= col d)`), or a seminaive rule — the `or` compiles to one backend
-    ///   rule per disjunct, each the surrounding conjunction conjoined with that
-    ///   disjunct and the shared action. Each split rule is an ordinary
-    ///   conjunctive rule, so seminaive evaluation and index-probe joins work
-    ///   normally: a delta on an outer atom drives an index probe of the atom a
-    ///   correlated equality constrains, with no cartesian product.
+    /// Two branch layouts, chosen by whether any disjunct is *correlated* (i.e.
+    /// references a variable bound by the surrounding conjunction that is not
+    /// common to every disjunct):
+    /// - **Independent.** The surrounding conjunction `C` is a continuation:
+    ///   scanned once and joined against the deduplicated union of the branch
+    ///   outputs. Output variables are the variables common to every disjunct.
+    /// - **Correlated.** `C` is prepended into every branch so each branch binds
+    ///   the shared output tuple itself (typically the surrounding row) and
+    ///   probes the disjunct's own atoms by the correlated columns. The output
+    ///   variables are the variables common to every (prepended) branch — the
+    ///   surrounding row. Deduplicating on that row gives disjunctive-semijoin
+    ///   semantics: a row matched via several branches is rebuilt exactly once.
     ///
-    /// Returns one `(name, core rule, backend rule id)` per compiled backend
-    /// rule (one for a fused union, one per disjunct when splitting).
+    /// Branches must be conjunctions of table atoms; a branch primitive is
+    /// rejected (a staleness relation can encode a `!=` filter instead).
     fn add_or_rule(
         &mut self,
         rule: &ast::ResolvedRule,
@@ -1239,65 +1241,87 @@ impl EGraph {
         requires_read_context: bool,
     ) -> Result<Vec<(String, core::ResolvedCoreRule, egglog_bridge::RuleId)>, Error> {
         // Split the body into the surrounding conjunction and the `or`s, then
-        // form the branches as the cartesian product of every `or`'s branches
-        // (each combined branch is a conjunction, with nested `or`s expanded the
-        // same way). A single `or` gives one branch per disjunct.
+        // form the disjuncts as the cartesian product of every `or`'s branches
+        // (each combined disjunct is a conjunction, with nested `or`s expanded
+        // the same way). A single `or` gives one disjunct per branch.
         let mut conj_facts: Vec<ast::ResolvedFact> = Vec::new();
-        let mut combined_branches: Vec<Vec<ast::ResolvedFact>> = vec![vec![]];
+        let mut disjuncts: Vec<Vec<ast::ResolvedFact>> = vec![vec![]];
         for fact in &rule.body {
             match fact {
                 ast::ResolvedFact::Or(_, branches) => {
                     let branch_expansions: Vec<Vec<ast::ResolvedFact>> =
                         branches.iter().flat_map(|b| expand_or_branch(b)).collect();
-                    let mut next =
-                        Vec::with_capacity(combined_branches.len() * branch_expansions.len());
-                    for combo in &combined_branches {
+                    let mut next = Vec::with_capacity(disjuncts.len() * branch_expansions.len());
+                    for combo in &disjuncts {
                         for expansion in &branch_expansions {
                             let mut new_combo = combo.clone();
                             new_combo.extend(expansion.iter().cloned());
                             next.push(new_combo);
                         }
                     }
-                    combined_branches = next;
+                    disjuncts = next;
                 }
                 other => conj_facts.push(other.clone()),
             }
         }
 
-        // Correlated (non-self-groundable) branches and seminaive rules can't use
-        // C's fused union node (its branches must bind the union's output vars
-        // themselves, and it forces naive mode). Fall back to splitting.
-        let fused_union_ok =
-            !seminaive && combined_branches.iter().all(|b| branch_self_groundable(b));
-        if !fused_union_ok {
-            return self.add_or_rule_split(
-                rule,
-                &conj_facts,
-                &combined_branches,
-                union_to_set,
-                seminaive,
-                no_decomp,
-                requires_read_context,
-            );
-        }
+        // A disjunct is *correlated* if it references a variable bound by the
+        // surrounding conjunction that is not common to every disjunct (e.g.
+        // `(UF_Math a al)` where `a` comes from the outer row). Such a branch
+        // cannot bind the shared output row on its own, so the surrounding
+        // conjunction is prepended into every branch; the branches then bind the
+        // row and probe their own atoms by the correlated columns. Independent
+        // `or`s keep the conjunction as a scanned-once continuation.
+        let conj_vars = {
+            let mut m = IndexMap::default();
+            collect_resolved_fact_vars(&conj_facts, &mut m);
+            m
+        };
+        let disjunct_common = common_branch_vars(&disjuncts);
+        let disjunct_common_names: IndexSet<String> =
+            disjunct_common.iter().map(|v| v.name.clone()).collect();
+        let correlated = disjuncts.iter().any(|d| {
+            let mut m = IndexMap::default();
+            collect_resolved_fact_vars(d, &mut m);
+            m.keys()
+                .any(|name| conj_vars.contains_key(name) && !disjunct_common_names.contains(name))
+        });
+
+        // Branch fact lists and continuation depend on the layout.
+        let (branch_fact_lists, continuation_facts): (Vec<Vec<ast::ResolvedFact>>, Vec<_>) =
+            if correlated {
+                let branches = disjuncts
+                    .iter()
+                    .map(|d| {
+                        let mut b = conj_facts.clone();
+                        b.extend(d.iter().cloned());
+                        b
+                    })
+                    .collect();
+                (branches, Vec::new())
+            } else {
+                (disjuncts.clone(), conj_facts.clone())
+            };
 
-        // The variables visible outside the `or`s (shared with the surrounding
-        // conjunction and the action) are the union's output variables: the
-        // variables that appear in every branch of an `or`. We take, for each
-        // combined branch, the intersection of variable sets across all combined
-        // branches — a variable common to every combined branch is exactly a
-        // variable common to every disjunct of every `or`.
-        let output_resolved_vars = common_branch_vars(&combined_branches);
+        // The union's output/dedup variables are the variables common to every
+        // branch (with the conjunction prepended in the correlated case), shared
+        // with the continuation and the action. `Unit`-sorted variables are
+        // excluded: they carry no information for deduplication and (e.g. the
+        // unit result of a term-encoding view lookup) may not be materialized as
+        // a runtime binding.
+        let output_resolved_vars: Vec<ResolvedVar> = common_branch_vars(&branch_fact_lists)
+            .into_iter()
+            .filter(|v| v.sort.name() != "Unit")
+            .collect();
 
-        // Compile the surrounding conjunction's query and the rule's actions
-        // together, so their flattened (fresh) variables are consistent. The
-        // `or`'s output variables are added to the action binding: they are not
-        // in the conjunction's atoms but are bound by the fused union at
-        // runtime, and the actions may read them.
+        // Compile the continuation's query and the rule's actions together, so
+        // their flattened (fresh) variables are consistent. The output variables
+        // are added to the action binding: they are bound by the fused union at
+        // runtime and the actions may read them.
         let conj_rule = ast::ResolvedRule {
             span: rule.span.clone(),
             head: rule.head.clone(),
-            body: conj_facts.clone(),
+            body: continuation_facts,
             name: rule.name.clone(),
             ruleset: rule.ruleset.clone(),
             eval_mode: rule.eval_mode,
@@ -1311,12 +1335,12 @@ impl EGraph {
             &output_resolved_vars,
         )?;
 
-        // Flatten each combined branch into a canonicalized core query. The
-        // grounded check is skipped: a branch variable may be grounded by the
-        // surrounding conjunction rather than the branch.
+        // Flatten each branch into a canonicalized core query. The grounded
+        // check is skipped: a branch variable may be grounded by the surrounding
+        // conjunction rather than the branch.
         let mut branch_queries: Vec<core::Query<ResolvedCall, ResolvedVar>> =
-            Vec::with_capacity(combined_branches.len());
-        for branch in &combined_branches {
+            Vec::with_capacity(branch_fact_lists.len());
+        for branch in &branch_fact_lists {
             let branch_rule = ast::ResolvedRule {
                 span: rule.span.clone(),
                 head: Default::default(),
@@ -1335,14 +1359,18 @@ impl EGraph {
             branch_queries.push(core_branch.body);
         }
 
-        // Build the backend rule. Union rules run in naive mode (seminaive
-        // delta through a union is unsupported).
         let rule_id = {
+            // Run in naive mode: the seminaive delta machinery constrains atoms
+            // by their position in `plan.atoms`, but a union's branch atoms live
+            // in per-branch sub-plans, so a delta focus can't reach them. The
+            // `:unsafe-seminaive` Read/Full RHS context (for action lookups) is
+            // still honored via `requires_read_context`.
+            let _ = seminaive;
             let mut rb = self.backend.new_rule(&rule.name, false);
             rb.set_no_decomp(no_decomp);
             let mut translator =
                 BackendRule::new(rb, &self.functions, &self.type_info, requires_read_context);
-            // Continuation (surrounding conjunction) atoms.
+            // Continuation (surrounding conjunction) atoms, if any.
             translator.query(&core_conj.body, rule.include_subsumed);
             // Branch atoms, recording which backend AtomIds belong to each branch.
             let mut branch_atom_ids = Vec::with_capacity(branch_queries.len());
@@ -1365,62 +1393,6 @@ impl EGraph {
         Ok(vec![(rule.name.clone(), core_conj, rule_id)])
     }
 
-    /// Strategy D: compile an `or` rule by splitting it into one ordinary
-    /// backend rule per disjunct, each conjoining the surrounding conjunction
-    /// with that disjunct and firing the shared action. See [`Self::add_or_rule`].
-    #[allow(clippy::too_many_arguments)]
-    fn add_or_rule_split(
-        &mut self,
-        rule: &ast::ResolvedRule,
-        conj_facts: &[ast::ResolvedFact],
-        combined_branches: &[Vec<ast::ResolvedFact>],
-        union_to_set: bool,
-        seminaive: bool,
-        no_decomp: bool,
-        requires_read_context: bool,
-    ) -> Result<Vec<(String, core::ResolvedCoreRule, egglog_bridge::RuleId)>, Error> {
-        let mut compiled = Vec::with_capacity(combined_branches.len());
-        for (i, branch) in combined_branches.iter().enumerate() {
-            // Each split rule is `conjunction ∧ branch => action`. Per-branch
-            // canonicalization merges each disjunct's equalities (e.g. `(= col
-            // d)`) independently, so a correlated variable resolves correctly in
-            // both the body and the shared action.
-            let mut body = conj_facts.to_vec();
-            body.extend(branch.iter().cloned());
-            let name = if i == 0 {
-                rule.name.clone()
-            } else {
-                format!("{}__or{i}", rule.name)
-            };
-            let split_rule = ast::ResolvedRule {
-                span: rule.span.clone(),
-                head: rule.head.clone(),
-                body,
-                name: name.clone(),
-                ruleset: rule.ruleset.clone(),
-                eval_mode: rule.eval_mode,
-                no_decomp: rule.no_decomp,
-                include_subsumed: rule.include_subsumed,
-            };
-            let core_rule = split_rule.to_canonicalized_core_rule(
-                &self.type_info,
-                &mut self.parser.symbol_gen,
-                union_to_set,
-            )?;
-            let rule_id = {
-                let mut rb = self.backend.new_rule(&name, seminaive);
-                rb.set_no_decomp(no_decomp);
-                let mut translator =
-                    BackendRule::new(rb, &self.functions, &self.type_info, requires_read_context);
-                translator.query(&core_rule.body, split_rule.include_subsumed);
-                translator.actions(&core_rule.head)?;
-                translator.build()
-            };
-            compiled.push((name, core_rule, rule_id));
-        }
-        Ok(compiled)
-    }
-
     fn eval_actions(&mut self, actions: &ResolvedActions) -> Result<(), Error> {
         let mut binding = IndexSet::default();
         let mut ctx = CoreActionContext::new(
@@ -3044,35 +3016,6 @@ impl<'a> BackendRule<'a> {
     }
 }
 
-/// Whether every non-global variable referenced by `branch` is bound by one of
-/// the branch's own table (function/relation) atoms. A self-groundable branch
-/// can be evaluated by C's fused union node, which requires each branch to bind
-/// the union's output variables itself. A branch that references a variable it
-/// does not bind — a *correlated* branch, e.g. `(= col d)` where `col` and `d`
-/// come from the surrounding conjunction — is not self-groundable and is
-/// compiled by splitting instead.
-fn branch_self_groundable(branch: &[ast::ResolvedFact]) -> bool {
-    let mut bound: IndexSet<String> = IndexSet::default();
-    for fact in branch {
-        if let ast::ResolvedFact::Fact(ResolvedExpr::Call(_, ResolvedCall::Func(_), _)) = fact {
-            fact.visit_vars(&mut |_, v| {
-                if !v.is_global_ref {
-                    bound.insert(v.name.clone());
-                }
-            });
-        }
-    }
-    let mut groundable = true;
-    for fact in branch {
-        fact.visit_vars(&mut |_, v| {
-            if !v.is_global_ref && !bound.contains(&v.name) {
-                groundable = false;
-            }
-        });
-    }
-    groundable
-}
-
 /// Expands one `or` branch (a conjunction of facts that may itself contain
 /// nested `or`s) into a list of purely-conjunctive fact lists — one per
 /// combination of the nested disjuncts. A branch with no nested `or` yields a
diff --git a/tests/disjunction.rs b/tests/disjunction.rs
index 19a196722..c9cb0beac 100644
--- a/tests/disjunction.rs
+++ b/tests/disjunction.rs
@@ -262,60 +262,73 @@ fn or_in_rewrite_condition() -> Result<(), Error> {
 ")
 }
 
-/// A *correlated* `or` whose branches each equate an outer column with a
-/// variable bound elsewhere in the surrounding conjunction — the e-graph
-/// rebuild pattern. Every branch references the outer-bound `a`/`b`/`c` (from
-/// `v`) and `d` (from the seminaive delta atom `u`); a `(!= d e)` primitive
-/// sits in the conjunction beside the `or`. The action reads another table
-/// (`f`) by function lookup. Under `:unsafe-seminaive` this must fire exactly
-/// for `v`-rows that mention a `u`-key in some column (with `d != e`).
+/// Correlated deduplicating rebuild (e-graph rebuild shape). The surrounding
+/// conjunction binds the row `(v a b c)`; each `or` branch references an outer
+/// column and probes a staleness relation `stale` on it, binding a branch-local
+/// leader. The row is rebuilt via a `leader` function lookup. A row stale in
+/// *two* columns matches two branches, but the fused deduplicating union keys on
+/// the shared output row `(a b c)`, so the action fires **exactly once** — the
+/// disjunctive-semijoin single-rebuild guarantee (not once per stale column,
+/// which is what rule-splitting would do). `fire` counts firings via `(+)`.
 #[test]
-fn or_correlated_seminaive_rebuild() -> Result<(), Error> {
+fn or_correlated_dedup_single_rebuild() -> Result<(), Error> {
     run("
 (relation v (i64 i64 i64))
-(relation u (i64 i64))
-(function f (i64) i64 :merge (max old new))
-(relation hit (i64 i64 i64))
+(relation stale (i64 i64))       ; (term, leader) for non-canonical terms
+(function leader (i64) i64 :merge (max old new))
+(function fire (i64 i64 i64) i64 :merge (+ old new))
+(relation rebuilt (i64 i64 i64))
 
-(set (f 1) 10) (set (f 2) 20) (set (f 3) 30)
-(set (f 4) 40) (set (f 5) 50) (set (f 6) 60)
-(set (f 7) 70) (set (f 9) 90)
+(set (leader 1) 11) (set (leader 2) 22) (set (leader 3) 3)
+(set (leader 4) 4) (set (leader 5) 55) (set (leader 6) 6)
+(stale 1 11) (stale 2 22) (stale 5 55)
 
-(v 1 2 3)
-(v 4 5 6)
-(v 7 7 9)
-
-(u 2 8)   ; d=2, e=8: hits (v 1 2 3) via column b
-(u 9 8)   ; d=9, e=8: hits (v 7 7 9) via column c
-(u 5 5)   ; d=e=5: filtered out by (!= d e), so (v 4 5 6) is not hit
+(v 1 2 3)   ; columns 1 AND 2 are stale -> matched by two branches
+(v 4 5 6)   ; only column 5 stale -> one branch
+(v 4 4 4)   ; nothing stale -> no branch
 
 (ruleset rr)
-(rule ((v a b c) (u d e) (!= d e) (OR (= a d) (= b d) (= c d)))
-      ((hit (f a) (f b) (f c)))
+(rule ((v a b c)
+       (OR ((stale a al)) ((stale b bl)) ((stale c cl))))
+      ((set (fire a b c) 1)
+       (rebuilt (leader a) (leader b) (leader c)))
       :ruleset rr :unsafe-seminaive)
-(run rr 10)
+(run rr 1)
 
-(check (hit 10 20 30))
-(check (hit 70 70 90))
-(fail (check (hit 40 50 60)))
+; row stale in two columns fires ONCE (dedup), not twice
+(check (= (fire 1 2 3) 1))
+(check (= (fire 4 5 6) 1))
+(fail (check (= (fire 4 4 4) 1)))
+; action ran and used the leader-function lookups
+(check (rebuilt 11 22 3))
+(check (rebuilt 4 55 6))
 ")
 }
 
-/// The same correlated pattern in plain (naive) mode also compiles by splitting
-/// and produces the correct fixpoint.
+/// A correlated dedup union whose action reads another table by function lookup
+/// (as in the real rebuild) and rewrites the row to its canonical form,
+/// deleting the stale one; run to a fixpoint.
 #[test]
-fn or_correlated_naive() -> Result<(), Error> {
+fn or_correlated_rebuild_to_fixpoint() -> Result<(), Error> {
     run("
 (relation v (i64 i64 i64))
-(relation u (i64 i64))
-(relation hit (i64 i64 i64))
-(v 1 2 3)
-(v 4 5 6)
-(u 2 8)
-(rule ((v a b c) (u d e) (OR (= a d) (= b d) (= c d)))
-      ((hit a b c)))
-(run 5)
-(check (hit 1 2 3))
-(fail (check (hit 4 5 6)))
+(relation stale (i64 i64))
+(function leader (i64) i64 :merge (max old new))
+
+(set (leader 1) 2) (set (leader 2) 2) (set (leader 3) 3)
+(stale 1 2)   ; term 1 is non-canonical, leader 2
+
+(v 1 1 3)     ; stale in columns 0 and 1
+
+(ruleset rr)
+(rule ((v a b c)
+       (OR ((stale a al)) ((stale b bl)) ((stale c cl))))
+      ((v (leader a) (leader b) (leader c))
+       (delete (v a b c)))
+      :ruleset rr :unsafe-seminaive)
+(run rr 3)
+
+(check (v 2 2 3))
+(fail (check (v 1 1 3)))
 ")
 }

From 752c791c17dc26f22fd0c4963e0fd392f4c37c31 Mon Sep 17 00:00:00 2001
From: Oliver Flatt <oflatt@gmail.com>
Date: Thu, 2 Jul 2026 16:47:29 +0000
Subject: [PATCH 4/4] Make the correlated union node seminaive / delta-driven
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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>
---
 CHANGELOG.md                |   2 +-
 core-relations/src/query.rs | 111 +++++++++++++++++++++++++++++++++++-
 docs/disjunction-design.md  |  49 ++++++++++++----
 egglog-bridge/src/rule.rs   |  48 +++++++++++++++-
 src/lib.rs                  |  32 ++++++-----
 tests/disjunction.rs        |  40 +++++++++++++
 6 files changed, 252 insertions(+), 30 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1268a91d3..9158908d8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,7 +2,7 @@
 
 ## [Unreleased] - ReleaseDate
 
-- **Disjunction (`or`) in rule bodies.** A rule body may now contain `(or (branch...) (branch...) ...)` (either spelling `or`/`OR`), where each branch is a conjunction of facts (or a single bare fact); the disjunction matches when at least one branch matches. A branch may be *correlated*: it may reference variables bound by the surrounding conjunction (e.g. `(v a b c)` outside, `(stale a al)` inside a branch). Variables usable outside the `or` are those bound by the surrounding conjunction plus those common to every branch; a branch-local variable that escapes its `or`, and an empty branch, are type errors. `or` is only allowed in rule bodies (including `rewrite` conditions), not in query-shaped commands like `check`, and is allowed under the term encoding (without proofs). It compiles to a single backend rule with a fused, **deduplicating** union node in the free-join engine: every branch is enumerated additively and its output tuple is materialized and deduplicated on the union's output variables, so the shared action fires exactly once per distinct output tuple. For a correlated `or`, the surrounding conjunction is prepended into each branch so the branches bind and dedup on the shared row (disjunctive-semijoin single-rebuild: a row matched via several branches rebuilds once); for an independent `or`, the conjunction is scanned once as a continuation joined against the deduplicated branch outputs. `or` rules run in naive mode. See `docs/disjunction-design.md`.
+- **Disjunction (`or`) in rule bodies.** A rule body may now contain `(or (branch...) (branch...) ...)` (either spelling `or`/`OR`), where each branch is a conjunction of facts (or a single bare fact); the disjunction matches when at least one branch matches. A branch may be *correlated*: it may reference variables bound by the surrounding conjunction (e.g. `(v a b c)` outside, `(stale a al)` inside a branch). Variables usable outside the `or` are those bound by the surrounding conjunction plus those common to every branch; a branch-local variable that escapes its `or`, and an empty branch, are type errors. `or` is only allowed in rule bodies (including `rewrite` conditions), not in query-shaped commands like `check`, and is allowed under the term encoding (without proofs). It compiles to a single backend rule with a fused, **deduplicating** union node in the free-join engine: every branch is enumerated additively and its output tuple is materialized and deduplicated on the union's output variables, so the shared action fires exactly once per distinct output tuple. For a correlated `or`, the surrounding conjunction is prepended into each branch so the branches bind and dedup on the shared row (disjunctive-semijoin single-rebuild: a row matched via several branches rebuilds once), and it runs **seminaive / delta-driven** — a new tuple in a branch atom drives an index probe of the row rather than a re-scan (semi-naive of a union of conjunctions = the union of the per-disjunct expansions). An independent `or` scans the conjunction once as a continuation joined against the deduplicated branch outputs and runs naive. See `docs/disjunction-design.md`.
 - Add typed `EGraph` extension state that clones with `EGraph` and is restored by `push`/`pop`.
 - Report full source file paths in egglog span and error messages.
 - Fix seminaive matching after nested containers rebuild in place by propagating dirty container ids through parent containers.
diff --git a/core-relations/src/query.rs b/core-relations/src/query.rs
index 2e48d11ef..b952a56f1 100644
--- a/core-relations/src/query.rs
+++ b/core-relations/src/query.rs
@@ -16,7 +16,7 @@ use crate::{
     free_join::{
         ActionId, AtomId, Database, ProcessedConstraints, SubAtom, TableId, TableInfo, VarInfo,
         Variable,
-        plan::{JoinHeader, JoinStages, Plan, PlanStrategy},
+        plan::{JoinHeader, JoinStage, JoinStages, Plan, PlanStrategy, UnionBranch},
     },
     pool::{Pooled, with_pool_set},
     table_spec::{ColumnId, Constraint},
@@ -274,6 +274,110 @@ impl<'outer> RuleSetBuilder<'outer> {
         )
     }
 
+    /// Reprocesses a union branch's header constraints against the current
+    /// database and adds `extra` timestamp constraints (per-atom), returning a
+    /// fresh [`UnionBranch`] over the same atoms and stages. Returns `None` if
+    /// any atom's constraints select zero rows (the branch is empty this epoch).
+    fn reprocess_union_branch(
+        &self,
+        branch: &UnionBranch,
+        extra: &[(AtomId, Constraint)],
+    ) -> Option<UnionBranch> {
+        let mut header = Vec::new();
+        for (atom_id, atom_info) in branch.atoms.iter() {
+            let mut constraints: Vec<Constraint> = branch
+                .header
+                .iter()
+                .filter(|h| h.atom == atom_id)
+                .flat_map(|h| h.constraints.iter().cloned())
+                .collect();
+            for (a, c) in extra {
+                if *a == atom_id {
+                    constraints.push(c.clone());
+                }
+            }
+            if constraints.is_empty() {
+                continue;
+            }
+            header.push(self.reprocess_constraints(atom_info.table, atom_id, &constraints)?);
+        }
+        Some(UnionBranch {
+            atoms: branch.atoms.clone(),
+            header,
+            stages: branch.stages.clone(),
+        })
+    }
+
+    /// Add a seminaive variant of a fused-union rule from a cached plan.
+    ///
+    /// Semi-naive of a union of conjunctions is the union of the per-disjunct
+    /// seminaive expansions: `seminaive(⋁ᵢ Bᵢ) = ⋃ᵢ seminaive(Bᵢ)`. Each entry
+    /// of `variants` is `(branch_index, per-atom timestamp constraints)` for one
+    /// such expansion term; it becomes one *variant branch* (the cached branch
+    /// `branch_index` narrowed by those constraints via its header). All variant
+    /// branches are collected into the single [`JoinStage::Union`] so they feed
+    /// the one deduplicating materialization and the shared action — so a row
+    /// matched via several branches is still processed once.
+    ///
+    /// Requires a cached union plan whose sole block-0 stage is a `Union` (as
+    /// produced by `plan_union`). Returns `None` if no variant branch is live.
+    pub fn add_union_rule_from_cached(
+        &mut self,
+        cached: &CachedPlan,
+        variants: &[(usize, Vec<(AtomId, Constraint)>)],
+    ) -> Option<RuleId> {
+        let Plan::DecomposedPlan(dp) = &cached.plan else {
+            panic!("add_union_rule_from_cached: cached plan is not a decomposed union plan");
+        };
+        let block0 = &dp.stages.blocks[0];
+        let JoinStage::Union { branches } = &block0.0.instrs[0] else {
+            panic!("add_union_rule_from_cached: block 0 is not a Union stage");
+        };
+
+        let mut new_branches = Vec::with_capacity(variants.len());
+        for (branch_index, extra) in variants {
+            if let Some(vb) = self.reprocess_union_branch(&branches[*branch_index], extra) {
+                new_branches.push(vb);
+            }
+        }
+        if new_branches.is_empty() {
+            return None;
+        }
+
+        // Reprocess the (possibly empty) continuation header against the current
+        // database, mirroring `get_rule_with_extra_constraints`.
+        let mut header = vec![];
+        self.reprocess_existing_headers(&mut header, &dp.atoms, &dp.header)?;
+
+        let action_id = self.rule_set.actions.next_id();
+        let new_block0 = (
+            JoinStages {
+                instrs: Arc::new(vec![JoinStage::Union {
+                    branches: new_branches,
+                }]),
+            },
+            block0.1.clone(),
+        );
+        let plan = Plan::DecomposedPlan(DecomposedPlan {
+            atoms: dp.atoms.clone(),
+            header,
+            stages: JoinStageBlocks {
+                blocks: vec![new_block0],
+            },
+            result_block: JoinStages {
+                instrs: dp.result_block.instrs.clone(),
+            },
+            actions: action_id,
+        });
+        let actual_action_id = self.rule_set.actions.push(cached.actions.clone());
+        debug_assert_eq!(action_id, actual_action_id);
+        Some(
+            self.rule_set
+                .plans
+                .push((plan, cached.desc.clone(), cached.symbol_map.clone())),
+        )
+    }
+
     /// Build the ruleset.
     pub fn build(self) -> RuleSet {
         self.rule_set
@@ -315,8 +419,9 @@ impl<'outer, 'a> QueryBuilder<'outer, 'a> {
     /// (the variables common to every branch).
     ///
     /// A union query is always planned as a single bag (tree-decomposition is
-    /// skipped), and is intended to be run in naive mode (seminaive delta
-    /// through a union is not supported).
+    /// skipped). Seminaive evaluation is delivered by
+    /// [`RuleSetBuilder::add_union_rule_from_cached`], which delta-drives each
+    /// branch (the union of the per-disjunct seminaive expansions).
     pub fn set_union(&mut self, branch_atoms: Vec<Vec<AtomId>>, output_vars: Vec<Variable>) {
         self.query.no_decomp = true;
         self.query.union = Some(UnionSpec {
diff --git a/docs/disjunction-design.md b/docs/disjunction-design.md
index 8931bba6c..15c9fbfe6 100644
--- a/docs/disjunction-design.md
+++ b/docs/disjunction-design.md
@@ -105,9 +105,10 @@ disjunctive-semijoin single-rebuild semantics.
    a correlated branch variable is grounded by the prepended `C`).
 6. Builds one backend rule: adds the continuation's atoms (`BackendRule::query`),
    then each branch's atoms (`query_union_branch`, recording their `AtomId`s),
-   calls `set_union_branches`, and adds the actions. The rule runs in **naive**
-   mode (see restrictions). Branch atoms must be table atoms; a primitive inside
-   a branch is rejected — a `!=` staleness filter is encoded as a relation (e.g.
+   calls `set_union_branches`, and adds the actions. A correlated rule runs
+   **seminaive / delta-driven** (see "Seminaive execution"); an independent one
+   runs naive. Branch atoms must be table atoms; a primitive inside a branch is
+   rejected — a `!=` staleness filter is encoded as a relation (e.g.
    `(stale term leader)` holding only non-canonical terms).
 
 ### Bridge (`egglog-bridge/src/rule.rs`)
@@ -174,15 +175,43 @@ matches two branches but produces the same `(a b c)` tuple, so the shared action
 rebuilds it **exactly once**. `:unsafe-seminaive` supplies the `Read`/`Full` RHS
 context the action needs for the `leader` lookups.
 
+### Seminaive (delta-driven) execution
+
+A correlated union runs **seminaive**: a new `stale`/`AddView` tuple drives an
+index probe of the other branch atom, rather than a per-iteration re-scan.
+
+The semi-naive expansion of a union of conjunctions is the union of the
+per-disjunct expansions: `seminaive(⋁ᵢ Bᵢ) = ⋃ᵢ seminaive(Bᵢ)`. Because a
+correlated `or` prepends the conjunction into every branch, each branch `Bᵢ`
+holds all of `O ∪ (branch i's atoms)`, so its semi-naive expansion is
+self-contained (delta constraints never cross branch boundaries — other branches
+are alternatives, not conjuncts).
+
+- **`egglog-bridge` `add_rules_from_cached`**: for a union rule it iterates each
+  branch and, per focus atom, builds the standard focus/old timestamp
+  constraints (`GeConst` on the focus atom's `ts_col`, `LtConst` on the atoms
+  before it) over that branch's atoms only. Each `(branch_index, constraints)` is
+  one *variant*. It calls `RuleSetBuilder::add_union_rule_from_cached`.
+- **`core-relations` `add_union_rule_from_cached`**: builds a single variant of
+  the cached union plan whose `JoinStage::Union` holds one *variant branch* per
+  variant — the cached branch narrowed by that variant's timestamp constraints
+  applied as extra `JoinHeader`s (`reprocess_union_branch`). All variant branches
+  feed the one deduplicating block-0 materialization and the shared action, so a
+  row reached via several branches (or several focus atoms) is still processed
+  once. This is how the branch delta constraint reaches the branch sub-plan: it
+  becomes a header on that branch, which `execute.rs`'s `JoinStage::Union`
+  handler already intersects into the branch's atom subsets before running it.
+
+Independent `or`s (no correlation) keep the scanned-once continuation and run
+naive.
+
 ### Restrictions
 
-- **Naive evaluation.** The rule runs naive: the seminaive delta machinery
-  constrains atoms by their position in the top-level plan's atom list, but a
-  union's branch atoms live in per-branch sub-plans a delta focus can't reach.
-  This is correct at a fixpoint (a rebuild rule that deletes the stale row
-  converges), but not incremental. Making the delta drive an index probe of a
-  branch atom (the true seminaive rebuild) needs the delta machinery extended to
-  reach `JoinStage::Union` branches — future work.
+- **Independent `or`s run naive** (re-matched each iteration). Only correlated
+  `or`s are delta-driven. (Seminaive of an independent `or` whose conjunction is
+  a continuation would need the delta split between the continuation and the
+  branches; prepending the conjunction into the branches, as the correlated path
+  does, is the route to make it delta-driven.)
 - **Primitives in branches** are rejected (a branch must be a conjunction of
   table atoms). Primitives in the surrounding conjunction are fine; a `!=`
   staleness filter is encoded as a staleness relation instead.
diff --git a/egglog-bridge/src/rule.rs b/egglog-bridge/src/rule.rs
index 415858d75..e4dd0eccb 100644
--- a/egglog-bridge/src/rule.rs
+++ b/egglog-bridge/src/rule.rs
@@ -211,9 +211,10 @@ impl RuleBuilder<'_> {
     /// (the variables common to every branch). See
     /// [`core_relations::QueryBuilder::set_union`].
     ///
-    /// A union rule is run in naive mode (seminaive delta through a union is not
-    /// supported), so callers should construct it via
-    /// `new_rule(desc, /* seminaive */ false)`.
+    /// A union rule may be seminaive: when built with `new_rule(desc, true)`,
+    /// [`Query::add_rules_from_cached`] delta-drives each branch (the union of
+    /// the per-disjunct seminaive expansions). This is intended for rules whose
+    /// branches each carry all their conjuncts (no continuation atoms).
     pub fn set_union_branches(
         &mut self,
         branch_atoms: Vec<Vec<AtomId>>,
@@ -840,6 +841,47 @@ impl Query {
             let _ = rsb.add_rule_from_cached_plan(&cached_plan.plan, &[]);
             return;
         }
+        if let Some((branch_atoms, _)) = &self.union {
+            // A fused union is `⋁ᵢ Bᵢ`; its semi-naive expansion is the union of
+            // the per-disjunct expansions. For each branch we generate the
+            // standard per-atom focus/old variants over that branch's atoms only
+            // (never across branch boundaries — other branches are alternatives,
+            // not conjuncts). Every variant becomes one branch of the single
+            // deduplicating union, so a new tuple in a branch atom drives that
+            // branch's probe while dedup keeps the shared action firing once.
+            let mut variants: Vec<(usize, Vec<(core_relations::AtomId, Constraint)>)> = Vec::new();
+            for (branch_index, atoms) in branch_atoms.iter().enumerate() {
+                'focus: for focus in 0..atoms.len() {
+                    let mut constraints = Vec::with_capacity(focus + 1);
+                    let focus_idx = atoms[focus].index();
+                    let ts_col = ColumnId::from_usize(self.atoms[focus_idx].2.ts_col());
+                    constraints.push((
+                        cached_plan.atom_mapping[focus_idx],
+                        Constraint::GeConst {
+                            col: ts_col,
+                            val: mid_ts.to_value(),
+                        },
+                    ));
+                    for old in &atoms[0..focus] {
+                        if mid_ts == Timestamp::new(0) {
+                            continue 'focus;
+                        }
+                        let old_idx = old.index();
+                        let ts_col = ColumnId::from_usize(self.atoms[old_idx].2.ts_col());
+                        constraints.push((
+                            cached_plan.atom_mapping[old_idx],
+                            Constraint::LtConst {
+                                col: ts_col,
+                                val: mid_ts.to_value(),
+                            },
+                        ));
+                    }
+                    variants.push((branch_index, constraints));
+                }
+            }
+            let _ = rsb.add_union_rule_from_cached(&cached_plan.plan, &variants);
+            return;
+        }
         if let Some(focus_atom) = self.sole_focus {
             // There is a single "focus" atom that we will constrain to look at new values.
             let (_, _, schema_info) = &self.atoms[focus_atom];
diff --git a/src/lib.rs b/src/lib.rs
index 3e468af53..8b5f802f7 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1268,10 +1268,7 @@ impl EGraph {
         // A disjunct is *correlated* if it references a variable bound by the
         // surrounding conjunction that is not common to every disjunct (e.g.
         // `(UF_Math a al)` where `a` comes from the outer row). Such a branch
-        // cannot bind the shared output row on its own, so the surrounding
-        // conjunction is prepended into every branch; the branches then bind the
-        // row and probe their own atoms by the correlated columns. Independent
-        // `or`s keep the conjunction as a scanned-once continuation.
+        // cannot bind the shared output row on its own.
         let conj_vars = {
             let mut m = IndexMap::default();
             collect_resolved_fact_vars(&conj_facts, &mut m);
@@ -1287,9 +1284,19 @@ impl EGraph {
                 .any(|name| conj_vars.contains_key(name) && !disjunct_common_names.contains(name))
         });
 
-        // Branch fact lists and continuation depend on the layout.
+        // The surrounding conjunction is **prepended** into every branch of a
+        // correlated `or`, so each branch binds the shared output row itself and
+        // probes its own atoms by the correlated columns. This also puts all of a
+        // branch's `O ∪ Bᵢ` atoms in one branch, which the per-branch seminaive
+        // delta expansion requires (see `add_union_rule_from_cached`). An
+        // independent `or` keeps the conjunction as a scanned-once continuation
+        // and runs naive.
+        let prepend = correlated;
+        // Seminaive (delta-driven) union execution is used for correlated rules
+        // (all atoms in branches); independent unions run naive.
+        let union_seminaive = seminaive && correlated;
         let (branch_fact_lists, continuation_facts): (Vec<Vec<ast::ResolvedFact>>, Vec<_>) =
-            if correlated {
+            if prepend {
                 let branches = disjuncts
                     .iter()
                     .map(|d| {
@@ -1360,13 +1367,12 @@ impl EGraph {
         }
 
         let rule_id = {
-            // Run in naive mode: the seminaive delta machinery constrains atoms
-            // by their position in `plan.atoms`, but a union's branch atoms live
-            // in per-branch sub-plans, so a delta focus can't reach them. The
-            // `:unsafe-seminaive` Read/Full RHS context (for action lookups) is
-            // still honored via `requires_read_context`.
-            let _ = seminaive;
-            let mut rb = self.backend.new_rule(&rule.name, false);
+            // Seminaive union rules delta-drive each branch: the bridge's
+            // `add_rules_from_cached` generates per-branch focus/old timestamp
+            // variants (`⋃ᵢ seminaive(Bᵢ)`), all feeding the one deduplicating
+            // materialization. This requires every atom of a branch to live in
+            // that branch, which `prepend` (correlated) guarantees.
+            let mut rb = self.backend.new_rule(&rule.name, union_seminaive);
             rb.set_no_decomp(no_decomp);
             let mut translator =
                 BackendRule::new(rb, &self.functions, &self.type_info, requires_read_context);
diff --git a/tests/disjunction.rs b/tests/disjunction.rs
index c9cb0beac..39a71494c 100644
--- a/tests/disjunction.rs
+++ b/tests/disjunction.rs
@@ -332,3 +332,43 @@ fn or_correlated_rebuild_to_fixpoint() -> Result<(), Error> {
 (fail (check (v 1 1 3)))
 ")
 }
+
+/// The correlated union is **delta-driven**, not a per-iteration re-scan. A
+/// global counter `nfire` sums the firings via `(+)`. Under seminaive delta each
+/// match fires exactly once; under naive re-evaluation the fixpoint would re-fire
+/// the matching row every iteration, so the fixpoint counter (`= 1`) alone rules
+/// out naive. Then adding ONE new `stale` edge and running one step fires only
+/// for the rows that edge newly makes stale (2 of them) — `nfire` goes 1 -> 3,
+/// independent of the table size — demonstrating an index probe by the new edge,
+/// not an O(N) re-scan that would also re-fire the already-stale row.
+#[test]
+fn or_correlated_seminaive_delta_driven() -> Result<(), Error> {
+    run("
+(relation v (i64 i64 i64))
+(relation stale (i64 i64))
+(function nfire () i64 :merge (+ old new))
+(set (nfire) 0)
+
+(v 1 20 30)
+(v 40 50 60)
+(v 70 80 90)
+(v 7 11 12)
+(v 13 7 14)
+(v 15 16 17)
+
+(stale 1 100)   ; initially only (v 1 20 30) is stale (column a = 1)
+
+(ruleset rr)
+(rule ((v a b c)
+       (OR ((stale a al)) ((stale b bl)) ((stale c cl))))
+      ((set (nfire) 1))
+      :ruleset rr :unsafe-seminaive)
+
+(run rr 100)
+(check (= (nfire) 1))   ; fired once for the one stale row (delta, not per-iteration)
+
+(stale 7 700)           ; newly makes (v 7 11 12) and (v 13 7 14) stale
+(run rr 1)
+(check (= (nfire) 3))   ; +2 only for the newly-affected rows; the old row is not re-fired
+")
+}