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); + } + } + } +}