From b5836ee09683d3ed31305d4e71a4cf7ae94d8b63 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 6 Sep 2026 18:05:49 +0000 Subject: [PATCH] A codomain is part of an e-node's identity, not a note beside it An e-class is the graph's assertion that its members are equal. abs(x) and domain(abs(x), Any) are not equal -- they evaluate differently -- and the graph put them in one class. Codomain lived in a side table keyed on shape alone, so the two hashed to the same e-node; the table then held whichever was inserted last, so extracting the narrow one returned Any; and Rebuild re-created every node from operator and children only, dropping the codomain on any union anywhere in the graph. Three defects, one cause. ENodeIdentityTest reproduced each before anything was changed, and holds all three now. Codomain is a field of ENode and part of Equals, GetHashCode and CompareTo. Add passes it into the node, Rebuild carries it through, Extract reads it off the node, and the side table is deleted. NeutralClass declines to fold a node that carries its own codomain, since folding domain(x * 1, Any) into x's class is the same conflation by another door. Op is untouched, so every reader of it is unchanged. This settles the question EqualitySaturationReviewFindings.md left open -- how much rides on an e-node beyond its bare shape -- for the only instance the library has, and gives the rule for the next one: identity must include everything that makes two entities unequal, and nothing else. A cached cost or hash is not that; a codomain is. The document says so now instead of calling it undecided. Full suite 9571 passed, 0 failed. Part of #746. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- .../Core/Transformations/EGraph.cs | 49 +++++---- .../EqualitySaturationReviewFindings.md | 15 +++ .../Core/Transformations/ENodeIdentityTest.cs | 101 ++++++++++++++++++ 3 files changed, 145 insertions(+), 20 deletions(-) create mode 100644 Sources/Tests/UnitTests/Core/Transformations/ENodeIdentityTest.cs diff --git a/Sources/AngouriMath/Core/Transformations/EGraph.cs b/Sources/AngouriMath/Core/Transformations/EGraph.cs index 37d5761dc..e91c1f8bf 100644 --- a/Sources/AngouriMath/Core/Transformations/EGraph.cs +++ b/Sources/AngouriMath/Core/Transformations/EGraph.cs @@ -18,18 +18,32 @@ namespace AngouriMath.Core.Transformations /// internal readonly struct ENode : IEquatable, IComparable { - internal ENode(string op, int[] children) + internal ENode(string op, int[] children, Domain? codomain = null) { Op = op ?? throw new ArgumentNullException(nameof(op)); Children = children ?? throw new ArgumentNullException(nameof(children)); + Codomain = codomain; } internal string Op { get; } internal int[] Children { get; } + /// + /// The the node carries where it differs from its type's + /// default, and where it does not. Part of the node's identity, + /// deliberately. An e-class is the graph's assertion that its members are equal, and + /// abs(x) is not equal to domain(abs(x), Any) — they evaluate differently — + /// so two nodes differing only here must hash apart, or the graph unions values that are + /// not the same value. This used to live in a side table keyed on shape alone; both then + /// landed in one class and extraction returned whichever was inserted last, and + /// Rebuild dropped it altogether. ENodeIdentityTest holds all three. + /// + internal Domain? Codomain { get; } + public bool Equals(ENode other) { - if (Op != other.Op || Children.Length != other.Children.Length) return false; + if (Op != other.Op || Codomain != other.Codomain || Children.Length != other.Children.Length) + return false; for (var i = 0; i < Children.Length; i++) if (Children[i] != other.Children[i]) return false; return true; @@ -50,6 +64,8 @@ public int CompareTo(ENode other) { var byOp = string.CompareOrdinal(Op, other.Op); if (byOp != 0) return byOp; + var byCodomain = Nullable.Compare(Codomain, other.Codomain); + if (byCodomain != 0) return byCodomain; if (Children.Length != other.Children.Length) return Children.Length.CompareTo(other.Children.Length); for (var i = 0; i < Children.Length; i++) @@ -61,14 +77,16 @@ public int CompareTo(ENode other) public override int GetHashCode() { var hash = Op.GetHashCode(); + hash = unchecked(hash * 31 + (Codomain is { } domain ? (int)domain + 1 : 0)); foreach (var child in Children) hash = unchecked(hash * 31 + child); return hash; } } /// - /// An e-graph: e-classes over a union-find, e-nodes keyed by operator and child class, - /// hash-consed. + /// An e-graph: e-classes over a union-find, e-nodes keyed by operator, child class and + /// non-default codomain, hash-consed. The codomain is in the key because an e-class is an + /// equality claim and a codomain is something two unequal entities can differ in. /// /// /// #746 tier 2's e-graph, @@ -90,18 +108,6 @@ internal sealed class EGraph private readonly Dictionary hashcons = new(); private readonly Dictionary> classes = new(); - /// - /// The the source carried at the exact - /// e-node a real entity was inserted as, where it differs from that node's own default -- - /// Add(string, int[]) has no to read it from, only - /// does. Extract(int, Func{Entity, double}) re-applies it - /// after rebuilding through , which builds through - /// a bare constructor and so restores nothing on its own -- unlike every other place this - /// codebase reconstructs a node, which copies it forward through a New(...) helper. - /// Caught in code review before this PR was merged. - /// - private readonly Dictionary codomains = new(); - /// How many e-classes this graph currently has. internal int ClassCount => classes.Count; @@ -137,8 +143,7 @@ private int NewClass() private int Add(string op, int[] children, Domain? codomain) { - var canonical = new ENode(op, children.Select(Find).ToArray()); - if (codomain is { } existingDomain) codomains[canonical] = existingDomain; + var canonical = new ENode(op, children.Select(Find).ToArray(), codomain); if (hashcons.TryGetValue(canonical, out var existing)) return Find(existing); // Folding on insertion: a neutral-element application denotes exactly the value its @@ -237,6 +242,10 @@ internal static IEnumerable NeutralFolds private int? NeutralClass(ENode node) { if (node.Children.Length != 2) return null; + // A node carrying a codomain of its own is not the value of its other operand: folding + // `domain(x * 1, Any)` into x's class would union it with a plain `x`, which is the + // same conflation the identity above exists to prevent. + if (node.Codomain is not null) return null; foreach (var leaf in NeutralLeaves) { if (neutralFolds.Contains((node.Op, leaf, 1)) && Holds(node.Children[1], leaf)) @@ -285,7 +294,7 @@ internal void Rebuild() foreach (var pair in classes.ToList()) foreach (var node in pair.Value.ToList()) { - var canonical = new ENode(node.Op, node.Children.Select(Find).ToArray()); + var canonical = new ENode(node.Op, node.Children.Select(Find).ToArray(), node.Codomain); if (seen.TryGetValue(canonical, out var other)) { if (Union(other, pair.Key)) changed = true; @@ -449,7 +458,7 @@ public void Offer(Entity candidate) ? TryParseLeaf(node.Op) : MatchPattern.ConstructNode(OperatorType(node.Op), parts); if (built is null) continue; - if (codomains.TryGetValue(node, out var domain)) built = built.WithCodomain(domain); + if (node.Codomain is { } domain) built = built.WithCodomain(domain); selection.Offer(built); } visiting.Remove(id); diff --git a/Sources/AngouriMath/Docs/Contributing/EqualitySaturationReviewFindings.md b/Sources/AngouriMath/Docs/Contributing/EqualitySaturationReviewFindings.md index de58d4e49..e8d809bf4 100644 --- a/Sources/AngouriMath/Docs/Contributing/EqualitySaturationReviewFindings.md +++ b/Sources/AngouriMath/Docs/Contributing/EqualitySaturationReviewFindings.md @@ -189,6 +189,21 @@ beyond its bare shape.** A general "attach anything, forget nothing" representat special cases extended as each is found. `InversePairTable.md` leaves the same question open for its own mechanism, and it is arguably the same question either way. +*Decided for the one live instance, by measurement rather than by preference.* `Codomain` was the +special case, kept in a side table keyed on shape alone — and that was wrong in three places at once. +`abs(x)` and `domain(abs(x), Any)` hashed to one e-node and so shared an e-class, which is the graph +asserting two unequal values are equal; extraction then returned whichever had been inserted last; +and `Rebuild` re-created every node from operator and children only, dropping the codomain on any +union. `ENodeIdentityTest` reproduced all three before anything was changed. + +The rule that falls out is not "attach anything" and not "special-case each": it is that **an +e-node's identity must include everything that makes two entities unequal**, because an e-class is +an equality claim. `Codomain` distinguishes unequal entities, so it is now a field of `ENode` and +part of `Equals`, `GetHashCode` and the ordering — and the side table is gone. Anything that is +*not* part of equality (a cached hash, a cost) stays off the node. That answers the question for +any future per-node datum too: ask whether two entities differing only in it are equal, and the +answer says which side of the line it goes. + What the fourteen closed findings say about it is worth recording, because it is not what the review expected. Only one of them turned out to depend on this decision at all — `Codomain`, which is still special-cased. The `Providedf` case, which this document originally offered as evidence that the diff --git a/Sources/Tests/UnitTests/Core/Transformations/ENodeIdentityTest.cs b/Sources/Tests/UnitTests/Core/Transformations/ENodeIdentityTest.cs new file mode 100644 index 000000000..704f5abf6 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/ENodeIdentityTest.cs @@ -0,0 +1,101 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +using AngouriMath.Core; +using AngouriMath.Core.Transformations; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// An e-node's identity has to include everything that makes two entities unequal, or the + /// graph unions values that are not the same value. is the one + /// piece of per-node data the library carries that is not a child, and it is exactly such a + /// thing: abs(x) and domain(abs(x), Any) are different entities that evaluate + /// differently, and an e-class holding both is asserting they are equal. + /// + [Trait("Area", "Core")] + public sealed class ENodeIdentityTest + { + [Fact] + public void ACodomainIsPartOfWhatMakesTwoEntitiesUnequal() + { + var narrow = "abs(x)".ToEntity(); + var wide = narrow.WithCodomain(Domain.Any); + + Assert.NotEqual(narrow, wide); + Assert.NotEqual(narrow.Codomain, wide.Codomain); + } + + /// + /// The defect, stated as the graph sees it: two unequal entities inserted separately + /// must not share an e-class, because an e-class is the graph's assertion that its + /// members are equal. + /// + [Fact] + public void TwoEntitiesDifferingOnlyInCodomainGetDifferentClasses() + { + var graph = new EGraph(); + var narrow = graph.AddEntity("abs(x)".ToEntity()); + var wide = graph.AddEntity("abs(x)".ToEntity().WithCodomain(Domain.Any)); + + Assert.NotEqual(graph.Find(narrow), graph.Find(wide)); + } + + /// + /// A rebuild re-creates every e-node canonically after a union. It used to do that from + /// the operator and children alone, dropping the codomain — so a union anywhere in the + /// graph quietly widened or narrowed unrelated nodes. Two unions here, one of them + /// touching a child of the codomain-bearing node so that its canonical form changes. + /// + [Fact] + public void ACodomainSurvivesARebuild() + { + var graph = new EGraph(); + var wide = graph.AddEntity("abs(x)".ToEntity().WithCodomain(Domain.Any)); + var y = graph.AddEntity("y".ToEntity()); + var x = graph.AddEntity("x".ToEntity()); + + graph.Union(x, y); + graph.Rebuild(); + + var extracted = graph.Extract(wide, e => e.Complexity); + Assert.NotNull(extracted); + Assert.Equal(Domain.Any, extracted!.Codomain); + } + + /// + /// And whichever is extracted must be the one that was put in, not the one that happened + /// to be inserted last. Inserted narrow-then-wide and wide-then-narrow, so that an + /// implementation where the last writer wins fails on one of the two orders. + /// + [Fact] + public void ExtractionReturnsTheCodomainThatWasInserted() + { + foreach (var wideFirst in new[] { false, true }) + { + var graph = new EGraph(); + var narrowEntity = "abs(x)".ToEntity(); + var wideEntity = narrowEntity.WithCodomain(Domain.Any); + + var first = graph.AddEntity(wideFirst ? wideEntity : narrowEntity); + var second = graph.AddEntity(wideFirst ? narrowEntity : wideEntity); + var narrow = wideFirst ? second : first; + var wide = wideFirst ? first : second; + + var narrowOut = graph.Extract(narrow, e => e.Complexity); + var wideOut = graph.Extract(wide, e => e.Complexity); + + Assert.NotNull(narrowOut); + Assert.NotNull(wideOut); + Assert.Equal(narrowEntity.Codomain, narrowOut!.Codomain); + Assert.Equal(Domain.Any, wideOut!.Codomain); + } + } + } +}