Repository navigation
Distribute over a sum before searching by parts (#779) - #782
Conversation
sin(a+f*x)^4 * (5 - 6*sin(a+f*x)^2) did not finish in twenty seconds.
Written as the difference it is -- 5*sin(a+f*x)^4 - 6*sin(a+f*x)^6 -- it
answers in 156 ms, and each piece answers on its own in under 1 ms.
The rule that would have found those two pieces is SolveBySplittingSum, and
it ran last, behind integration by parts. So the search ran first and spent
the whole budget on an expression that linearity would have taken apart
immediately. The caller waited over twenty seconds to be told nothing.
Moving linearity in front of by parts cannot cost an answer: splitting
returns null unless *every* term integrates, so a sum that only comes out
whole still falls through to by parts below. That is what makes this a
reordering rather than a trade -- there is no input that by parts answers
and this now refuses.
Nor can it blow the tree up. The expansion is bounded by
MaxExpansionTermCount, which returns null rather than building the terms,
which is what the "this may expand to too many terms" note was guarding.
sin(a+f*x)^4 * (5 - 6*sin(a+f*x)^2) >20 s, no answer -> 1.4 s, answered
Every answer in the new test is checked by differentiating it back and
comparing at points, and the reported case is wrapped in a budget so that a
regression fails the run rather than hanging it.
A separate gap is pinned by the same file rather than fixed here: two powers
of one base in a product are never merged, so sin(x)^4 * (-6) * sin(x)^2 is
declined though it is -6*sin(x)^6, and x^2/x is declined though it is x.
Measured on master, so it is pre-existing; filed as #781.
5393 unit tests and 130 F# tests pass, suite duration unchanged at 3m53s;
casbench 113/117 with 0 wrong and 0 timeout, propcheck 0 failures,
rootcheck 596/596, simpsweep 10463/10463.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Verification re-run on this branch alone, rather than inferred from the branch I first measured on:
What I did not measure. #779 reports that Rubi family 4 times out on 372 of a 696-problem sample (53%), and notes that several of those are this shape but that the fraction was not measured. This PR does not quantify that either — I tried, and a single pass over family 4 runs 50–60 minutes because a case that hangs leaks its thread ( So: please do not read this PR as moving the 53%. What is measured is the reported integrand going from no answer in 20 s to an answer in 1.4 s, with no regression in any harness. Whether it moves family 4 as a whole is still open, and worth a run by anyone who wants the number. |
Closes #779.
The defect
Those are the same function. Each piece answers on its own in under a millisecond.
Cause
SolveBySplittingSumis the rule that would find those two pieces, and it ran last — behindSolveIntegratingByParts. So on a product with a sum inside it, the by-parts search ran first and spent the whole budget on an expression that linearity would have taken apart immediately. The caller waited over twenty seconds to be told nothing.Fix
Move linearity in front of by parts. One statement swapped.
It cannot cost an answer. Splitting returns
nullunless every term integrates:so a sum that only comes out whole still falls through to by parts below. There is no input that by parts answers and this now refuses — which is what makes it a reordering rather than a trade.
It cannot blow the tree up either. The expansion is bounded by
MaxExpansionTermCount, which returnsnullrather than building the terms — that is what the old// this may expand to too many termsnote was guarding, and the guard is inside the expansion, not in the ordering.Measured
sin(a+f*x)^4 * (5 - 6*sin(a+f*x)^2)Verification, on this branch:
Every answer in the new test is checked by differentiating it back and comparing at sample points, so what is asserted is that it is an antiderivative, not what form it is written in. The reported case is wrapped in a 15-second budget, so a regression fails the run instead of hanging it.
The test also covers the shapes most likely to be disturbed by the move —
x*(1+x),(x+1)*(x+2),cos(x)*(1+x),e^x*(1+x)— and asserts by parts is still reached, viax*cos(x),x*ln(x)andx^2*e^x.A separate gap, pinned rather than fixed
While measuring this I found that two powers of one base in a product are never merged:
sin(x)^4 * (-6) * sin(x)^2is declined though it is-6·sin(x)^6, andx^2/xis declined though it isx. Measured on master, so it is pre-existing and not caused by this change.It is filed as #781 and pinned here by
PowersOfOneBaseAreNotMerged, so that fixing it fails a test expecting the old behaviour rather than passing silently.🤖 Generated with Claude Code