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

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.
      */

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;
+    }
+
 
 }

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