Proof caching: external database

key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java

@@ -4,6 +4,7 @@
 package de.uka.ilkd.key.control;
 
 import java.io.File;
+import java.nio.file.Path;
 import java.util.List;
 import java.util.Properties;
 import java.util.function.Consumer;
@@ -298,7 +299,19 @@ public static KeYEnvironment<DefaultUserInterfaceControl> load(File keyFile)
     }
 
     /**
-     * Disposes this {@link KeYEnvironment}.
+     * Load a proof from the specified file.
+     *
+     * @param keyFile file to load
+     * @return environment with loaded proof
+     * @throws ProblemLoaderException on error during proof loading
+     */
+    public static KeYEnvironment<DefaultUserInterfaceControl> load(Path keyFile)
+            throws ProblemLoaderException {
+        return load(keyFile.toFile());
+    }
+
+    /**
+     * Disposes this {@link KeYEnvironment} by disposing the loaded proof.
      */
     public void dispose() {
         if (loadedProof != null && !loadedProof.isDisposed()) {

key.core/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachedFile.java

@@ -0,0 +1,16 @@
+/* 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.gui.plugins.caching;
+
+import java.nio.file.Path;
+
+/**
+ * A file used by some cached proof as part of the {@link CachingDatabase}.
+ *
+ * @param file path to the file (always located in ~/.key/cachedProofs)
+ * @param hash {@link String#hashCode()} of this file's content
+ * @author Arne Keller
+ */
+public record CachedFile(Path file, int hash) {
+}

key.core/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachedProofBranch.java

@@ -0,0 +1,213 @@
+/* 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.gui.plugins.caching;
+
+import java.nio.file.Path;
+import java.util.*;
+
+import de.uka.ilkd.key.java.Services;
+import de.uka.ilkd.key.logic.Sequent;
+import de.uka.ilkd.key.pp.LogicPrinter;
+
+/**
+ * Data object about a proof branch cached on disk.
+ *
+ * @author Arne Keller
+ */
+public class CachedProofBranch {
+
+    /**
+     * File the cached proof is stored in.
+     */
+    public final Path proofFile;
+    /**
+     * Name of the cached proof.
+     */
+    public final String proofName;
+    /**
+     * The choice settings used in the proof.
+     */
+    public final String choiceSettings;
+    /**
+     * KeY version used to create the proof.
+     */
+    public final String keyVersion;
+    /**
+     * Step index of the cached branch.
+     */
+    public final int stepIndex;
+
+    /**
+     * Referenced files the proof depends on.
+     */
+    private final Collection<CachedFile> referencedFiles;
+    /**
+     * Java classes the proof loaded.
+     */
+    private final List<String> javaClasses;
+    /**
+     * Antecedent part of the sequent of the cached branch.
+     */
+    private final List<String> sequentAnte;
+    /**
+     * Succedent part of the sequent of the cached branch.
+     */
+    private final List<String> sequentSucc;
+    /**
+     * Types of the functions present on the sequent.
+     */
+    private final Map<String, String> typesFunctions;
+    /**
+     * Types of the location variables present on the sequent.
+     */
+    private final Map<String, String> typesLocVars;
+
+    /**
+     * Create a new data object about a cached proof branch.
+     *
+     * @param proofFile the file the proof is stored in
+     * @param proofName the name of the cached proof
+     * @param referencedFiles java/key files referenced by the proof
+     * @param keyVersion KeY version used to save the proof
+     * @param choiceSettings choice settings of the proof
+     * @param stepIndex step index of the referenced node
+     * @param sequent sequent of that node
+     * @param services services of that node's proof
+     * @param javaClasses java classes the proof loaded
+     */
+    public CachedProofBranch(Path proofFile, String proofName,
+            Collection<CachedFile> referencedFiles,
+            String choiceSettings,
+            String keyVersion,
+            int stepIndex, Sequent sequent, Services services, List<String> javaClasses) {
+        this.proofFile = proofFile;
+        this.proofName = proofName;
+        this.referencedFiles = referencedFiles;
+        this.keyVersion = keyVersion;
+        this.choiceSettings = choiceSettings;
+        this.stepIndex = stepIndex;
+        this.sequentAnte = new ArrayList<>();
+        var ante = sequent.antecedent();
+        for (int i = 0; i < ante.size(); i++) {
+            sequentAnte.add(
+                LogicPrinter.quickPrintTerm(ante.get(i).formula(), services, true, false, false));
+        }
+        this.sequentSucc = new ArrayList<>();
+        var succ = sequent.succedent();
+        for (int i = 0; i < succ.size(); i++) {
+            sequentSucc.add(
+                LogicPrinter.quickPrintTerm(succ.get(i).formula(), services, true, false, false));
+        }
+        var typeCollector = new TypeCollectingVisitor();
+        typeCollector.visit(sequent);
+
+        this.typesFunctions = typeCollector.getTypes();
+        this.typesLocVars = typeCollector.getTypesLocVars();
+        this.javaClasses = javaClasses;
+    }
+
+    /**
+     * Create a new data object about a cached proof branch.
+     *
+     * @param proofFile the file the proof is stored in
+     * @param proofName name of the cached proof
+     * @param referencedFiles files referenced by the proof
+     * @param choiceSettings choice settings of the proof
+     * @param keyVersion KeY version used to save the cached proof branch
+     * @param stepIndex step index of the referenced node
+     * @param sequentAnte antecedent part of the sequent of that node
+     * @param sequentSucc succedent part of the sequent of that node
+     * @param typesFunctions types of the functions present in the sequent
+     * @param typesLocVars types of the location variables present in the sequent
+     * @param javaClasses java classes the proof depends on
+     */
+    public CachedProofBranch(Path proofFile, String proofName,
+            Collection<CachedFile> referencedFiles,
+            String choiceSettings,
+            String keyVersion,
+            int stepIndex, List<String> sequentAnte, List<String> sequentSucc,
+            Map<String, String> typesFunctions,
+            Map<String, String> typesLocVars,
+            List<String> javaClasses) {
+        this.proofFile = proofFile;
+        this.proofName = proofName;
+        this.referencedFiles = referencedFiles;
+        this.keyVersion = keyVersion;
+        this.choiceSettings = choiceSettings;
+        this.stepIndex = stepIndex;
+        this.sequentAnte = sequentAnte;
+        this.sequentSucc = sequentSucc;
+        this.typesFunctions = typesFunctions;
+        this.typesLocVars = typesLocVars;
+        this.javaClasses = javaClasses;
+    }
+
+    /**
+     * Determine whether this cached proof branch can be used to close the provided sequent.
+     * Returns true if the provided formulas are a superset of this branch.
+     *
+     * @param anteFormulas antecedent
+     * @param succFormulas succedent
+     * @param sequent the sequent
+     * @return whether this cached proof branch can close the new proof branch
+     */
+    public boolean isCacheHitFor(Set<String> anteFormulas, Set<String> succFormulas,
+            Sequent sequent) {
+        var typeCollector = new TypeCollectingVisitor();
+        typeCollector.visit(sequent);
+        for (var entry : typeCollector.getTypes().entrySet()) {
+            var ourType = typesFunctions.get(entry.getKey());
+            if (ourType == null) {
+                continue;
+            }
+            if (!ourType.equals(entry.getValue())) {
+                return false;
+            }
+        }
+        for (var entry : typeCollector.getTypesLocVars().entrySet()) {
+            var ourType = typesLocVars.get(entry.getKey());
+            if (ourType == null) {
+                continue;
+            }
+            if (!ourType.equals(entry.getValue())) {
+                return false;
+            }
+        }
+        for (var ante : sequentAnte) {
+            if (!anteFormulas.contains(ante)) {
+                return false;
+            }
+        }
+        for (var succ : sequentSucc) {
+            if (!succFormulas.contains(succ)) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    public Map<String, String> getTypesFunctions() {
+        return Collections.unmodifiableMap(typesFunctions);
+    }
+
+    public Map<String, String> getTypesLocVars() {
+        return Collections.unmodifiableMap(typesLocVars);
+    }
+
+    public Collection<CachedFile> getReferencedFiles() {
+        return Collections.unmodifiableCollection(referencedFiles);
+    }
+
+    public List<String> getSequentAnte() {
+        return Collections.unmodifiableList(sequentAnte);
+    }
+
+    public List<String> getSequentSucc() {
+        return Collections.unmodifiableList(sequentSucc);
+    }
+
+    public List<String> getJavaClasses() {
+        return Collections.unmodifiableList(javaClasses);
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/gui/plugins/caching/TypeCollectingVisitor.java

@@ -0,0 +1,56 @@
+/* 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.gui.plugins.caching;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import de.uka.ilkd.key.logic.Sequent;
+import de.uka.ilkd.key.logic.Term;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+
+import org.key_project.logic.Visitor;
+import org.key_project.logic.op.Function;
+
+public class TypeCollectingVisitor implements Visitor<Term> {
+    private final Map<String, String> types = new HashMap<>();
+    private final Map<String, String> typesLocVars = new HashMap<>();
+
+    public void visit(Sequent sequent) {
+        for (int i = 1; i <= sequent.size(); i++) {
+            var f = sequent.getFormulabyNr(i);
+            f.formula().execPreOrder(this);
+        }
+    }
+
+    @Override
+    public void visit(Term visited) {
+        var op = visited.op();
+        if (op instanceof Function function) {
+            types.put(function.name().toString(), function.argsToString());
+        }
+        if (op instanceof LocationVariable locationVariable) {
+            typesLocVars.put(locationVariable.name().toString(),
+                locationVariable.getKeYJavaType().toString());
+        }
+    }
+
+    @Override
+    public void subtreeEntered(Term subtreeRoot) {
+
+    }
+
+    @Override
+    public void subtreeLeft(Term subtreeRoot) {
+
+    }
+
+    public Map<String, String> getTypes() {
+        return types;
+    }
+
+    public Map<String, String> getTypesLocVars() {
+        return typesLocVars;
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java

@@ -119,8 +119,8 @@ public PosTableLayouter layouter() {
         return layouter;
     }
 
-    public static SequentViewLogicPrinter quickPrinter(Services services,
-            boolean usePrettyPrinting, boolean useUnicodeSymbols) {
+    private static SequentViewLogicPrinter quickPrinter(Services services,
+            boolean usePrettyPrinting, boolean useUnicodeSymbols, boolean printLabels) {
         final NotationInfo ni = new NotationInfo();
         if (services != null) {
             ni.refresh(services, usePrettyPrinting, useUnicodeSymbols);
@@ -129,7 +129,9 @@ public static SequentViewLogicPrinter quickPrinter(Services services,
         // Use a SequentViewLogicPrinter instead of a plain LogicPrinter,
         // because the SequentViewLogicPrinter respects default TermLabel visibility
         // settings.
-        return SequentViewLogicPrinter.purePrinter(ni, services, new TermLabelVisibilityManager());
+        var visibilityManager = new TermLabelVisibilityManager();
+        visibilityManager.setShowLabels(printLabels);
+        return SequentViewLogicPrinter.purePrinter(ni, services, visibilityManager);
     }
 
     /**
@@ -141,7 +143,7 @@ public static SequentViewLogicPrinter quickPrinter(Services services,
      */
     public static String quickPrintTerm(Term t, Services services) {
         return quickPrintTerm(t, services, NotationInfo.DEFAULT_PRETTY_SYNTAX,
-            NotationInfo.DEFAULT_UNICODE_ENABLED);
+            NotationInfo.DEFAULT_UNICODE_ENABLED, true);
     }
 
     /**
@@ -151,11 +153,12 @@ public static String quickPrintTerm(Term t, Services services) {
      * @param services services.
      * @param usePrettyPrinting whether to use pretty-printing.
      * @param useUnicodeSymbols whether to use unicode symbols.
+     * @param printLabels whether to print labels.
      * @return the printed term.
      */
     public static String quickPrintTerm(Term t, Services services, boolean usePrettyPrinting,
-            boolean useUnicodeSymbols) {
-        var p = quickPrinter(services, usePrettyPrinting, useUnicodeSymbols);
+            boolean useUnicodeSymbols, boolean printLabels) {
+        var p = quickPrinter(services, usePrettyPrinting, useUnicodeSymbols, printLabels);
         p.printTerm(t);
         return p.result();
     }
@@ -169,7 +172,7 @@ public static String quickPrintTerm(Term t, Services services, boolean usePretty
      */
     public static String quickPrintSemisequent(Semisequent s, Services services) {
         var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX,
-            NotationInfo.DEFAULT_UNICODE_ENABLED);
+            NotationInfo.DEFAULT_UNICODE_ENABLED, true);
         p.printSemisequent(s);
         return p.result();
     }
@@ -183,7 +186,7 @@ public static String quickPrintSemisequent(Semisequent s, Services services) {
      */
     public static String quickPrintSequent(Sequent s, Services services) {
         var p = quickPrinter(services, NotationInfo.DEFAULT_PRETTY_SYNTAX,
-            NotationInfo.DEFAULT_UNICODE_ENABLED);
+            NotationInfo.DEFAULT_UNICODE_ENABLED, true);
         p.printSequent(s);
         return p.result();
     }

key.core/src/main/java/de/uka/ilkd/key/pp/NotationInfo.java

@@ -100,8 +100,8 @@ public final class NotationInfo {
 
     public static boolean DEFAULT_PRETTY_SYNTAX = true;
     /**
-     * Whether the very fancy notation is enabled in which Unicode characters for logical operators
-     * are printed.
+     * Whether the very fancy notation is enabled by default in which Unicode characters for logical
+     * operators are printed.
      */
     public static boolean DEFAULT_UNICODE_ENABLED = false;