Saturation.Run takes a WorkBudget with a Time and can overshoot it by an order of magnitude.
Measured
Safe ceiling (RulesUpTo(Rearranges)), WorkBudget { Steps = 20_000, Time = 2 s }, one input per
graph, over the growth corpus of RuleGrowthAgreesWithTheCorpusTest (3,630 generated shapes):
| input |
build |
wall |
1/2 * 2 * (1/2) ^ 2 |
d9b8b374 (before #1198) |
69.2 s against a 2 s budget |
(2 - 0) * 1/2 * -1/2 |
d9b8b374 |
7.3 s |
x / x * x * 1/2 |
98a9420c (after #1198) |
4.4 s |
2 ^ (-1) / sqrt(1/2) |
98a9420c |
stopped by the step ceiling at 0.8 s, 1,072 e-nodes — the budget worked there |
After #1198 folded constants on insertion the 60-second cases are gone, but the 2× overshoot on a
7-node input remains, so it is not the constant runaway that caused it.
What it probably is, unverified
BudgetLedger's remarks say the bound is cooperative and checked once per branch. In
Saturation.Run the check is per class and per rule inside a pass; one rule attempt on one class
extracts a witness term for every member and runs TryApply on each, and on a class with a few
hundred members that single attempt is where the seconds go. If so the fix is to consult the
ledger inside the witness loop (or to charge witness extraction as steps), not to tighten the
clock. This has not been instrumented; the numbers above are the whole of what is known.
Why it matters
A budget that can be overshot 35× is not a bound, and the graph is offered to callers behind
Transformation.CanonicalizationOverGraph(budget) on the strength of being bounded. Nothing
wrong is answered — extraction was correct on every case above — so this is filed as minor.
Found while measuring #746 tier 2 item 4 (PR #1198).
Saturation.Runtakes aWorkBudgetwith aTimeand can overshoot it by an order of magnitude.Measured
Safe ceiling (
RulesUpTo(Rearranges)),WorkBudget { Steps = 20_000, Time = 2 s }, one input pergraph, over the growth corpus of
RuleGrowthAgreesWithTheCorpusTest(3,630 generated shapes):1/2 * 2 * (1/2) ^ 2d9b8b374(before #1198)(2 - 0) * 1/2 * -1/2d9b8b374x / x * x * 1/298a9420c(after #1198)2 ^ (-1) / sqrt(1/2)98a9420cAfter #1198 folded constants on insertion the 60-second cases are gone, but the 2× overshoot on a
7-node input remains, so it is not the constant runaway that caused it.
What it probably is, unverified
BudgetLedger's remarks say the bound is cooperative and checked once per branch. InSaturation.Runthe check is per class and per rule inside a pass; one rule attempt on one classextracts a witness term for every member and runs
TryApplyon each, and on a class with a fewhundred members that single attempt is where the seconds go. If so the fix is to consult the
ledger inside the witness loop (or to charge witness extraction as steps), not to tighten the
clock. This has not been instrumented; the numbers above are the whole of what is known.
Why it matters
A budget that can be overshot 35× is not a bound, and the graph is offered to callers behind
Transformation.CanonicalizationOverGraph(budget)on the strength of being bounded. Nothingwrong is answered — extraction was correct on every case above — so this is filed as minor.
Found while measuring #746 tier 2 item 4 (PR #1198).