Move strategies to NCore

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/PrepareInfFlowContractPreBranchesMacro.java

@@ -9,20 +9,22 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.strategy.AbstractFeatureStrategy;
-import de.uka.ilkd.key.strategy.Strategy;
+import de.uka.ilkd.key.strategy.JavaAbstractFeatureStrategy;
 
 import org.key_project.logic.Name;
 import org.key_project.prover.proof.ProofGoal;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.strategy.Strategy;
 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.TopRuleAppCost;
 
 import org.jspecify.annotations.NonNull;
 
+import static de.uka.ilkd.key.strategy.StaticFeatureCollection.hasLabel;
+
 
 /**
  * The macro UseInformationFlowContractMacro applies all applicable information flow contracts.
@@ -67,7 +69,7 @@ public String getDescription() {
      * This strategy accepts all rule apps for which the rule name starts with a string in the
      * admitted set and rejects everything else.
      */
-    protected static class RemovePostStrategy extends AbstractFeatureStrategy {
+    protected static class RemovePostStrategy extends JavaAbstractFeatureStrategy {
 
         private final Name NAME = new Name("RemovePostStrategy");
 

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java

@@ -62,7 +62,7 @@ protected Set<String> getAdmittedRuleNames() {
     }
 
     @Override
-    protected Strategy<@NonNull Goal> createStrategy(Proof proof,
+    protected org.key_project.prover.strategy.Strategy<@NonNull Goal> createStrategy(Proof proof,
             PosInOccurrence posInOcc) {
         return new SelfCompExpansionStrategy(getAdmittedRuleNames());
     }
@@ -110,7 +110,7 @@ protected boolean allowOSS() {
      * This strategy accepts all rule apps for which the rule name is in the admitted set or has
      * INF_FLOW_UNFOLD_PREFIX as a prefix and rejects everything else.
      */
-    private class SelfCompExpansionStrategy implements Strategy<Goal> {
+    private class SelfCompExpansionStrategy implements JavaStrategy {
 
         private final Name NAME = new Name(
             SelfcompositionStateExpansionMacro.SelfCompExpansionStrategy.class.getSimpleName());
@@ -134,7 +134,7 @@ public Name name() {
             if ((admittedRuleNames.contains(name) || name.startsWith(INF_FLOW_UNFOLD_PREFIX))
                     && ruleApplicationInContextAllowed(ruleApp, pio, goal)) {
                 ModularJavaDLStrategyFactory strategyFactory = new ModularJavaDLStrategyFactory();
-                Strategy<@NonNull Goal> dlStrategy =
+                org.key_project.prover.strategy.Strategy<@NonNull Goal> dlStrategy =
                     strategyFactory.create(goal.proof(), new StrategyProperties());
                 RuleAppCost costs = dlStrategy.computeCost(ruleApp, pio, goal, mState);
                 if ("orLeft".equals(name)) {
@@ -154,7 +154,7 @@ public boolean isApprovedApp(RuleApp app, PosInOccurrence pio,
 
         @Override
         public void instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal,
-                RuleAppCostCollector collector) {
+                org.key_project.prover.strategy.RuleAppCostCollector collector) {
         }
 
         @Override

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/UseInformationFlowContractMacro.java

@@ -14,13 +14,13 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.strategy.RuleAppCostCollector;
-import de.uka.ilkd.key.strategy.Strategy;
+import de.uka.ilkd.key.strategy.JavaStrategy;
 
 import org.key_project.logic.Name;
 import org.key_project.prover.proof.ProofGoal;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.strategy.RuleAppCostCollector;
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.NumberRuleAppCost;
 import org.key_project.prover.strategy.costbased.RuleAppCost;
@@ -166,7 +166,7 @@ private String getAppRuleName(Node parent) {
      * This strategy accepts all rule apps for which the rule name starts with a string in the
      * admitted set and rejects everything else.
      */
-    protected class PropExpansionStrategy implements Strategy<Goal> {
+    protected class PropExpansionStrategy implements JavaStrategy {
 
         private final Name NAME =
             new Name(UseInformationFlowContractMacro.PropExpansionStrategy.class.getSimpleName());

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java

@@ -25,7 +25,6 @@
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.TermBuilder;
-import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.logic.label.ParameterlessTermLabel;
 import de.uka.ilkd.key.logic.op.JFunction;
 import de.uka.ilkd.key.logic.op.LocationVariable;
@@ -43,6 +42,7 @@
 import de.uka.ilkd.key.speclang.BlockContract;
 import de.uka.ilkd.key.util.MiscTools;
 
+import org.key_project.logic.LogicServices;
 import org.key_project.logic.Name;
 import org.key_project.logic.op.Function;
 import org.key_project.prover.sequent.PosInOccurrence;
@@ -101,7 +101,7 @@ private InfFlowBlockContractInternalRule() {
 
     @Override
     public BlockContractInternalBuiltInRuleApp<? extends BlockContractInternalRule> createApp(
-            PosInOccurrence occurrence, TermServices services) {
+            PosInOccurrence occurrence, LogicServices services) {
         return new InfFlowBlockContractInternalBuiltInRuleApp(this, occurrence);
     }
 

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java

@@ -32,6 +32,7 @@
 import de.uka.ilkd.key.speclang.LoopSpecification;
 import de.uka.ilkd.key.util.MiscTools;
 
+import org.key_project.logic.LogicServices;
 import org.key_project.logic.Name;
 import org.key_project.logic.Namespace;
 import org.key_project.logic.op.Function;
@@ -58,8 +59,8 @@ public Name name() {
 
     @Override
     public InfFlowLoopInvariantBuiltInRuleApp createApp(PosInOccurrence pos,
-            TermServices services) {
-        return new InfFlowLoopInvariantBuiltInRuleApp(this, pos, services);
+            LogicServices services) {
+        return new InfFlowLoopInvariantBuiltInRuleApp(this, pos, (TermServices) services);
     }
 
     @Override

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java

@@ -10,7 +10,6 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
-import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
@@ -20,6 +19,7 @@
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
+import org.key_project.logic.LogicServices;
 import org.key_project.logic.Name;
 import org.key_project.logic.op.Function;
 import org.key_project.prover.rules.RuleAbortException;
@@ -119,7 +119,7 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
      * {@inheritDoc}
      */
     @Override
-    public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
+    public IBuiltInRuleApp createApp(PosInOccurrence pos, LogicServices services) {
         return new DefaultBuiltInRuleApp(this, pos);
     }
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java

@@ -8,16 +8,15 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.TermBuilder;
-import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp;
 import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import de.uka.ilkd.key.rule.QueryExpand;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 
+import org.key_project.logic.LogicServices;
 import org.key_project.logic.Name;
 import org.key_project.logic.op.Function;
 import org.key_project.logic.sort.Sort;
@@ -150,7 +149,7 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
 
     /**
      * Checks if the query term is supported. The functionality is identical to
-     * {@link QueryExpand#isApplicable(Goal, PosInOccurrence)}.
+     * {@link BuiltInRule#isApplicable(org.key_project.prover.proof.ProofGoal, PosInOccurrence)}.
      *
      * @param goal The {@link Goal}.
      * @param pmTerm The {@link JTerm} to with the query to check.
@@ -182,7 +181,7 @@ private boolean isApplicableQuery(Goal goal, JTerm pmTerm,
      * {@inheritDoc}
      */
     @Override
-    public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) {
+    public IBuiltInRuleApp createApp(PosInOccurrence pos, LogicServices services) {
         return new DefaultBuiltInRuleApp(this, pos);
     }
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java

@@ -26,13 +26,13 @@
 import org.jspecify.annotations.NonNull;
 
 /**
- * {@link Strategy} used to simplify {@link JTerm}s in side proofs.
+ * {@link JavaStrategy} used to simplify {@link JTerm}s in side proofs.
  *
  * @author Martin Hentschel
  */
 public class SimplifyTermStrategy extends JavaCardDLStrategy {
     /**
-     * The {@link Name} of the side proof {@link Strategy}.
+     * The {@link Name} of the side proof {@link JavaStrategy}.
      */
     public static final Name name = new Name("Simplify Term Strategy");
 
@@ -100,7 +100,8 @@ public static class Factory implements StrategyFactory {
          * {@inheritDoc}
          */
         @Override
-        public Strategy<Goal> create(Proof proof, StrategyProperties sp) {
+        public org.key_project.prover.strategy.Strategy<Goal> create(Proof proof,
+                StrategyProperties sp) {
             return new SimplifyTermStrategy(proof, sp);
         }
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionStrategy.java

@@ -8,14 +8,13 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.strategy.JavaCardDLStrategy;
-import de.uka.ilkd.key.strategy.Strategy;
+import de.uka.ilkd.key.strategy.JavaStrategy;
 import de.uka.ilkd.key.strategy.StrategyFactory;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.strategy.definition.IDefaultStrategyPropertiesFactory;
 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;
@@ -27,23 +26,28 @@
 import org.key_project.prover.proof.rulefilter.SetRuleFilter;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.strategy.Strategy;
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.RuleAppCost;
 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;
 import org.key_project.prover.strategy.costbased.termProjection.TermBuffer;
 
 import org.jspecify.annotations.NonNull;
 
+import static de.uka.ilkd.key.strategy.StaticFeatureCollection.hasLabel;
+
 /**
- * {@link Strategy} to use for symbolic execution.
+ * {@link JavaStrategy} to use for symbolic execution.
  */
 public class SymbolicExecutionStrategy extends JavaCardDLStrategy {
     /**
-     * The {@link Name} of the symbolic execution {@link Strategy}.
+     * The {@link Name} of the symbolic execution {@link JavaStrategy}.
      */
     public static final Name name = new Name("Symbolic Execution Strategy");
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java

@@ -48,8 +48,8 @@
 import de.uka.ilkd.key.settings.StrategySettings;
 import de.uka.ilkd.key.speclang.Contract;
 import de.uka.ilkd.key.speclang.OperationContract;
+import de.uka.ilkd.key.strategy.JavaStrategy;
 import de.uka.ilkd.key.strategy.ModularJavaDLStrategyFactory;
-import de.uka.ilkd.key.strategy.Strategy;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor;
 import de.uka.ilkd.key.symbolic_execution.SymbolicExecutionTreeBuilder;
@@ -2564,7 +2564,7 @@ private static JTerm computeTacletAppBranchCondition(Node parent, Node node, boo
             boolean improveReadability) throws ProofInputException {
         if (!(parent.getAppliedRuleApp() instanceof TacletApp app)) {
             throw new ProofInputException(
-                "Only TacletApp is allowed in branch computation but rule \""
+                "Only ITacletApp is allowed in branch computation but rule \""
                     + parent.getAppliedRuleApp() + "\" was found.");
         }
         Services services = node.proof().getServices();
@@ -4314,7 +4314,7 @@ private static ImmutableArray<JTerm> extractValueFromUpdate(
 
     /**
      * Initializes the {@link Proof} of the given {@link SymbolicExecutionTreeBuilder} so that the
-     * correct {@link Strategy} is used.
+     * correct {@link JavaStrategy} is used.
      *
      * @param builder The {@link SymbolicExecutionTreeBuilder} to initialize.
      */

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/TestGenMacro.java

@@ -11,14 +11,14 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.strategy.Strategy;
 import de.uka.ilkd.key.testgen.TestGenerationSettings;
 
 import org.key_project.logic.Name;
 import org.key_project.prover.proof.ProofGoal;
 import org.key_project.prover.rules.Rule;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.strategy.Strategy;
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.NumberRuleAppCost;
 import org.key_project.prover.strategy.costbased.RuleAppCost;

key.core.wd/src/main/java/de/uka/ilkd/key/wd/macro/WellDefinednessMacro.java

@@ -9,15 +9,16 @@
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.ContractPO;
 import de.uka.ilkd.key.proof.init.FunctionalOperationContractPO;
-import de.uka.ilkd.key.strategy.RuleAppCostCollector;
-import de.uka.ilkd.key.strategy.Strategy;
+import de.uka.ilkd.key.strategy.JavaStrategy;
 import de.uka.ilkd.key.wd.*;
 import de.uka.ilkd.key.wd.po.*;
 
 import org.key_project.logic.Name;
 import org.key_project.prover.proof.ProofGoal;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.strategy.RuleAppCostCollector;
+import org.key_project.prover.strategy.Strategy;
 import org.key_project.prover.strategy.costbased.MutableState;
 import org.key_project.prover.strategy.costbased.NumberRuleAppCost;
 import org.key_project.prover.strategy.costbased.RuleAppCost;
@@ -95,7 +96,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals,
      * This strategy accepts all rule apps for which the rule name is a Well-Definedness rule and
      * rejects everything else.
      */
-    private static class WellDefinednessStrategy implements Strategy<Goal> {
+    private static class WellDefinednessStrategy implements JavaStrategy {
 
         private static final Name NAME = new Name(WellDefinednessStrategy.class.getSimpleName());
 

key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java

@@ -70,7 +70,7 @@ public class TacletFindModel extends AbstractTableModel {
     /**
      * Create new data model for tree.
      *
-     * @param app the TacletApp where to get the necessary entries
+     * @param app the ITacletApp where to get the necessary entries
      * @param services services.
      * @param nss universal namespace of variables, minimum for input in a row.
      * @param scm the abbreviation map.

key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java

@@ -216,7 +216,7 @@ public void setManualInput(int i, String s) {
     }
 
     /**
-     * replaces the TacletApp of this ApplyTacletDialogModel by an TacletApp where all name
+     * replaces the ITacletApp of this ApplyTacletDialogModel by an ITacletApp where all name
      * conflicts are resolved and thus the parser is enabled to accept variables from the context or
      * the prefix of the Taclet.
      *

key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java

@@ -18,6 +18,7 @@
 import de.uka.ilkd.key.logic.TermServices;
 import de.uka.ilkd.key.util.Debug;
 
+import org.key_project.ldt.IIntLdt;
 import org.key_project.logic.Name;
 import org.key_project.logic.op.Function;
 import org.key_project.util.ExtList;
@@ -33,7 +34,7 @@
  * convert java number types to their logic counterpart.
  */
 @SuppressWarnings("unused")
-public final class IntegerLDT extends LDT {
+public final class IntegerLDT extends LDT implements IIntLdt {
     private static final Logger LOGGER = LoggerFactory.getLogger(IntegerLDT.class);
 
     public static final Name NAME = new Name("int");

key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java

@@ -441,7 +441,7 @@ public ProgramElementName getTemporaryNameProposal(String basename) {
     @Override
     public String getProposal(TacletApp app, SchemaVariable var, Services services, Node undoAnchor,
             ImmutableList<String> previousProposals) {
-        // determine posOfDeclaration from TacletApp
+        // determine posOfDeclaration from ITacletApp
         ContextStatementBlockInstantiation cie = app.instantiations().getContextInstantiation();
         PosInProgram posOfDeclaration = (cie == null ? null : cie.prefix());