Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
76def51
The e-graph moves from a harness into the kernel, behind an explicit …
Rafael-SOWNet Aug 28, 2026
476dc3d
The inverse-pair table is not Growth's small extension, and here is why
Rafael-SOWNet Aug 28, 2026
41f8121
A review caught the e-graph silently changing what it claimed to pres…
Rafael-SOWNet Aug 29, 2026
d2feaa0
Spec: a real e-matcher for EqualitySaturation
Rafael-SOWNet Aug 29, 2026
a1b4c1a
Implementation plan for the real e-matcher
Rafael-SOWNet Aug 29, 2026
2dcfa2b
Matching.MatchedRules gains a real All, and a test stops reflecting o…
Rafael-SOWNet Aug 29, 2026
6703480
EBindings: Bindings' cons-list, over e-class ids instead of entities
Rafael-SOWNet Aug 29, 2026
688ef61
MatchPattern.NodeCount: an exact structural count, for Growth to use
Rafael-SOWNet Aug 29, 2026
638b7a9
MatchedRule.Growth: an exact node-count classification, not a string-…
Rafael-SOWNet Aug 29, 2026
4ac0e7c
EGraph.ContainsLeaf and .RuntimeType: what e-matching needs from the …
Rafael-SOWNet Aug 29, 2026
a95f048
WIP: CanEMatch/EMatch/ETryBuild on MatchPattern, ExactPattern and Gat…
Rafael-SOWNet Aug 29, 2026
ddb4482
WIP: AnyPattern e-matches and e-builds
Rafael-SOWNet Aug 29, 2026
afd41fb
NodePattern e-matches recursively, trying both orders when commutative
Rafael-SOWNet Aug 29, 2026
f43548f
AnyPattern.EMatch: decline rather than crash on a wrong-typed extract…
Rafael-SOWNet Aug 29, 2026
d2e34e2
MatchedRule.TryEMatchApply: what TryApply does, against an e-class di…
Rafael-SOWNet Aug 29, 2026
00e3a2d
EqualitySaturation draws rules from Matching.MatchedRules and e-match…
Rafael-SOWNet Aug 29, 2026
6493f60
Cache a failed extraction too, so TryTerm re-extracts at most once pe…
Rafael-SOWNet Aug 29, 2026
c83c06c
Verification: e-matching agrees with matching, crosses a union, and b…
Rafael-SOWNet Aug 29, 2026
83be875
EMatchingAgreesWithMatching asserts its own skip list instead of trus…
Rafael-SOWNet Aug 29, 2026
90d1b71
Plan addendum: close the final review's Critical rule-collapse finding
Rafael-SOWNet Aug 29, 2026
6c9fa76
A code-built rule can declare its own Growth, the same way Soundness …
Rafael-SOWNet Aug 29, 2026
03b3f83
A first batch of code-built rules declare a Growth they can justify b…
Rafael-SOWNet Aug 29, 2026
1a59917
Close the final review: restore the exception guard, measure SafeRule…
Rafael-SOWNet Aug 29, 2026
a2604dc
Correct an inverted fact and drop unresolvable review-label citations
Rafael-SOWNet Aug 29, 2026
2b43dd6
Merge master after #1101 squash-merged: this branch already carries i…
Rafael-SOWNet Aug 29, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions Sources/AngouriMath/Core/Transformations/EGraph.cs
Original file line number Diff line number Diff line change
Expand Up @@ -309,5 +309,23 @@ internal int AddEntity(Entity expr)

private static Type OperatorType(string op)
=> OperatorTypes.TryGetValue(op, out var type) ? type : typeof(void);

/// <summary>
/// Whether the e-class <paramref name="id"/> already contains a leaf equal to
/// <paramref name="leaf"/> -- the same check <see cref="NeutralClass"/> uses for a
/// neutral element, offered for <see cref="Matching.MatchPattern"/>'s
/// <c>ExactPattern.EMatch</c> to use for a literal.
/// </summary>
internal bool ContainsLeaf(int id, Entity leaf) => Holds(id, Key(leaf));

/// <summary>
/// The runtime <see cref="Type"/> an e-node builds as: a leaf's, by re-parsing its
/// printed form, or a non-leaf's operator type, by the same lookup <c>Extract</c>
/// uses to reconstruct one. <c>typeof(void)</c> where neither succeeds.
/// </summary>
internal static Type RuntimeType(ENode node)
=> node.Children.Length == 0
? TryParseLeaf(node.Op)?.GetType() ?? typeof(void)
: OperatorType(node.Op);
}
}
214 changes: 214 additions & 0 deletions Sources/AngouriMath/Core/Transformations/Matching/MatchPattern.cs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
using System;
using System.Collections.Generic;
using System.Linq;
using AngouriMath.Core.Transformations;

namespace AngouriMath.Core.Transformations.Matching
{
Expand Down Expand Up @@ -75,6 +76,44 @@ internal int Count
internal Bindings With(string name, Entity value) => new(this, name, value);
}

/// <summary>
/// The e-graph counterpart of <see cref="Bindings"/>: a set of named holes, each standing for
/// an e-class id rather than an <see cref="Entity"/>. Same cons-list shape, for the same reason
/// -- see <see cref="Bindings"/>'s own remarks -- plus one concrete win it gets for free: a name
/// bound twice (<c>x - x -&gt; 0</c>'s repeated <c>x</c>) becomes an O(1) class-id comparison
/// instead of an <see cref="Entity.Equals(Entity)"/> call.
/// </summary>
internal sealed class EBindings
{
private readonly EBindings? tail;
private readonly string? name;
private readonly int value;

internal static EBindings Empty { get; } = new(null, null, 0);

private EBindings(EBindings? tail, string? name, int value)
{
this.tail = tail;
this.name = name;
this.value = value;
}

internal bool TryGet(string wanted, out int found)
{
for (var at = this; at is not null; at = at.tail)
if (at.name == wanted)
{
found = at.value;
return true;
}
found = 0;
return false;
}

/// <summary>A new set with one more name bound, sharing this one as its tail.</summary>
internal EBindings With(string name, int value) => new(this, name, value);
}

/// <summary>
/// The left-hand side of a rewrite rule, as a <b>value</b> rather than as an arm of a
/// <c>switch</c>.
Expand Down Expand Up @@ -267,6 +306,13 @@ private protected virtual bool TryMatchChoiceCore(
/// </remarks>
internal abstract bool IsBuildable { get; }

/// <summary>
/// How many nodes this pattern is, counted structurally -- used to classify a
/// <see cref="MatchedRule"/>'s <see cref="RewriteRuleGrowth"/> exactly, in place of the
/// public registry's string-length proxy over rendered pattern text.
/// </summary>
internal abstract int NodeCount { get; }

/// <summary>
/// The expression this pattern stands for under <paramref name="bindings"/>, or
/// <see langword="false"/> where those bindings do not satisfy it.
Expand All @@ -290,6 +336,37 @@ private protected virtual bool TryMatchChoiceCore(
/// </remarks>
internal abstract bool TryBuild(Bindings bindings, out Entity built);

/// <summary>
/// Whether this pattern can match an e-class directly, without ever materialising a term
/// from it. Structural and independent of any bindings -- computed once per pattern, not
/// per attempt. False only for <see cref="GatheredPattern"/> and for any
/// <see cref="NodePattern"/> containing one.
/// </summary>
internal abstract bool CanEMatch { get; }

/// <summary>
/// Every way this pattern can match the e-class <paramref name="classId"/>, extending
/// <paramref name="bindings"/> -- the e-graph counterpart of <see cref="Match"/>. Only
/// meaningful where <see cref="CanEMatch"/>; a caller must check that first.
/// </summary>
/// <param name="graph">The e-graph <paramref name="classId"/> belongs to.</param>
/// <param name="classId">The e-class to match against.</param>
/// <param name="bindings">The bindings so far, extended rather than replaced.</param>
/// <param name="cost">
/// Used only where a lazily-extracted witness is needed (an inline <c>where</c> predicate)
/// -- see the remarks on <c>Docs/Contributing/EMatching.md</c>'s "lazy extraction" section.
/// </param>
internal abstract IEnumerable<EBindings> EMatch(
EGraph graph, int classId, EBindings bindings, Func<Entity, double> cost);

/// <summary>
/// The e-class this pattern stands for under <paramref name="bindings"/>, built without
/// materialising a term -- the e-graph counterpart of <see cref="TryBuild"/>. Only
/// meaningful where <see cref="CanEMatch"/>.
/// </summary>
internal abstract bool ETryBuild(
EGraph graph, EBindings bindings, Func<Entity, double> cost, out int classId);

/// <summary>
/// Builds a node of <paramref name="nodeType"/> over <paramref name="children"/>, or
/// <see langword="null"/> where this cannot -- see the remarks on <see cref="Construct"/>,
Expand Down Expand Up @@ -495,6 +572,8 @@ private protected override bool TryMatchOnceCore(

internal override bool IsBuildable => true;

internal override int NodeCount => 1;

internal override bool TryBuild(Bindings bindings, out Entity built)
{
built = null!;
Expand All @@ -507,6 +586,53 @@ internal override bool TryBuild(Bindings bindings, out Entity built)
built = value;
return true;
}

internal override bool CanEMatch => true;

internal override IEnumerable<EBindings> EMatch(
EGraph graph, int classId, EBindings bindings, Func<Entity, double> cost)
{
if (bindings.TryGet(name, out var already))
{
if (graph.Find(already) == graph.Find(classId)) yield return bindings;
yield break;
}
var eligible = required is null
|| graph.NodesOf(classId).Any(node => required.IsAssignableFrom(EGraph.RuntimeType(node)));
if (!eligible) yield break;
if (where is not null)
{
var witness = graph.Extract(classId, cost);
// The same guard ETryBuild applies before calling `where`: `where` is
// compiled from `Any<T>(name, where)` as an unguarded cast to T (see that
// factory, above), so a witness the eligibility check above did not itself
// require to be of type T -- the cheapest overall representative of the
// class, not the cheapest one of type T -- would throw InvalidCastException
// rather than simply fail to match. Declining here is a missed match, which
// is a legitimate answer; a crash is not.
if (witness is null
|| (required is not null && !required.IsInstanceOfType(witness))
|| !where(witness))
yield break;
}
yield return bindings.With(name, classId);
}

internal override bool ETryBuild(
EGraph graph, EBindings bindings, Func<Entity, double> cost, out int classId)
{
classId = 0;
if (!bindings.TryGet(name, out var bound)) return false;
if (required is not null || where is not null)
{
var witness = graph.Extract(bound, cost);
if (witness is null) return false;
if (required is not null && !required.IsInstanceOfType(witness)) return false;
if (where is not null && !where(witness)) return false;
}
classId = bound;
return true;
}
}

private sealed class ExactPattern : MatchPattern
Expand Down Expand Up @@ -542,11 +668,28 @@ private protected override bool TryMatchOnceCore(

internal override bool IsBuildable => true;

internal override int NodeCount => 1;

internal override bool TryBuild(Bindings bindings, out Entity built)
{
built = value;
return true;
}

internal override bool CanEMatch => true;

internal override IEnumerable<EBindings> EMatch(
EGraph graph, int classId, EBindings bindings, Func<Entity, double> cost)
{
if (graph.ContainsLeaf(classId, value)) yield return bindings;
}

internal override bool ETryBuild(
EGraph graph, EBindings bindings, Func<Entity, double> cost, out int classId)
{
classId = graph.AddEntity(value);
return true;
}
}

private sealed class NodePattern : MatchPattern
Expand All @@ -566,11 +709,16 @@ internal NodePattern(Type nodeType, MatchPattern[] children, bool commutative)
buildable = CanConstruct(nodeType, children.Length)
&& children.All(child => child.IsBuildable);
deterministic = !commutative && children.All(child => child.IsDeterministic);
nodeCount = 1 + children.Sum(child => child.NodeCount);
canEMatch = children.All(child => child.CanEMatch);
}

/// <summary>Settled here because it depends on nothing that changes afterwards.</summary>
private readonly bool buildable;

/// <summary>Settled here for the same reason as <see cref="buildable"/>.</summary>
private readonly bool canEMatch;

/// <summary>
/// Settled here for the same reason as <see cref="buildable"/>, and it matters more:
/// <c>MatchedRule.TryApply</c> reads it on <b>every attempt</b>, and a rewrite pass
Expand All @@ -581,6 +729,11 @@ internal NodePattern(Type nodeType, MatchPattern[] children, bool commutative)
/// </summary>
private readonly bool deterministic;

/// <summary>Settled here for the same reason as <see cref="buildable"/>.</summary>
private readonly int nodeCount;

internal override int NodeCount => nodeCount;

internal override IEnumerable<string> BoundNames => children.SelectMany(c => c.BoundNames);

public override string ToString()
Expand Down Expand Up @@ -731,6 +884,48 @@ internal override bool TryBuild(Bindings bindings, out Entity built)
built = node;
return true;
}

internal override bool CanEMatch => canEMatch;

internal override IEnumerable<EBindings> EMatch(
EGraph graph, int classId, EBindings bindings, Func<Entity, double> cost)
{
foreach (var node in graph.NodesOf(classId))
{
if (node.Op != nodeType.Name || node.Children.Length != children.Length) continue;
foreach (var solution in EMatchInOrder(graph, node.Children, bindings, 0, cost))
yield return solution;
if (!commutative) continue;
var swapped = new[] { node.Children[1], node.Children[0] };
foreach (var solution in EMatchInOrder(graph, swapped, bindings, 0, cost))
yield return solution;
}
}

private IEnumerable<EBindings> EMatchInOrder(
EGraph graph, int[] actual, EBindings bindings, int index, Func<Entity, double> cost)
{
if (index == children.Length)
{
yield return bindings;
yield break;
}
foreach (var head in children[index].EMatch(graph, actual[index], bindings, cost))
foreach (var rest in EMatchInOrder(graph, actual, head, index + 1, cost))
yield return rest;
}

internal override bool ETryBuild(
EGraph graph, EBindings bindings, Func<Entity, double> cost, out int classId)
{
classId = 0;
var parts = new int[children.Length];
for (var i = 0; i < children.Length; i++)
if (!children[i].ETryBuild(graph, bindings, cost, out parts[i]))
return false;
classId = graph.Add(nodeType.Name, parts);
return true;
}
}

private sealed class GatheredPattern : MatchPattern
Expand All @@ -751,8 +946,15 @@ internal GatheredPattern(Type nodeType, string restName, MatchPattern[] parts)
this.nodeType = nodeType;
this.restName = restName ?? throw new ArgumentNullException(nameof(restName));
this.parts = parts;
// An approximation, not the true size: the "rest" this gathers is open-ended and
// its actual length is only known once a match commits to one. Counted as the
// one node a single wildcard would be. See this plan's Global Constraints for why
// this is an accepted, bounded imprecision rather than a defect to fix here.
NodeCount = 1 + parts.Sum(part => part.NodeCount) + 1;
}

internal override int NodeCount { get; }

private bool OverSum => nodeType == typeof(Entity.Sumf);

internal override IEnumerable<string> BoundNames
Expand Down Expand Up @@ -875,6 +1077,18 @@ internal override bool TryBuild(Bindings bindings, out Entity built)
return true;
}

internal override bool CanEMatch => false;

internal override IEnumerable<EBindings> EMatch(
EGraph graph, int classId, EBindings bindings, Func<Entity, double> cost)
=> throw new NotSupportedException(
$"{nameof(GatheredPattern)} does not e-match; check {nameof(CanEMatch)} first.");

internal override bool ETryBuild(
EGraph graph, EBindings bindings, Func<Entity, double> cost, out int classId)
=> throw new NotSupportedException(
$"{nameof(GatheredPattern)} does not e-match; check {nameof(CanEMatch)} first.");

private Entity Combine(Entity left, Entity right)
=> OverSum ? new Entity.Sumf(left, right) : new Entity.Mulf(left, right);

Expand Down
Loading
Loading