diff --git a/Sources/AngouriMath/Docs/Contributing/InversePairTable.md b/Sources/AngouriMath/Docs/Contributing/InversePairTable.md index 6f0e631c5..dddbc91d2 100644 --- a/Sources/AngouriMath/Docs/Contributing/InversePairTable.md +++ b/Sources/AngouriMath/Docs/Contributing/InversePairTable.md @@ -125,7 +125,22 @@ section arguing that behaviour is a better source than derivation. What this is and is not: - **It is a lower bound, and a cheap one.** A pair that never fires on the corpus is invisible to it, - and a pair split across two sets never meets. It cannot enumerate the table. + and — for the single-set observation above — a pair split across two sets never meets. It cannot + enumerate the table. + + *Saturation meets the cross-set case, because it runs every set at once.* The first pair found + that way is `ExpandMultipleAngle / sine-of-a-whole-multiple-of-an-angle` against + `Trigonometric / a-sine-times-a-cosine-of-one-angle-is-half-the-doubled-sine` — `sin(2x)` to + `2 sin x cos x` and straight back to `sin(2x) / 2`. On `sin(2x) + cos(2x)` at the widest ceiling + the graph reaches 254 e-nodes without saturating and extracts the input unchanged; remove either + direction and it saturates at about twenty. An e-graph is supposed to absorb an inverse pair, and + this one is not absorbed because its two forms differ by a coefficient that two `Common` rules — + `a-numeric-factor-floats-out-of-a-product-of-functions` and + `a-reciprocal-rational-factor-is-a-division` — rearrange non-confluently, so each pass produces a + fresh spelling rather than a merge. Found by ablation, one set and then one rule at a time, and + held by `SaturationAblationTest` in both directions. It is also the measured answer to what + #746 tier 2 called "a scheduling policy for `Expands`/`Unknown` rules": on this input the + runaway is not a tier, it is one pair. - **It needs no reversibility mechanism at all**, which is the whole of what makes it available today: it is behaviour observed at the top of the pipeline, not a property computed about a rule. - **It answers the question equality saturation actually asks.** The consumer in the opening quote diff --git a/Sources/Tests/UnitTests/Core/Transformations/SaturationAblationTest.cs b/Sources/Tests/UnitTests/Core/Transformations/SaturationAblationTest.cs new file mode 100644 index 000000000..118088bc7 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/SaturationAblationTest.cs @@ -0,0 +1,152 @@ +// +// 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 System; +using System.Collections.Generic; +using System.Linq; +using AngouriMath.Core; +using AngouriMath.Core.Budgets; +using AngouriMath.Core.Transformations; +using AngouriMath.Core.Transformations.Matching; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// What makes saturation at the widest ceiling run away, found by taking rules out one at a + /// time rather than by reasoning about tiers. + /// + /// + /// + /// The blow-up is not the unjudged rules as a class. It is one inverse pair, split across + /// two sets. #746 + /// tier 2's open item was phrased as "a scheduling policy for Expands/Unknown + /// rules", on the observation that sin(2x) + cos(2x) reaches 254 e-nodes without + /// saturating under the Unknown ceiling. Ablating every set in turn: removing any one + /// of Common, ExpandMultipleAngle or Trigonometric makes it saturate at + /// about twenty nodes, and removing CollapseMultipleFractions makes it worse + /// (618 — that set was acting as a brake). Ablating the rules of those three sets in turn + /// names four: + /// + /// + /// ExpandMultipleAngle / sine-of-a-whole-multiple-of-an-angle — sin(2x) to + /// 2 sin x cos x; + /// Trigonometric / a-sine-times-a-cosine-of-one-angle-is-half-the-doubled-sine — + /// sin x cos x to sin(2x) / 2, the exact inverse; + /// Common / a-numeric-factor-floats-out-of-a-product-of-functions and + /// Common / a-reciprocal-rational-factor-is-a-division — which keep respelling the + /// 2 · and / 2 between the two, so the two forms never land in one e-class and + /// every pass makes a fresh spelling instead of merging. + /// + /// + /// An e-graph is supposed to absorb an inverse pair — both directions land in one class and + /// it stops. This pair does not, because its two forms differ by a coefficient the + /// Common rules rearrange non-confluently. That is a precise thing, and it is the + /// first cross-set inverse pair anything here has measured: + /// Docs/Contributing/InversePairTable.md says single-set observation "never meets" a + /// pair split across two sets, and saturation meets it because it runs every set at once. + /// + /// + /// Pinned in both directions. The runaway is a known non-saturation, and each of the four + /// rules is asserted to be load-bearing for it — so fixing the pair deletes entries here + /// rather than leaving names that mean nothing, and a fifth rule joining the cycle fails. + /// + /// + [Trait("Area", "Core")] + public sealed class SaturationAblationTest + { + private const string Runaway = "sin(2 * x) + cos(2 * x)"; + + /// + /// Saturating at twenty nodes takes a few hundred steps; the runaway is past 250 nodes by + /// thirty thousand and keeps going. Three thousand steps separates the two cleanly, and + /// the step ceiling rather than the wall is what bounds a non-culprit ablation — there are + /// about a hundred of those, and at a three-second wall each they cost the suite five + /// minutes. The second is a backstop, not the bound. + /// + private static readonly WorkBudget Quick = new() { Steps = 3_000, Time = TimeSpan.FromSeconds(1) }; + + private static readonly (string Set, string Rule)[] LoadBearing = + { + ("Common", "a-numeric-factor-floats-out-of-a-product-of-functions"), + ("Common", "a-reciprocal-rational-factor-is-a-division"), + ("ExpandMultipleAngle", "sine-of-a-whole-multiple-of-an-angle"), + ("Trigonometric", "a-sine-times-a-cosine-of-one-angle-is-half-the-doubled-sine"), + }; + + private static IReadOnlyList Widest(Func keep) => + MatchedRules.All + .SelectMany(set => set.Rules.Select(rule => (set, rule))) + .Where(pair => keep(pair.set, pair.rule)) + .Select(pair => pair.rule) + .Where(rule => rule.Soundness is Soundness.Sound or Soundness.SoundUnderAssumptions) + .ToList(); + + private static (bool Saturated, int Nodes) Saturate(string source, IReadOnlyList rules) + { + var graph = new EGraph(); + graph.AddEntity(source.ToEntity()); + var ledger = BudgetLedger.For(nameof(SaturationAblationTest), Quick); + var saturated = Saturation.Run(graph, rules, ledger, node => node.Complexity); + return (saturated, graph.NodeCount); + } + + [Fact] + public void TheWidestCeilingDoesNotSaturateOnTheKnownRunaway() + { + var (saturated, nodes) = Saturate(Runaway, Widest((_, _) => true)); + Assert.False(saturated, + $"{Runaway} saturates now, at {nodes} nodes. The inverse pair above has been " + + "resolved; delete this and the load-bearing list rather than leave them."); + } + + [Fact] + public void EachOfTheFourRulesIsLoadBearingForTheRunaway() + { + var stillRunsAway = new List(); + foreach (var (setName, ruleName) in LoadBearing) + { + var rules = Widest((set, rule) => !(set.Name == setName && rule.Name == ruleName)); + Assert.True(rules.Count == Widest((_, _) => true).Count - 1, + $"{setName}/{ruleName} is not a rule in the registry any more; the entry is stale"); + var (saturated, nodes) = Saturate(Runaway, rules); + if (!saturated) + stillRunsAway.Add($"{setName}/{ruleName} removed: still {nodes} nodes and unsaturated"); + } + + Assert.True(stillRunsAway.Count == 0, + "these entries are no longer load-bearing for the runaway and should be deleted:\n" + + string.Join("\n", stillRunsAway)); + } + + /// + /// And no rule outside those four is load-bearing on its own — the pair is the whole of + /// it. Ablating every other rule of the three implicated sets must leave the runaway + /// intact, so a fifth rule joining the cycle is a change this notices. + /// + [Fact] + public void NoOtherRuleOfTheImplicatedSetsIsLoadBearing() + { + var implicated = new[] { "Common", "ExpandMultipleAngle", "Trigonometric" }; + var newlyLoadBearing = new List(); + foreach (var set in MatchedRules.All.Where(s => implicated.Contains(s.Name))) + foreach (var rule in set.Rules) + { + if (LoadBearing.Contains((set.Name, rule.Name))) continue; + var rules = Widest((s, r) => !ReferenceEquals(r, rule)); + var (saturated, nodes) = Saturate(Runaway, rules); + if (saturated) + newlyLoadBearing.Add($"{set.Name}/{rule.Name}: removing it saturates at {nodes}"); + } + + Assert.True(newlyLoadBearing.Count == 0, + "these rules are now load-bearing for the runaway and belong in the list above:\n" + + string.Join("\n", newlyLoadBearing)); + } + } +}