diff --git a/egglog/egglog-bridge/src/lib.rs b/egglog/egglog-bridge/src/lib.rs index 69fe57e..8296d93 100644 --- a/egglog/egglog-bridge/src/lib.rs +++ b/egglog/egglog-bridge/src/lib.rs @@ -1064,6 +1064,27 @@ pub enum MergeFn { /// [`MergeFn::OldCol`] / [`MergeFn::NewCol`]. The length determines the number of value /// columns of the function. Columns(Vec), + /// Insert a full row (the `args` evaluate to keys + values) into the given function's table, + /// respecting that table's own merge. Returns this column's old value (meant to be discarded + /// inside a [`MergeFn::Seq`]); declares the target as a write-dependency so the side write is + /// safe during batched merges. Models a `(set (f ...) v)` action inside a merge. + TableInsert(FunctionId, Vec), + /// Evaluate each merge function in order for its effects and return the value of the last. + /// Models an action-block merge: leading entries are effects (e.g. [`MergeFn::TableInsert`] / + /// [`MergeFn::Construct`]) and the last is the value. + Seq(Vec), + /// Mint a value-tuple constructor inside a merge and return its (freshly minted) output column. + /// `args` evaluate to the key columns; the first value column (the output) is minted from the + /// table's `FreshId` default and the remaining value columns are written from `value_args`. + Construct(FunctionId, Vec, Vec), + /// If `a` and `b` evaluate equal, run and return `then`, otherwise run and return `els`. + /// General conditional for guarding merge-action bodies. + IfEq { + a: Box, + b: Box, + then: Box, + els: Box, + }, } impl MergeFn { @@ -1093,6 +1114,29 @@ impl MergeFn { cols.iter() .for_each(|col| col.fill_deps(egraph, read_deps, write_deps)); } + TableInsert(func, args) => { + write_deps.insert(egraph.funcs[*func].table); + args.iter() + .for_each(|arg| arg.fill_deps(egraph, read_deps, write_deps)); + } + Seq(items) => { + items + .iter() + .for_each(|item| item.fill_deps(egraph, read_deps, write_deps)); + } + Construct(func, args, value_args) => { + read_deps.insert(egraph.funcs[*func].table); + write_deps.insert(egraph.funcs[*func].table); + args.iter() + .chain(value_args.iter()) + .for_each(|arg| arg.fill_deps(egraph, read_deps, write_deps)); + } + IfEq { a, b, then, els } => { + a.fill_deps(egraph, read_deps, write_deps); + b.fill_deps(egraph, read_deps, write_deps); + then.fill_deps(egraph, read_deps, write_deps); + els.fill_deps(egraph, read_deps, write_deps); + } AssertEq | Old | New | OldCol(..) | NewCol(..) | Const(..) => {} } } @@ -1215,6 +1259,53 @@ impl MergeFn { .collect::>(), } } + MergeFn::TableInsert(func, args) => ResolvedMergeFn::TableInsert { + table: TableAction::new(egraph, *func), + args: args + .iter() + .map(|arg| arg.resolve(function_name, egraph)) + .collect::>(), + }, + MergeFn::Seq(items) => ResolvedMergeFn::Seq( + items + .iter() + .map(|item| item.resolve(function_name, egraph)) + .collect::>(), + ), + MergeFn::Construct(func, args, value_args) => { + let func_info = &egraph.funcs[*func]; + let num_values = func_info.schema.len() - func_info.n_keys; + debug_assert_eq!( + func_info.schema.len(), + args.len() + num_values, + "Construct for {function_name}: key arity must be schema minus value columns for {}", + func_info.name + ); + debug_assert_eq!( + value_args.len() + 1, + num_values, + "Construct for {function_name}: value_args must fill every value column \ + except the minted output for {}", + func_info.name + ); + ResolvedMergeFn::Construct { + table: TableAction::new(egraph, *func), + args: args + .iter() + .map(|arg| arg.resolve(function_name, egraph)) + .collect::>(), + value_args: value_args + .iter() + .map(|arg| arg.resolve(function_name, egraph)) + .collect::>(), + } + } + MergeFn::IfEq { a, b, then, els } => ResolvedMergeFn::IfEq { + a: Box::new(a.resolve(function_name, egraph)), + b: Box::new(b.resolve(function_name, egraph)), + then: Box::new(then.resolve(function_name, egraph)), + els: Box::new(els.resolve(function_name, egraph)), + }, } } } @@ -1245,6 +1336,27 @@ enum ResolvedMergeFn { args: Vec, panic: ExternalFunctionId, }, + /// `(set (f ...) v)` inside a merge: insert a full row into `table`, respecting its own merge. + TableInsert { + table: TableAction, + args: Vec, + }, + /// Run each item in order for its effects; return the value of the last. + Seq(Vec), + /// Mint a value-tuple constructor inside a merge (first value column minted via `FreshId`, + /// `value_args` for the remaining value columns) and return its minted output. + Construct { + table: TableAction, + args: Vec, + value_args: Vec, + }, + /// If `a == b` run `then`, otherwise run `els`. + IfEq { + a: Box, + b: Box, + then: Box, + els: Box, + }, } impl ResolvedMergeFn { @@ -1329,6 +1441,51 @@ impl ResolvedMergeFn { cur[n_keys + self_col] }) } + ResolvedMergeFn::TableInsert { table, args } => { + let row = args + .iter() + .map(|arg| arg.run(state, cur, new, n_keys, self_col, ts)) + .collect::>(); + // Insert respects the target table's own merge; `TableAction::insert` appends the + // timestamp/subsume columns. + table.insert(state, row.into_iter()); + // Return value is discarded by the enclosing `Seq`. + cur[n_keys + self_col] + } + ResolvedMergeFn::Seq(items) => { + let mut result = cur[n_keys + self_col]; + for item in items { + result = item.run(state, cur, new, n_keys, self_col, ts); + } + result + } + ResolvedMergeFn::Construct { + table, + args, + value_args, + } => { + let key = args + .iter() + .map(|arg| arg.run(state, cur, new, n_keys, self_col, ts)) + .collect::>(); + let vals = value_args + .iter() + .map(|arg| arg.run(state, cur, new, n_keys, self_col, ts)) + .collect::>(); + // Constructor: always mints on miss, so this is `Some`. + table + .lookup_or_insert_multi(state, &key, &vals) + .unwrap_or(cur[n_keys + self_col]) + } + ResolvedMergeFn::IfEq { a, b, then, els } => { + let av = a.run(state, cur, new, n_keys, self_col, ts); + let bv = b.run(state, cur, new, n_keys, self_col, ts); + if av == bv { + then.run(state, cur, new, n_keys, self_col, ts) + } else { + els.run(state, cur, new, n_keys, self_col, ts) + } + } } } } @@ -1487,6 +1644,47 @@ impl TableAction { } } + /// Multi-value variant of [`TableAction::lookup_or_insert`] for a value-tuple constructor + /// `(children) -> (output, extra...)`: the first value column (`output`) is minted (the + /// configured `FreshId` default) and the rest are written from `provided_vals` (e.g. a proof). + /// Returns the minted `output`. + /// + /// Idempotent: an already-present key returns its existing `output` and writes nothing. Write + /// operation, only safe in action/merge contexts. + pub fn lookup_or_insert_multi( + &self, + state: &mut ExecutionState, + key: &[Value], + provided_vals: &[Value], + ) -> Option { + match self.default { + Some(default) => { + debug_assert_eq!( + self.table_math.n_vals(), + 1 + provided_vals.len(), + "lookup_or_insert_multi: provided_vals must fill every value \ + column except the minted first one" + ); + let timestamp = + MergeVal::Constant(Value::from_usize(state.read_counter(self.timestamp))); + // Non-key columns, in order: [output (minted), provided.., ts, subsume?]. + let mut merge_vals = SmallVec::<[MergeVal; 4]>::new(); + merge_vals.push(default); + merge_vals.extend(provided_vals.iter().map(|v| MergeVal::Constant(*v))); + merge_vals.push(timestamp); + if self.table_math.subsume { + merge_vals.push(MergeVal::Constant(NOT_SUBSUMED)); + } + // The first value column (the minted output) is at `ret_val_col()`. + Some( + state.predict_val(self.table, key, merge_vals.iter().copied()) + [self.table_math.ret_val_col()], + ) + } + None => self.lookup(state, key), + } + } + /// Insert a row into this table. pub fn insert(&self, state: &mut ExecutionState, row: impl Iterator) { let ts = Value::from_usize(state.read_counter(self.timestamp)); diff --git a/egglog/egglog-bridge/src/rule.rs b/egglog/egglog-bridge/src/rule.rs index 141b44f..78b7b33 100644 --- a/egglog/egglog-bridge/src/rule.rs +++ b/egglog/egglog-bridge/src/rule.rs @@ -471,8 +471,8 @@ impl RuleBuilder<'_> { /// /// `entries` should match the number of keys to the function. pub fn subsume(&mut self, func: FunctionId, entries: &[QueryEntry]) { - // First, insert a subsumed value if the tuple is new. - let ret = self.lookup_with_subsumed( + // Ensure the row exists (panics otherwise); its value is re-read per column below. + let _ret = self.lookup_with_subsumed( func, entries, QueryEntry::Const { @@ -484,26 +484,32 @@ impl RuleBuilder<'_> { let info = &self.egraph.funcs[func]; let schema_math = info.schema_math(); assert!(info.can_subsume); - assert_eq!(entries.len() + 1, info.schema.len()); + assert_eq!(entries.len(), schema_math.num_keys()); + let n_vals = schema_math.n_vals(); let entries = entries.to_vec(); let table = info.table; - let ret: QueryEntry = ret.into(); self.add_callback(move |inner, rb| { // Then, add a tuple subsuming the entry, but only if the entry isn't already subsumed. - // Look up the current subsume value. - let mut dst_entries = inner.convert_all(&entries); + let keys = inner.convert_all(&entries); let cur_subsume_val = rb.lookup( table, - &dst_entries, + &keys, ColumnId::from_usize(schema_math.subsume_col()), )?; + // Re-read every value column so subsumption preserves the whole row (tuple-output views + // carry more than one value, e.g. the e-class and its proof). + let mut dst_entries = keys.clone(); + for i in 0..n_vals { + let v = rb.lookup(table, &keys, ColumnId::from_usize(schema_math.val_col(i)))?; + dst_entries.push(v.into()); + } schema_math.write_table_row( &mut dst_entries, RowVals { timestamp: inner.next_ts(), subsume: Some(SUBSUMED.into()), - ret_val: Some(inner.convert(&ret)), + ret_val: None, }, ); rb.insert_if_eq( diff --git a/egglog/src/ast/desugar.rs b/egglog/src/ast/desugar.rs index 1dcf2fb..26db050 100644 --- a/egglog/src/ast/desugar.rs +++ b/egglog/src/ast/desugar.rs @@ -71,6 +71,7 @@ pub(crate) fn desugar_command( presort_and_args: None, uf: None, proof_func: None, + proof_ctors: None, unionable: true, }); } @@ -91,6 +92,7 @@ pub(crate) fn desugar_command( presort_and_args: Some((sort, args)), uf: None, proof_func: None, + proof_ctors: None, unionable: true, }); } @@ -145,6 +147,7 @@ pub(crate) fn desugar_command( presort_and_args, uf, proof_func, + proof_ctors, unionable, } => vec![NCommand::Sort { span, @@ -152,6 +155,7 @@ pub(crate) fn desugar_command( presort_and_args, uf, proof_func, + proof_ctors, unionable, }], Command::AddRuleset(span, name) => vec![NCommand::AddRuleset(span, name)], @@ -235,6 +239,7 @@ fn desugar_prove(parser: &mut Parser, span: Span, query: Vec) -> Vec) -> Vec, + /// The global proof-constructor names `(congr, trans, sym)`, recorded once on the `Proof` + /// sort by proof desugaring so a desugared program re-parses self-contained (the native + /// congruence merge needs them). See `:internal-proof-names`. + proof_ctors: Option<(String, String, String)>, /// Whether values of this sort can be unioned. /// Defaults to true for user-defined sorts. /// Set to false for relations and term tables that should not allow union. @@ -117,6 +121,7 @@ where presort_and_args, uf, proof_func, + proof_ctors, unionable, } => GenericCommand::Sort { span: span.clone(), @@ -124,6 +129,7 @@ where presort_and_args: presort_and_args.clone(), uf: uf.clone(), proof_func: proof_func.clone(), + proof_ctors: proof_ctors.clone(), unionable: *unionable, }, GenericNCommand::Function(f) => match f.subtype { @@ -243,6 +249,7 @@ where presort_and_args, uf, proof_func, + proof_ctors, unionable, } => GenericNCommand::Sort { span, @@ -250,6 +257,7 @@ where presort_and_args, uf, proof_func, + proof_ctors, unionable, }, GenericNCommand::Function(func) => GenericNCommand::Function(func.visit_exprs(f)), @@ -559,6 +567,10 @@ where /// The name of the proof function for this sort. /// Set by proof desugaring to record where proofs are stored for this sort. proof_func: Option, + /// The global proof-constructor names `(congr, trans, sym)`, recorded once on the `Proof` + /// sort by proof desugaring so a desugared program re-parses self-contained. See + /// `:internal-proof-names`. + proof_ctors: Option<(String, String, String)>, /// Whether values of this sort can be unioned. /// Defaults to true for user-defined sorts. /// Set to false for relations and term tables that should not allow union. @@ -964,6 +976,7 @@ where presort_and_args: None, uf, proof_func, + proof_ctors, .. } => { write!(f, "(sort {name}")?; @@ -973,6 +986,9 @@ where if let Some(pf) = proof_func { write!(f, " :internal-proof-func {pf}")?; } + if let Some((congr, trans, sym)) = proof_ctors { + write!(f, " :internal-proof-names {congr} {trans} {sym}")?; + } write!(f, ")") } GenericCommand::Sort { @@ -1742,6 +1758,7 @@ where presort_and_args, uf, proof_func, + proof_ctors, unionable, } => GenericCommand::Sort { span, @@ -1749,6 +1766,7 @@ where presort_and_args, uf: uf.map(&mut *fun), proof_func: proof_func.map(&mut *fun), + proof_ctors: proof_ctors.map(|(c, t, s)| (fun(c), fun(t), fun(s))), unionable, }, GenericCommand::Datatype { @@ -2021,6 +2039,7 @@ where presort_and_args, uf, proof_func, + proof_ctors, unionable, } => GenericCommand::Sort { span, @@ -2028,6 +2047,7 @@ where presort_and_args, uf, proof_func, + proof_ctors, unionable, }, GenericCommand::Datatype { diff --git a/egglog/src/ast/parse.rs b/egglog/src/ast/parse.rs index 85957e8..a11c623 100644 --- a/egglog/src/ast/parse.rs +++ b/egglog/src/ast/parse.rs @@ -362,6 +362,7 @@ impl Parser { presort_and_args: None, uf: None, proof_func: None, + proof_ctors: None, unionable: true, }], [name, call @ Sexp::List(..)] => { @@ -375,13 +376,15 @@ impl Parser { )), uf: None, proof_func: None, + proof_ctors: None, unionable: true, }] } [name, rest @ ..] => { - // Parse :internal-uf and :internal-proof-func annotations + // Parse :internal-uf, :internal-proof-func, and :internal-proof-names annotations let mut uf = None; let mut proof_func = None; + let mut proof_ctors = None; for (key, val) in self.parse_options(rest)? { match (key, val) { (":internal-uf", [uf_func]) => { @@ -391,10 +394,17 @@ impl Parser { proof_func = Some(pf.expect_atom("internal-proof-func function name")?); } + (":internal-proof-names", [congr, trans, sym]) => { + proof_ctors = Some(( + congr.expect_atom("congruence constructor name")?, + trans.expect_atom("transitivity constructor name")?, + sym.expect_atom("symmetry constructor name")?, + )); + } _ => { return error!( span, - "usages:\n(sort )\n(sort :internal-uf )\n(sort :internal-proof-func )\n(sort ( *))" + "usages:\n(sort )\n(sort :internal-uf )\n(sort :internal-proof-func )\n(sort :internal-proof-names )\n(sort ( *))" ); } } @@ -405,6 +415,7 @@ impl Parser { presort_and_args: None, uf, proof_func, + proof_ctors, unionable: true, }] } diff --git a/egglog/src/constraint.rs b/egglog/src/constraint.rs index f3a1385..464559e 100644 --- a/egglog/src/constraint.rs +++ b/egglog/src/constraint.rs @@ -871,9 +871,16 @@ impl CoreAction { } CoreAction::Change(span, _change, head, args) => { let mut args = args.clone(); - // Add a dummy last output argument - let var = symbol_gen.fresh(head); - args.push(AtomTerm::Var(span.clone(), var)); + // Add a dummy output argument per output column (tuple-output views have more than + // one), so the atom matches the function's full arity for constraint solving. + let num_outputs = typeinfo + .get_func_type(head) + .map(|t| t.num_outputs()) + .unwrap_or(1); + for _ in 0..num_outputs { + let var = symbol_gen.fresh(head); + args.push(AtomTerm::Var(span.clone(), var)); + } Ok(get_literal_and_global_constraints(&args, typeinfo) .chain(get_atom_application_constraints( diff --git a/egglog/src/extract.rs b/egglog/src/extract.rs index 1ddb71a..9679e3b 100644 --- a/egglog/src/extract.rs +++ b/egglog/src/extract.rs @@ -715,11 +715,19 @@ impl Function { } } - /// For view tables (with term_constructor), the effective output sort is the last input column. - /// For regular tables, it's the output sort. + /// Whether this is the proof-mode functional-dependency view `(children) -> (eclass, proof)`, + /// where the e-class is the first output column rather than the last input column. + fn is_fd_view(&self) -> bool { + self.decl.term_constructor.is_some() && !self.schema.extra_outputs.is_empty() + } + + /// For view tables (with term_constructor), the effective output sort is the last input column + /// (old form) or the first output column (FD tuple view). For regular tables, it's the output. /// This is used by extraction to determine which sort a table produces values for. pub(crate) fn extraction_output_sort(&self) -> &ArcSort { - if self.decl.term_constructor.is_some() { + if self.is_fd_view() { + &self.schema.output + } else if self.decl.term_constructor.is_some() { self.schema.input.last().unwrap() } else { &self.schema.output @@ -727,9 +735,10 @@ impl Function { } /// Returns the number of children for extraction purposes. - /// For view tables, this excludes the last column (the e-class). + /// For old-form view tables, this excludes the last input column (the e-class); FD tuple views + /// key on children only, so all inputs are children. pub(crate) fn extraction_num_children(&self) -> usize { - if self.decl.term_constructor.is_some() { + if self.decl.term_constructor.is_some() && !self.is_fd_view() { self.schema.input.len() - 1 } else { self.schema.input.len() @@ -749,13 +758,12 @@ impl Function { /// For view tables, the e-class is the last input column (second-to-last in the row). /// For regular tables, it's the last column (the actual output). pub(crate) fn extraction_output_index(&self) -> usize { - if self.decl.term_constructor.is_some() { - // For view tables: input is [children..., eclass], output is view_sort - // Row is [children..., eclass, view_sort] - // We want eclass which is at index input.len() - 1 + if self.decl.term_constructor.is_some() && !self.is_fd_view() { + // Old-form view: row is [children..., eclass, view_sort]; eclass at input.len() - 1. self.schema.input.len() - 1 } else { - // For regular tables: row is [inputs..., output] + // Regular table: [inputs..., output]. FD view: [children..., eclass, proof]; the eclass + // is the first output column, at index input.len(). self.schema.input.len() } } diff --git a/egglog/src/lib.rs b/egglog/src/lib.rs index 914c028..961c133 100644 --- a/egglog/src/lib.rs +++ b/egglog/src/lib.rs @@ -830,6 +830,56 @@ impl EGraph { } } + /// Build the native congruence `:merge` for a term-encoding constructor view + /// `(children) -> (eclass, proof)` (proof mode). Returns `None` for any function that isn't such + /// a view, leaving the ordinary merge lowering in place. + /// + /// On an FD conflict (two congruent terms share the same canonical children) the merge keeps the + /// current `(eclass, proof)` and stages the congruence edge `(@UF_S new_eclass old_eclass) = + /// (Trans new_proof (Sym old_proof))` — the exact edge and proof the rule-encoded congruence + /// would produce — so the existing UF/path-compression/rebuild machinery is unchanged. + fn native_congruence_merge( + &self, + decl: &ResolvedFunctionDecl, + output: &ArcSort, + num_outputs: usize, + ) -> Option { + use egglog_bridge::MergeFn; + // Detected purely by shape: a term-constructor view with an eq-sort first output and a + // second (proof) output. This shape is only ever emitted by the proof encoder, so we don't + // gate on `proofs_enabled` — that lets a re-parsed desugared program (run in a fresh, non- + // proof egraph) rebuild the same merge, which is what makes the encoding self-contained. + if !(decl.term_constructor.is_some() && num_outputs == 2 && output.is_eq_sort()) { + return None; + } + let uf_name = self.proof_state.uf_parent.get(&decl.schema.output)?; + let uf_id = self.functions.get(uf_name)?.backend_id; + let trans_id = self + .functions + .get(&self.proof_state.proof_names.eq_trans_constructor)? + .backend_id; + let sym_id = self + .functions + .get(&self.proof_state.proof_names.eq_sym_constructor)? + .backend_id; + // (Sym old_proof) then (Trans new_proof (Sym old_proof)), proving new_eclass = old_eclass. + let sym = MergeFn::Construct(sym_id, vec![MergeFn::OldCol(1)], vec![]); + let trans = MergeFn::Construct(trans_id, vec![MergeFn::NewCol(1), sym], vec![]); + // Column 0 (eclass): keep the old eclass; when it differs from the new one, stage the union + // edge into @UF_S first. + let eclass_col = MergeFn::IfEq { + a: Box::new(MergeFn::OldCol(0)), + b: Box::new(MergeFn::NewCol(0)), + then: Box::new(MergeFn::OldCol(0)), + els: Box::new(MergeFn::Seq(vec![ + MergeFn::TableInsert(uf_id, vec![MergeFn::NewCol(0), MergeFn::OldCol(0), trans]), + MergeFn::OldCol(0), + ])), + }; + // Column 1 (proof): keep the old proof. + Some(MergeFn::Columns(vec![eclass_col, MergeFn::Old])) + } + fn declare_function(&mut self, decl: &ResolvedFunctionDecl) -> Result<(), Error> { let get_sort = |name: &String| match self.type_info.get_sort_by_name(name) { Some(sort) => Ok(sort.clone()), @@ -861,23 +911,30 @@ impl EGraph { }; use egglog_bridge::{DefaultVal, MergeFn}; - let merge = match decl.subtype { - FunctionSubtype::Constructor => MergeFn::UnionId, - FunctionSubtype::Custom => match &decl.merge { - // A tuple-output merge is a `(values e0 e1 ...)` form: each `ei` becomes the merge - // for output column `i`. - Some(GenericExpr::Call(_, ResolvedCall::Values(_), cols)) => MergeFn::Columns( - cols.iter() - .map(|e| self.translate_expr_to_mergefn(e)) - .collect::, _>>()?, - ), - Some(expr) => self.translate_expr_to_mergefn(expr)?, - // No merge clause: assert equality per output column. - None if num_outputs > 1 => { - MergeFn::Columns((0..num_outputs).map(|_| MergeFn::AssertEq).collect()) - } - None => MergeFn::AssertEq, - }, + let merge = if let Some(m) = self.native_congruence_merge(decl, &output, num_outputs) { + // Term-encoding constructor view `(children) -> (eclass, proof)`: resolve congruence via + // a native :merge that stages the congruence edge into the per-sort UF table, instead of + // a rule-encoded self-join. + m + } else { + match decl.subtype { + FunctionSubtype::Constructor => MergeFn::UnionId, + FunctionSubtype::Custom => match &decl.merge { + // A tuple-output merge is a `(values e0 e1 ...)` form: each `ei` becomes the merge + // for output column `i`. + Some(GenericExpr::Call(_, ResolvedCall::Values(_), cols)) => MergeFn::Columns( + cols.iter() + .map(|e| self.translate_expr_to_mergefn(e)) + .collect::, _>>()?, + ), + Some(expr) => self.translate_expr_to_mergefn(expr)?, + // No merge clause: assert equality per output column. + None if num_outputs > 1 => { + MergeFn::Columns((0..num_outputs).map(|_| MergeFn::AssertEq).collect()) + } + None => MergeFn::AssertEq, + }, + } }; let backend_id = self.backend.add_table(egglog_bridge::FunctionConfig { schema: input @@ -1644,6 +1701,7 @@ impl EGraph { name, uf, proof_func, + proof_ctors, .. } => { // If the sort has a :internal-uf field, store the mapping for extraction @@ -1657,6 +1715,15 @@ impl EGraph { .proof_func_parent .insert(name.clone(), proof_func_name); } + // The Proof sort's :internal-proof-names records the global proof-constructor names. + // Repopulating them makes a re-parsed desugared program self-contained (the native + // congruence merge looks Trans/Sym up by name). + if let Some((congr, trans, sym)) = proof_ctors { + let names = &mut self.proof_state.proof_names; + names.congr_constructor = congr; + names.eq_trans_constructor = trans; + names.eq_sym_constructor = sym; + } log::info!("Declared sort {name}.") } ResolvedNCommand::Function(fdecl) => { diff --git a/egglog/src/prelude.rs b/egglog/src/prelude.rs index d32e5eb..8a1f363 100644 --- a/egglog/src/prelude.rs +++ b/egglog/src/prelude.rs @@ -758,6 +758,7 @@ pub fn add_sort(egraph: &mut EGraph, name: &str) -> Result, E presort_and_args: None, uf: None, proof_func: None, + proof_ctors: None, unionable: true, }]) } diff --git a/egglog/src/proofs/proof_encoding.rs b/egglog/src/proofs/proof_encoding.rs index ecc97e0..dcabc53 100644 --- a/egglog/src/proofs/proof_encoding.rs +++ b/egglog/src/proofs/proof_encoding.rs @@ -228,6 +228,31 @@ impl<'a> ProofInstrumentor<'a> { let delete_subsume_ruleset = self.proof_names().delete_subsume_ruleset_name.clone(); let fresh_name = self.egraph.parser.symbol_gen.fresh("delete_rule"); + // The FD tuple view is keyed by children only; match its value tuple to delete by key. + // Subsumption is not supported on a multi-output view (the bridge subsume path is + // single-output), and no proof workload subsumes constructor terms, so it is omitted. + if self.native_merge_view(fdecl) { + let e = self.fresh_var(); + let pf = self.fresh_var(); + let e2 = self.fresh_var(); + let pf2 = self.fresh_var(); + // Deletion removes the row by key; subsumption marks it subsumed (kept for size/proofs + // but excluded from matching). + return format!( + "(rule (({to_delete_name} {child_names}) + (= (values {e} {pf}) ({view_name} {child_names}))) + ((delete ({view_name} {child_names})) + (delete ({to_delete_name} {child_names}))) + :ruleset {delete_subsume_ruleset} + :name \"{fresh_name}\") + (rule (({subsumed_name} {child_names}) + (= (values {e2} {pf2}) ({view_name} {child_names}))) + ((subsume ({view_name} {child_names}))) + :ruleset {delete_subsume_ruleset} + :name \"{fresh_name}_subsume\")" + ); + } + format!( "(rule (({to_delete_name} {child_names}) ({view_name} {child_names} out)) @@ -433,6 +458,9 @@ impl<'a> ProofInstrumentor<'a> { &view_name, &rebuilding_ruleset, ) + } else if self.native_merge_view(fdecl) { + // Congruence is resolved by the view's native `:merge`; no rule needed. + String::new() } else { self.handle_congruence(fdecl, &child_names, &rebuilding_ruleset) } @@ -443,6 +471,12 @@ impl<'a> ProofInstrumentor<'a> { /// The view table stores child terms and their eclass. /// The view table is mutated using delete, but we never delete from term tables. /// We re-use the original name of the function for the term table. + /// Whether this function's view is the proof-mode functional-dependency tuple view + /// `(children) -> (eclass, proof)` whose native `:merge` resolves congruence. + fn native_merge_view(&self, fdecl: &ResolvedFunctionDecl) -> bool { + fdecl.subtype == FunctionSubtype::Constructor && self.egraph.proof_state.proofs_enabled + } + fn term_and_view(&mut self, fdecl: &ResolvedFunctionDecl) -> Vec { let schema = &fdecl.schema; let out_type = schema.output.clone(); @@ -499,9 +533,20 @@ impl<'a> ProofInstrumentor<'a> { if fdecl.internal_let { view_flags.push_str(" :internal-let"); } - let view_decl = format!( - "(function {view_name} ({view_sorts}) {proof_type} :merge old :internal-term-constructor {name}{view_flags})" - ); + // In proof mode, a constructor's view is a functional-dependency tuple + // `(children) -> (eclass, proof)` whose native `:merge` resolves congruence (see + // `EGraph::native_congruence_merge`). Other functions keep the `(children eclass) -> proof` + // form with a congruence/merge rule. + let fd_view = self.native_merge_view(fdecl); + let view_decl = if fd_view { + format!( + "(function {view_name} ({in_sorts}) ({out_type} {proof_type}) :merge (values old0 old1) :internal-term-constructor {name}{view_flags})" + ) + } else { + format!( + "(function {view_name} ({view_sorts}) {proof_type} :merge old :internal-term-constructor {name}{view_flags})" + ) + }; self.parse_program(&format!( " (sort {fresh_sort}) @@ -523,6 +568,9 @@ impl<'a> ProofInstrumentor<'a> { /// Rules that update the views when children change. fn rebuilding_rules(&mut self, fdecl: &ResolvedFunctionDecl) -> Vec { + if self.native_merge_view(fdecl) { + return self.rebuilding_rules_fd(fdecl); + } let types = fdecl.resolved_schema.view_types(); // Check if there are any eq-sort columns at all; if not, no rebuild rule needed. @@ -647,6 +695,99 @@ impl<'a> ProofInstrumentor<'a> { self.parse_program(&rule) } + /// Rebuild rule for a proof-mode functional-dependency constructor view + /// `(children) -> (eclass, proof)`: canonicalize the child keys and the eclass value through the + /// UF, re-`set` at the canonical children (which triggers the congruence `:merge` on collision), + /// and delete the stale row. + fn rebuilding_rules_fd(&mut self, fdecl: &ResolvedFunctionDecl) -> Vec { + let types = fdecl.resolved_schema.view_types(); + // The last column is the eclass (output); the rest are children (keys). + let n = types.len(); + let child = |i: usize| format!("c{i}_"); + let children_vars: Vec = (0..n - 1).map(child).collect(); + let child_types = &types[..n - 1]; + let eclass_type = &types[n - 1]; + + let view_name = self.view_name(&fdecl.name); + let (query_view, eclass_var, view_prf) = self.query_fd_view(&fdecl.name, &children_vars); + + // UF lookups for eq-sort children (keys) and the eclass (value). + let mut uf_queries: Vec = vec![]; + let mut child_leaders: Vec = vec![]; + let mut bool_neq: Vec = vec![]; + let mut child_uf_proofs: Vec> = vec![]; + for (i, ty) in child_types.iter().enumerate() { + if ty.is_eq_sort() { + let leader = format!("c{i}_leader_"); + let uf_fn = self.uf_function_name(ty.name()); + let ci = child(i); + let pair = self.fresh_var(); + uf_queries.push(format!( + "(= {pair} ({uf_fn} {ci})) + (= {leader} (pair-first {pair}))" + )); + child_uf_proofs.push(Some(format!("(pair-second {pair})"))); + bool_neq.push(format!("(bool-!= {ci} {leader})")); + child_leaders.push(leader); + } else { + child_leaders.push(child(i)); + child_uf_proofs.push(None); + } + } + // eclass leader (the value column; always eq-sort for a constructor). + let eclass_leader = self.fresh_var(); + let eclass_uf_fn = self.uf_function_name(eclass_type.name()); + let eclass_pair = self.fresh_var(); + uf_queries.push(format!( + "(= {eclass_pair} ({eclass_uf_fn} {eclass_var})) + (= {eclass_leader} (pair-first {eclass_pair}))" + )); + let eclass_uf_prf = format!("(pair-second {eclass_pair})"); + bool_neq.push(format!("(bool-!= {eclass_var} {eclass_leader})")); + + // Proof chain: congruence for each eq-sort child, then transitivity for the eclass update. + // `view_prf : eclass = f(children)`; after congruence, `eclass = f(child_leaders)`; and + // `eclass_uf_prf : eclass = eclass_leader`, so `final_pf : eclass_leader = f(child_leaders)`. + let trans = self.proof_names().eq_trans_constructor.clone(); + let congr = self.proof_names().congr_constructor.clone(); + let sym = self.proof_names().eq_sym_constructor.clone(); + let mut current_proof = view_prf.clone(); + let mut proof_parts: Vec = vec![]; + for (i, ty) in child_types.iter().enumerate() { + if !ty.is_eq_sort() { + continue; + } + let uf_prf = child_uf_proofs[i].as_ref().unwrap(); + let np = self.fresh_var(); + proof_parts.push(format!("(let {np} ({congr} {current_proof} {i} {uf_prf}))")); + current_proof = np; + } + let final_pf = self.fresh_var(); + proof_parts.push(format!( + "(let {final_pf} ({trans} ({sym} {eclass_uf_prf}) {current_proof}))" + )); + + let uf_query_str = uf_queries.join("\n "); + let filter = format!("(guard (or {}))", bool_neq.join(" ")); + let proof_code = proof_parts.join("\n"); + let updated = self.update_fd_view(&fdecl.name, &child_leaders, &eclass_leader, &final_pf); + let children_str = ListDisplay(&children_vars, " "); + let fresh_name = self.egraph.parser.symbol_gen.fresh("rebuild_rule"); + let rule = format!( + "(rule ({query_view} + {uf_query_str} + {filter}) + ( + {proof_code} + {updated} + (delete ({view_name} {children_str})) + ) + :ruleset {} :name \"{fresh_name}\" :internal-include-subsumed)", + self.proof_names().rebuilding_ruleset_name + ); + self.parse_program(&rule) + } + /// Rules that update the to_subsume tables when children change. /// copied from above and changed to remove last param since we dont deal with output value in to subsumed rows, removed proof flags since we dont need proofs for this, and changed from function returning unit to constructor for to subsume fn rebuilding_subsumed_rules(&mut self, fdecl: &ResolvedFunctionDecl) -> Vec { @@ -883,11 +1024,19 @@ impl<'a> ProofInstrumentor<'a> { let args_str = ListDisplay(new_args, " "); let proof = { - // View is always a function; query it and bind the output let view_proof_var = self.fresh_var(); - res.push(format!( - "(= {view_proof_var} ({view_name} {args_str} {fv}))" - )); + // In proof mode a constructor view is the FD tuple + // `(children) -> (eclass, proof)`: bind the eclass (`fv`) and proof from + // the tuple. Without proofs it's the `(children eclass) -> Unit` form. + if self.egraph.proof_state.proofs_enabled { + res.push(format!( + "(= (values {fv} {view_proof_var}) ({view_name} {args_str}))" + )); + } else { + res.push(format!( + "(= {view_proof_var} ({view_name} {args_str} {fv}))" + )); + } if self.proofs_enabled() { let mut proof = view_proof_var; for (i, arg_proof) in arg_proofs.into_iter().enumerate() { @@ -1049,6 +1198,23 @@ impl<'a> ProofInstrumentor<'a> { view_update } + /// Write a row into the proof-mode functional-dependency view + /// `(set (@FView children) (values eclass proof))`. Re-setting an existing `children` key with a + /// different `eclass` triggers the view's native congruence `:merge`. + fn update_fd_view( + &mut self, + fname: &str, + children: &[String], + eclass: &str, + proof: &str, + ) -> String { + let view_name = self.view_name(fname); + format!( + "(set ({view_name} {}) (values {eclass} {proof}))", + ListDisplay(children, " ") + ) + } + /// Return some code adding to the view and term tables. /// For constructors, `args` should not include the eclass of the resulting term (since it may not exist yet). /// For custom functions, `args` should include all arguments (including the output for the function). @@ -1121,7 +1287,14 @@ impl<'a> ProofInstrumentor<'a> { }; res.push(proof_str); - res.push(self.update_view(&func_type.name, &args_with_fv, &view_proof_var)); + if func_type.subtype == FunctionSubtype::Constructor + && self.egraph.proof_state.proofs_enabled + { + // FD view: children are the key, the fresh term is the eclass value. + res.push(self.update_fd_view(&func_type.name, args, &fv, &view_proof_var)); + } else { + res.push(self.update_view(&func_type.name, &args_with_fv, &view_proof_var)); + } // add to uf table to initialize eclass for constructors if func_type.subtype == FunctionSubtype::Constructor { @@ -1145,6 +1318,20 @@ impl<'a> ProofInstrumentor<'a> { (query, pf_var) } + /// Query the proof-mode functional-dependency view by its `children` key, binding fresh + /// variables for the `eclass` and `proof` output columns: `(= (values e pf) (@FView children))`. + /// Returns `(query, eclass_var, proof_var)`. + fn query_fd_view(&mut self, fname: &str, children: &[String]) -> (String, String, String) { + let view_name = self.view_name(fname); + let eclass_var = self.fresh_var(); + let pf_var = self.fresh_var(); + let query = format!( + "(= (values {eclass_var} {pf_var}) ({view_name} {}))", + ListDisplay(children, " ") + ); + (query, eclass_var, pf_var) + } + // Add to view and term tables, returning a variable for the created term. fn instrument_action_expr( &mut self, @@ -1349,6 +1536,7 @@ impl<'a> ProofInstrumentor<'a> { presort_and_args: presort_and_args.clone(), uf: Some(uf_name), proof_func, + proof_ctors: None, unionable: *unionable, }); res.extend(self.declare_sort(name)); diff --git a/egglog/src/proofs/proof_encoding_helpers.rs b/egglog/src/proofs/proof_encoding_helpers.rs index ed02ef8..0a5e0d3 100644 --- a/egglog/src/proofs/proof_encoding_helpers.rs +++ b/egglog/src/proofs/proof_encoding_helpers.rs @@ -373,7 +373,7 @@ impl ProofInstrumentor<'_> { " (sort {proof_list_sort}) (sort {ast_sort}) ;; wrap sorts in this for proofs -(sort {proof_datatype}) +(sort {proof_datatype} :internal-proof-names {congr_constructor} {eq_trans_constructor} {eq_sym_constructor}) (constructor {pcons} ({proof_datatype} {proof_list_sort}) {proof_list_sort} :internal-hidden) (constructor {pnil} () {proof_list_sort} :internal-hidden) diff --git a/egglog/src/serialize.rs b/egglog/src/serialize.rs index 83ab829..ed2d847 100644 --- a/egglog/src/serialize.rs +++ b/egglog/src/serialize.rs @@ -148,7 +148,13 @@ impl EGraph { truncated_functions.push(name.clone()); return false; } - let (out, inps) = row.vals.split_last().unwrap(); + // Split the row into key columns and value columns by the function's input arity. + // Tuple-output functions (e.g. the proof-mode `(children) -> (eclass, proof)` view) + // have more than one value column; the first value column is the e-class / output + // that serialization tracks, and any extra columns (a proof) are not serialized. + let n_keys = function.schema.input.len(); + let inps = &row.vals[..n_keys]; + let out = &row.vals[n_keys]; let class_id = self.value_to_class_id(&function.schema.output, *out); if function.decl.internal_let { let_bindings diff --git a/egglog/src/typechecking.rs b/egglog/src/typechecking.rs index 9d097ef..147c491 100644 --- a/egglog/src/typechecking.rs +++ b/egglog/src/typechecking.rs @@ -441,6 +441,7 @@ impl EGraph { presort_and_args, uf, proof_func, + proof_ctors, unionable, } => { // Note this is bad since typechecking should be pure and idempotent @@ -456,6 +457,7 @@ impl EGraph { presort_and_args: presort_and_args.clone(), uf: uf.clone(), proof_func: proof_func.clone(), + proof_ctors: proof_ctors.clone(), unionable: *unionable, } } @@ -760,8 +762,13 @@ impl TypeInfo { fdecl.span.clone(), )); } - // View tables (with term_constructor) must have at least one input (the e-class) - if fdecl.term_constructor.is_some() && fdecl.schema.input.is_empty() { + // View tables (with term_constructor) must have at least one input (the e-class), except the + // proof-mode functional-dependency tuple view `(children) -> (eclass, proof)`, which keys on + // children only (a 0-arg constructor's view then has no inputs). + if fdecl.term_constructor.is_some() + && fdecl.schema.input.is_empty() + && !fdecl.schema.is_tuple_output() + { return Err(TypeError::TermConstructorNoInputs( fdecl.name.clone(), fdecl.span.clone(), @@ -782,11 +789,11 @@ impl TypeInfo { let is_tuple = fdecl.schema.is_tuple_output(); // Tuple outputs are only meaningful for custom functions (which carry a functional - // dependency from keys to a tuple of values). Constructors and view tables mint/track a - // single e-class id. - if is_tuple - && (fdecl.subtype == FunctionSubtype::Constructor || fdecl.term_constructor.is_some()) - { + // dependency from keys to a tuple of values). Constructors mint a single e-class id, so they + // may not be tuple-output. Term-constructor *views* may be tuple-output: the proof-mode + // encoder emits `(children) -> (eclass, proof)` views (an internal-only annotation, so this + // can't be reached by user input). + if is_tuple && fdecl.subtype == FunctionSubtype::Constructor { return Err(TypeError::TupleOutputNotAllowed( fdecl.name.clone(), fdecl.span.clone(),