Fix for a performance regression (#3607)

Author: unp1

key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java

@@ -126,9 +126,9 @@ private void initIfChoiceModels() {
 
         if (size > 0) {
             ImmutableArray<AssumesFormulaInstantiation> antecCand =
-                AssumesFormulaInstSeq.createList(seq, true);
+                AssumesFormulaInstSeq.createList(seq, true, services);
             ImmutableArray<AssumesFormulaInstantiation> succCand =
-                AssumesFormulaInstSeq.createList(seq, false);
+                AssumesFormulaInstSeq.createList(seq, false, services);
 
             Iterator<SequentFormula> it = ifseq.iterator();
             Term ifFma;

key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java

@@ -12,7 +12,6 @@
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.TermTacletAppIndex;
 import de.uka.ilkd.key.proof.TermTacletAppIndexCacheSet;
-import de.uka.ilkd.key.rule.AssumesFormulaInstantiationCache;
 import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial;
 import de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial;
 import de.uka.ilkd.key.strategy.IfInstantiationCachePool;
@@ -24,6 +23,8 @@
 
 import org.key_project.logic.op.Operator;
 import org.key_project.logic.sort.Sort;
+import org.key_project.prover.proof.SessionCaches;
+import org.key_project.prover.rules.instantiation.caches.AssumesFormulaInstantiationCache;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.strategy.costbased.RuleAppCost;
 import org.key_project.util.LRUCache;
@@ -69,7 +70,7 @@
  *
  * @author Martin Hentschel
  */
-public class ServiceCaches {
+public class ServiceCaches implements SessionCaches {
     /**
      * The maximal number of index entries in {@link #getTermTacletAppIndexCache()}.
      */
@@ -221,7 +222,7 @@ public final IfInstantiationCachePool getIfInstantiationCache() {
         return ifInstantiationCache;
     }
 
-    public final AssumesFormulaInstantiationCache getIfFormulaInstantiationCache() {
+    public final AssumesFormulaInstantiationCache getAssumesFormulaInstantiationCache() {
         return assumesFormulaInstantiationCache;
     }
 

key.core/src/main/java/de/uka/ilkd/key/java/Services.java

@@ -21,14 +21,15 @@
 
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.Name;
+import org.key_project.prover.proof.ProofServices;
 import org.key_project.util.lookup.Lookup;
 
 /**
  * This is a collection of common services to the KeY prover. Services include information on the
  * underlying Java model and a converter to transform Java program elements to logic (where
  * possible) and back.
  */
-public class Services implements TermServices, LogicServices {
+public class Services implements TermServices, LogicServices, ProofServices {
     /**
      * the proof
      */

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

@@ -859,8 +859,8 @@ public ImmutableList<TacletApp> findIfFormulaInstantiations(Sequent seq, Service
         return findIfFormulaInstantiationsHelp(
             createSemisequentList(taclet().assumesSequent().succedent()),
             createSemisequentList(taclet().assumesSequent().antecedent()),
-            AssumesFormulaInstSeq.createList(seq, false),
-            AssumesFormulaInstSeq.createList(seq, true),
+            AssumesFormulaInstSeq.createList(seq, false, services),
+            AssumesFormulaInstSeq.createList(seq, true, services),
             ImmutableSLList.nil(), matchConditions(), services);
     }
 

key.core/src/main/java/de/uka/ilkd/key/strategy/AssumesInstantiator.java

@@ -73,8 +73,8 @@ public void findAssumesFormulaInstantiations() {
             addResult(tacletAppContainer.getTacletApp());
         } else {
             final Services services = getServices();
-            allAntecFormulas = AssumesFormulaInstSeq.createList(p_seq, true);
-            allSuccFormulas = AssumesFormulaInstSeq.createList(p_seq, false);
+            allAntecFormulas = AssumesFormulaInstSeq.createList(p_seq, true, services);
+            allSuccFormulas = AssumesFormulaInstSeq.createList(p_seq, false, services);
             findIfFormulaInstantiationsHelp(ifSequent.succedent().asList().reverse(), //// Matching
                                                                                       //// with the
                                                                                       //// last

key.ncore.calculus/src/main/java/org/key_project/prover/proof/ProofServices.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 org.key_project.prover.proof;
+
+/**
+ * provides access to services related to proof search
+ */
+public interface ProofServices {
+    /**
+     * provides access to the caching infrastructure of a proof session
+     *
+     * @return the caches used during proof search
+     */
+    SessionCaches getCaches();
+}

key.ncore.calculus/src/main/java/org/key_project/prover/proof/SessionCaches.java

@@ -0,0 +1,18 @@
+/* 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 org.key_project.prover.proof;
+
+import org.key_project.prover.rules.instantiation.caches.AssumesFormulaInstantiationCache;
+
+/**
+ * Provides access to caches used during proof search
+ */
+public interface SessionCaches {
+    /**
+     * returns the cache relevant for matching assumes formulas
+     *
+     * @return the cache relevant for matching assumes formulas
+     */
+    AssumesFormulaInstantiationCache getAssumesFormulaInstantiationCache();
+}

key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/AssumesFormulaInstSeq.java

@@ -5,6 +5,8 @@
 
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.PosInTerm;
+import org.key_project.prover.proof.ProofServices;
+import org.key_project.prover.rules.instantiation.caches.AssumesFormulaInstantiationCache;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.Semisequent;
 import org.key_project.prover.sequent.Sequent;
@@ -58,15 +60,9 @@ public String toString(LogicServices services) {
     /**
      * Create a list with all formulas of a given semi-sequent
      */
-    public static ImmutableArray<AssumesFormulaInstantiation> createList(Sequent p_s,
+    private static ImmutableArray<AssumesFormulaInstantiation> createListHelp(Sequent p_s,
+            Semisequent semi,
             boolean inAntecedent) {
-        Semisequent semi;
-        if (inAntecedent) {
-            semi = p_s.antecedent();
-        } else {
-            semi = p_s.succedent();
-        }
-
         final AssumesFormulaInstSeq[] assumesInstFromSeq =
             new AssumesFormulaInstSeq[semi.size()];
         int i = assumesInstFromSeq.length - 1;
@@ -79,6 +75,26 @@ public static ImmutableArray<AssumesFormulaInstantiation> createList(Sequent p_s
         return new ImmutableArray<>(assumesInstFromSeq);
     }
 
+    /**
+     * Retrieves a list with all formulas of a given semi-sequent
+     */
+    public static ImmutableArray<AssumesFormulaInstantiation> createList(Sequent p_s,
+            boolean inAntecedent,
+            ProofServices services) {
+        final AssumesFormulaInstantiationCache cache =
+            services.getCaches().getAssumesFormulaInstantiationCache();
+        final Semisequent semi = inAntecedent ? p_s.antecedent() : p_s.succedent();
+
+        ImmutableArray<AssumesFormulaInstantiation> val = cache.get(inAntecedent, semi);
+
+        if (val == null) {
+            val = createListHelp(p_s, semi, inAntecedent);
+            cache.put(inAntecedent, semi, val);
+        }
+
+        return val;
+    }
+
     @Override
     public String toString() {
         return toString(null);

…le/AssumesFormulaInstantiationCache.java …es/AssumesFormulaInstantiationCache.javakey.core/src/main/java/de/uka/ilkd/key/rule/AssumesFormulaInstantiationCache.java renamed to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/caches/AssumesFormulaInstantiationCache.java key.core/src/main/java/de/uka/ilkd/key/rule/AssumesFormulaInstantiationCache.java renamed to key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/caches/AssumesFormulaInstantiationCache.java

@@ -1,7 +1,7 @@
 /* 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;
+package org.key_project.prover.rules.instantiation.caches;
 
 import java.util.concurrent.locks.ReentrantReadWriteLock;
 import java.util.concurrent.locks.ReentrantReadWriteLock.ReadLock;