Performance (5/5): operator-indexed parking of assumes-incomplete rule-app bases

[unp1]

This PR is 5/5 of a performance series that prepares a clearer match → evaluate → apply pipeline before larger optimisations; it builds on the compiled matcher (1/5, #3831).

📖 Developer docs: Performance Optimizations (3.1)

Intended Change

Profiling the rule-app queue shows the dominant remaining churn comes from assumes-incomplete taclet bases that are re-popped and re-expanded every single round only to produce nothing: 96.8% of queue pops fail at an unmatched \assumes, and 97–99.6% of the resulting re-expansions yield no new instance. This PR stops re-expanding such bases until a formula they could actually match appears — an operator-indexed parking scheme.

Mechanism:

• A base whose \assumes formulas are effectively indexable (every assumes top operator is concrete, or a schema variable already bound by the find-match) is parked out of the active queue, indexed by those concrete top operator(s).
• On each round, exactly the parked bases whose operator matches a formula added or modified that round are woken and re-inserted — the same round their non-parked counterpart would first see that formula as "new" and re-expand to the instance. The wake set is computed from the changed formula's update-prefix spine (a sound superset, since the assumes matcher strips the update context before matching).
• Bases with an unbound-generic assumes top (which could match anything) are never parked; they behave exactly as today.

Because a woken base re-expands on the identical round with the identical age and cost, the result is byte-identical for the parking mechanism itself. All index structures are insertion-ordered (LinkedHashMap/LinkedHashSet) so no non-determinism is introduced.

This PR also drops the order-fragile lenOfSeqSubEQ heuristic from automode (the taclet stays defined, only its \heuristics is commented out). That taclet is redundant for completeness (the direct lenOfSeqSub suffices — full RAP closes all goals without it) but is order-fragile: it can dead-end a goal via a duplicate/cycle guard when its own result reproduces the equation it started from. The original rule order avoided this by luck; any reordering (including parking) can expose it. Removing it makes automode robust to rule-order changes.

flowchart LR
  A["assumes-incomplete base"] --> B{"indexable?"}
  B -- no --> C["re-expand each round"]
  B -- yes --> D["park; wake on matching op"]

Loading

Type of pull request

• New feature (queue optimization) + taclet rule-base change (drop lenOfSeqSubEQ heuristic)
• There are changes to the (Java) code and to the taclet rule base

Performance

Measured on the 6-problem perfTest set (median of 3 runs). Parking is not byte-identical (it can shift proof shapes — all still close), so the table reports both node counts and automode time.

Problem	main nodes	main (ms)	this PR nodes	this PR (ms)	speedup
symmArray	14601	21396	14512	15667	1.37×
gemplusDecimal/add	27083	11474	27740	9880	1.16×
ArrayList.remove.1	8016	3629	7993	2642	1.37×
SimplifiedLinkedList.remove	54444	28903	55300	18232	1.59×
Saddleback_search	31218	23510	33759	15785	1.49×
coincidence_count/project	12041	4935	11907	3113	1.59×
Total		93847		65319	1.44×

Node counts shift slightly (parking is not byte-identical — all proofs still close), confirming it is a queue-scheduling change rather than a different search.

Parking targets the wasted re-expansions of assumes-incomplete bases. Across the six problems:

Config	assumes-incomplete re-expansions	of which empty (no new match)
main	71.8 M	71.1 M (99.0%)
this PR	16.4 M	15.7 M (95.7%)

That is ~4.4× fewer; the remaining re-expansions are mostly non-indexable bases (unbound-generic \assumes tops) that parking deliberately leaves in the queue.

Ensuring quality

• Provability-safe on the full real RAP suite (681 goals) once the redundant order-fragile lenOfSeqSubEQ is dropped.
• Only effectively-indexable bases parked; over-waking is harmless (a spuriously woken base re-expands to nothing and re-parks); only missing a wake could diverge, and that cannot happen for an indexable base.
• compile + spotless + nullness clean.
• Active by default (the previous -Dkey.queue.parkAssumes gate is removed).

---

📖 Conceptual overview in the developer docs: Performance Optimizations (3.1)

Additional information and contact(s)

This PR has been done with AI tooling support.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.