Skip to content

Commit eb3a044

Browse files
A codomain is part of an e-node's identity, not a note beside it (#1191)
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. Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
1 parent aea71c6 commit eb3a044

3 files changed

Lines changed: 145 additions & 20 deletions

File tree

‎Sources/AngouriMath/Core/Transformations/EGraph.cs‎

Lines changed: 29 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -18,18 +18,32 @@ namespace AngouriMath.Core.Transformations
1818
/// </summary>
1919
internal readonly struct ENode : IEquatable<ENode>, IComparable<ENode>
2020
{
21-
internal ENode(string op, int[] children)
21+
internal ENode(string op, int[] children, Domain? codomain = null)
2222
{
2323
Op = op ?? throw new ArgumentNullException(nameof(op));
2424
Children = children ?? throw new ArgumentNullException(nameof(children));
25+
Codomain = codomain;
2526
}
2627

2728
internal string Op { get; }
2829
internal int[] Children { get; }
2930

31+
/// <summary>
32+
/// The <see cref="Entity.Codomain"/> the node carries where it differs from its type's
33+
/// default, and <see langword="null"/> where it does not. <b>Part of the node's identity,
34+
/// deliberately.</b> An e-class is the graph's assertion that its members are equal, and
35+
/// <c>abs(x)</c> is not equal to <c>domain(abs(x), Any)</c> — they evaluate differently —
36+
/// so two nodes differing only here must hash apart, or the graph unions values that are
37+
/// not the same value. This used to live in a side table keyed on shape alone; both then
38+
/// landed in one class and extraction returned whichever was inserted last, and
39+
/// <c>Rebuild</c> dropped it altogether. <c>ENodeIdentityTest</c> holds all three.
40+
/// </summary>
41+
internal Domain? Codomain { get; }
42+
3043
public bool Equals(ENode other)
3144
{
32-
if (Op != other.Op || Children.Length != other.Children.Length) return false;
45+
if (Op != other.Op || Codomain != other.Codomain || Children.Length != other.Children.Length)
46+
return false;
3347
for (var i = 0; i < Children.Length; i++)
3448
if (Children[i] != other.Children[i]) return false;
3549
return true;
@@ -50,6 +64,8 @@ public int CompareTo(ENode other)
5064
{
5165
var byOp = string.CompareOrdinal(Op, other.Op);
5266
if (byOp != 0) return byOp;
67+
var byCodomain = Nullable.Compare(Codomain, other.Codomain);
68+
if (byCodomain != 0) return byCodomain;
5369
if (Children.Length != other.Children.Length)
5470
return Children.Length.CompareTo(other.Children.Length);
5571
for (var i = 0; i < Children.Length; i++)
@@ -61,14 +77,16 @@ public int CompareTo(ENode other)
6177
public override int GetHashCode()
6278
{
6379
var hash = Op.GetHashCode();
80+
hash = unchecked(hash * 31 + (Codomain is { } domain ? (int)domain + 1 : 0));
6481
foreach (var child in Children) hash = unchecked(hash * 31 + child);
6582
return hash;
6683
}
6784
}
6885

6986
/// <summary>
70-
/// An e-graph: e-classes over a union-find, e-nodes keyed by operator and child class,
71-
/// hash-consed.
87+
/// An e-graph: e-classes over a union-find, e-nodes keyed by operator, child class and
88+
/// non-default codomain, hash-consed. The codomain is in the key because an e-class is an
89+
/// equality claim and a codomain is something two unequal entities can differ in.
7290
/// </summary>
7391
/// <remarks>
7492
/// <a href="https://github.com/asc-community/AngouriMath/issues/746">#746</a> tier 2's e-graph,
@@ -90,18 +108,6 @@ internal sealed class EGraph
90108
private readonly Dictionary<ENode, int> hashcons = new();
91109
private readonly Dictionary<int, HashSet<ENode>> classes = new();
92110

93-
/// <summary>
94-
/// The <see cref="Entity.Codomain"/> the source <see cref="Entity"/> carried at the exact
95-
/// e-node a real entity was inserted as, where it differs from that node's own default --
96-
/// <c>Add(string, int[])</c> has no <see cref="Entity"/> to read it from, only
97-
/// <see cref="AddEntity"/> does. <c>Extract(int, Func{Entity, double})</c> re-applies it
98-
/// after rebuilding through <see cref="MatchPattern.ConstructNode"/>, which builds through
99-
/// a bare constructor and so restores nothing on its own -- unlike every other place this
100-
/// codebase reconstructs a node, which copies it forward through a <c>New(...)</c> helper.
101-
/// Caught in code review before this PR was merged.
102-
/// </summary>
103-
private readonly Dictionary<ENode, Domain> codomains = new();
104-
105111
/// <summary>How many e-classes this graph currently has.</summary>
106112
internal int ClassCount => classes.Count;
107113

@@ -137,8 +143,7 @@ private int NewClass()
137143

138144
private int Add(string op, int[] children, Domain? codomain)
139145
{
140-
var canonical = new ENode(op, children.Select(Find).ToArray());
141-
if (codomain is { } existingDomain) codomains[canonical] = existingDomain;
146+
var canonical = new ENode(op, children.Select(Find).ToArray(), codomain);
142147
if (hashcons.TryGetValue(canonical, out var existing))
143148
return Find(existing);
144149
// Folding on insertion: a neutral-element application denotes exactly the value its
@@ -237,6 +242,10 @@ internal static IEnumerable<string> NeutralFolds
237242
private int? NeutralClass(ENode node)
238243
{
239244
if (node.Children.Length != 2) return null;
245+
// A node carrying a codomain of its own is not the value of its other operand: folding
246+
// `domain(x * 1, Any)` into x's class would union it with a plain `x`, which is the
247+
// same conflation the identity above exists to prevent.
248+
if (node.Codomain is not null) return null;
240249
foreach (var leaf in NeutralLeaves)
241250
{
242251
if (neutralFolds.Contains((node.Op, leaf, 1)) && Holds(node.Children[1], leaf))
@@ -285,7 +294,7 @@ internal void Rebuild()
285294
foreach (var pair in classes.ToList())
286295
foreach (var node in pair.Value.ToList())
287296
{
288-
var canonical = new ENode(node.Op, node.Children.Select(Find).ToArray());
297+
var canonical = new ENode(node.Op, node.Children.Select(Find).ToArray(), node.Codomain);
289298
if (seen.TryGetValue(canonical, out var other))
290299
{
291300
if (Union(other, pair.Key)) changed = true;
@@ -449,7 +458,7 @@ public void Offer(Entity candidate)
449458
? TryParseLeaf(node.Op)
450459
: MatchPattern.ConstructNode(OperatorType(node.Op), parts);
451460
if (built is null) continue;
452-
if (codomains.TryGetValue(node, out var domain)) built = built.WithCodomain(domain);
461+
if (node.Codomain is { } domain) built = built.WithCodomain(domain);
453462
selection.Offer(built);
454463
}
455464
visiting.Remove(id);

‎Sources/AngouriMath/Docs/Contributing/EqualitySaturationReviewFindings.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -189,6 +189,21 @@ beyond its bare shape.** A general "attach anything, forget nothing" representat
189189
special cases extended as each is found. `InversePairTable.md` leaves the same question open for its
190190
own mechanism, and it is arguably the same question either way.
191191

192+
*Decided for the one live instance, by measurement rather than by preference.* `Codomain` was the
193+
special case, kept in a side table keyed on shape alone — and that was wrong in three places at once.
194+
`abs(x)` and `domain(abs(x), Any)` hashed to one e-node and so shared an e-class, which is the graph
195+
asserting two unequal values are equal; extraction then returned whichever had been inserted last;
196+
and `Rebuild` re-created every node from operator and children only, dropping the codomain on any
197+
union. `ENodeIdentityTest` reproduced all three before anything was changed.
198+
199+
The rule that falls out is not "attach anything" and not "special-case each": it is that **an
200+
e-node's identity must include everything that makes two entities unequal**, because an e-class is
201+
an equality claim. `Codomain` distinguishes unequal entities, so it is now a field of `ENode` and
202+
part of `Equals`, `GetHashCode` and the ordering — and the side table is gone. Anything that is
203+
*not* part of equality (a cached hash, a cost) stays off the node. That answers the question for
204+
any future per-node datum too: ask whether two entities differing only in it are equal, and the
205+
answer says which side of the line it goes.
206+
192207
What the fourteen closed findings say about it is worth recording, because it is not what the review
193208
expected. Only one of them turned out to depend on this decision at all — `Codomain`, which is still
194209
special-cased. The `Providedf` case, which this document originally offered as evidence that the
Lines changed: 101 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,101 @@
1+
//
2+
// Copyright (c) 2019-2026 Angouri.
3+
// AngouriMath is licensed under MIT.
4+
// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.
5+
// Website: https://am.angouri.org.
6+
//
7+
8+
using AngouriMath.Core;
9+
using AngouriMath.Core.Transformations;
10+
using AngouriMath.Extensions;
11+
using Xunit;
12+
13+
namespace AngouriMath.Tests.Core.Transformations
14+
{
15+
/// <summary>
16+
/// An e-node's identity has to include everything that makes two entities unequal, or the
17+
/// graph unions values that are not the same value. <see cref="Entity.Codomain"/> is the one
18+
/// piece of per-node data the library carries that is not a child, and it is exactly such a
19+
/// thing: <c>abs(x)</c> and <c>domain(abs(x), Any)</c> are different entities that evaluate
20+
/// differently, and an e-class holding both is asserting they are equal.
21+
/// </summary>
22+
[Trait("Area", "Core")]
23+
public sealed class ENodeIdentityTest
24+
{
25+
[Fact]
26+
public void ACodomainIsPartOfWhatMakesTwoEntitiesUnequal()
27+
{
28+
var narrow = "abs(x)".ToEntity();
29+
var wide = narrow.WithCodomain(Domain.Any);
30+
31+
Assert.NotEqual(narrow, wide);
32+
Assert.NotEqual(narrow.Codomain, wide.Codomain);
33+
}
34+
35+
/// <summary>
36+
/// The defect, stated as the graph sees it: two unequal entities inserted separately
37+
/// must not share an e-class, because an e-class is the graph's assertion that its
38+
/// members are equal.
39+
/// </summary>
40+
[Fact]
41+
public void TwoEntitiesDifferingOnlyInCodomainGetDifferentClasses()
42+
{
43+
var graph = new EGraph();
44+
var narrow = graph.AddEntity("abs(x)".ToEntity());
45+
var wide = graph.AddEntity("abs(x)".ToEntity().WithCodomain(Domain.Any));
46+
47+
Assert.NotEqual(graph.Find(narrow), graph.Find(wide));
48+
}
49+
50+
/// <summary>
51+
/// A rebuild re-creates every e-node canonically after a union. It used to do that from
52+
/// the operator and children alone, dropping the codomain — so a union anywhere in the
53+
/// graph quietly widened or narrowed unrelated nodes. Two unions here, one of them
54+
/// touching a child of the codomain-bearing node so that its canonical form changes.
55+
/// </summary>
56+
[Fact]
57+
public void ACodomainSurvivesARebuild()
58+
{
59+
var graph = new EGraph();
60+
var wide = graph.AddEntity("abs(x)".ToEntity().WithCodomain(Domain.Any));
61+
var y = graph.AddEntity("y".ToEntity());
62+
var x = graph.AddEntity("x".ToEntity());
63+
64+
graph.Union(x, y);
65+
graph.Rebuild();
66+
67+
var extracted = graph.Extract(wide, e => e.Complexity);
68+
Assert.NotNull(extracted);
69+
Assert.Equal(Domain.Any, extracted!.Codomain);
70+
}
71+
72+
/// <summary>
73+
/// And whichever is extracted must be the one that was put in, not the one that happened
74+
/// to be inserted last. Inserted narrow-then-wide and wide-then-narrow, so that an
75+
/// implementation where the last writer wins fails on one of the two orders.
76+
/// </summary>
77+
[Fact]
78+
public void ExtractionReturnsTheCodomainThatWasInserted()
79+
{
80+
foreach (var wideFirst in new[] { false, true })
81+
{
82+
var graph = new EGraph();
83+
var narrowEntity = "abs(x)".ToEntity();
84+
var wideEntity = narrowEntity.WithCodomain(Domain.Any);
85+
86+
var first = graph.AddEntity(wideFirst ? wideEntity : narrowEntity);
87+
var second = graph.AddEntity(wideFirst ? narrowEntity : wideEntity);
88+
var narrow = wideFirst ? second : first;
89+
var wide = wideFirst ? first : second;
90+
91+
var narrowOut = graph.Extract(narrow, e => e.Complexity);
92+
var wideOut = graph.Extract(wide, e => e.Complexity);
93+
94+
Assert.NotNull(narrowOut);
95+
Assert.NotNull(wideOut);
96+
Assert.Equal(narrowEntity.Codomain, narrowOut!.Codomain);
97+
Assert.Equal(Domain.Any, wideOut!.Codomain);
98+
}
99+
}
100+
}
101+
}

0 commit comments

Comments
 (0)