Isabelle Translation

.gitlab-ci.yml

@@ -26,10 +26,10 @@ before_script:
   - export SONAR_SCANNER_OPTS="-Xmx8G"
 
 stages:
-    - primary
-    - secondary
-    - ternary
-    - deploy
+  - primary
+  - secondary
+  - ternary
+  - deploy
 
 compile:classes:
   stage: primary

build.gradle

@@ -353,9 +353,9 @@ subprojects {
             // specific delimiter: normally just 'package', but spotless crashes for files in default package
             // (see https://github.com/diffplug/spotless/issues/30), therefore 'import' is needed. '//' is for files
             // with completely commented out code (which would probably better just be removed in future).
-            if(project.name == 'recoder') {
+            if (project.name == 'recoder') {
                 licenseHeaderFile("$rootDir/gradle/header-recoder", '(package|import|//)')
-            }else {
+            } else {
                 licenseHeaderFile("$rootDir/gradle/header", '(package|import|//)')
             }
         }

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());
             }

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

@@ -0,0 +1,178 @@
+/* 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 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;
+
+/**
+ * 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 ExternalSolverRule rule;
+    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.rule = rule.newRule();
+        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 BuiltInRule rule() {
+        return rule;
+    }
+
+    @Override
+    public String displayName() {
+        return title;
+    }
+
+    /**
+     * Interface for the rules of external solvers
+     */
+    public interface ExternalSolverRule extends BuiltInRule {
+        Name name = new Name("ExternalSolverRule");
+
+        ExternalSolverRule newRule();
+
+        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;
+        }
+
+
+        /**
+         * 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";
+        }
+
+        @Override
+        String toString();
+
+        @Override
+        default Name name() {
+            return name;
+        }
+
+    }
+
+    /**
+     * 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;
+    }
+
+    /**
+     * 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

@@ -9,22 +9,19 @@
 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;
 
 /**
- * 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 +34,31 @@ 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 ExternalSolverRule newRule() {
+            return new SMTRule();
+        }
+
+        @Override
         public SMTRuleApp createApp(String successfulSolverName) {
             return new SMTRuleApp(this, null, successfulSolverName);
         }
@@ -81,6 +70,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 +81,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.
@@ -115,16 +98,12 @@ public ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp)
             return goal.split(1);
         }
 
-        @Override
-        public boolean isApplicableOnSubTerms() {
-            return false;
-        }
-
         @Override
         public String displayName() {
             return "SMT";
         }
 
+        @Override
         public String toString() {
             return displayName();
         }
@@ -133,9 +112,9 @@ public String toString() {
         public Name name() {
             return name;
         }
-
     }
 
+    @Override
     public SMTRuleApp setTitle(String title) {
         return new SMTRuleApp(RULE, pio, ifInsts, title);
     }
@@ -168,5 +147,4 @@ public SMTRuleApp tryToInstantiate(Goal goal) {
         }
         return app.setIfInsts(ImmutableList.fromList(ifInsts));
     }
-
 }

key.ui/build.gradle

@@ -33,6 +33,7 @@ dependencies {
     runtimeOnly project(":keyext.exploration")
     runtimeOnly project(":keyext.slicing")
     runtimeOnly project(":keyext.proofmanagement")
+    runtimeOnly project(":keyext.isabelletranslation")
 }
 
 task createExamplesZip(type: Zip) {

keyext.isabelletranslation/build.gradle

@@ -0,0 +1,7 @@
+description "Translation of Sequents to Isabelle"
+
+dependencies {
+    implementation project(':key.core')
+    implementation project(':key.ui')
+    implementation("de.unruh:scala-isabelle_2.13:0.4.3-RC1")
+}