Performance (3/5): skip the checkPrefix prefix-walk when no transformer is present

[unp1]

This PR is 3/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

RewriteTaclet.checkPrefix walks the entire root-to-position prefix (PIOPathIterator) at every position it is asked about. During taclet-index construction / one-step simplification of a deep term that is O(depth) per position over ~d positions — i.e. O(d²), the dominant cost on deeply nested terms such as chained if-then-else. A JFR profile on a trivial 3-node proof showed 54% self-time in checkPrefix.

Key observation: for an unrestricted (NONE) rewrite taclet — the common case — the only prefix-dependent outcome of that walk is a veto when a Transformer occurs on the path. The update-context / polarity / modality handling is all guarded by a non-NONE restriction, and the computed polarity is discarded. So if the formula provably contains no Transformer anywhere, no prefix can either, and the walk can be skipped entirely.

"Formula contains a Transformer" is computed once and cached per term (JTerm.containsTransformerRecursive, mirroring the existing containsJavaBlockRecursive). That makes the check O(1) amortized and drops the per-position prefix cost from O(depth) to O(1) in the transformer-free case; the O(d²) on deep terms becomes O(d).

Behaviour-preserving: it only short-circuits a provably-equivalent case. Restricted taclets and transformer-bearing formulas still take the full walk.

flowchart LR
  A["checkPrefix"] --> B{"no Transformer?"}
  B -- yes --> C["skip walk (O of 1)"]
  B -- no --> D["full walk (O of depth)"]

Loading

Type of pull request

• Refactoring (behaviour should not change — short-circuits a provably-equivalent case)
• There are changes to the (Java) code

Performance

Measured on the 6-problem perfTest set (median of 3 runs; byte-identical proofs, node counts unchanged). Plus a synthetic deep nested-if-then-else microbenchmark that isolates the O(d²)→O(d) effect.

Problem	main time (ms)	this PR (ms)	speedup
symmArray	21396	21358	1.00×
gemplusDecimal/add	11474	11150	1.03×
ArrayList.remove.1	3629	3556	1.02×
SimplifiedLinkedList.remove	28903	28634	1.01×
Saddleback_search	23510	23356	1.01×
coincidence_count/project	4935	4902	1.01×
Total	93847	92956	1.01×

Node counts identical to main (proofs unchanged). The effect on these six real-world problems is marginal (~1.01×) because their terms are shallow — checkPrefix is not their bottleneck. The change targets the O(d²) blow-up on deep terms: on a synthetic depth-400 nested if-then-else it is ~1407 ms → ~526 ms (≈2.7×). It is included because (a) it is essentially free and behaviour-preserving, and (b) deep-term proofs do occur in practice.

Ensuring quality

• Behaviour-preserving; full RAP closes the same goals with identical proofs.
• compile + spotless + nullness clean.
• Active by default (the previous -Dkey.incrementalPrefix gate is removed; fast path is unconditional).

---

📖 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.