From e3b2cd9714eb27d920e1fa2a271f3dca6a88cca6 Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Mon, 7 Sep 2026 11:40:36 +0000 Subject: [PATCH] Extraction is a fixed point from the leaves up, and a budget is honoured to the millisecond #1199 recorded Saturation overshooting a two-second wall by up to thirty-five times. Instrumenting the loop on the worst input put 99% of the time in e-match attempts, one of which ran 1.9 s on a thirteen-member class; timing the steps of that one attempt's first binding put the whole 1.9 s in a single graph.Extract of one bound class -- on a graph of 253 e-nodes. The walk was top-down with a visiting-set cycle guard and a memo that fills only on completion, and a graph full of union-made cycles defeats that: any class on the stack blocks memoisation of everything beneath it, so sibling paths walk the same subgraph again and again. That, not the ledger, was the overshoot. Extraction is now a fixed point from the leaves up: a round recomputes every class from its children's current best, in class order and member order so ties fall the same way they did, and the rounds stop when one changes nothing. No recursion, so no depth guard and no stack to exhaust -- a chain three hundred deep extracts as itself where it used to come back null. The result is kept for as long as the graph does not change and the cost is the same delegate, and only a union can change what an existing class extracts as, so Union is where it is dropped. And the e-matcher charges the ledger once per binding it tries after the first, so an attempt over a class with a thousand members is a thousand steps and not one. Measured on the inputs of #1199, same budget of 20,000 steps and 2 s: total 2000 ms and 2000 ms where it was 2435 and 2595, the longest single attempt 4 ms where it was 1918, the longest extraction 3 ms. The Transformations tests hold every pin they held, the corpus figures included. One of my own claims does not survive this and is corrected where it was made. With the walk no longer the cost, the inputs #1200 called a stall are two things: x ^ 2 / x, x / x * -x and x / x * x * 1/2 are genuine runaways, ten to twelve thousand e-nodes in thirty seconds, and 2 * x * 1/2 and its relatives plateau at some 560 e-nodes and stop only when 200,000 steps run out. "Bounded at 135-583 e-nodes after thirty seconds" was the slow extraction, not the graph. ConstantFoldTest says so now, and its pin is renamed to what it pins: bounded by the budget, and extracting right. Part of #746. Fixes #1199. Full suite 9610 passed, 0 failed. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- .../Core/Transformations/EGraph.cs | 114 +++++++++++------- .../Transformations/Matching/MatchedRule.cs | 17 +++ .../Core/Transformations/Saturation.cs | 6 +- .../Core/Transformations/ConstantFoldTest.cs | 27 +++-- .../Core/Transformations/EGraphTest.cs | 15 ++- 5 files changed, 115 insertions(+), 64 deletions(-) diff --git a/Sources/AngouriMath/Core/Transformations/EGraph.cs b/Sources/AngouriMath/Core/Transformations/EGraph.cs index e4ffadba9..f58701a45 100644 --- a/Sources/AngouriMath/Core/Transformations/EGraph.cs +++ b/Sources/AngouriMath/Core/Transformations/EGraph.cs @@ -98,14 +98,6 @@ public override int GetHashCode() /// internal sealed class EGraph { - /// - /// How deep 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. - /// - private const int MaxExtractionDepth = 256; - private readonly List parent = new(); private readonly Dictionary hashcons = new(); private readonly Dictionary> classes = new(); @@ -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); @@ -408,7 +401,25 @@ internal int AddEntity(Entity expr) /// type does not build. /// internal Entity? Extract(int id, Func cost) - => Extract(id, new Cheapest(cost), new Dictionary(), new HashSet()); + { + // 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? extractMemo; + private Func? memoCost; /// /// The least entity the e-class can be built as under @@ -421,7 +432,7 @@ internal int AddEntity(Entity expr) /// well-defined expression where "the least member" is. See . /// internal Entity? ExtractLeast(int id, IComparer order) - => Extract(id, new Least(order), new Dictionary(), new HashSet()); + => ExtractAll(new Least(order)).TryGetValue(Find(id), out var least) ? least : null; /// /// How Extract chooses between the members of one e-class. A @@ -488,46 +499,61 @@ public void Offer(Entity candidate) public readonly Entity? Best => best; } - private Entity? Extract(int id, TSelection seed, - Dictionary memo, HashSet visiting) + /// + /// The best member of every class under , 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. + /// + private Dictionary ExtractAll(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(); + var leaves = new Dictionary(); + // 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; } diff --git a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs index 123addd56..2044a1043 100644 --- a/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs +++ b/Sources/AngouriMath/Core/Transformations/Matching/MatchedRule.cs @@ -264,14 +264,31 @@ private MatchedRule( /// internal bool TryEMatchApply( EGraph graph, int classId, Func cost, out int resultClassId) + => TryEMatchApply(graph, classId, cost, null, out resultClassId); + + /// + /// , charging + /// 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 from + /// ends the attempt as not matched; the caller's ledger says why. + /// https://github.com/asc-community/AngouriMath/issues/1199 + /// + internal bool TryEMatchApply( + EGraph graph, int classId, Func cost, Func? 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) { diff --git a/Sources/AngouriMath/Core/Transformations/Saturation.cs b/Sources/AngouriMath/Core/Transformations/Saturation.cs index 0703d2ba0..130ad9657 100644 --- a/Sources/AngouriMath/Core/Transformations/Saturation.cs +++ b/Sources/AngouriMath/Core/Transformations/Saturation.cs @@ -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 spend = () => ledger.Spend(); + var saturated = false; while (!saturated && !ledger.Exhausted) { @@ -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; } diff --git a/Sources/Tests/UnitTests/Core/Transformations/ConstantFoldTest.cs b/Sources/Tests/UnitTests/Core/Transformations/ConstantFoldTest.cs index 8c0690014..1cd4fa83d 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/ConstantFoldTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/ConstantFoldTest.cs @@ -35,14 +35,18 @@ namespace AngouriMath.Tests.Core.Transformations /// to 7, and the run from more than ten minutes to 24 seconds. /// /// - /// What is left is a stall, not a runaway. The seven are a rational coefficient - /// beside a variable — 2 * x * 1/2, x / x * -x, x ^ 2 / x — whose - /// spellings 1/2 * x, x / 2, x * 2 ^ (-1) the Rearranges 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 RunawayBreadthTest 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. + /// What is left is bounded by the budget and by nothing else. The seven are a + /// rational coefficient beside a variable — 2 * x * 1/2, x / x * -x, + /// x ^ 2 / x — whose spellings 1/2 * x, x / 2, x * 2 ^ (-1) the + /// Rearranges rules keep exchanging. Measured once extraction stopped being the + /// cost (#1199): + /// x ^ 2 / x, x / x * -x and x / x * x * 1/2 are genuine runaways, + /// ten to twelve thousand e-nodes in thirty seconds; 2 * x * 1/2 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 RunawayBreadthTest that the coefficient rules are confluent on plain + /// arithmetic is true of the three inputs it pins and not of the family. /// /// /// On the corpus the ceiling is cheap and finds a little more. Every one of the 40 @@ -131,11 +135,12 @@ public void ConstantOnlyArithmeticSaturatesAtTheSafeCeiling(string source) } /// - /// 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. /// [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" }; diff --git a/Sources/Tests/UnitTests/Core/Transformations/EGraphTest.cs b/Sources/Tests/UnitTests/Core/Transformations/EGraphTest.cs index ce3a75167..24ca601cc 100644 --- a/Sources/Tests/UnitTests/Core/Transformations/EGraphTest.cs +++ b/Sources/Tests/UnitTests/Core/Transformations/EGraphTest.cs @@ -282,15 +282,14 @@ public void ExtractSettlesACostTieOnADefinedOrder() } /// - /// 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 - /// cannot be caught, so it takes the process - /// down instead of failing one call. + /// used to recurse through an e-class's children and decline + /// to build past 256 levels, because a 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 + /// for that input while the guard existed. /// [Fact] - public void ExtractDeclinesToBuildPastItsDepthCap() + public void ExtractBuildsAChainDeeperThanTheOldCap() { Entity deep = "x".ToEntity(); for (var i = 0; i < 300; i++) deep += 1; @@ -299,7 +298,7 @@ public void ExtractDeclinesToBuildPastItsDepthCap() var extracted = graph.Extract(root, CostModel.Default.Cost); - Assert.Null(extracted); + Assert.Equal(deep, extracted); } ///