RuleApp interface for all external solvers (prep for #3514) (#3521)

WolframPfeifer · web-flow · commit c19bb8e54936 · 2024-11-13T18:06:48.000Z
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
@@ -22,7 +22,6 @@
 import de.uka.ilkd.key.rule.*;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.rule.merge.MergeRule;
-import de.uka.ilkd.key.smt.SMTRuleApp;
 import de.uka.ilkd.key.strategy.AutomatedRuleApplicationManager;
 import de.uka.ilkd.key.strategy.QueueRuleApplicationManager;
 import de.uka.ilkd.key.strategy.Strategy;
@@ -627,7 +626,7 @@ public ImmutableList<Goal> apply(final RuleApp ruleApp) {
         } else {
             proof.replace(this, goalList);
             if (ruleApp instanceof TacletApp tacletApp && tacletApp.taclet().closeGoal()
-                    || ruleApp instanceof SMTRuleApp) {
+                    || ruleApp instanceof AbstractExternalSolverRuleApp) {
                 // the first new goal is the one to be closed
                 proof.closeGoal(goalList.head());
             }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java
@@ -0,0 +1,112 @@
+/* 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.rule;
+
+import de.uka.ilkd.key.logic.*;
+import de.uka.ilkd.key.proof.Goal;
+
+import org.key_project.util.collection.ImmutableList;
+
+/**
+ * The rule application that is used when a goal is closed by means of an external solver. So far it
+ * stores the rule that that has been used and a title containing some information for the user.
+ * <p>
+ * {@link de.uka.ilkd.key.smt.SMTRuleApp}
+ */
+public abstract class AbstractExternalSolverRuleApp extends AbstractBuiltInRuleApp {
+    protected final String title;
+    protected final String successfulSolverName;
+
+    /**
+     * Creates a new AbstractExternalSolverRuleApp,
+     *
+     * @param rule the ExternalSolverRule to apply
+     * @param pio the position in the term to apply the rule to
+     * @param unsatCore an unsat core consisting of the formulas that are needed to prove the goal
+     *        (optional null)
+     * @param successfulSolverName the name of the solver used to find the proof
+     * @param title the title of this rule app
+     */
+    protected AbstractExternalSolverRuleApp(ExternalSolverRule rule, PosInOccurrence pio,
+            ImmutableList<PosInOccurrence> unsatCore,
+            String successfulSolverName, String title) {
+        super(rule, pio, unsatCore);
+        this.title = title;
+        this.successfulSolverName = successfulSolverName;
+    }
+
+    /**
+     * Gets the title of this rule application
+     *
+     * @return title of this application
+     */
+    public String getTitle() {
+        return title;
+    }
+
+    /**
+     * Gets the name of the successful solver
+     *
+     * @return name of the successful solver
+     */
+    public String getSuccessfulSolverName() {
+        return successfulSolverName;
+    }
+
+    @Override
+    public String displayName() {
+        return title;
+    }
+
+    /**
+     * Interface for the rules of external solvers
+     */
+    public interface ExternalSolverRule extends BuiltInRule {
+        AbstractExternalSolverRuleApp createApp(String successfulSolverName);
+
+        /**
+         * Create a new rule application with the given solver name and unsat core.
+         *
+         * @param successfulSolverName solver that produced this result
+         * @param unsatCore formulas required to prove the result
+         * @return rule application instance
+         */
+        AbstractExternalSolverRuleApp createApp(String successfulSolverName,
+                ImmutableList<PosInOccurrence> unsatCore);
+
+        @Override
+        AbstractExternalSolverRuleApp createApp(PosInOccurrence pos, TermServices services);
+
+
+        @Override
+        default boolean isApplicable(Goal goal, PosInOccurrence pio) {
+            return false;
+        }
+
+        @Override
+        default boolean isApplicableOnSubTerms() {
+            return false;
+        }
+
+        @Override
+        String displayName();
+
+        @Override
+        String toString();
+    }
+
+    /**
+     * Sets the title (needs to create a new instance for this)
+     *
+     * @param title new title for rule app
+     * @return copy of this with the new title
+     */
+    public abstract AbstractExternalSolverRuleApp setTitle(String title);
+
+    @Override
+    public AbstractExternalSolverRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts) {
+        setMutable(ifInsts);
+        return this;
+    }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java
@@ -9,22 +9,21 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.proof.Goal;
-import de.uka.ilkd.key.rule.AbstractBuiltInRuleApp;
+import de.uka.ilkd.key.rule.AbstractExternalSolverRuleApp;
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.RuleApp;
 
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.NonNull;
+
 /**
- * The rule application that is used when a goal is closed by means of an external solver. So far it
+ * The rule application that is used when a goal is closed by means of an SMT solver. So far it
  * stores the rule that that has been used and a title containing some information for the user.
  */
-public class SMTRuleApp extends AbstractBuiltInRuleApp {
-
+public class SMTRuleApp extends AbstractExternalSolverRuleApp {
     public static final SMTRule RULE = new SMTRule();
-    private final String title;
-    private final String successfulSolverName;
 
     /**
      * Create a new rule app without ifInsts (will be null).
@@ -37,39 +36,26 @@ public class SMTRuleApp extends AbstractBuiltInRuleApp {
         this(rule, pio, null, successfulSolverName);
     }
 
-    SMTRuleApp(SMTRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> unsatCore,
+    SMTRuleApp(ExternalSolverRule rule, PosInOccurrence pio,
+            ImmutableList<PosInOccurrence> unsatCore,
             String successfulSolverName) {
-        super(rule, pio, unsatCore);
-        this.title = "SMT: " + successfulSolverName;
-        this.successfulSolverName = successfulSolverName;
+        super(rule, pio, unsatCore, successfulSolverName, "SMT: " + successfulSolverName);
     }
 
     @Override
     public SMTRuleApp replacePos(PosInOccurrence newPos) {
         return new SMTRuleApp(RULE, newPos, ifInsts, successfulSolverName);
     }
 
-    public String getTitle() {
-        return title;
-    }
-
-    public String getSuccessfulSolverName() {
-        return successfulSolverName;
-    }
-
     @Override
     public BuiltInRule rule() {
         return RULE;
     }
 
-    @Override
-    public String displayName() {
-        return title;
-    }
-
-    public static class SMTRule implements BuiltInRule {
+    public static class SMTRule implements ExternalSolverRule {
         public static final Name name = new Name("SMTRule");
 
+        @Override
         public SMTRuleApp createApp(String successfulSolverName) {
             return new SMTRuleApp(this, null, successfulSolverName);
         }
@@ -81,6 +67,7 @@ public SMTRuleApp createApp(String successfulSolverName) {
          * @param unsatCore formulas required to prove the result
          * @return rule application instance
          */
+        @Override
         public SMTRuleApp createApp(String successfulSolverName,
                 ImmutableList<PosInOccurrence> unsatCore) {
             return new SMTRuleApp(this, null, unsatCore, successfulSolverName);
@@ -91,13 +78,6 @@ public SMTRuleApp createApp(PosInOccurrence pos, TermServices services) {
             return new SMTRuleApp(this, null, "");
         }
 
-
-        @Override
-        public 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.
@@ -108,23 +88,20 @@ public boolean isApplicable(Goal goal, PosInOccurrence pio) {
          * @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);
             }
             return goal.split(1);
         }
 
-        @Override
-        public boolean isApplicableOnSubTerms() {
-            return false;
-        }
-
         @Override
         public String displayName() {
             return "SMT";
         }
 
+        @Override
         public String toString() {
             return displayName();
         }
@@ -133,9 +110,9 @@ public String toString() {
         public Name name() {
             return name;
         }
-
     }
 
+    @Override
     public SMTRuleApp setTitle(String title) {
         return new SMTRuleApp(RULE, pio, ifInsts, title);
     }
@@ -168,5 +145,4 @@ public SMTRuleApp tryToInstantiate(Goal goal) {
         }
         return app.setIfInsts(ImmutableList.fromList(ifInsts));
     }
-
 }
