removed default implementations for AbstractExternalSolverRuleApp around RULE field

Author: BookWood7th

key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java

@@ -3,14 +3,9 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.rule;
 
-import java.util.ArrayList;
-import java.util.List;
-
-import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.proof.Goal;
 
-import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 
 /**
@@ -20,7 +15,6 @@
  * {@link de.uka.ilkd.key.smt.SMTRuleApp}
  */
 public abstract class AbstractExternalSolverRuleApp extends AbstractBuiltInRuleApp {
-    protected final ExternalSolverRule rule;
     protected final String title;
     protected final String successfulSolverName;
 
@@ -38,7 +32,6 @@ protected AbstractExternalSolverRuleApp(ExternalSolverRule rule, PosInOccurrence
             ImmutableList<PosInOccurrence> unsatCore,
             String successfulSolverName, String title) {
         super(rule, pio, unsatCore);
-        this.rule = rule.newRule();
         this.title = title;
         this.successfulSolverName = successfulSolverName;
     }
@@ -61,11 +54,6 @@ public String getSuccessfulSolverName() {
         return successfulSolverName;
     }
 
-    @Override
-    public BuiltInRule rule() {
-        return rule;
-    }
-
     @Override
     public String displayName() {
         return title;
@@ -75,10 +63,6 @@ public String displayName() {
      * Interface for the rules of external solvers
      */
     public interface ExternalSolverRule extends BuiltInRule {
-        Name name = new Name("ExternalSolverRule");
-
-        ExternalSolverRule newRule();
-
         AbstractExternalSolverRuleApp createApp(String successfulSolverName);
 
         /**
@@ -100,42 +84,16 @@ default boolean isApplicable(Goal goal, PosInOccurrence pio) {
             return false;
         }
 
-
-        /**
-         * Create a new goal (to be closed in {@link Goal#apply(RuleApp)} directly afterwards)
-         * with the same sequent as the given one.
-         *
-         * @param goal the Goal on which to apply <tt>ruleApp</tt>
-         * @param services the Services with the necessary information about the java programs
-         * @param ruleApp the rule application to be executed
-         * @return a list with an identical goal as the given <tt>goal</tt>
-         */
-        @Override
-        default ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp) {
-            if (goal.proof().getInitConfig().getJustifInfo().getJustification(newRule()) == null) {
-                goal.proof().getInitConfig().registerRule(newRule(), () -> false);
-            }
-            return goal.split(1);
-        }
-
         @Override
         default boolean isApplicableOnSubTerms() {
             return false;
         }
 
         @Override
-        default String displayName() {
-            return "ExternalSolver";
-        }
+        String displayName();
 
         @Override
         String toString();
-
-        @Override
-        default Name name() {
-            return name;
-        }
-
     }
 
     /**
@@ -151,28 +109,4 @@ public AbstractExternalSolverRuleApp setIfInsts(ImmutableList<PosInOccurrence> i
         setMutable(ifInsts);
         return this;
     }
-
-    /**
-     * Create a new RuleApp with the same pio (in this case, that will probably be null as the
-     * AbstractExternalSolver rule is applied to the complete sequent) as this one.
-     * Add all top level formulas of the goal
-     * to the RuleApp's ifInsts.
-     *
-     * @param goal the goal to instantiate the current RuleApp on
-     * @return a new RuleApp with the same pio and all top level formulas of the goal as ifInsts
-     */
-    @Override
-    public AbstractExternalSolverRuleApp tryToInstantiate(Goal goal) {
-        AbstractExternalSolverRuleApp app = rule.createApp(pio, goal.proof().getServices());
-        Sequent seq = goal.sequent();
-        List<PosInOccurrence> ifInsts = new ArrayList<>();
-        for (SequentFormula ante : seq.antecedent()) {
-            ifInsts.add(new PosInOccurrence(ante, PosInTerm.getTopLevel(), true));
-        }
-        for (SequentFormula succ : seq.succedent()) {
-            ifInsts.add(new PosInOccurrence(succ, PosInTerm.getTopLevel(), false));
-        }
-        return app.setIfInsts(ImmutableList.fromList(ifInsts));
-    }
-
 }

key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java

@@ -13,6 +13,7 @@
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.RuleApp;
 
+import org.jspecify.annotations.NonNull;
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 
@@ -53,11 +54,6 @@ public BuiltInRule rule() {
     public static class SMTRule implements ExternalSolverRule {
         public static final Name name = new Name("SMTRule");
 
-        @Override
-        public ExternalSolverRule newRule() {
-            return new SMTRule();
-        }
-
         @Override
         public SMTRuleApp createApp(String successfulSolverName) {
             return new SMTRuleApp(this, null, successfulSolverName);
@@ -91,6 +87,7 @@ public SMTRuleApp createApp(PosInOccurrence pos, TermServices services) {
          * @return a list with an identical goal as the given <tt>goal</tt>
          */
         @Override
+        @NonNull
         public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp) {
             if (goal.proof().getInitConfig().getJustifInfo().getJustification(RULE) == null) {
                 goal.proof().getInitConfig().registerRule(RULE, () -> false);