diff --git a/Sources/AngouriMath/Docs/Contributing/EqualitySaturationReviewFindings.md b/Sources/AngouriMath/Docs/Contributing/EqualitySaturationReviewFindings.md index 20177e9af..de58d4e49 100644 --- a/Sources/AngouriMath/Docs/Contributing/EqualitySaturationReviewFindings.md +++ b/Sources/AngouriMath/Docs/Contributing/EqualitySaturationReviewFindings.md @@ -174,6 +174,14 @@ whitelist rather than the node model: `Providedf` is an ordinary two-child node, `Construct` a line for it was the whole fix. What remains is genuinely about the node model — per-node data that is not a child, of which `Codomain` is the only instance the library has today. +*And narrower again, measured rather than argued.* **No written pattern can put a condition into the +graph at all.** Only 35 of the 324 rules have a right-hand side written as a pattern, and none of +them mentions `provided` — so a `Providedf` reaches an e-class only along the code-built path, where +a rule extracts a witness term, runs code on it and puts the result back. That is worth knowing +before anyone reopens this: the union that would need a meaning is not one e-matching can currently +form. `ProvidedInAnEClassTest.NoWrittenPatternIntroducesACondition` holds it at zero, so the first +two-sided conditional rule fails there rather than quietly making the question live again. + ## What is not decided here The one question above, restated as the decision it is: **how much should ride along on an e-node diff --git a/Sources/Tests/UnitTests/Core/Transformations/ProvidedInAnEClassTest.cs b/Sources/Tests/UnitTests/Core/Transformations/ProvidedInAnEClassTest.cs new file mode 100644 index 000000000..713cfb145 --- /dev/null +++ b/Sources/Tests/UnitTests/Core/Transformations/ProvidedInAnEClassTest.cs @@ -0,0 +1,125 @@ +// +// 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 an e-class does with a , which is the one question + /// Docs/Contributing/EqualitySaturationReviewFindings.md leaves open and the thing + /// standing between the rewrite graph and a production caller. + /// + [Trait("Area", "Core")] + public sealed class ProvidedInAnEClassTest + { + private static Entity? Saturate(string source, RewriteRuleGrowth ceiling) + { + var graph = new EGraph(); + var root = graph.AddEntity(source.ToEntity()); + var ledger = BudgetLedger.For(nameof(ProvidedInAnEClassTest), + new WorkBudget { Steps = 200_000, Time = TimeSpan.FromSeconds(20) }); + Saturation.Run(graph, Saturation.RulesUpTo(ceiling), ledger, + node => node.Complexity); + return graph.Extract(root, node => node.Complexity); + } + + /// + /// A condition is not a decoration on a value, and a union says it is. Two nodes + /// join an e-class when the graph is told they are equal. p and + /// p provided c are not equal — they differ exactly where c is false, + /// which is the only place the condition was written for — so a rule producing the second + /// from the first is asking the graph to record something untrue, and extraction may then + /// hand back either. + /// + [Fact] + public void AConditionedValueIsNotTheValue() + { + var bare = "1".ToEntity(); + var conditioned = "1 provided not x = 0".ToEntity(); + + Assert.NotEqual(bare, conditioned); + Assert.Equal("1", bare.Substitute("x", 0).Evaled.Stringize()); + Assert.Equal("NaN", conditioned.Substitute("x", 0).Evaled.Stringize()); + } + + /// + /// No condition can enter the graph through a written pattern. Which narrows the + /// open question considerably: a Providedf reaches an e-class only along the + /// code-built path, where a rule extracts a witness term, runs code on it and puts the + /// result back. + /// + /// + /// Only 35 of the 324 rules have a right-hand side written as a pattern at all, and none + /// of those mentions a condition — so the case + /// EqualitySaturationReviewFindings.md leaves open cannot arise from e-matching as + /// it stands. It arises from the other 289. Asserted at zero so that writing the first + /// two-sided conditional rule fails here rather than quietly making the question live. + /// + [Fact] + public void NoWrittenPatternIntroducesACondition() + { + var withCondition = Saturation.RulesUpTo(RewriteRuleGrowth.Unknown) + .Where(rule => rule.Right is not null + && rule.Right.ToString()!.Contains("provided")) + .ToList(); + + Assert.True(withCondition.Count == 0, + $"{withCondition.Count} two-sided rules now mention a condition — " + + "the e-class question is live for them, and what a union of `p` with " + + "`p provided c` is supposed to mean has to be decided before they fire: " + + string.Join(", ", withCondition.Select(r => r.Name))); + } + + /// + /// The safe ceiling is nearly inert on ordinary input. Four of these five come back + /// exactly as they went in; only the Pythagorean identity moves. That is not a defect in + /// the expressions — it is what the graph can do today with the rules it is allowed to + /// use, and it is the measurement + /// #746 tier 2 needs + /// before the graph is wired into anything. + /// + /// + /// SafeRules is RulesUpTo(Rearranges), 142 of 324 rules. The 152 sitting at + /// Unknown are excluded by design, since their growth was never judged — so the + /// ceiling that is safe to run finds little, and the ceiling that finds things admits + /// rewrites nobody measured. That trade is the open part of tier 2, and this pins where it + /// currently sits rather than describing it. + /// + [Fact] + public void TheSafeCeilingIsNearlyInertOnOrdinaryInput() + { + var moved = new List(); + var still = new List(); + foreach (var source in new[] + { + "(a + b) / (a * b)", "x / x", "(x + 1) / (x + 1)", + "sin(x) ^ 2 + cos(x) ^ 2", "(x + 1) * (x - 1)", + }) + { + var extracted = Saturate(source, RewriteRuleGrowth.Rearranges); + if (extracted is null || extracted == source.ToEntity()) + still.Add(source); + else + moved.Add($"{source} -> {extracted.Stringize()}"); + } + + Assert.True(still.Count == 4 && moved.Count == 1, + $"the safe ceiling moved {moved.Count} of 5 and left {still.Count}; it was 1 and 4.\n" + + "moved:\n" + string.Join("\n", moved) + + "\nunchanged:\n" + string.Join("\n", still)); + } + } +}