Improve reasoning about heaps

key.core/build.gradle

@@ -412,6 +412,11 @@ tasks.register("testRAP", Test) {
     systemProperty 'key.matcher.compiled',
         (project.findProperty('matcher.compiled')
                 ?: System.getProperty('key.matcher.compiled', 'false'))
+    // forward the cost-reuse verification switch to the proof runs in each fork; default off,
+    // enable with -PcostReuse.verify=true (or -Dkey.strategy.costReuse.verify=true)
+    systemProperty 'key.strategy.costReuse.verify',
+        (project.findProperty('costReuse.verify')
+                ?: System.getProperty('key.strategy.costReuse.verify', 'false'))
     // (statistics are always written per-process, <statisticsFile>.<pid>.csv; see
     // ProveTest.getStatisticsFile -- combine the per-fork files after the run.)
     // set heap size for the test JVM(s) (overridable with -PrapHeap=8g for the large examples)

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

@@ -31,6 +31,7 @@
 import org.key_project.prover.rules.Taclet;
 import org.key_project.prover.rules.instantiation.caches.AssumesFormulaInstantiationCache;
 import org.key_project.prover.sequent.PosInOccurrence;
+import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.ConcurrentLruCache;
 import org.key_project.util.collection.ImmutableSet;
 import org.key_project.util.collection.Pair;
@@ -140,6 +141,17 @@ public class ServiceCaches implements SessionCaches {
     private final Map<org.key_project.logic.Term, TriggersSet> triggerSetCache =
         new ConcurrentLruCache<>(1000);
 
+    /**
+     * Per-formula operator-occurrence summary for the quantifier instantiation tie-break (which
+     * operators occur in a sequent formula, and which at proving polarity). A sequent step
+     * replaces few formulas, and the {@link SequentFormula} objects
+     * are immutable and shared across the sequents of a branch, so the summary is memoised per
+     * formula rather than recomputed per sequent. The value is opaque here (an
+     * {@code Instantiation.OccInfo}) to keep this package independent of the strategy package.
+     */
+    private final Map<SequentFormula, Object> formulaOccurrenceCache =
+        new ConcurrentLruCache<>(10000);
+
     /**
      * Map from <code>Term</code>(allTerm) to <code>ClausesGraph</code>
      */
@@ -239,6 +251,10 @@ public final Map<org.key_project.logic.Term, Monomial> getMonomialCache() {
         return monomialCache;
     }
 
+    public final Map<SequentFormula, Object> getFormulaOccurrenceCache() {
+        return formulaOccurrenceCache;
+    }
+
     public final Map<org.key_project.logic.Term, Polynomial> getPolynomialCache() {
         return polynomialCache;
     }

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

@@ -5,6 +5,7 @@
 
 
 import java.util.Collection;
+import java.util.HashMap;
 import java.util.Map;
 import java.util.TreeMap;
 
@@ -44,11 +45,19 @@ public final class TypeConverter {
     private final TermBuilder tb;
     private final Services services;
 
-    // Maps LDT names to LDT instances.
+    // Maps LDT names to LDT instances. The map stays sorted by name so that getLDTFor visits
+    // the theories in a fixed order, independent of the run.
     private final Map<Name, LDT> LDTs = new TreeMap<>();
 
+    // The typed accessors below are called at high frequency from the proof-search strategy
+    // (for example by the arithmetic heuristics for every candidate weighing), so lookups go
+    // through this class-keyed map: a class hashes by identity, so a lookup costs no name
+    // comparison. The map is filled generically when the theories are created; adding a new
+    // theory needs no change in this class.
+    private final Map<Class<? extends LDT>, LDT> ldtsByClass = new HashMap<>();
+
+    /** the heap theory, kept directly because this class itself uses it throughout */
     private HeapLDT heapLDT = null;
-    // private IntegerLDT integerLDT = null;
 
     TypeConverter(Services s) {
         this.services = s;
@@ -61,8 +70,22 @@ public void init() {
 
     private void init(Map<Name, LDT> map) {
         LDTs.putAll(map);
-        heapLDT = getHeapLDT();
-        // integerLDT = getIntegerLDT();
+        for (LDT ldt : map.values()) {
+            ldtsByClass.put(ldt.getClass(), ldt);
+        }
+        heapLDT = getLDT(HeapLDT.class);
+    }
+
+    /**
+     * The theory of the given class, or {@code null} if no such theory is registered. Theories
+     * are looked up by their exact class.
+     *
+     * @param ldtClass the class of the theory
+     * @return the theory instance of that class
+     * @param <T> the type of the theory
+     */
+    public <T extends LDT> T getLDT(Class<T> ldtClass) {
+        return ldtClass.cast(ldtsByClass.get(ldtClass));
     }
 
 
@@ -81,55 +104,57 @@ private LDT getLDT(Name ldtName) {
     }
 
     public JavaDLTheory getJavaDLTheory() {
-        return (JavaDLTheory) getLDT(JavaDLTheory.NAME);
+        return getLDT(JavaDLTheory.class);
     }
 
     public IntegerLDT getIntegerLDT() {
-        return (IntegerLDT) getLDT(IntegerLDT.NAME);
+        return getLDT(IntegerLDT.class);
     }
 
     public FloatLDT getFloatLDT() {
-        return (FloatLDT) getLDT(FloatLDT.NAME);
+        return getLDT(FloatLDT.class);
     }
 
     public DoubleLDT getDoubleLDT() {
-        return (DoubleLDT) getLDT(DoubleLDT.NAME);
+        return getLDT(DoubleLDT.class);
     }
 
     public RealLDT getRealLDT() {
-        return (RealLDT) getLDT(RealLDT.NAME);
+        return getLDT(RealLDT.class);
     }
 
     public BooleanLDT getBooleanLDT() {
-        return (BooleanLDT) getLDT(BooleanLDT.NAME);
+        return getLDT(BooleanLDT.class);
     }
 
     public LocSetLDT getLocSetLDT() {
-        return (LocSetLDT) getLDT(LocSetLDT.NAME);
+        return getLDT(LocSetLDT.class);
     }
 
     public HeapLDT getHeapLDT() {
-        return (HeapLDT) getLDT(HeapLDT.NAME);
+        return heapLDT;
     }
 
+
+
     public PermissionLDT getPermissionLDT() {
-        return (PermissionLDT) getLDT(PermissionLDT.NAME);
+        return getLDT(PermissionLDT.class);
     }
 
     public SeqLDT getSeqLDT() {
-        return (SeqLDT) getLDT(SeqLDT.NAME);
+        return getLDT(SeqLDT.class);
     }
 
     public SortLDT getSortLDT() {
-        return (SortLDT) getLDT(SortLDT.NAME);
+        return getLDT(SortLDT.class);
     }
 
     public MapLDT getMapLDT() {
-        return (MapLDT) getLDT(MapLDT.NAME);
+        return getLDT(MapLDT.class);
     }
 
     public CharListLDT getCharListLDT() {
-        return (CharListLDT) getLDT(CharListLDT.NAME);
+        return getLDT(CharListLDT.class);
     }
 
     public Collection<LDT> getLDTs() {

key.core/src/main/java/de/uka/ilkd/key/java/ast/JavaNonTerminalProgramElement.java

@@ -89,10 +89,16 @@ public boolean equals(Object o) {
 
     @Override
     protected int computeHashCode() {
-        int localHash = 17 * super.computeHashCode();
+        // Fold the children with a multiplier that is 3 (mod 8): such a multiplier has maximal
+        // multiplicative order modulo 2^32, so its powers mix the low bits. The previous 17 is
+        // 1 (mod 16), so 17^n stayed 1 (mod 16) and barely moved the low bits -- structurally
+        // repetitive programs then accumulated near-linear low bits and collided into the same hash
+        // buckets. Equal programs still get equal hashes, so this only redistributes, never breaks.
+        final int mult = 0x01000193;
+        int localHash = mult * super.computeHashCode();
         for (int i = 0, sz = getChildCount(); i < sz; i++) {
             final ProgramElement pe = getChildAt(i);
-            localHash = 17 * localHash + (pe == null ? 0 : pe.hashCode());
+            localHash = mult * localHash + (pe == null ? 0 : pe.hashCode());
         }
         return localHash;
     }