Faster proof encoding: congruence via :merge + single self-referential UF (~1.8x)

egglog-experimental/src/fresh_macro.rs

@@ -88,7 +88,7 @@ fn desugar_fresh_rule(
         name: constructor_name.clone(),
         schema: Schema {
             input: schema,
-            output: output_sort,
+            outputs: vec![output_sort],
         },
         cost: first_opts.cost,
         unextractable: first_opts.unextractable,

egglog-experimental/src/primitive.rs

@@ -263,6 +263,8 @@ fn required_context(egraph: &mut EGraph, expr: &ResolvedExpr) -> Context {
                     }
                 }
                 ResolvedCall::Primitive(_) => Context::Pure,
+                // `values` builds/destructures a tuple value; it reads or writes no tables.
+                ResolvedCall::Values(_) => Context::Pure,
                 ResolvedCall::Func(func) => match func.subtype {
                     FunctionSubtype::Constructor => Context::Write,
                     FunctionSubtype::Custom => Context::Read,

egglog-experimental/src/set_cost.rs

@@ -114,7 +114,7 @@ impl Macro<Vec<Command>> for SetCostDeclarations {
                     if !*unextractable {
                         let cost_table_name = get_cost_table_name(name);
                         let mut cost_table_schema = schema.clone();
-                        cost_table_schema.output = "i64".into();
+                        cost_table_schema.outputs = vec!["i64".into()];
                         cost_table_commands.push(Command::Function {
                             span: span.clone(),
                             name: cost_table_name,

egglog-experimental/src/table_rows.rs

@@ -40,7 +40,7 @@ pub(crate) fn table_layout(egraph: &EGraph, name: &str, span: Span) -> Result<Ta
     Ok(TableLayout {
         subtype: func.subtype(),
         input_sorts: schema.input.clone(),
-        output_sort: schema.output.clone(),
+        output_sort: schema.output().clone(),
     })
 }
 

egglog/CHANGELOG.md

@@ -2,6 +2,34 @@
 
 ## [Unreleased] - ReleaseDate
 
+- **Single self-referential union-find (proof mode).** The proof term encoding now
+  represents each sort's union-find as one native-tuple function `@UF : (S) -> (S, Proof)`
+  (parent + a proof `key = parent`) with a self-referential `:merge`, replacing the former
+  two-table `@UF_S (S S) -> Proof` relation plus `@UF_Sf` index. Constructor-view congruence
+  and the UF self-merge both keep the smaller e-class and stage an oriented displaced edge,
+  so the `single_parent`/`uf_function_index` rules and per-term self-loop seeds are gone. This
+  mirrors the term (non-proof) encoding's single-table `@UF : (S) -> S`.
+- **Tuple-output functions.** A function may declare more than one output sort, e.g.
+  `(function interval (Math) (i64 i64) :merge (values (max old0 new0) (min old1 new1)))`. Such a
+  function stores its outputs as separate value columns; the functional dependency is
+  `keys -> (value0, value1, ...)`. Outputs are destructured in queries with
+  `(= (values lo hi) (interval x))`, written with `(set (interval x) (values 0 100))`, and merged
+  with a `(values ...)` clause whose `i`-th element merges column `i` using the bound variables
+  `old0`, `new0`, `old1`, `new1`, .... Tuple outputs are only allowed for plain functions (not
+  constructors, relations, or view tables) and are not supported by the term/proof encoding.
+- **`:merge` action blocks.** A `:merge` may be a value-producing action block
+  `:merge (<action>* <result-expr>)`: the actions run first (with `old`/`new` bound), then the
+  trailing expression is the merged value. Actions may be `let` (bind an intermediate value used by
+  later actions or the result), `set` (write another function), or `union` (unify two eclasses). A
+  bare `:merge <expr>` (no actions) is unchanged.
+- Built-in keywords (most command, action, and schedule heads such as `function`, `set`, `union`,
+  `rule`, `run`, ..., plus the tuple constructor `values`) are now reserved and may no longer be
+  used as user identifiers (function/sort/constructor/relation/variant names or variables). Names
+  starting with `:` may not be used as identifiers (definition names), since that prefix marks
+  option keywords (`:merge`, `:cost`, ...); it is still accepted in expression position so command
+  macros can consume their own option markers (e.g. `:until`). The common-word commands `input` and
+  `output` are only partially reserved: they remain usable as variables, but not as definition names
+  or as the head of a call expression.
 - 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.

egglog/core-relations/src/dependency_graph.rs

@@ -55,6 +55,14 @@ impl DependencyGraph {
     pub(crate) fn strata(&self) -> impl Iterator<Item = &IndexSet<TableId>> {
         self.levels.iter().map(|(_, tables)| tables)
     }
+    /// Whether this table's merge reads another table (has a read dependency). Tables with read
+    /// dependencies sit above level 0; tables with only write dependencies (or none) are at level
+    /// 0. Used to decide whether the dependency-agnostic `merge_simple` fast path is safe.
+    pub(crate) fn has_read_deps(&self, table: TableId) -> bool {
+        self.to_level
+            .get(table)
+            .is_some_and(|level| *level != LevelId::new(0))
+    }
     pub(crate) fn write_deps(&self, table: TableId) -> impl Iterator<Item = TableId> + '_ {
         self.write_deps
             .get(table)

egglog/core-relations/src/free_join/mod.rs

@@ -523,7 +523,16 @@ impl Database {
         loop {
             to_merge.clear();
             let to_merge_vec = self.notification_list.reset();
-            if to_merge_vec.len() < 4 {
+            // `merge_simple` is faster but ignores read/write-dependency ordering, so it is only
+            // sound when no dirty table's merge reads another table (e.g. a `Construct`/`Function`
+            // lookup inside a `:merge`). With a read dependency, an unordered merge could observe a
+            // stale, not-yet-merged target — and a `Construct` could then mint a duplicate id — so
+            // fall back to the dependency-ordered strata path however few tables are dirty.
+            if to_merge_vec.len() < 4
+                && !to_merge_vec
+                    .iter()
+                    .any(|table| self.deps.has_read_deps(*table))
+            {
                 ever_changed |= self.merge_simple(to_merge_vec);
                 break;
             }
@@ -607,7 +616,16 @@ impl Database {
         while !to_merge.is_empty() {
             for table_id in to_merge.iter().copied() {
                 let mut info = self.tables.unwrap_val(table_id);
-                let mut es = ExecutionState::new(self.read_only_view(), Default::default());
+                // Pre-seed the table's OWN buffer so a self-referential merge — one that stages a
+                // write back into its own table (e.g. the term encoder's `@UF` recursive
+                // parent-union) — can stage it. The table has been `unwrap_val`'d out of
+                // `self.tables`, so the lazy `new_buffer()` path (which indexes `self.tables`) would
+                // fail for the self id. Staged rows land in `pending_state` and are picked up on the
+                // next fixpoint iteration of this loop. Non-self-referential merges get an empty,
+                // never-touched buffer. (The strata path in `merge_all` handles this via write-deps.)
+                let mut bufs = DenseIdMap::default();
+                bufs.insert(table_id, info.table.new_buffer());
+                let mut es = ExecutionState::new(self.read_only_view(), bufs);
                 changed |= info.table.merge(&mut es).added || es.changed;
                 self.tables.insert(table_id, info);
             }
@@ -625,10 +643,14 @@ impl Database {
     pub fn merge_table(&mut self, table: TableId) -> bool {
         let mut info = self.tables.unwrap_val(table);
         self.total_size_estimate = self.total_size_estimate.wrapping_sub(info.table.len());
-        let table_changed = info.table.merge(&mut ExecutionState::new(
-            self.read_only_view(),
-            Default::default(),
-        ));
+        // Pre-seed the table's own write buffer so a self-referential merge can stage a write back
+        // into itself (the table has been `unwrap_val`'d out, so the lazy `new_buffer()` path would
+        // fail for the self id). This mirrors `merge_simple`; see the comment there.
+        let mut bufs = DenseIdMap::default();
+        bufs.insert(table, info.table.new_buffer());
+        let table_changed = info
+            .table
+            .merge(&mut ExecutionState::new(self.read_only_view(), bufs));
         self.total_size_estimate = self.total_size_estimate.wrapping_add(info.table.len());
         self.tables.insert(table, info);
         table_changed.added

egglog/egglog-ast/src/generic_ast.rs

@@ -42,6 +42,20 @@ pub struct GenericActions<Head: Clone + Display, Leaf: Clone + PartialEq + Eq +
     pub Vec<GenericAction<Head, Leaf>>,
 );
 
+/// The `:merge` of a function: a *value-producing action block*. On a functional-dependency
+/// conflict, the `actions` run (with `old`/`new` — or `old0`/`new0`/... for tuple outputs — bound
+/// to the conflicting values), then `result` is evaluated to the merged value(s). A plain
+/// `:merge <expr>` has no actions (see [`GenericMerge::result_only`]).
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct GenericMerge<Head, Leaf>
+where
+    Head: Clone + Display,
+    Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+    pub actions: GenericActions<Head, Leaf>,
+    pub result: GenericExpr<Head, Leaf>,
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub enum GenericAction<Head, Leaf>
 where

egglog/egglog-ast/src/generic_ast_helpers.rs

@@ -331,6 +331,67 @@ where
     }
 }
 
+impl<Head, Leaf> GenericMerge<Head, Leaf>
+where
+    Head: Clone + Display,
+    Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+    /// A merge with no actions: just a result expression (the `:merge <expr>` form).
+    pub fn result_only(result: GenericExpr<Head, Leaf>) -> Self {
+        Self {
+            actions: GenericActions::default(),
+            result,
+        }
+    }
+
+    /// Applies `f` to every expression in the merge's actions and result.
+    pub fn visit_exprs(
+        self,
+        f: &mut impl FnMut(GenericExpr<Head, Leaf>) -> GenericExpr<Head, Leaf>,
+    ) -> Self {
+        Self {
+            actions: self.actions.visit_exprs(f),
+            result: self.result.visit_exprs(f),
+        }
+    }
+
+    /// Applies the `head` and `leaf` mappings to every symbol in the merge.
+    pub fn map_symbols<Head2, Leaf2>(
+        self,
+        head: &mut impl FnMut(Head) -> Head2,
+        leaf: &mut impl FnMut(Leaf) -> Leaf2,
+    ) -> GenericMerge<Head2, Leaf2>
+    where
+        Head2: Clone + Display,
+        Leaf2: Clone + PartialEq + Eq + Display + Hash,
+    {
+        GenericMerge {
+            actions: self.actions.map_symbols(head, leaf),
+            result: self.result.map_symbols(head, leaf),
+        }
+    }
+}
+
+impl<Head, Leaf> Display for GenericMerge<Head, Leaf>
+where
+    Head: Clone + Display,
+    Leaf: Clone + PartialEq + Eq + Display + Hash,
+{
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        if self.actions.is_empty() {
+            // Result-only: `:merge <expr>`.
+            write!(f, "{}", self.result)
+        } else {
+            // Action block: `:merge (<action>* <result>)`.
+            write!(f, "(")?;
+            for action in self.actions.iter() {
+                write!(f, "{action} ")?;
+            }
+            write!(f, "{})", self.result)
+        }
+    }
+}
+
 impl<Head, Leaf> GenericAction<Head, Leaf>
 where
     Head: Clone + Display,

egglog/egglog-bridge/examples/ac.rs

@@ -15,13 +15,17 @@ fn main() {
         let mut egraph = EGraph::default();
         let int_base = egraph.base_values_mut().register_type::<i64>();
         let num_table = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Base(int_base), ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "num".into(),
             can_subsume: false,
         });
         let add_table = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id; 3],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,

egglog/egglog-bridge/examples/math.rs

@@ -20,13 +20,17 @@ fn main() {
         let string_ty = egraph.base_values_mut().register_type::<&'static str>();
         // tables
         let diff = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "diff".into(),
             can_subsume: false,
         });
         let integral = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -35,13 +39,17 @@ fn main() {
         });
 
         let add = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
             name: "add".into(),
             can_subsume: false,
         });
         let sub = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -50,6 +58,8 @@ fn main() {
         });
 
         let mul = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -58,6 +68,8 @@ fn main() {
         });
 
         let div = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -66,6 +78,8 @@ fn main() {
         });
 
         let pow = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -74,6 +88,8 @@ fn main() {
         });
 
         let ln = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -82,6 +98,8 @@ fn main() {
         });
 
         let sqrt = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -90,6 +108,8 @@ fn main() {
         });
 
         let sin = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -98,6 +118,8 @@ fn main() {
         });
 
         let cos = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Id, ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -106,6 +128,8 @@ fn main() {
         });
 
         let rat = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Base(rational_ty), ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,
@@ -114,6 +138,8 @@ fn main() {
         });
 
         let var = egraph.add_table(FunctionConfig {
+            n_vals: 1,
+            n_identity_vals: None,
             schema: vec![ColumnTy::Base(string_ty), ColumnTy::Id],
             default: DefaultVal::FreshId,
             merge: MergeFn::UnionId,