diff --git a/Sources/Tests/UnitTests/Core/Transformations/RuleSetTerminationTest.cs b/Sources/Tests/UnitTests/Core/Transformations/RuleSetTerminationTest.cs new file mode 100644 index 000000000..ab6887ff7 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/RuleSetTerminationTest.cs @@ -0,0 +1,221 @@ +// +// 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.Collections.Generic; +using System.Linq; +using AngouriMath; +using AngouriMath.Core.Transformations; +using AngouriMath.Extensions; +using Xunit; + +namespace AngouriMath.Tests.Core.Transformations +{ + /// + /// Every rule set in the registry reaches a fixed point when it is iterated. + /// + /// + /// + /// #746 tier 2 asks for + /// "termination checked by tooling rather than asserted by authors". The tooling existed and + /// lived in a workspace harness, so it answered for whoever ran it and for no one else. A + /// non-terminating rule set is a hang rather than a wrong answer, and a hang is what the + /// suite is worst at reporting, so this is the check worth having where the build can see it. + /// + /// + /// Two questions, because they have different answers. Alone is what tier 2 asks: rules + /// as first-class data means a caller may apply one set by itself. Composed is how the + /// simplifier actually runs them, with the normalisation between passes. A set that settles + /// only in composition is half a rewrite system, and until this test there was nothing saying + /// which ones those were outside a generated report. + /// + /// + [Trait("Area", "Core")] + public sealed class RuleSetTerminationTest + { + /// Applications before a set is called non-terminating on an input. + private const int MaxPasses = 64; + + /// + /// The sets that cycle when iterated on their own and settle once the normalisation runs + /// between passes. Named rather than counted: a count going from two to two says nothing + /// when one set has been fixed and another has started, and a name is what a failure + /// needs to be actionable. + /// + /// + /// Power splits a power of a product — (2 * x) ^ 2 to 2 ^ 2 * x ^ 2 — + /// and something has to fold 2 ^ 2 before the result stops being a power of a + /// product. NumericNeat rewrites --x through a product of ones that only + /// collapses when the normalisation multiplies them out. Both are the same shape: a rule + /// whose right-hand side is a fixed point only after arithmetic that the set itself does + /// not do. + /// + private static readonly HashSet SettleOnlyComposed = new() { "Power", "NumericNeat" }; + + private static readonly string[] Leaves = { "x", "y", "2", "-1", "1/2", "1", "0" }; + + private static readonly string[] Unary = + { + "-({0})", "1 / ({0})", "({0}) ^ 2", "sqrt({0})", "sin({0})", "abs({0})", + }; + + private static readonly string[] Binary = + { + "({0}) + ({1})", "({0}) - ({1})", "({0}) * ({1})", "({0}) / ({1})", "({0}) ^ ({1})", + }; + + /// + /// Parsed once. Rebuilding it per rule set parsed the same few hundred strings thirty + /// times over, which is the whole cost of this test and none of its coverage. + /// + private static readonly IReadOnlyList Inputs = BuildCorpus(); + + private static List BuildCorpus() + { + var level1 = new List(Leaves); + var level2 = new List(); + foreach (var shape in Unary) + foreach (var inner in level1) + level2.Add(string.Format(shape, inner)); + foreach (var shape in Binary) + foreach (var left in level1) + foreach (var right in level1) + level2.Add(string.Format(shape, left, right)); + + // A third level, and it is load-bearing: the shapes that cycle are a unary applied + // to something already compound -- `(2 * x) ^ 2`, `--x`, `sqrt(1/2 * 2)`. Without it + // this corpus reproduces none of them and the list below reads as empty, which is + // exactly what the second assertion caught the first time it ran. + var level3 = new List(); + foreach (var shape in Unary) + foreach (var inner in level2) + level3.Add(string.Format(shape, inner)); + + var parsed = new List(); + foreach (var source in level1.Concat(level2).Concat(level3)) + { + try { parsed.Add(source.ToEntity()); } + catch { /* the generator makes some strings the parser declines */ } + } + return parsed; + } + + private static bool Terminates(RewriteRuleSet set, Entity from, bool normalise, out Entity stuck) + { + var current = from; + for (var pass = 0; pass < MaxPasses; pass++) + { + Entity applied; + try + { + applied = normalise + ? set.ApplyOnce(current).InnerSimplified + : set.ApplyOnce(current); + } + catch + { + // A set that throws has not claimed anything about termination. + stuck = current; + return true; + } + if (applied.Equals(current)) + { + stuck = current; + return true; + } + current = applied; + } + stuck = current; + return false; + } + + /// + /// The sets that reach no fixed point even with the normalisation between passes, + /// which is how the simplifier runs them. + /// + /// + /// Common has a three-cycle on -x * 1/2: + /// Mulf(-1/2, x) to Mulf(-1, Divf(x, 2)) to Divf(Mulf(-1, x), 2) and + /// back — three trees printing as two strings, which is why it wants writing down as + /// shapes. Two rules disagree about whether c * x or (c * x) / d is the + /// destination. Simplify bounds its own iteration and does not hang, so this is a + /// property of the set rather than a defect a caller sees today + /// (#1056). + /// + private static readonly HashSet NeverSettle = new() { "Common" }; + + /// + /// With the normalisation between passes — how the simplifier runs them — every set + /// settles except those named, and the naming is asserted in both directions. + /// + [Fact] + public void OnlyTheNamedSetsReachNoFixedPoint() + { + var cycling = new SortedSet(); + var examples = new List(); + foreach (var set in RewriteRules.All) + foreach (var expr in Inputs) + { + Entity once; + try { once = set.ApplyOnce(expr); } catch { continue; } + if (once.Equals(expr)) + continue; + if (!Terminates(set, once, normalise: true, out var stuck)) + { + cycling.Add(set.Name); + if (examples.Count < 10) + examples.Add($"{set.Name} on `{expr.Stringize()}`, stuck at `{stuck.Stringize()}`"); + } + } + + var started = cycling.Except(NeverSettle).ToList(); + Assert.True(started.Count == 0, + "these sets reach no fixed point in " + MaxPasses + " passes even with the " + + "normalisation between them: " + string.Join(", ", started) + + "\n" + string.Join("\n", examples)); + + var stopped = NeverSettle.Except(cycling).ToList(); + Assert.True(stopped.Count == 0, + "these sets terminate now and should leave the list: " + string.Join(", ", stopped)); + } + + /// + /// Iterated on its own, every set settles except the two named — and those two must still + /// be the ones named, so that a set which starts cycling is a failure rather than a + /// number that moved. + /// + [Fact] + public void OnlyTheNamedSetsNeedTheNormalisationToSettle() + { + var cycling = new SortedSet(); + foreach (var set in RewriteRules.All) + foreach (var expr in Inputs) + { + Entity once; + try { once = set.ApplyOnce(expr); } catch { continue; } + if (once.Equals(expr)) + continue; + if (!Terminates(set, once, normalise: false, out _)) + cycling.Add(set.Name); + } + + // A set that reaches no fixed point even composed reaches none alone either, so the + // two lists together are what may cycle here. + var known = new HashSet(SettleOnlyComposed); + known.UnionWith(NeverSettle); + + var started = cycling.Except(known).ToList(); + Assert.True(started.Count == 0, + "these sets have started cycling when iterated alone: " + string.Join(", ", started)); + + // The other direction, so the list cannot outlive what it describes. + var stopped = known.Except(cycling).ToList(); + Assert.True(stopped.Count == 0, + "these sets no longer need the normalisation and should leave the list: " + + string.Join(", ", stopped)); + } + } +}