From 5e6d5f10bc48ed88b8f33979804f96c0b0babee2 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 8 Jan 2026 14:43:55 +0100 Subject: [PATCH 1/4] Avoid cost computation for rules in rule sets like simplify, concrete, simplify_prog etc. --- .../main/java/de/uka/ilkd/key/proof/Goal.java | 3 +- .../strategy/DelegatingRuleAppManager.java | 94 +++++++++++++++++++ 2 files changed, 96 insertions(+), 1 deletion(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index 94fa280399..cda36f1cf9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/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(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java new file mode 100644 index 0000000000..2277c70057 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java @@ -0,0 +1,94 @@ +/* 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 { + + private static String[] ruleSetNames = + { "alpha", "concrete", "simplify", "simplify_prog", "simplify_expression" }; + + private HashSet ruleSets = new HashSet<>(); + + private final RuleApplicationManager costBasedAppManager; + private ImmutableList queue; + private Goal goal; + private RuleApp nextApp; + + public DelegatingRuleAppManager(RuleApplicationManager 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 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().size() == 1 && + tapp.taclet().getRuleSets().exists(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 rule, PosInOccurrence pos) { + for (RuleApp ruleApp : rule) { + ruleAdded(ruleApp, pos); + } + } +} From ac4c463ecc46a81906f63518f828b85c6174c4c3 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 8 Jan 2026 15:17:20 +0100 Subject: [PATCH 2/4] Minor hack to play nice with two competing rules --- .../uka/ilkd/key/strategy/DelegatingRuleAppManager.java | 8 +++++--- .../resources/de/uka/ilkd/key/proof/rules/loopRules.key | 2 +- .../de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key | 1 + 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java index 2277c70057..4f11380922 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java @@ -19,7 +19,8 @@ public class DelegatingRuleAppManager implements RuleApplicationManager { private static String[] ruleSetNames = - { "alpha", "concrete", "simplify", "simplify_prog", "simplify_expression" }; + { "alpha", "concrete", "simplify", "simplify_prog", "simplify_prog_subset", + "simplify_expression" }; private HashSet ruleSets = new HashSet<>(); @@ -76,8 +77,9 @@ public void setGoal(Goal p_goal) { @Override public void ruleAdded(RuleApp rule, PosInOccurrence pos) { - if (rule instanceof NoPosTacletApp tapp && tapp.taclet().getRuleSets().size() == 1 && - tapp.taclet().getRuleSets().exists(rs -> ruleSets.contains(rs.name().toString()))) { + 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 { diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopRules.key index e68b443361..d838fbc8a2 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopRules.key +++ b/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 { diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key index 8141bd44ac..be5406e5a1 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key +++ b/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; From dc77649e5b844cb90f5f2ff16e9b945ed3a9b5ec Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 8 Jan 2026 15:28:39 +0100 Subject: [PATCH 3/4] a few more rulesets --- .../de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java index 4f11380922..93dd8f7101 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java @@ -20,7 +20,8 @@ public class DelegatingRuleAppManager implements RuleApplicationManager { private static String[] ruleSetNames = { "alpha", "concrete", "simplify", "simplify_prog", "simplify_prog_subset", - "simplify_expression" }; + "simplify_expression", "update_elim", "update_apply_on_update", "update_apply", + "update_join", "elimQuantifier" }; private HashSet ruleSets = new HashSet<>(); From 35eec36a8ec5ce90990b823fe60ebbf6f79f066c Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 8 Jan 2026 15:44:22 +0100 Subject: [PATCH 4/4] moved 'simplify' ruleset back to cost-based as some rules rely on becoming more expensive than others later on --- .../de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java index 93dd8f7101..1c844465c3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/DelegatingRuleAppManager.java @@ -19,9 +19,10 @@ public class DelegatingRuleAppManager implements RuleApplicationManager { private static String[] ruleSetNames = - { "alpha", "concrete", "simplify", "simplify_prog", "simplify_prog_subset", - "simplify_expression", "update_elim", "update_apply_on_update", "update_apply", - "update_join", "elimQuantifier" }; + { "alpha", "concrete", "simplify_prog", "simplify_prog_subset", + "simplify_expression", "simplify_literals", + "update_elim", "update_apply_on_update", "update_apply", "update_join", + "elimQuantifier" }; private HashSet ruleSets = new HashSet<>();