Skip to content

Extraction is a fixed point from the leaves up, and a budget is honoured to the millisecond #1202

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Rafael-SOWNet merged 1 commit into from
Sep 7, 2026
Merged

Extraction is a fixed point from the leaves up, and a budget is honoured to the millisecond #1202

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
114 changes: 70 additions & 44 deletions Sources/AngouriMath/Core/Transformations/EGraph.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,14 +98,6 @@ public override int GetHashCode()
/// </remarks>
internal sealed class EGraph
{
/// <summary>
/// How deep <see cref="Extract(int, Func{Entity, double})"/> will chain through child
/// classes before declining to build. A crash guard rather than a quality knob: textbook
/// input nests nowhere near this far, so the cap is only reached where the alternative is
/// an uncatchable stack overflow.
/// </summary>
private const int MaxExtractionDepth = 256;

private readonly List<int> parent = new();
private readonly Dictionary<ENode, int> hashcons = new();
private readonly Dictionary<int, HashSet<ENode>> classes = new();
Expand Down Expand Up @@ -336,6 +328,7 @@ internal bool Union(int left, int right)
left = Find(left);
right = Find(right);
if (left == right) return false;
extractMemo = null;
parent[right] = left;
foreach (var node in classes[right]) classes[left].Add(node);
classes.Remove(right);
Expand Down Expand Up @@ -408,7 +401,25 @@ internal int AddEntity(Entity expr)
/// type <see cref="MatchPattern.ConstructNode"/> does not build.
/// </summary>
internal Entity? Extract(int id, Func<Entity, double> cost)
=> Extract(id, new Cheapest(cost), new Dictionary<int, Entity>(), new HashSet<int>());
{
// One extraction of the whole graph, kept for as long as the graph does not change
// and the cost is the same delegate. Only a union can change what an existing class
// extracts as -- a new class never alters an old one -- so Union is where it is
// dropped. Before this, every witness an e-match attempt wanted was a fresh walk,
// once per bound name per binding and once per predicated hole per candidate class,
// and one such walk of a 253-node graph took 1.9 s: the walk was top-down with a
// cycle guard, and a graph full of union-made cycles defeats a memo that fills only
// on completion. https://github.com/asc-community/AngouriMath/issues/1199
if (!ReferenceEquals(cost, memoCost) || extractMemo is null)
{
memoCost = cost;
extractMemo = ExtractAll(new Cheapest(cost));
}
return extractMemo.TryGetValue(Find(id), out var best) ? best : null;
}

private Dictionary<int, Entity>? extractMemo;
private Func<Entity, double>? memoCost;

/// <summary>
/// The least entity the e-class <paramref name="id"/> can be built as under
Expand All @@ -421,7 +432,7 @@ internal int AddEntity(Entity expr)
/// well-defined expression where "the least member" is. See <see cref="EntityOrder"/>.
/// </remarks>
internal Entity? ExtractLeast(int id, IComparer<Entity> order)
=> Extract(id, new Least(order), new Dictionary<int, Entity>(), new HashSet<int>());
=> ExtractAll(new Least(order)).TryGetValue(Find(id), out var least) ? least : null;

/// <summary>
/// How <c>Extract</c> chooses between the members of one e-class. A
Expand Down Expand Up @@ -488,46 +499,61 @@ public void Offer(Entity candidate)
public readonly Entity? Best => best;
}

private Entity? Extract<TSelection>(int id, TSelection seed,
Dictionary<int, Entity> memo, HashSet<int> visiting)
/// <summary>
/// The best member of every class under <paramref name="seed"/>, from the leaves up: a
/// round recomputes each class from its children's current best, and the rounds stop
/// when one changes nothing. No recursion, so no depth to guard and no stack to exhaust;
/// a member that reaches back into its own class through a union is built from that
/// class's current best and offered like any other, and loses to it under any selection
/// that does not prefer the larger of two writings of one thing. Rounds are bounded by
/// the longest chain of classes, and capped at the class count for a selection that is
/// not monotone in its children.
/// </summary>
private Dictionary<int, Entity> ExtractAll<TSelection>(TSelection seed)
where TSelection : struct, ISelection
{
id = Find(id);
if (memo.TryGetValue(id, out var done)) return done;
// visiting is the chain currently being expanded, so its size is this call's depth.
// The cycle guard below bounds that chain only by the number of distinct classes,
// which unions grow past the input expression's own syntactic depth -- and a
// StackOverflowException cannot be caught, so exhausting the stack takes the process
// down rather than failing one call. Declining to build is the answer the cycle case
// already gives, and the same shape as Gruntz's own MaxDepth.
if (visiting.Count >= MaxExtractionDepth) return null;
if (!visiting.Add(id)) return null; // a cycle; the other node will do
var selection = seed;
selection.Begin();
// Ordered, not as the set enumerates: where the selection ties, the answer is
// whichever candidate was reached first, and set order is neither specified nor
// stable across processes.
foreach (var node in NodesOf(id).OrderBy(node => node))
var best = new Dictionary<int, Entity>();
var leaves = new Dictionary<string, Entity?>();
// Ordered, not as the dictionary enumerates: where the selection ties, the answer is
// whichever candidate was reached first, and dictionary and set order are neither
// specified nor stable across processes.
var ids = classes.Keys.OrderBy(id => id).ToList();
for (var round = 0; round <= ids.Count; round++)
{
var parts = new Entity[node.Children.Length];
var ok = true;
for (var i = 0; i < parts.Length && ok; i++)
var changed = false;
foreach (var id in ids)
{
var part = Extract(node.Children[i], seed, memo, visiting);
if (part is null) ok = false;
else parts[i] = part;
var selection = seed;
selection.Begin();
foreach (var node in classes[id].OrderBy(node => node))
{
var parts = new Entity[node.Children.Length];
var ok = true;
for (var i = 0; i < parts.Length && ok; i++)
if (best.TryGetValue(Find(node.Children[i]), out var part)) parts[i] = part;
else ok = false;
if (!ok) continue;
Entity? built;
if (parts.Length == 0)
{
if (!leaves.TryGetValue(node.Op, out built))
leaves[node.Op] = built = TryParseLeaf(node.Op);
}
else built = MatchPattern.ConstructNode(OperatorType(node.Op), parts);
if (built is null) continue;
if (node.Codomain is { } domain) built = built.WithCodomain(domain);
selection.Offer(built);
}
var chosen = selection.Best;
if (chosen is null) continue;
if (!best.TryGetValue(id, out var incumbent) || !chosen.Equals(incumbent))
{
best[id] = chosen;
changed = true;
}
}
if (!ok) continue;
Entity? built = parts.Length == 0
? TryParseLeaf(node.Op)
: MatchPattern.ConstructNode(OperatorType(node.Op), parts);
if (built is null) continue;
if (node.Codomain is { } domain) built = built.WithCodomain(domain);
selection.Offer(built);
if (!changed) break;
}
visiting.Remove(id);
var best = selection.Best;
if (best is not null) memo[id] = best;
return best;
}

Expand Down
17 changes: 17 additions & 0 deletions Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -264,14 +264,31 @@ private MatchedRule(
/// </summary>
internal bool TryEMatchApply(
EGraph graph, int classId, Func<Entity, double> cost, out int resultClassId)
=> TryEMatchApply(graph, classId, cost, null, out resultClassId);

/// <summary>
/// <see cref="TryEMatchApply(EGraph, int, Func{Entity, double}, out int)"/>, charging
/// <paramref name="spend"/> once for every binding tried after the first. A binding tried
/// is a match attempt: the caller charged the first, and an attempt over a class with a
/// thousand members is a thousand of them and not one -- which is what let a two-second
/// budget run for sixty-nine. A <see langword="false"/> from <paramref name="spend"/>
/// ends the attempt as not matched; the caller's ledger says why.
/// https://github.com/asc-community/AngouriMath/issues/1199
/// </summary>
internal bool TryEMatchApply(
EGraph graph, int classId, Func<Entity, double> cost, Func<bool>? spend, out int resultClassId)
{
if (!Left.CanEMatch)
throw new InvalidOperationException(
$"'{Name}' cannot e-match; check {nameof(Left)}.{nameof(MatchPattern.CanEMatch)} first.");

resultClassId = 0;
var first = true;
foreach (var ebindings in Left.EMatch(graph, classId, EBindings.Empty, cost))
{
if (!first && spend is not null && !spend()) return false;
first = false;

Bindings? entityBindings = null;
bool TryEntityBindings(out Bindings result)
{
Expand Down
6 changes: 5 additions & 1 deletion Sources/AngouriMath/Core/Transformations/Saturation.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,10 @@ bool ChargeGrowthSinceLastCall()
return ledger.Spend(delta);
}

// Handed to the e-matcher so that a binding tried is a step, not only the attempt --
// allocated once here rather than per attempt.
Func<bool> spend = () => ledger.Spend();

var saturated = false;
while (!saturated && !ledger.Exhausted)
{
Expand Down Expand Up @@ -189,7 +193,7 @@ bool TryTerm(out Entity value)
// wrote, and a predicate that throws on a shape it did not expect must
// decline the candidate, not escape Apply.
bool matched;
try { matched = rule.TryEMatchApply(graph, id, witnessCost, out other); }
try { matched = rule.TryEMatchApply(graph, id, witnessCost, spend, out other); }
catch { continue; }
if (!matched) continue;
}
Expand Down
27 changes: 16 additions & 11 deletions Sources/Tests/UnitTests/Core/Transformations/ConstantFoldTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,14 +35,18 @@ namespace AngouriMath.Tests.Core.Transformations
/// to 7, and the run from more than ten minutes to 24 seconds.
/// </para>
/// <para>
/// <b>What is left is a stall, not a runaway.</b> The seven are a rational coefficient
/// beside a variable — <c>2 * x * 1/2</c>, <c>x / x * -x</c>, <c>x ^ 2 / x</c> — whose
/// spellings <c>1/2 * x</c>, <c>x / 2</c>, <c>x * 2 ^ (-1)</c> the <c>Rearranges</c> rules
/// keep exchanging. Given fifteen times the budget they still report no fixed point, but
/// the graph barely grows (135–583 e-nodes after thirty seconds) and every one extracts
/// the right answer. So the claim in <c>RunawayBreadthTest</c> that the coefficient rules
/// are confluent on plain arithmetic is true of the three inputs it pins and not of the
/// family; the honest statement is that they are bounded and correct, and not confluent.
/// <b>What is left is bounded by the budget and by nothing else.</b> The seven are a
/// rational coefficient beside a variable — <c>2 * x * 1/2</c>, <c>x / x * -x</c>,
/// <c>x ^ 2 / x</c> — whose spellings <c>1/2 * x</c>, <c>x / 2</c>, <c>x * 2 ^ (-1)</c> the
/// <c>Rearranges</c> rules keep exchanging. Measured once extraction stopped being the
/// cost (<a href="https://github.com/asc-community/AngouriMath/issues/1199">#1199</a>):
/// <c>x ^ 2 / x</c>, <c>x / x * -x</c> and <c>x / x * x * 1/2</c> are genuine runaways,
/// ten to twelve thousand e-nodes in thirty seconds; <c>2 * x * 1/2</c> and its relatives
/// plateau at some 560 e-nodes and stop only when 200,000 steps run out. An earlier
/// version of this remark called them stalls at 135–583 e-nodes, which was the slow
/// extraction and not the graph. Every one extracts the right answer regardless, and the
/// claim in <c>RunawayBreadthTest</c> that the coefficient rules are confluent on plain
/// arithmetic is true of the three inputs it pins and not of the family.
/// </para>
/// <para>
/// <b>On the corpus the ceiling is cheap and finds a little more.</b> Every one of the 40
Expand Down Expand Up @@ -131,11 +135,12 @@ public void ConstantOnlyArithmeticSaturatesAtTheSafeCeiling(string source)
}

/// <summary>
/// Pinned in both directions: an entry that starts saturating is to be deleted, and one
/// whose graph grows past a thousand e-nodes has stopped being a stall.
/// Pinned in both directions under a three-thousand-step budget: an entry that starts
/// saturating is to be deleted, and one whose graph passes a thousand e-nodes within
/// those steps has changed character. The extraction must be right either way.
/// </summary>
[Fact]
public void ACoefficientBesideAVariableStallsRatherThanRunsAway()
public void ACoefficientBesideAVariableIsBoundedByTheBudgetAndExtractsRight()
{
var stalls = new[] { "2 * x * 1/2", "x * 1/2 * 2", "x ^ 2 / x", "x / x * -x" };
var answers = new[] { "x", "x", "x", "-x" };
Expand Down
15 changes: 7 additions & 8 deletions Sources/Tests/UnitTests/Core/Transformations/EGraphTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -282,15 +282,14 @@ public void ExtractSettlesACostTieOnADefinedOrder()
}

/// <summary>
/// <see cref="EGraph.Extract"/> recurses through an e-class's children, and its cycle
/// guard bounds the chain only by the number of distinct classes -- which unions grow
/// past the input expression's own syntactic depth. Past the cap it declines to build,
/// the same answer the cycle case already gives, rather than exhausting the stack: a
/// <see cref="System.StackOverflowException"/> cannot be caught, so it takes the process
/// down instead of failing one call.
/// <see cref="EGraph.Extract"/> used to recurse through an e-class's children and decline
/// to build past 256 levels, because a <see cref="System.StackOverflowException"/> cannot
/// be caught. It is a fixed point from the leaves up now, with no stack to exhaust, so a
/// chain three hundred deep extracts as itself -- this test asserted <see langword="null"/>
/// for that input while the guard existed.
/// </summary>
[Fact]
public void ExtractDeclinesToBuildPastItsDepthCap()
public void ExtractBuildsAChainDeeperThanTheOldCap()
{
Entity deep = "x".ToEntity();
for (var i = 0; i < 300; i++) deep += 1;
Expand All @@ -299,7 +298,7 @@ public void ExtractDeclinesToBuildPastItsDepthCap()

var extracted = graph.Extract(root, CostModel.Default.Cost);

Assert.Null(extracted);
Assert.Equal(deep, extracted);
}

/// <summary>
Expand Down
Loading