Wire the scoped e-graph as an equality-saturation sink - #117
Open
MesTTo wants to merge 5 commits into
Open
Conversation
MesTTo
changed the title
Adds the thin fact layer over the interning base: FactId liveness via a weight tombstone (remove_fact tombstones, insert_fact revives the same FactId, the Lucene "live documents" model), live_fact_count, and facts_by_relation, an index from a relation head to its facts so a consumer (EGraph::from_equalities, RelationAdjacency::from_sidecar) scans one relation instead of the whole sidecar. Deliberately excludes incremental maintenance (prefix staleness watermarks, delta application, PathMap re-sync scans): incremental maintenance is deferred project-wide, and PathMap's own shared_node_id COW identity is the right staleness primitive when it becomes needed, not a value-count watermark.
Replaces the hand-rolled 128-bit FNV in TermIdentitySidecar with the canonical Expr::hash (gxhash128 over the term's byte span), the same structural hash the rest of MORK already uses. The hash is only a collision-bucket filter -- exact encoded bytes are compared before an identity is reused -- so the swap cannot change which terms share a TermId, on ground or adversarial input. Modeled in Alloy (fac22_term_identity in MesTTo/alloy-mork): HashSwapPreservesIdentity is UNSAT. Addresses the maintainer's "reuse, don't reimplement" direction (no bespoke hash where the crate has one). term_identity (4) and egraph (2) suites pass.
Exposes egraph.rs as a grounded sink `(egraph <term | (= a b)>)`, behind a new default-off `egraph` feature. It accumulates matched terms and equalities into a scoped e-graph, runs congruence closure at finalize, and writes each member's cheapest-extracted canonical form back as a `(canon <member> <rep>)` atom, which ordinary queries then read. This is the grounded sink/source shape Adam asked for (a mechanism behind the IO machinery, like z3), modeled on the ACT/Remove write-back sinks. Reuses egraph.rs (union-find + egg-style rebuild + cheapest extraction) and the term-identity sidecar for interning; nothing is reimplemented. The pattern is relational e-matching / egglog (Zhang et al., POPL 2022 / PLDI 2023): the pattern body is the conjunctive query, this sink is the equality-saturation half. Feature-gated so the default build compiles identical code (0 regressions by construction and by the full test suite). Two end-to-end tests cover saturation and congruence read-through; a runnable resources/egraph_saturation.mm2 example is included. The soundness contract is modeled in Alloy (fac23_egraph_sink in MesTTo/alloy-mork): the source reads the congruence closure correctly through extraction, one canonical representative per class.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a scoped e-graph (e-class union-find + egg-style congruence closure + cheapest extraction) and wires it as a grounded sink
(egraph <term | (= a b)>)behind a default-offegraphfeature — the sink shape from the MORKification discussion (a grounded mechanism behind the IO machinery, like z3). It accumulates matched terms and equalities, runs congruence closure at finalize, and writes each member's cheapest canonical form back as a(canon <member> <rep>)atom that ordinary queries read. Reuses the term-identity sidecar for interning andExpr::hashfor the structural hash; nothing reimplemented.Feature-gated, so the default build is unchanged — 0 benchmark regressions, verified across the full suite (byte-identical deterministic counters + clean interleaved-timing parity). Two end-to-end tests (saturation + congruence read-through), a runnable
resources/egraph_saturation.mm2, and the soundness contract modeled in Alloy (github.com/MesTTo/alloy-mork: fac22 hash-swap, fac23 sink).