Move strategies to NCore

.gitignore

@@ -67,6 +67,7 @@ key/key.ui/examples/**/**.proof
 
 # generated by the antlr plugin of IntelliJ
 key.core/src/main/antlr4/gen/
+*.tokens
 
 scripts/tools/checkstyle/key_checks_incremental.xml
 checkstyle-diff.txt

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

@@ -10,12 +10,12 @@
 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 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;
@@ -138,17 +138,9 @@ private String getAppRuleName(Node parent) {
             return parentRuleName;
         }
 
-
-        @Override
-        protected RuleAppCost instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal,
-                MutableState mState) {
-            return computeCost(app, pio, goal, mState);
-        }
-
         @Override
         public boolean isStopAtFirstNonCloseableGoal() {
             return false;
         }
     }
-
 }

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

@@ -12,10 +12,7 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.ProofOblInput;
-import de.uka.ilkd.key.strategy.JavaCardDLStrategyFactory;
-import de.uka.ilkd.key.strategy.RuleAppCostCollector;
-import de.uka.ilkd.key.strategy.Strategy;
-import de.uka.ilkd.key.strategy.StrategyProperties;
+import de.uka.ilkd.key.strategy.*;
 
 import org.key_project.logic.Name;
 import org.key_project.prover.proof.ProofGoal;
@@ -65,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());
     }
@@ -113,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());
@@ -136,10 +133,10 @@ public Name name() {
             String name = ruleApp.rule().name().toString();
             if ((admittedRuleNames.contains(name) || name.startsWith(INF_FLOW_UNFOLD_PREFIX))
                     && ruleApplicationInContextAllowed(ruleApp, pio, goal)) {
-                JavaCardDLStrategyFactory strategyFactory = new JavaCardDLStrategyFactory();
-                Strategy<@NonNull Goal> javaDlStrategy =
+                ModularJavaDLStrategyFactory strategyFactory = new ModularJavaDLStrategyFactory();
+                org.key_project.prover.strategy.Strategy<@NonNull Goal> dlStrategy =
                     strategyFactory.create(goal.proof(), new StrategyProperties());
-                RuleAppCost costs = javaDlStrategy.computeCost(ruleApp, pio, goal, mState);
+                RuleAppCost costs = dlStrategy.computeCost(ruleApp, pio, goal, mState);
                 if ("orLeft".equals(name)) {
                     costs = costs.add(NumberRuleAppCost.create(100));
                 }
@@ -157,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

@@ -5,18 +5,16 @@
 
 import java.util.ArrayList;
 
-import de.uka.ilkd.key.logic.JTerm;
 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;
@@ -28,23 +26,26 @@
 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;
 
 /**
- * {@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");
 
@@ -85,7 +86,7 @@ private SymbolicExecutionStrategy(Proof proof, StrategyProperties sp) {
                 .equals(sp.get(StrategyProperties.SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY))) {
             // Make sure that an immediately alias check is performed by doing cuts of objects to
             // find out if they can be the same or not
-            RuleSetDispatchFeature instRsd = getInstantiationDispatcher();
+            RuleSetDispatchFeature instRsd = getDispatcher(StrategyAspect.Instantiation);
             enableInstantiate();
             final TermBuffer<Goal> buffer = new TermBuffer<>();
             Feature originalCut = instRsd.get(getHeuristic("cut"));
@@ -106,7 +107,7 @@ private SymbolicExecutionStrategy(Proof proof, StrategyProperties sp) {
      * {@inheritDoc}
      */
     @Override
-    protected Feature setupApprovalF() {
+    protected @NonNull Feature setupApprovalF() {
         Feature result = super.setupApprovalF();
         // Make sure that cuts are only applied if the cut term is not already part of the sequent.
         // This check is performed exactly before the rule is applied because the sequent might has
@@ -122,17 +123,17 @@ protected Feature setupApprovalF() {
      * {@inheritDoc}
      */
     @Override
-    protected Feature setupGlobalF(Feature dispatcher) {
+    protected @NonNull Feature setupGlobalF(@NonNull Feature dispatcher) {
         Feature globalF = super.setupGlobalF(dispatcher);
         // Make sure that modalities without symbolic execution label are executed first because
         // they might forbid rule application on modalities with symbolic execution label (see loop
         // body branches)
         globalF = add(globalF, ifZero(not(new BinaryFeature() {
             @Override
-            protected <Goal extends ProofGoal<@NonNull Goal>> boolean filter(RuleApp app,
-                    PosInOccurrence pos, Goal goal, MutableState mState) {
+            protected <GOAL extends ProofGoal<@NonNull GOAL>> boolean filter(RuleApp app,
+                    PosInOccurrence pos, GOAL goal, MutableState mState) {
                 return pos != null
-                        && SymbolicExecutionUtil.hasSymbolicExecutionLabel((JTerm) pos.subTerm());
+                        && SymbolicExecutionUtil.hasSymbolicExecutionLabel(pos.subTerm());
             }
         }), longConst(-3000)));
         // Make sure that the modality which executes a loop body is preferred against the
@@ -141,9 +142,9 @@ protected Feature setupGlobalF(Feature dispatcher) {
             add(globalF,
                 ifZero(add(new Feature() {
                     @Override
-                    public <Goal extends ProofGoal<@NonNull Goal>> RuleAppCost computeCost(
+                    public <GOAL extends ProofGoal<@NonNull GOAL>> RuleAppCost computeCost(
                             RuleApp app, PosInOccurrence pos,
-                            Goal goal, MutableState mState) {
+                            GOAL goal, MutableState mState) {
                         return pos != null ? cost(0) : TopRuleAppCost.INSTANCE;
                     }
                 },
@@ -302,7 +303,7 @@ public static class Factory implements StrategyFactory {
          * {@inheritDoc}
          */
         @Override
-        public StrategySettingsDefinition getSettingsDefinition() {
+        public @NonNull StrategySettingsDefinition getSettingsDefinition() {
             // Properties
             OneOfStrategyPropertyDefinition methodTreatment = new OneOfStrategyPropertyDefinition(
                 StrategyProperties.METHOD_OPTIONS_KEY, "Method Treatment",

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

@@ -46,8 +46,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.JavaCardDLStrategyFactory;
-import de.uka.ilkd.key.strategy.Strategy;
+import de.uka.ilkd.key.strategy.JavaStrategy;
+import de.uka.ilkd.key.strategy.ModularJavaDLStrategyFactory;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor;
 import de.uka.ilkd.key.symbolic_execution.SymbolicExecutionTreeBuilder;
@@ -2562,7 +2562,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();
@@ -4312,7 +4312,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.
      */
@@ -4325,7 +4325,7 @@ public static void initializeStrategy(SymbolicExecutionTreeBuilder builder) {
                 new SymbolicExecutionStrategy.Factory().create(proof, strategyProperties));
         } else {
             proof.setActiveStrategy(
-                new JavaCardDLStrategyFactory().create(proof, strategyProperties));
+                new ModularJavaDLStrategyFactory().create(proof, strategyProperties));
         }
     }