Avoid cost computation for rules in rule sets like simplify, concrete, simplify_prog etc.

key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java

@@ -23,6 +23,7 @@
 import de.uka.ilkd.key.rule.TacletApp;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.rule.merge.MergeRule;
+import de.uka.ilkd.key.strategy.DelegatingRuleAppManager;
 import de.uka.ilkd.key.strategy.QueueRuleApplicationManager;
 import de.uka.ilkd.key.strategy.Strategy;
 import de.uka.ilkd.key.util.properties.MapProperties;
@@ -140,7 +141,7 @@ public Goal(Node node, TacletIndex tacletIndex, BuiltInRuleAppIndex builtInRuleA
         this.goalStrategy = null;
         this.strategyInfos = new MapProperties();
         this.tagManager = new FormulaTagManager(this);
-        setRuleAppManager(new QueueRuleApplicationManager());
+        setRuleAppManager(new DelegatingRuleAppManager(new QueueRuleApplicationManager()));
         this.localNamespaces =
             node.proof().getServices().getNamespaces().copyWithParent().copyWithParent();
     }

key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java

@@ -0,0 +1,98 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.strategy;
+
+import java.util.Arrays;
+import java.util.HashSet;
+
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.rule.NoPosTacletApp;
+
+import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.strategy.RuleApplicationManager;
+import org.key_project.prover.strategy.costbased.NumberRuleAppCost;
+import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSLList;
+
+public class DelegatingRuleAppManager implements RuleApplicationManager<Goal> {
+
+    private static String[] ruleSetNames =
+        { "alpha", "concrete", "simplify_prog", "simplify_prog_subset",
+            "simplify_expression", "simplify_literals",
+            "update_elim", "update_apply_on_update", "update_apply", "update_join",
+            "elimQuantifier" };
+
+    private HashSet<String> ruleSets = new HashSet<>();
+
+    private final RuleApplicationManager<Goal> costBasedAppManager;
+    private ImmutableList<RuleAppContainer> queue;
+    private Goal goal;
+    private RuleApp nextApp;
+
+    public DelegatingRuleAppManager(RuleApplicationManager<Goal> costRuleAppMgr) {
+        this.costBasedAppManager = costRuleAppMgr;
+        queue = ImmutableSLList.nil();
+        ruleSets.addAll(Arrays.asList(ruleSetNames));
+    }
+
+    @Override
+    public void clearCache() {
+        costBasedAppManager.clearCache();
+    }
+
+    @Override
+    public RuleApp peekNext() {
+        RuleApp next = nextApp;
+        if (next == null && !queue.isEmpty()) {
+            var myQueue = queue;
+            while (next == null && !myQueue.isEmpty()) {
+                next = myQueue.head().completeRuleApp(goal);
+                myQueue = myQueue.tail();
+            }
+            queue = myQueue;
+        }
+        nextApp = next == null ? costBasedAppManager.peekNext() : next;
+        return nextApp;
+    }
+
+    @Override
+    public RuleApp next() {
+        final RuleApp next = peekNext();
+        nextApp = null;
+        return next;
+    }
+
+    @Override
+    public RuleApplicationManager<Goal> copy() {
+        DelegatingRuleAppManager copy = new DelegatingRuleAppManager(costBasedAppManager.copy());
+        copy.queue = queue;
+        return copy;
+    }
+
+    @Override
+    public void setGoal(Goal p_goal) {
+        this.goal = p_goal;
+        costBasedAppManager.setGoal(p_goal);
+    }
+
+    @Override
+    public void ruleAdded(RuleApp rule, PosInOccurrence pos) {
+        if (rule instanceof NoPosTacletApp tapp &&
+                tapp.taclet().getRuleSets().stream()
+                        .allMatch(rs -> ruleSets.contains(rs.name().toString()))) {
+            queue = queue.prepend(new FindTacletAppContainer(tapp, pos,
+                NumberRuleAppCost.getZeroCost(), goal, goal.getTime()));
+        } else {
+            costBasedAppManager.ruleAdded(rule, pos);
+        }
+    }
+
+    @Override
+    public void rulesAdded(ImmutableList<? extends RuleApp> rule, PosInOccurrence pos) {
+        for (RuleApp ruleApp : rule) {
+            ruleAdded(ruleApp, pos);
+        }
+    }
+}

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopRules.key

@@ -49,7 +49,7 @@
         \find(\modality{#allmodal}{.. #forloop ...}\endmodality (post))
         \varcond(\newLabel(#innerLabel), \newLabel(#outerLabel))
         \replacewith(\modality{#allmodal}{.. #for-to-while(#innerLabel, #outerLabel, #forloop) ...}\endmodality (post))
-        \heuristics(simplify_prog)
+        \heuristics(simplify_prog, loop_rewrite)
     };
 
     arrayInitialisation {

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key

@@ -54,6 +54,7 @@
     loop_expand;
     loop_scope_inv_taclet;
     loop_scope_expand;
+    loop_rewrite;
 
     javaIntegerSemantics;
     executeIntegerAssignment;