Repository navigation
A cost model reaches an API, not only an ambient setting - #1102
Merged
Merged
Conversation
#746 tier 2's own row names this remaining, in its own words: "a cost model that reaches an API rather than an ambient setting". Checked against the actual API surface rather than assumed: `Entity.Simplify(int level = 2)` has no overload taking a `CostModel`, and the only way to change what candidate `Simplify` prefers is `MathS.Settings.ComplexityCriteria.Set(...)` around the call. That setting was already safe to use -- `Setting<T>` is async-local, not thread-static, so one caller's override cannot leak into another's concurrent call, the same design `MathS.Settings.Budget` and `BudgetLedger.For` already share -- but it is not a place in the addressable API `Transformation` is, which is what tier 2's own wording asks for. `Transformation.SimplificationAtLevel(int level, CostModel costModel)` is that place. It does not thread an explicit cost parameter through `Simplificator` -- that would be a second candidate-search pipeline to keep in step with the one `Entity.Simplify(int)` actually runs, which is exactly the risk the existing pipeline was written once to avoid. It scopes the existing, already-tested `ComplexityCriteria` setting for the duration of this one call instead, so `Simplify`'s own behaviour is the thing being configured rather than a parallel implementation of it. `CostModel.Default` given explicitly behaves identically to the overload without one, and passing it is how a caller states that on purpose. TDD: a spy `CostModel` proves the given model is the one actually consulted (not the ambient default); a before/after check on `MathS.Settings.ComplexityCriteria.IsOverriden` proves the scope does not leak past the call; and `CostModel.Default` given explicitly is checked against the plain overload to prove it changes nothing when the caller asks for what was already happening. `PublicApi.txt` regenerated for the one new public member. Full suite: 8797 tests, 8783 passed, 14 skipped (pre-existing), 0 failed.
This was referenced Aug 29, 2026
Open
Member
Author
|
A code review flagged one finding against this PR specifically: Recorded rather than fixed here, alongside thirteen other findings from the same review pass (mostly against #1101): (Edited to repoint the link: #1101 has since merged, so the document is on |
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 29, 2026
…agnosed The review pass on #1101/#1102 recorded thirteen findings it did not fix. Four of them were independent of the open design question about e-node metadata, so they go first. `Extract` declines a candidate its cost model cannot rank. `here >= bestCost` is false whenever either side is NaN, so a NaN cost became the incumbent cheapest and every candidate after it then won unconditionally -- the answer stopped being the cheapest and became whichever member the enumeration reached last. A cost model that throws is already declined by the surrounding catch; one that answers NaN is saying the same thing. `Extract` settles a cost tie on a defined order. HashSet enumeration order is unspecified and string hashing is randomised per process, so one run's tie-break was not the next run's. ENode gains a total order -- ordinal on the operator, then children. `Extract` declines to build past a depth of 256. Its cycle guard bounds the chain only by the number of distinct classes, which unions grow past the input's own syntactic depth, and a StackOverflowException cannot be caught. Same shape as Gruntz.MaxDepth. `WorkBudget.Steps` now bounds something. This is the one the review got wrong: it was recorded as a timing defect -- the growth charge landing after a sweep rather than before the next one. Measuring it found the timing is not the problem. Steps charged the e-graph's node-count growth, and SafeRules is by construction the rules whose Growth does not expand, so on ordinary input the ledger was charged nothing whatever: under Steps = 0, three of five varied expressions ran the entire sweep to saturation and reported that they had completed, never having reached a ceiling. Time was the only bound really holding. A step is now one unit of work attempted, charged before the attempt, as Buchberger, FGLM and MatchPattern all charge; the growth charge stays alongside it and moves after the sweep; and Rebuild's full-graph rescan is charged for the first time. The findings document is updated to match, including the correction to its own account of the budget finding -- the wrong diagnosis was the more flattering one, since a bound that is slightly late reads as a rounding error where a bound that never fires is the feature missing. Full suite: 8885 passed, 14 skipped (pre-existing), 0 failed.
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 30, 2026
* Close four of the recorded e-graph review findings, one of them misdiagnosed The review pass on #1101/#1102 recorded thirteen findings it did not fix. Four of them were independent of the open design question about e-node metadata, so they go first. `Extract` declines a candidate its cost model cannot rank. `here >= bestCost` is false whenever either side is NaN, so a NaN cost became the incumbent cheapest and every candidate after it then won unconditionally -- the answer stopped being the cheapest and became whichever member the enumeration reached last. A cost model that throws is already declined by the surrounding catch; one that answers NaN is saying the same thing. `Extract` settles a cost tie on a defined order. HashSet enumeration order is unspecified and string hashing is randomised per process, so one run's tie-break was not the next run's. ENode gains a total order -- ordinal on the operator, then children. `Extract` declines to build past a depth of 256. Its cycle guard bounds the chain only by the number of distinct classes, which unions grow past the input's own syntactic depth, and a StackOverflowException cannot be caught. Same shape as Gruntz.MaxDepth. `WorkBudget.Steps` now bounds something. This is the one the review got wrong: it was recorded as a timing defect -- the growth charge landing after a sweep rather than before the next one. Measuring it found the timing is not the problem. Steps charged the e-graph's node-count growth, and SafeRules is by construction the rules whose Growth does not expand, so on ordinary input the ledger was charged nothing whatever: under Steps = 0, three of five varied expressions ran the entire sweep to saturation and reported that they had completed, never having reached a ceiling. Time was the only bound really holding. A step is now one unit of work attempted, charged before the attempt, as Buchberger, FGLM and MatchPattern all charge; the growth charge stays alongside it and moves after the sweep; and Rebuild's full-graph rescan is charged for the first time. The findings document is updated to match, including the correction to its own account of the budget finding -- the wrong diagnosis was the more flattering one, since a bound that is slightly late reads as a rounding error where a bound that never fires is the feature missing. Full suite: 8885 passed, 14 skipped (pre-existing), 0 failed. * One table of buildable node types, and it is three times longer Three more of the recorded findings, all with one cause: the fourteen node types `MatchPattern.Construct` built were what it had accumulated, not a boundary anyone chose. `EGraph` kept a second copy of that list to resolve an e-node's operator back to a type, next to a doc comment on `Construct` warning that a list written twice is a list that drifts. Now one table holds the type, its arity and the constructor call together, and `BuildableNodeTypes`, the name lookup and `CanConstruct` are all derived from its keys -- there is no second list left to drift from. A table rather than a chain of `nodeType == typeof(T)` tests also makes it O(1) rather than linear in the list, which matters more now. `Extract` silently no-opped on any root outside the list, and a rule wrapping a conditional result in `Providedf` -- the registry's own convention -- had that result unioned onto a class nothing could build. Both were the same gap. The table now holds 44 types: every node type whose constructor takes one or two Entity children, less two binders. Comparisons, connectives, the inverse trigonometric functions, floor/ceil/round, mod, gcd, min/max, the set operations and Providedf all rebuild now, where before an expression rooted at any of them came back unchanged reporting `Changed = false` -- indistinguishable from being already at its cheapest. What stays out is now a statement rather than an accident. Binders, because the e-graph has no notion of a bound variable's scope and DirectChildren hands out a capture-avoidingly renamed body, so rebuilding one would produce a term meaning something else. Variable-arity nodes, because the table keys on an arity of one or two. Six rules gain a reverse direction as a consequence -- the four inverse-trigonometric round trips and the two set idempotences, whose left-hand pattern named a type that could not be built. Each reversed rule is Expands, so none joins SafeRules and saturation is unchanged. Two tests that used Modf as their example of an unbuildable node now use Integralf, which is unbuildable for a reason that will not change: it carries an optional range beside its two children. Full suite: 8906 passed, 14 skipped (pre-existing), 0 failed. * The last four recorded findings, and none of them needed the open design question `RewriteRecording` could not see `EqualitySaturation` at all: it is populated inside `RewriteRuleSet.ApplyOnce`, and saturation asks rules directly, so a caller who opened a recording got a real rewrite with an empty derivation and nothing to distinguish "introspection cannot see this" from "there was nothing to see". Now the pass is noted -- one edge, input to output, under the transformation's own name. Deliberately not finer than the pass. A rule set records each firing because a firing there is the rewrite: the node it matched leaves and the replacement takes its place. A firing in saturation adds another member to an e-class whose members are all already believed equal, and the answer is then chosen by Extract from all of them at once. Most firings contribute nothing to what extraction picked, and none is a step on a route from input to output, because there is no route. Reporting them as RewriteSteps would name rewrites that are not in the answer. `MatchPattern.RequiredRootType` was already there and never consulted, so every rule ran a full pattern match against every class of every pass. A pattern requiring a root type cannot match a class holding no node of it, and being a necessary condition is what makes it a filter: it licenses skipping a rule, never firing one. Gathering each class's types once per sweep and consulting them cuts match attempts about thirteenfold -- 1076 steps to 78 on the largest of four expressions, 87 to 3 on `x + 0` -- with the same answer in every case. `NeutralClass` hand-rolled an identity table that InnerSimplify already implements and tests, with nothing keeping the two in step; the divergence would have been silent in the worst direction, the e-graph merging two classes the rest of the library no longer believes equal. It is derived now, by asking InnerSimplified whether `op(x, leaf)` really is `x`. That settles the asymmetries without anyone having to remember them -- `0 - x` is a negation, `1 / x` a reciprocal, `1 ^ x` the constant 1 -- and handles what a written table cannot: an arm answering with a condition attached does not answer with the bare operand, so no fold is claimed. `Entity.SimplifiedRate` answered one cost model's question with another's cached number: the cache is one slot per instance and the criteria is ambient, so the two do not agree about what the cached number is a rate of. Not merely stale -- `Simplificator.PickSimplest` compares candidates by this property, so it weighed one model's cached rate against another's fresh one and chose on the strength of it. Cached now only while nobody has scoped the setting, which is the `IsOverriden` test `BudgetLedger.For` already applies to the budget, and one ambient read rather than a read plus a delegate comparison on a hot path. Fourteen of the fifteen findings are now closed. What remains is a design question rather than a defect -- how much should ride along on an e-node beyond its bare shape -- and the notable thing is how little of the cluster actually depended on it: one finding, Codomain. The Providedf case this document had offered as evidence for it was the buildable-type table and nothing deeper. Full suite: 8919 passed, 14 skipped (pre-existing), 0 failed. * Drop a documented workaround for the rate cache, now that the cache is fixed MathS.Settings.ComplexityCriteria's own example read its rate through FromString(expr, useCache: false), to keep the parser from handing back an instance whose SimplifiedRate had already been computed under the default criteria. That was a workaround for the bug the previous commit fixed, and a doc teaching a workaround for a bug that is gone is worse than no doc. Measured both ways before changing it: with the cache left on, the example prints the same 24 / 24 / 2 / 1 it prints with it defeated. * Pay no allocation for the pre-filter, and say what it can miss Two corrections to the root-type filter added a commit ago. `held.Any(type => required.IsAssignableFrom(type))` captures `required`, so it allocated a closure every time the exact-type test missed -- which is most rules of most classes, since the filter's whole job is to miss. Paying an allocation to avoid a pattern match is not a pre-filter. Written as a loop instead. And the set is gathered before the class's sweep, so a union later in that same sweep can add a type it does not have, and a rule can be skipped in the pass where it had just become applicable. That costs nothing and is worth saying rather than leaving a reader to work out: a union is exactly what sets `merged`, so there is another pass, and the set is gathered again there. Full suite: 8919 passed, 14 skipped (pre-existing), 0 failed.
Rafael-SOWNet
added a commit
that referenced
this pull request
Sep 10, 2026
…cause there has been a rule for one since #1102 `1/(1 + x^6)` had no antiderivative. The library factors `x^6 + 1` into `(x^2 + 1)(x^4 - x^2 + 1)` -- correctly, `Factorize` returns exactly that -- and integrates each of those on its own. Only the split was missing. The coprime splitter reads the factorisation and refuses to produce a decomposition whose pieces no rule can integrate, which is the right shape for a guard and is what keeps declining cheap. What it said was: A linear factor is read at any multiplicity, and a quadratic one only at the first: there is no rule for a numerator over (x^2 + c)^k, and none for an irreducible factor of degree three or more at all. The last clause stopped being true when TrySplitBiquadraticOverTheReals arrived: it factors `x^4 + p x^2 + q` into two real quadratics, which is why `1/(x^4 - x^2 + 1)` is answered on its own. The guard was a claim about the rule set written as a condition in a loop, and it went stale the way such a claim does. It is a named method now, one line per shape saying which rule reads it, so that the next rule added has somewhere obvious to be recorded. Widened by exactly one shape: a biquadratic quartic at multiplicity one. Only the even-powered form -- that rule reads `x^4 + p x^2 + q` and nothing else, and a general quartic still has none. Newly answered, each verified by differentiating back at five points: 1/(1 + x^6) x^2/(1 + x^6) 1/(x*(1 + x^6)) And `(1 - x^4)/(1 + x^4 + x^8)`, which is the integrand the guard's own comment cites as the reason it exists. It declined in 203ms and now answers in about 4s. That is the trade this makes, and it is the one the guard was always meant to allow once a rule existed: the comment's objection was to searching for an answer that was not there, not to spending time on one that is. `DecliningStaysCheap` moves to `(1 - x^4)/((1 + x^2)*(x^4 + x + 1))`, whose quartic has an odd power in it and so still reaches the guard -- 80ms to decline. The guard is real and still needs a case that exercises it. Still declined, and each for its own reason: `x^6 + 2` is irreducible over the rationals so there is nothing to split; `x^12 + 1` is `(x^4 + 1)(x^8 - x^4 + 1)` and the degree-8 factor has no rule; `x^5 + 1` leaves a general quartic, which is not biquadratic. Suites: UnitTests 8514 and 1543, FSharpWrapperUnitTests 134, InteractiveWrapperUnitTests 18, TerminalUnitTests 41. Measured on Rubi's independent test suites, both arms on this machine: before (2dbeedf) 913/1774, 0 wrong, 13 timeouts, 722s after 914/1774, 0 wrong, 13 timeouts, 730s Read as a list rather than a number, three verdicts moved. Two are answers that were not there: `1/(-1 + x^8)`, which used to spend the budget, and `(1 + x^4)/(1 + x^6)`. The third is `tanh(x)^5/sech(x)^4`, which measures 31.5s on master and 31.0s here against a 5s budget and is graded differently from run to run -- the answer cache is process-wide and the harness restarts its worker after a timeout, so a case that far past the budget depends on what ran before it. #718 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Rafael-SOWNet
added a commit
that referenced
this pull request
Sep 10, 2026
…cause there has been a rule for one since #1102 (#1254) `1/(1 + x^6)` had no antiderivative. The library factors `x^6 + 1` into `(x^2 + 1)(x^4 - x^2 + 1)` -- correctly, `Factorize` returns exactly that -- and integrates each of those on its own. Only the split was missing. The coprime splitter reads the factorisation and refuses to produce a decomposition whose pieces no rule can integrate, which is the right shape for a guard and is what keeps declining cheap. What it said was: A linear factor is read at any multiplicity, and a quadratic one only at the first: there is no rule for a numerator over (x^2 + c)^k, and none for an irreducible factor of degree three or more at all. The last clause stopped being true when TrySplitBiquadraticOverTheReals arrived: it factors `x^4 + p x^2 + q` into two real quadratics, which is why `1/(x^4 - x^2 + 1)` is answered on its own. The guard was a claim about the rule set written as a condition in a loop, and it went stale the way such a claim does. It is a named method now, one line per shape saying which rule reads it, so that the next rule added has somewhere obvious to be recorded. Widened by exactly one shape: a biquadratic quartic at multiplicity one. Only the even-powered form -- that rule reads `x^4 + p x^2 + q` and nothing else, and a general quartic still has none. Newly answered, each verified by differentiating back at five points: 1/(1 + x^6) x^2/(1 + x^6) 1/(x*(1 + x^6)) And `(1 - x^4)/(1 + x^4 + x^8)`, which is the integrand the guard's own comment cites as the reason it exists. It declined in 203ms and now answers in about 4s. That is the trade this makes, and it is the one the guard was always meant to allow once a rule existed: the comment's objection was to searching for an answer that was not there, not to spending time on one that is. `DecliningStaysCheap` moves to `(1 - x^4)/((1 + x^2)*(x^4 + x + 1))`, whose quartic has an odd power in it and so still reaches the guard -- 80ms to decline. The guard is real and still needs a case that exercises it. Still declined, and each for its own reason: `x^6 + 2` is irreducible over the rationals so there is nothing to split; `x^12 + 1` is `(x^4 + 1)(x^8 - x^4 + 1)` and the degree-8 factor has no rule; `x^5 + 1` leaves a general quartic, which is not biquadratic. Suites: UnitTests 8514 and 1543, FSharpWrapperUnitTests 134, InteractiveWrapperUnitTests 18, TerminalUnitTests 41. Measured on Rubi's independent test suites, both arms on this machine: before (2dbeedf) 913/1774, 0 wrong, 13 timeouts, 722s after 914/1774, 0 wrong, 13 timeouts, 730s Read as a list rather than a number, three verdicts moved. Two are answers that were not there: `1/(-1 + x^8)`, which used to spend the budget, and `(1 + x^4)/(1 + x^6)`. The third is `tanh(x)^5/sech(x)^4`, which measures 31.5s on master and 31.0s here against a 5s budget and is graded differently from run to run -- the answer cache is process-wide and the harness restarts its worker after a timeout, so a case that far past the budget depends on what ran before it. #718 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
#746 tier 2's own row names this remaining, in its own words: "a cost model that reaches an API rather than an ambient setting." Verified against the actual surface rather than assumed —
Entity.Simplify(int level = 2)has noCostModeloverload, and the only existing way to change whatSimplifyprefers isMathS.Settings.ComplexityCriteria.Set(...)around the call.Transformation.SimplificationAtLevel(int level, CostModel costModel)— the new, addressable place. It does not thread an explicit cost parameter throughSimplificator(a second candidate-search pipeline to keep in step with the oneSimplifyactually runs); it scopes the existing, already-testedMathS.Settings.ComplexityCriteriasetting for the duration of one call.CostModel.Defaultgiven explicitly behaves identically to the overload without one — passing it is how a caller states that on purpose.Independent of #1101 — this doesn't touch the e-graph work at all, so it's cut from
masterdirectly rather than stacked.Test plan
CostModelproves the given model is the one actually consulted, not the ambient default.MathS.Settings.ComplexityCriteria.IsOverridenis checked false before and after the call, proving the scope doesn't leak.CostModel.Defaultgiven explicitly is checked against the plainSimplificationAtLevel(level)overload — identical output.PublicApi.txtregenerated for the one new public member — diff is exactly that one line.🤖 Generated with Claude Code