Moved up some features and slightly generalized others

unp1 · unp1 · commit 087b1c749a78 · 2026-02-12T16:53:59.000+01:00
diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionStrategy.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionStrategy.java
@@ -15,7 +15,6 @@
 import de.uka.ilkd.key.strategy.definition.OneOfStrategyPropertyDefinition;
 import de.uka.ilkd.key.strategy.definition.StrategyPropertyValueDefinition;
 import de.uka.ilkd.key.strategy.definition.StrategySettingsDefinition;
-import de.uka.ilkd.key.strategy.feature.*;
 import de.uka.ilkd.key.strategy.feature.instantiator.OneOfCP;
 import de.uka.ilkd.key.strategy.termProjection.FocusProjection;
 import de.uka.ilkd.key.symbolic_execution.rule.ModalitySideProofRule;
@@ -33,6 +32,7 @@
 import org.key_project.prover.strategy.costbased.TopRuleAppCost;
 import org.key_project.prover.strategy.costbased.feature.BinaryFeature;
 import org.key_project.prover.strategy.costbased.feature.ConditionalFeature;
+import org.key_project.prover.strategy.costbased.feature.CountBranchFeature;
 import org.key_project.prover.strategy.costbased.feature.Feature;
 import org.key_project.prover.strategy.costbased.feature.RuleSetDispatchFeature;
 import org.key_project.prover.strategy.costbased.feature.ScaleFeature;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java
@@ -440,11 +440,11 @@ public TacletApp addCheckedInstantiation(SchemaVariable sv, JTerm term, Services
      *
      * @return ImmutableSet<SchemaVariable> with SchemaVariables that have not been instantiated yet
      */
+    @Override
     public @NonNull ImmutableSet<SchemaVariable> uninstantiatedVars() {
         return calculateNonInstantiatedSV();
     }
 
-
     /**
      * returns true if the given {@link SchemaVariable} must be explicitly instantiated it does not
      * check whether sv is already instantiated or not
@@ -957,6 +957,7 @@ public PosTacletApp setPosInOccurrence(PosInOccurrence pos,
     /**
      * @return true iff the if-instantiation list is not null or no if sequent is needed
      */
+    @Override
     public boolean assumesInstantionsComplete() {
         return assumesFormulaInstantiations != null || taclet().assumesSequent().isEmpty();
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/IntroducedSymbolBy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/IntroducedSymbolBy.java
@@ -17,6 +17,8 @@
 import org.key_project.prover.strategy.costbased.feature.Feature;
 import org.key_project.prover.strategy.costbased.termProjection.ProjectionToTerm;
 
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 public class IntroducedSymbolBy extends BinaryTacletAppFeature {
     private final Name ruleSetName;
     private final Name schemaVar;
@@ -37,7 +39,8 @@ protected IntroducedSymbolBy(ProjectionToTerm<Goal> termWithTopLevelOpToCheck, N
     }
 
     @Override
-    protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
+    protected boolean filter(@MonotonicNonNull TacletApp app, PosInOccurrence pos, Goal goal,
+            MutableState mState) {
         final Node root = goal.proof().root();
 
         Node n = goal.node();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/BinaryTacletAppFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/BinaryTacletAppFeature.java
@@ -7,6 +7,7 @@
 import de.uka.ilkd.key.rule.TacletApp;
 
 import org.key_project.prover.proof.ProofGoal;
+import org.key_project.prover.rules.ITacletApp;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.strategy.costbased.MutableState;
@@ -37,7 +38,7 @@ protected BinaryTacletAppFeature(boolean p_nonTacletValue) {
     final protected <PGoal extends ProofGoal<@NonNull PGoal>> boolean filter(RuleApp app,
             PosInOccurrence pos,
             PGoal goal, MutableState mState) {
-        if (app instanceof TacletApp tacletApp) {
+        if (app instanceof ITacletApp tacletApp) {
             return filter(tacletApp, pos, (Goal) goal, mState);
         }
         return nonTacletValue;
@@ -51,7 +52,7 @@ protected BinaryTacletAppFeature(boolean p_nonTacletValue) {
      * @param pos position where <code>app</code> is to be applied
      * @param goal the goal on which <code>app</code> is to be applied
      * @param mState the MutableState used to store modifiable information
-     * @return true iff the the result of the feature is supposed to be zero.
+     * @return true iff the result of the feature is supposed to be zero.
      */
     protected abstract boolean filter(TacletApp app, PosInOccurrence pos, Goal goal,
             MutableState mState);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java
@@ -15,6 +15,8 @@
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.feature.Feature;
 
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 /**
  * This feature checks that an equation is not applied to itself. This means that the focus of the
  * rule application must not be one side of an equation that is the instantiation of the first
@@ -27,7 +29,8 @@ public class CheckApplyEqFeature extends BinaryTacletAppFeature {
     private CheckApplyEqFeature() {}
 
     @Override
-    protected boolean filter(TacletApp p_app, PosInOccurrence pos, Goal goal, MutableState mState) {
+    protected boolean filter(@MonotonicNonNull TacletApp p_app, PosInOccurrence pos, Goal goal,
+            MutableState mState) {
         assert pos != null : "Need to know the position of " + "the application of the taclet";
 
         AssumesFormulaInstantiation ifInst = p_app.assumesFormulaInstantiations().head();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndIfFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndIfFeature.java
@@ -14,6 +14,8 @@
 import org.key_project.prover.strategy.costbased.feature.Feature;
 import org.key_project.util.collection.ImmutableList;
 
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 /**
  * Binary feature that returns zero iff the <tt>\assumes</tt>- and find-formula of a Taclet are
  * matched to different members of the sequent. If a taclet has more than one formula in its
@@ -27,7 +29,8 @@ public class DiffFindAndIfFeature extends BinaryTacletAppFeature {
     private DiffFindAndIfFeature() {}
 
     @Override
-    protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
+    protected boolean filter(@MonotonicNonNull TacletApp app, PosInOccurrence pos, Goal goal,
+            MutableState mState) {
         assert pos != null : "Feature is only applicable to rules with find";
 
         ImmutableList<AssumesFormulaInstantiation> list = app.assumesFormulaInstantiations();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndReplacewithFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndReplacewithFeature.java
@@ -14,6 +14,8 @@
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.feature.Feature;
 
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY;
 
 /**
@@ -28,15 +30,18 @@ public class DiffFindAndReplacewithFeature extends BinaryTacletAppFeature {
     private DiffFindAndReplacewithFeature() {}
 
     @Override
-    protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
+    protected boolean filter(@MonotonicNonNull TacletApp app, PosInOccurrence pos, Goal goal,
+            MutableState mState) {
         assert pos != null && app.rule() instanceof RewriteTaclet
                 : "Feature is only applicable to rewrite taclets";
 
-        for (TacletGoalTemplate template : app.rule().goalTemplates()) {
-            final JTerm replaceWith = ((RewriteTacletGoalTemplate) template).replaceWith();
-            if (replaceWith.equalsModProperty(pos.subTerm(),
-                IRRELEVANT_TERM_LABELS_PROPERTY)) {
-                return false;
+        for (TacletGoalTemplate template : app.taclet().goalTemplates()) {
+            if (template instanceof RewriteTacletGoalTemplate rwTGT) {
+                final JTerm replaceWith = rwTGT.replaceWith();
+                if (replaceWith.equalsModProperty(pos.subTerm(),
+                    IRRELEVANT_TERM_LABELS_PROPERTY)) {
+                    return false;
+                }
             }
         }
         return true;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/EqNonDuplicateAppFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/EqNonDuplicateAppFeature.java
@@ -10,6 +10,8 @@
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.feature.Feature;
 
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 
 /**
  * Binary feature that returns zero iff a certain Taclet app has not already been performed.
@@ -24,7 +26,7 @@ public class EqNonDuplicateAppFeature extends AbstractNonDuplicateAppFeature {
     private EqNonDuplicateAppFeature() {}
 
     @Override
-    public boolean filter(TacletApp app, PosInOccurrence pos,
+    public boolean filter(@MonotonicNonNull TacletApp app, PosInOccurrence pos,
             Goal goal, MutableState mState) {
         assert pos != null : "Feature is only applicable to rules with find";
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MatchedAssumesFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MatchedAssumesFeature.java
@@ -10,6 +10,8 @@
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.feature.Feature;
 
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 /**
  * Binary features that returns zero iff the if-formulas of a Taclet are instantiated or the Taclet
  * does not have any if-formulas.
@@ -21,7 +23,8 @@ public final class MatchedAssumesFeature extends BinaryTacletAppFeature {
     private MatchedAssumesFeature() {}
 
     @Override
-    protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
+    protected boolean filter(@MonotonicNonNull TacletApp app, PosInOccurrence pos, Goal goal,
+            MutableState mState) {
         return app.assumesInstantionsComplete();
     }
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java
@@ -12,6 +12,8 @@
 import org.key_project.prover.strategy.costbased.feature.Feature;
 import org.key_project.util.collection.ImmutableList;
 
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 /**
  * This feature checks that the position of application is not contained in the if-formulas. If the
  * rule application is admissible, zero is returned.
@@ -23,7 +25,8 @@ public class NoSelfApplicationFeature extends BinaryTacletAppFeature {
     private NoSelfApplicationFeature() {}
 
     @Override
-    protected boolean filter(TacletApp p_app, PosInOccurrence pos, Goal goal, MutableState mState) {
+    protected boolean filter(@MonotonicNonNull TacletApp p_app, PosInOccurrence pos, Goal goal,
+            MutableState mState) {
         assert pos != null
                 : "NoSelfApplicationFeature: Need to know the position of the application of the taclet";
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NonDuplicateAppFeature.java
@@ -10,6 +10,8 @@
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.feature.Feature;
 
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 
 /**
  * Binary feature that returns zero iff a certain Taclet app has not already been performed
@@ -19,7 +21,7 @@ public class NonDuplicateAppFeature extends AbstractNonDuplicateAppFeature {
     public static final Feature INSTANCE = new NonDuplicateAppFeature();
 
     @Override
-    public boolean filter(TacletApp app, PosInOccurrence pos,
+    public boolean filter(@MonotonicNonNull TacletApp app, PosInOccurrence pos,
             Goal goal, MutableState mState) {
         if (!app.assumesInstantionsComplete()) {
             return true;
@@ -30,8 +32,7 @@ public boolean filter(TacletApp app, PosInOccurrence pos,
 
     @Override
     protected boolean comparePio(TacletApp newApp, TacletApp oldApp,
-            PosInOccurrence newPio,
-            PosInOccurrence oldPio) {
+            PosInOccurrence newPio, PosInOccurrence oldPio) {
         return oldPio.equals(newPio);
     }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/PolynomialValuesCmpFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/PolynomialValuesCmpFeature.java
@@ -103,8 +103,9 @@ protected boolean compare(Polynomial leftPoly, Polynomial rightPoly) {
     @Override
     protected boolean filter(TacletApp app, PosInOccurrence pos,
             Goal goal, MutableState mState) {
-        return compare(getPolynomial(left, leftCoeff, app, pos, goal, mState),
-            getPolynomial(right, rightCoeff, app, pos, goal, mState));
+        final TacletApp tacletApp = (TacletApp) app;
+        return compare(getPolynomial(left, leftCoeff, tacletApp, pos, goal, mState),
+            getPolynomial(right, rightCoeff, tacletApp, pos, goal, mState));
     }
 
     protected abstract boolean compare(Polynomial leftPoly, Polynomial rightPoly);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TriggerVarInstantiatedFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TriggerVarInstantiatedFeature.java
@@ -11,6 +11,8 @@
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.feature.Feature;
 
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
 public class TriggerVarInstantiatedFeature extends BinaryTacletAppFeature {
 
     public static final Feature INSTANCE = new TriggerVarInstantiatedFeature();
@@ -19,7 +21,8 @@ private TriggerVarInstantiatedFeature() {
     }
 
     @Override
-    protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
+    protected boolean filter(@MonotonicNonNull TacletApp app, PosInOccurrence pos, Goal goal,
+            MutableState mState) {
         assert app.taclet().hasTrigger();
 
         SVInstantiationProjection instProj = SVInstantiationProjection
diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/ITacletApp.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/ITacletApp.java
@@ -3,10 +3,12 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.prover.rules;
 
+import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.instantiation.MatchResultInfo;
 import org.key_project.prover.rules.instantiation.SVInstantiations;
 import org.key_project.util.collection.ImmutableList;
+import org.key_project.util.collection.ImmutableSet;
 
 import org.jspecify.annotations.NonNull;
 
@@ -28,4 +30,16 @@ default SVInstantiations instantiations() {
     MatchResultInfo matchConditions();
 
     ImmutableList<AssumesFormulaInstantiation> assumesFormulaInstantiations();
+
+    boolean assumesInstantionsComplete();
+
+    /**
+     * returns the variables that have not yet been instantiated and need to be instantiated to
+     * apply the Taclet. (These are not all SchemaVariables like the one that appear only in the
+     * addrule sections)
+     *
+     * @return ImmutableSet<SchemaVariable> with SchemaVariables that have not been instantiated yet
+     */
+    @NonNull
+    ImmutableSet<SchemaVariable> uninstantiatedVars();
 }
diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/CountBranchFeature.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/CountBranchFeature.java
@@ -1,17 +1,15 @@
 /* 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.feature;
-
-import de.uka.ilkd.key.rule.Taclet;
+package org.key_project.prover.strategy.costbased.feature;
 
 import org.key_project.prover.proof.ProofGoal;
 import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.rules.Taclet;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.NumberRuleAppCost;
 import org.key_project.prover.strategy.costbased.RuleAppCost;
-import org.key_project.prover.strategy.costbased.feature.Feature;
 
 import org.jspecify.annotations.NonNull;
 

Original file line number	Diff line number	Diff line change
`@@ -440,11 +440,11 @@ public TacletApp addCheckedInstantiation(SchemaVariable sv, JTerm term, Services`
`440`	`440`	`*`
`441`	`441`	`* @return ImmutableSet<SchemaVariable> with SchemaVariables that have not been instantiated yet`
`442`	`442`	`*/`
	`443`	`+ @Override`
`443`	`444`	`public @NonNull ImmutableSet<SchemaVariable> uninstantiatedVars() {`
`444`	`445`	`return calculateNonInstantiatedSV();`
`445`	`446`	`}`
`446`	`447`
`447`		`-`
`448`	`448`	`/**`
`449`	`449`	`* returns true if the given {@link SchemaVariable} must be explicitly instantiated it does not`
`450`	`450`	`* check whether sv is already instantiated or not`
`@@ -957,6 +957,7 @@ public PosTacletApp setPosInOccurrence(PosInOccurrence pos,`
`957`	`957`	`/**`
`958`	`958`	`* @return true iff the if-instantiation list is not null or no if sequent is needed`
`959`	`959`	`*/`
	`960`	`+ @Override`
`960`	`961`	`public boolean assumesInstantionsComplete() {`
`961`	`962`	`return assumesFormulaInstantiations != null \|\| taclet().assumesSequent().isEmpty();`
`962`	`963`	`}`