From ff102550fe9e8b04c9fbfe2d9272a3037ac157b3 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 15 Jun 2026 17:46:57 +0200 Subject: [PATCH] perf(checkPrefix): skip the prefix walk when the formula has no transformer RewriteTaclet.checkPrefix walks the whole 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^2) -- the dominant cost on deeply nested terms such as chained if-then-else (a JFR profile showed 54% self-time in checkPrefix on a trivial 3-node proof). 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/polarity/modality handling is guarded by a non-NONE restriction and the polarity is discarded. So if the formula provably contains no Transformer anywhere, no prefix can, and the walk can be skipped. "Formula contains a Transformer" is computed once and cached per term (JTerm.containsTransformerRecursive, mirroring containsJavaBlockRecursive), giving O(1) amortized and dropping the per-position prefix cost from O(depth) to O(1) in the transformer-free case; the O(d^2) 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. --- .../java/de/uka/ilkd/key/logic/JTerm.java | 10 +++++++++ .../java/de/uka/ilkd/key/logic/TermImpl.java | 22 +++++++++++++++++++ .../de/uka/ilkd/key/rule/RewriteTaclet.java | 8 +++++++ 3 files changed, 40 insertions(+) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java b/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java index dc84ea2b302..834f47ef7bb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java @@ -119,6 +119,16 @@ public interface JTerm */ boolean containsJavaBlockRecursive(); + /** + * Checks if this {@link JTerm} or one of its direct or indirect children has a + * {@link de.uka.ilkd.key.logic.op.Transformer} operator. Cached; used by + * {@link de.uka.ilkd.key.rule.RewriteTaclet#checkPrefix} to skip the prefix walk in the common + * transformer-free case. + * + * @return {@code true} iff a transformer occurs anywhere in the term tree + */ + boolean containsTransformerRecursive(); + /** * Returns a human-readable source of this term. For example the filename with line and offset. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java index 42063167176..505b7a872a5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java @@ -81,6 +81,9 @@ private enum ThreeValuedTruth { */ private ThreeValuedTruth containsJavaBlockRecursive = ThreeValuedTruth.UNKNOWN; + /** caches whether this term or a (direct/indirect) child has a {@link Transformer} operator. */ + private ThreeValuedTruth containsTransformerRecursive = ThreeValuedTruth.UNKNOWN; + // ------------------------------------------------------------------------- // constructors // ------------------------------------------------------------------------- @@ -441,5 +444,24 @@ public boolean containsJavaBlockRecursive() { return containsJavaBlockRecursive == ThreeValuedTruth.TRUE; } + @Override + public boolean containsTransformerRecursive() { + if (containsTransformerRecursive == ThreeValuedTruth.UNKNOWN) { + ThreeValuedTruth result = ThreeValuedTruth.FALSE; + if (op instanceof Transformer) { + result = ThreeValuedTruth.TRUE; + } else { + for (int i = 0, arity = subs.size(); i < arity; i++) { + if (subs.get(i).containsTransformerRecursive()) { + result = ThreeValuedTruth.TRUE; + break; + } + } + } + this.containsTransformerRecursive = result; + } + return containsTransformerRecursive == ThreeValuedTruth.TRUE; + } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java index 95de43b22f2..7d1cd26f955 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java @@ -37,6 +37,7 @@ * structure described by the term of the find-part. */ public class RewriteTaclet extends FindTaclet { + /** * creates a Schematic Theory Specific Rule (Taclet) with the given parameters that represents a * rewrite rule. @@ -108,6 +109,13 @@ private boolean veto(JTerm t) { public MatchConditions checkPrefix( PosInOccurrence p_pos, MatchConditions p_mc) { + // Fast path: for an unrestricted taclet the loop below only vetoes on a Transformer on the + // path; if the formula has none at all (cached), neither can the prefix, so the O(depth) + // walk is skipped. + if (applicationRestriction().equals(ApplicationRestriction.NONE) + && !((JTerm) p_pos.sequentFormula().formula()).containsTransformerRecursive()) { + return p_mc; + } int polarity = p_pos.isInAntec() ? -1 : 1; // init polarity SVInstantiations svi = p_mc.getInstantiations(); // this is assumed to hold