diff --git a/Sources/AngouriMath/Core/Transformations/Saturation.cs b/Sources/AngouriMath/Core/Transformations/Saturation.cs index 130ad9657..9f20e526f 100644 --- a/Sources/AngouriMath/Core/Transformations/Saturation.cs +++ b/Sources/AngouriMath/Core/Transformations/Saturation.cs @@ -109,8 +109,18 @@ private static readonly Lazy> safeRules /// witness, never the answer: what the caller finally extracts is the caller's own /// business, and is where a cheapest-form and a canonical-form caller differ. /// + /// + /// A caller's own stop, asked after every pass that merged something; + /// ends the run without the graph's fixed point having been reached. A caller that + /// extracts an answer passes "the extraction has not changed for two passes": that is + /// the fixed point which matters to it, and it comes where the graph's own may never — + /// on a rational coefficient beside a variable, the regrouping rules add a fresh e-node + /// to the root's class on every pass while its cheapest member stopped changing on the + /// third (#1200). + /// passes nothing: it needs a union, not an extraction. + /// internal static bool Run(EGraph graph, IReadOnlyList rules, - BudgetLedger ledger, Func witnessCost) + BudgetLedger ledger, Func witnessCost, Func? settled = null) { var chargedNodes = graph.NodeCount; bool ChargeGrowthSinceLastCall() @@ -220,6 +230,7 @@ bool TryTerm(out Entity value) if (!ledger.Spend()) break; graph.Rebuild(); if (!merged) saturated = true; + else if (settled is not null && settled()) break; } return saturated; } diff --git a/Sources/AngouriMath/Core/Transformations/Transformation.Catalogue.cs b/Sources/AngouriMath/Core/Transformations/Transformation.Catalogue.cs index 81fc2fc01..af6c1d136 100644 --- a/Sources/AngouriMath/Core/Transformations/Transformation.Catalogue.cs +++ b/Sources/AngouriMath/Core/Transformations/Transformation.Catalogue.cs @@ -470,10 +470,17 @@ public static Transformation EqualitySaturation(WorkBudget budget, CostModel cos /// What this is not. Not a canonical form for the language — no such thing /// exists here, since zero-equivalence is undecidable, and /// Docs/Contributing/CanonicalForm.md states that boundary. It is a canonical form - /// modulo these rules and this budget: equal trees mean the rules proved the two - /// expressions equal, different trees mean they did not, and a budget that ran out is - /// reported rather than hidden. Nothing in the library calls this — like - /// it is offered, not applied. + /// modulo these rules, this budget, and the answer having settled: equal trees mean + /// the rules proved the two expressions equal, different trees mean they did not, and a + /// budget that ran out is reported rather than hidden. The run stops once the least + /// member of the input's class has survived two passes unchanged, which is the fixed + /// point that matters to an extraction and comes where the graph's own may never — on + /// a rational coefficient beside a variable the regrouping rules add a member on every + /// pass for as long as they are allowed (#1200), + /// and the answer was settled on the third. Measured on the corpus and on those inputs, + /// no answer moved and the nine of them went from two seconds to milliseconds. Nothing + /// in the library calls this — like it is offered, not + /// applied. /// /// /// @@ -673,10 +680,31 @@ internal EqualitySaturationTransformation(WorkBudget budget, CostModel costModel graph.Rebuild(); var ledger = BudgetLedger.For(Name, budget); - Saturation.Run(graph, SafeRules, ledger, costModel.Cost); + // Stop once the answer has: after two passes in which the cheapest member of the + // root's class did not change, further merging can only add members this + // extraction would not choose. That is the fixed point a caller who extracts + // cares about, and on #1200's inputs it comes on the third pass where the + // graph's own never does. Measured on the corpus, no answer moves. + Entity? last = null; + var unchanged = 0; + bool Settled() + { + var now = graph.Extract(root, costModel.Cost); + unchanged = now is not null && now.Equals(last) ? unchanged + 1 : 0; + last = now; + return unchanged >= SettledPasses; + } + Saturation.Run(graph, SafeRules, ledger, costModel.Cost, Settled); ledger.Report(); return graph.Extract(root, costModel.Cost) ?? input; } + + /// + /// How many consecutive passes the extracted answer must survive unchanged before + /// the run stops on the answer rather than on the graph. Two, not one: a pass can + /// leave the cheapest member alone while adding what the next pass will improve on. + /// + private const int SettledPasses = 2; } /// @@ -711,7 +739,18 @@ internal GraphCanonicalizationTransformation(WorkBudget budget, RewriteRuleGrowt graph.Rebuild(); var ledger = BudgetLedger.For(Name, budget); - Saturation.Run(graph, rules, ledger, CostModel.Default.Cost); + // The same stop as EqualitySaturationTransformation's, on the least member + // rather than the cheapest, since that is what this extracts. + Entity? last = null; + var unchanged = 0; + bool Settled() + { + var now = graph.ExtractLeast(root, EntityOrder.Canonical); + unchanged = now is not null && now.Equals(last) ? unchanged + 1 : 0; + last = now; + return unchanged >= 2; + } + Saturation.Run(graph, rules, ledger, CostModel.Default.Cost, Settled); ledger.Report(); // The least member, not the cheapest: a cost model ties, and a tie would make the