Definitional Skolem constants

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java

@@ -53,6 +53,8 @@
 
 import org.jspecify.annotations.Nullable;
 
+import static org.key_project.logic.op.Function.FunctionKind.SKOLEM;
+
 /**
  * <p>
  * Rule for the application of {@link BlockContract}s.
@@ -115,8 +117,7 @@ protected ImmutableList<Goal> splitIntoGoals(final Goal goal, final BlockContrac
             final JTerm contextUpdate,
             final JTerm remembranceUpdate, final ImmutableSet<LocationVariable> localOutVariables,
             final GoalsConfigurator configurator, final Services services) {
-        final ImmutableList<Goal> result = goal.split(3);
-        return result;
+        return goal.split(3);
     }
 
     @Override
@@ -305,7 +306,7 @@ protected static ProofObligationVars generateProofObligationVariables(
 
         final JTerm heapAtPre = tb.var(variables.remembranceHeaps.get(baseHeap));
         final Name heapAtPostName = new Name(tb.newName("heap_After_BLOCK"));
-        final JTerm heapAtPost = tb.func(new JFunction(heapAtPostName, heapAtPre.sort(), true));
+        final JTerm heapAtPost = tb.func(new JFunction(heapAtPostName, heapAtPre.sort(), SKOLEM));
         final JTerm selfAtPre = hasSelf ? tb.var(variables.self) : tb.NULL();
         final JTerm selfAtPost = hasSelf ? buildAfterVar(selfAtPre, "BLOCK", services) : tb.NULL();
 

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java

@@ -45,6 +45,8 @@
 
 import org.jspecify.annotations.NullMarked;
 
+import static org.key_project.logic.op.Function.FunctionKind.SKOLEM;
+
 @NullMarked
 public class InfFlowWhileInvariantRule extends WhileInvariantRule {
     private static final Name NAME = new Name("InfFlow Loop Invariant");
@@ -177,7 +179,7 @@ private static InfFlowData prepareSetUpOfInfFlowValidityGoal(final Goal infFlowG
         HeapLDT heapLDT = services.getTypeConverter().getHeapLDT();
         Name heapAtPreName = new Name(tb.newName(baseHeap + "_Before_LOOP"));
         final Function heapAtPreFunc =
-            new JFunction(heapAtPreName, heapLDT.targetSort(), true);
+            new JFunction(heapAtPreName, heapLDT.targetSort(), SKOLEM);
         services.getNamespaces().functions().addSafely(heapAtPreFunc);
         final JTerm heapAtPre = tb.func(heapAtPreFunc);
 

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

@@ -383,8 +383,7 @@ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException {
                         // sv instanceof SkolemTermSV
                         final Named n = namespaces().lookupLogicSymbol(new Name(idd.name()));
                         if (n == null) {
-                            result = result.createSkolemConstant(idd.name(), sv, sort, true,
-                                services);
+                            result = result.createSkolemConstant(idd.name(), sv, sort, true, goal);
                         } else {
                             throw new SVInstantiationParserException(idd.name(),
                                 createPosition(irow),

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

@@ -26,7 +26,6 @@
 import de.uka.ilkd.key.strategy.quantifierHeuristics.Metavariable;
 import de.uka.ilkd.key.strategy.quantifierHeuristics.TriggersSet;
 
-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.Taclet;
@@ -81,11 +80,8 @@
  * whose
  * value could be recomputed to something different, after an eviction, under a different access
  * order; for those, approximate or striped eviction was observed to change proofs. Caches whose
- * value does not depend on access order do not need this (for example
- * {@link #introductionTimeCache},
- * whose value is the depth at which an operator was introduced below the proof root and is the same
- * for every goal beneath that point). The weak-keyed caches instead stay wrapped in
- * {@link Collections#synchronizedMap}.
+ * value does not depend on access order do not need this. The weak-keyed caches instead stay
+ * wrapped in {@link Collections#synchronizedMap}.
  * </p>
  *
  * @author Martin Hentschel
@@ -112,13 +108,6 @@ public class ServiceCaches implements SessionCaches {
         new ConcurrentLruCache<>(1000);
 
 
-    /**
-     * the introduction time cache used by {@code AbstractMonomialSmallerThanFeature} for Skolem
-     * constants
-     */
-    private final Map<Operator, Integer> introductionTimeCache =
-        new ConcurrentLruCache<>(10000);
-
     /**
      * Per-proof cache for {@code CostReuse}'s feature-locality classification (taclet -> its
      * reuse-eligibility verdict). Held here, like the other proof-scoped caches, so it is freed
@@ -237,14 +226,6 @@ public final Map<JTerm, TermInfo> getBetaCandidates() {
         return betaCandidates;
     }
 
-    /**
-     * returns the introduction time cache used by {@code AbstractMonomialSmallerThanFeature} for
-     * Skolem constants
-     */
-    public final Map<Operator, Integer> getIntroductionTimeCache() {
-        return introductionTimeCache;
-    }
-
     public final Map<Taclet, CostReuse.ConditionalEligibility> getCostReuseClassificationCache() {
         return costReuseClassificationCache;
     }

key.core/src/main/java/de/uka/ilkd/key/logic/op/JFunction.java

@@ -16,26 +16,42 @@
 import org.key_project.logic.sort.Sort;
 import org.key_project.util.collection.ImmutableArray;
 
+import static org.key_project.logic.op.Function.FunctionKind.ORDINARY;
+
 
 /**
  * Objects of this class represent function and predicate symbols in JavaDL. Note that program
- * variables are a
- * separate syntactic category, and not a type of function.
+ * variables are a separate syntactic category, and not a type of function.
  * <br>
  * <strong>As soon as {@link AbstractTermTransformer#METASORT} is generalized, this class
  * may be deleted.</strong>
  */
 public class JFunction extends Function implements Sorted, Operator {
 
-
     // -------------------------------------------------------------------------
     // constructors
     // -------------------------------------------------------------------------
 
+    /**
+     * Creates a function symbol with the specified signature and kind
+     *
+     * @param name the Name of the function symbol
+     * @param sort the Sort of the function symbol
+     * @param argSorts the Sorts of its parameters
+     * @param whereToBind if it is a binder the position where the bound variable is in scope (can
+     *        be used)
+     * @param unique a boolean indicating whether the symbol is unique
+     * @param kind the kind of the function symbol
+     * @param isRigid a boolean specifying whether the symbol is state depending (i.e., can have
+     *        different values
+     *        in different states)
+     * @param introductionTime the introduction time of the symbol, or a
+     *        {@link Function#UNRECORDED}, if none available (e.g. existed from the beginning)
+     */
     JFunction(Name name, Sort sort, ImmutableArray<Sort> argSorts,
             ImmutableArray<Boolean> whereToBind, boolean unique, boolean isRigid,
-            boolean isSkolemConstant) {
-        super(name, argSorts, sort, whereToBind, isRigid, unique, isSkolemConstant);
+            FunctionKind kind, int introductionTime) {
+        super(name, argSorts, sort, whereToBind, isRigid, unique, kind, introductionTime);
 
         assert sort != JavaDLTheory.UPDATE;
         assert !(unique && sort == JavaDLTheory.FORMULA);
@@ -45,12 +61,26 @@ public class JFunction extends Function implements Sorted, Operator {
 
     public JFunction(Name name, Sort sort, ImmutableArray<Sort> argSorts,
             ImmutableArray<Boolean> whereToBind, boolean unique) {
-        this(name, sort, argSorts, whereToBind, unique, true, false);
+        this(name, sort, argSorts, whereToBind, unique, true, ORDINARY, UNRECORDED);
     }
 
+    /**
+     * Creates a function symbol with the specified signature and kind
+     *
+     * @param name the Name of the function symbol
+     * @param sort the Sort of the function symbol
+     * @param argSorts the Sorts of its parameters
+     * @param whereToBind if it is a binder the position where the bound variable is in scope (can
+     *        be used)
+     * @param unique a boolean indicating whether the symbol is unique
+     * @param kind the kind of the function symbol
+     * @param introductionTime the introduction time of the symbol, or a
+     *        {@link Function#UNRECORDED}, if none available (e.g. existed from the beginning)
+     */
     public JFunction(Name name, Sort sort, ImmutableArray<Sort> argSorts,
-            ImmutableArray<Boolean> whereToBind, boolean unique, boolean isSkolemConstant) {
-        this(name, sort, argSorts, whereToBind, unique, true, isSkolemConstant);
+            ImmutableArray<Boolean> whereToBind, boolean unique, FunctionKind kind,
+            int introductionTime) {
+        this(name, sort, argSorts, whereToBind, unique, true, kind, introductionTime);
     }
 
     public JFunction(Name name, Sort sort, Sort[] argSorts, Boolean[] whereToBind,
@@ -59,16 +89,8 @@ public JFunction(Name name, Sort sort, Sort[] argSorts, Boolean[] whereToBind,
             whereToBind == null ? null : new ImmutableArray<>(whereToBind), unique);
     }
 
-    public JFunction(Name name, Sort sort, Sort[] argSorts, Boolean[] whereToBind,
-            boolean unique,
-            boolean isSkolemConstant) {
-        this(name, sort, new ImmutableArray<>(argSorts),
-            whereToBind == null ? null : new ImmutableArray<>(whereToBind), unique,
-            isSkolemConstant);
-    }
-
     JFunction(Name name, Sort sort, ImmutableArray<Sort> argSorts, boolean isRigid) {
-        this(name, sort, argSorts, null, false, isRigid, false);
+        this(name, sort, argSorts, null, false, isRigid, ORDINARY, UNRECORDED);
     }
 
     public JFunction(Name name, Sort sort, ImmutableArray<Sort> argSorts) {
@@ -79,16 +101,19 @@ public JFunction(Name name, Sort sort, Sort... argSorts) {
         this(name, sort, argSorts, null, false);
     }
 
-    public JFunction(Name name, Sort sort, boolean isSkolemConstant, Sort... argSorts) {
-        this(name, sort, argSorts, null, false, isSkolemConstant);
-    }
-
     public JFunction(Name name, Sort sort) {
         this(name, sort, new ImmutableArray<>(), null, false);
     }
 
-    public JFunction(Name name, Sort sort, boolean isSkolemConstant) {
-        this(name, sort, new ImmutableArray<>(), null, false, true, isSkolemConstant);
+    /**
+     * Creates a constant of the given kind
+     */
+    public JFunction(Name name, Sort sort, FunctionKind kind) {
+        this(name, sort, new ImmutableArray<>(), null, false, true, kind, UNRECORDED);
+    }
+
+    public JFunction(Name name, Sort sort, FunctionKind kind, int introductionTime) {
+        this(name, sort, new ImmutableArray<>(), null, false, true, kind, introductionTime);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java

@@ -22,6 +22,9 @@
 
 import org.jspecify.annotations.NonNull;
 
+import static org.key_project.logic.op.Function.FunctionKind.ORDINARY;
+import static org.key_project.logic.op.Function.FunctionKind.SKOLEM;
+
 /// A concrete instance of a [ParametricFunctionDecl].
 public class ParametricFunctionInstance extends JFunction {
     /**
@@ -52,8 +55,8 @@ public static ParametricFunctionInstance get(ParametricFunctionDecl decl,
     private ParametricFunctionInstance(ParametricFunctionDecl base,
             ImmutableList<GenericArgument> args, ImmutableArray<Sort> argSorts, Sort sort) {
         super(makeName(base, args), sort, argSorts, base.getWhereToBind(), base.isUnique(),
-            base.isRigid(),
-            base.isSkolemConstant());
+            base.isRigid(), base.isSkolemConstant() ? SKOLEM : ORDINARY,
+            UNRECORDED);
         this.base = base;
         this.args = args;
     }

key.core/src/main/java/de/uka/ilkd/key/logic/op/SchemaVariableFactory.java

@@ -96,7 +96,14 @@ public static ProgramSV createProgramSV(ProgramElementName name, ProgramSVSort s
      * creates a SchemaVariable representing a skolem term
      */
     public static SkolemTermSV createSkolemTermSV(Name name, Sort s) {
-        return new SkolemTermSV(name, s);
+        return new SkolemTermSV(name, s, false);
+    }
+
+    /**
+     * @param definitional whether the created constants are definitional symbols
+     */
+    public static SkolemTermSV createSkolemTermSV(Name name, Sort s, boolean definitional) {
+        return new SkolemTermSV(name, s, definitional);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java

@@ -16,18 +16,29 @@
  */
 public final class SkolemTermSV extends JOperatorSV implements TerminalSyntaxElement {
 
+    /** whether the constants created for this schema variable are definitional symbols */
+    private final boolean definitional;
+
     /**
      * Creates a new schema variable that is used as placeholder for skolem terms.
      *
      * @param name the Name of the SchemaVariable
      * @param sort the Sort of the SchemaVariable and the matched type allowed to match a list of
      *        program constructs
+     * @param definitional whether the created constants are definitional symbols, declared as
+     *        {@code \skolemTerm[definitional]}
      */
-    SkolemTermSV(Name name, Sort sort) {
+    SkolemTermSV(Name name, Sort sort, boolean definitional) {
         super(name, sort, true, false);
+        this.definitional = definitional;
         assert sort != JavaDLTheory.UPDATE;
     }
 
+    /** @return whether the constants created for this schema variable are definitional symbols */
+    public boolean isDefinitional() {
+        return definitional;
+    }
+
     @Override
     public boolean isSkolemTerm() {
         return true;

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java

@@ -114,8 +114,7 @@ public Object visitDatatype_decl(JavaKeYParser.Datatype_declContext ctx) {
                 }
                 if (genericParams == null) {
                     Function fn =
-                        new JFunction(new Name(argName), argSort, new Sort[] { sort }, null,
-                            false, false);
+                        new JFunction(new Name(argName), argSort, new Sort[] { sort }, null, false);
                     dtFnNamespace.add(fn);
                 } else {
                     var fn = new ParametricFunctionDecl(new Name(argName), genericParams,
@@ -124,7 +123,7 @@ public Object visitDatatype_decl(JavaKeYParser.Datatype_declContext ctx) {
                 }
             }
             if (genericParams == null) {
-                var fn = new JFunction(name, sort, args, null, true, false);
+                var fn = new JFunction(name, sort, args, null, true);
                 functions().addSafely(fn);
                 docsSpace().setDocumentation(fn, doc);
             } else {

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java

@@ -1233,7 +1233,8 @@ protected JOperatorSV declareSchemaVariable(ParserRuleContext ctx, String name,
             if (makeVariableSV) {
                 v = SchemaVariableFactory.createVariableSV(new Name(name), s);
             } else if (makeSkolemTermSV) {
-                v = SchemaVariableFactory.createSkolemTermSV(new Name(name), s);
+                v = SchemaVariableFactory.createSkolemTermSV(new Name(name), s,
+                    mods.definitional());
             } else if (makeTermLabelSV) {
                 v = SchemaVariableFactory.createTermLabelSV(new Name(name));
             } else {