Formalize LocSet as Set of Locations

key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdGeneralRules.key

@@ -2,6 +2,10 @@
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
 
+\sorts {
+    \generic E1, E2;
+}
+
 \schemaVariables {
     \formula f;
     \term any s, t;
@@ -149,12 +153,13 @@
     };
 
     wd_Pair {
-
+        \schemaVar \term E1 e1;
+        \schemaVar \term E2 e2;
         \find(
-            wd(pair(s, t))
+            wd(pair<E1,E2>(e1, e2))
         )
         \replacewith(
-            wd(s) & wd(t)
+            wd(e1) & wd(e2)
         )
         \heuristics(simplify)
     };

key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdLocSetRules.key

@@ -2,6 +2,10 @@
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
 
+\sorts {
+    \generic E;
+}
+
 \schemaVariables {
     \term int i, j;
     \term Heap h;
@@ -11,6 +15,8 @@
     \term Object o;
     \term Field f;
     \term LocSet l, s;
+    \term E e;
+    \term Set<E> s1, s2;
 }
 
 \rules(wdChecks:on) {
@@ -67,7 +73,7 @@
     wd_LocSet_Singleton {
 
         \find(
-            wd(singleton(o, f))
+            wd(singleton<Loc>(pair<Object,Field>(o, f)))
         )
         \varcond(
             \not \isArray(o),
@@ -82,7 +88,7 @@
     wd_LocSet_Singleton_Static {
 
         \find(
-            wd(singleton(o, f))
+            wd(singleton<Loc>(pair<Object,Field>(o, f)))
         )
         \varcond(
             \not \isArray(o),
@@ -97,7 +103,7 @@
     wd_LocSet_Singleton_Arr {
 
         \find(
-            wd(singleton(o, arr(i)))
+            wd(singleton<Loc>(pair<Object,Field>(o, arr(i))))
         )
         \varcond(
             \isArray(o)
@@ -111,7 +117,7 @@
     wd_LocSet_Singleton_Quant {
 
         \find(
-            \forall c; wd(singleton(o, f))
+            \forall c; wd(singleton<Loc>(pair<Object,Field>(o, f)))
         )
         \varcond(
             \not \isArray(o)
@@ -125,31 +131,31 @@
     wd_LocSet_Union {
 
         \find(
-            wd(union(l, s))
+            wd(union<E>(s1, s2))
         )
         \replacewith(
-            wd(l) & wd(s)
+            wd(s1) & wd(s2)
         )
         \heuristics(simplify)
     };
 
     wd_LocSet_Intersect {
         \find(
-            wd(intersect(l, s))
+            wd(intersect<E>(s1, s2))
         )
         \replacewith(
-            wd(l) & wd(s)
+            wd(s1) & wd(s2)
         )
         \heuristics(simplify)
     };
 
     wd_LocSet_Diff {
 
         \find(
-            wd(setMinus(l, s))
+            wd(setMinus<E>(s1, s2))
         )
         \replacewith(
-            wd(l) & wd(s)
+            wd(s1) & wd(s2)
         )
         \heuristics(simplify)
     };
@@ -201,21 +207,21 @@
     wd_LocSet_InfiniteUnion {
 
         \find(
-            wd(infiniteUnion{a;}(l))
+            wd(infiniteUnion<E>{a;}(s1))
         )
         \replacewith(
-            \forall a; wd(l)
+            \forall a; wd(s1)
         )
         \heuristics(simplify)
     };
 
     wd_LocSet_InfiniteUnion2 {
 
         \find(
-            wd(infiniteUnion{a, b;}(l))
+            wd(infiniteUnion<E>{a, b;}(s1))
         )
         \replacewith(
-            \forall a; (\forall b; wd(l))
+            \forall a; (\forall b; wd(s1))
         )
         \heuristics(simplify)
         \displayname "wd_LocSet_InfiniteUnion"
@@ -224,7 +230,7 @@
     wd_LocSet_Pred_ElementOf {
 
         \find(
-            WD(elementOf(o, f, l))
+            WD(elementOf<Loc>(pair<Object,Field>(o, f), l))
         )
         \varcond(
             \not \isStaticField(f)
@@ -238,7 +244,7 @@
     wd_LocSet_Pred_ElementOf_Static {
 
         \find(
-            WD(elementOf(o, f, l))
+            WD(elementOf<Loc>(pair<Object,Field>(o, f), l))
         )
         \varcond(
             \isStaticField(f)
@@ -252,20 +258,20 @@
     wd_LocSet_Pred_Subset {
 
         \find(
-            WD(subset(l, s))
+            WD(subset<E>(s1, s2))
         )
         \replacewith(
-            wd(l) & wd(s)
+            wd(s1) & wd(s2)
         )
         \heuristics(simplify)
     };
 
     wd_LocSet_Pred_Disjoint {
         \find(
-            WD(disjoint(l, s))
+            WD(disjoint<E>(s1, s2))
         )
         \replacewith(
-            wd(l) & wd(s)
+            wd(s1) & wd(s2)
         )
         \heuristics(simplify)
     };

key.core/build.gradle

@@ -402,7 +402,7 @@ tasks.register("testRAP", Test) {
 
     forkEvery = 1
     // run the regression proofs on up to 10 parallel JVMs (overridable with -PrapForks=N)
-    maxParallelForks = (project.findProperty('rapForks') ?: '10') as int
+    maxParallelForks = (project.findProperty('rapForks') ?: '4') as int
     useJUnitPlatform()
     it.filter {
         it.includeTestsMatching "de.uka.ilkd.key.proof.runallproofs.gen.*"

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

@@ -4,7 +4,6 @@
 package de.uka.ilkd.key.java;
 
 
-import java.util.Collection;
 import java.util.HashMap;
 import java.util.Map;
 import java.util.TreeMap;
@@ -47,13 +46,14 @@ public final class TypeConverter {
     // 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<>();
+    private final Map<Name, ParametricLDT> PLDTs = 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<>();
+    private final Map<Class<? extends AbstractLDT>, AbstractLDT> ldtsByClass = new HashMap<>();
 
     /** the heap theory, kept directly because this class itself uses it throughout */
     private HeapLDT heapLDT = null;
@@ -64,15 +64,19 @@ public final class TypeConverter {
     }
 
     public void init() {
-        init(LDT.getNewLDTInstances(services));
+        init(LDT.getNewLDTInstances(services), ParametricLDT.getNewLDTInstances(services));
     }
 
-    private void init(Map<Name, LDT> map) {
+    private void init(Map<Name, LDT> map, Map<Name, ParametricLDT> pMap) {
         LDTs.putAll(map);
         for (LDT ldt : map.values()) {
             ldtsByClass.put(ldt.getClass(), ldt);
         }
         heapLDT = getLDT(HeapLDT.class);
+        PLDTs.putAll(pMap);
+        for (ParametricLDT ldt : pMap.values()) {
+            ldtsByClass.put(ldt.getClass(), ldt);
+        }
     }
 
     /**
@@ -83,7 +87,7 @@ private void init(Map<Name, LDT> map) {
      * @return the theory instance of that class
      * @param <T> the type of the theory
      */
-    public <T extends LDT> T getLDT(Class<T> ldtClass) {
+    public <T extends AbstractLDT> T getLDT(Class<T> ldtClass) {
         return ldtClass.cast(ldtsByClass.get(ldtClass));
     }
 
@@ -98,10 +102,6 @@ public LDT getLDTFor(Sort s) {
         return null;
     }
 
-    private LDT getLDT(Name ldtName) {
-        return LDTs.get(ldtName);
-    }
-
     public JavaDLTheory getJavaDLTheory() {
         return getLDT(JavaDLTheory.class);
     }
@@ -156,12 +156,7 @@ public CharListLDT getCharListLDT() {
         return getLDT(CharListLDT.class);
     }
 
-    public Collection<LDT> getLDTs() {
-        return LDTs.values();
-    }
-
     private JTerm translateOperator(Operator op, ExecutionContext ec) {
-
         final JTerm[] subs = new JTerm[op.getArity()];
         for (int i = 0, n = op.getArity(); i < n; i++) {
             subs[i] = convertToLogicElement(op.getExpressionAt(i), ec);
@@ -176,7 +171,7 @@ private JTerm translateOperator(Operator op, ExecutionContext ec) {
             }
         }
 
-        LDT responsibleLDT = getResponsibleLDT(op, subs, services, ec);
+        AbstractLDT responsibleLDT = getResponsibleLDT(op, subs, services, ec);
         if (responsibleLDT != null) {
             return tb.func(responsibleLDT.getFunctionFor(op, services, ec), subs);
         } else if (op instanceof BinaryOperator bo
@@ -393,9 +388,11 @@ private JTerm convertLiteralExpression(Literal lit) {
         if (lit instanceof NullLiteral) {
             return tb.NULL();
         } else {
-            LDT ldt = LDTs.get(lit.getLDTName());
+            AbstractLDT ldt = LDTs.get(lit.getLDTName());
             if (ldt != null) {
                 return ldt.translateLiteral(lit, services);
+            } else if ((ldt = PLDTs.get(lit.getLDTName())) != null) {
+                return ldt.translateLiteral(lit, services);
             } else {
                 Debug.fail("Unknown literal type", lit);
                 return null;
@@ -563,6 +560,11 @@ public Expression convertToProgramElement(JTerm term) {
                     return model.translateTerm(term, null, services);
                 }
             }
+            for (ParametricLDT model : PLDTs.values()) {
+                if (model.hasLiteralFunction(function)) {
+                    return model.translateTerm(term, null, services);
+                }
+            }
         }
 
         final ExtList children = new ExtList();
@@ -578,6 +580,11 @@ public Expression convertToProgramElement(JTerm term) {
                     return model.translateTerm(term, children, services);
                 }
             }
+            for (ParametricLDT model : PLDTs.values()) {
+                if (model.containsFunction(function)) {
+                    return model.translateTerm(term, children, services);
+                }
+            }
             Expression tryTranslate = translateJavaCast(term, children);
             if (tryTranslate != null) {
                 return tryTranslate;
@@ -982,17 +989,22 @@ public boolean isBooleanType(Type t) {
 
     public TypeConverter copy(Services services) {
         TypeConverter TC = new TypeConverter(services);
-        TC.init(LDTs);
+        TC.init(LDTs, PLDTs);
         return TC;
     }
 
-    private LDT getResponsibleLDT(Operator op, JTerm[] subs,
+    private AbstractLDT getResponsibleLDT(Operator op, JTerm[] subs,
             Services services, ExecutionContext ec) {
         for (LDT ldt : LDTs.values()) {
             if (ldt.isResponsible(op, subs, services, ec)) {
                 return ldt;
             }
         }
+        for (ParametricLDT ldt : PLDTs.values()) {
+            if (ldt.isResponsible(op, subs, services, ec)) {
+                return ldt;
+            }
+        }
         return null;
     }
 }