diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java index dce83519c86..483decb16b6 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowBlockContractInternalRule.java +++ b/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; + /** *

* Rule for the application of {@link BlockContract}s. @@ -115,8 +117,7 @@ protected ImmutableList splitIntoGoals(final Goal goal, final BlockContrac final JTerm contextUpdate, final JTerm remembranceUpdate, final ImmutableSet localOutVariables, final GoalsConfigurator configurator, final Services services) { - final ImmutableList 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(); diff --git a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java b/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java index 6eecc350626..36b42a640b5 100644 --- a/key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowWhileInvariantRule.java +++ b/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); diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java index 8a4f42ba874..d092426b34c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java +++ b/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), diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java b/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java index 75ca962199d..6cff4cc61c9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java +++ b/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}. *

* * @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 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 getBetaCandidates() { return betaCandidates; } - /** - * returns the introduction time cache used by {@code AbstractMonomialSmallerThanFeature} for - * Skolem constants - */ - public final Map getIntroductionTimeCache() { - return introductionTimeCache; - } - public final Map getCostReuseClassificationCache() { return costReuseClassificationCache; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/JFunction.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/JFunction.java index 6f28c1c962c..7a829c957af 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/JFunction.java +++ b/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. *
* As soon as {@link AbstractTermTransformer#METASORT} is generalized, this class * may be deleted. */ 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 argSorts, ImmutableArray 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 argSorts, ImmutableArray 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 argSorts, - ImmutableArray whereToBind, boolean unique, boolean isSkolemConstant) { - this(name, sort, argSorts, whereToBind, unique, true, isSkolemConstant); + ImmutableArray 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 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 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); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java index 2341d53507d..8d48a31d888 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ParametricFunctionInstance.java +++ b/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 args, ImmutableArray 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; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SchemaVariableFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SchemaVariableFactory.java index 8bdfe393e56..64b3c4ff919 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SchemaVariableFactory.java +++ b/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); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java index 4d16791b80d..2a3f4f5454d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/op/SkolemTermSV.java +++ b/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; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java index eb189bf0ec1..dd3aa4273b4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java +++ b/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 { diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index 46d5bf6c071..dd4db64b434 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/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 { diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/SchemaVariableModifierSet.java b/key.core/src/main/java/de/uka/ilkd/key/parser/SchemaVariableModifierSet.java index 773cd2bcd31..fdbac43a791 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/parser/SchemaVariableModifierSet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/parser/SchemaVariableModifierSet.java @@ -9,52 +9,53 @@ public abstract class SchemaVariableModifierSet { private boolean strict = false; private boolean rigid = false; private boolean list = false; - + private boolean definitional = false; public boolean rigid() { return rigid; } - protected boolean rigidEnabled() { return false; } - public boolean strict() { return strict; } - protected boolean strictEnabled() { return false; } - public boolean list() { return list; } - protected boolean listEnabled() { return false; } + public boolean definitional() { + return definitional; + } + + protected boolean definitionalEnabled() { + return false; + } + /** * @return true iff option is a valid modifier for the considered kind * of schema variables */ public boolean addModifier(String option) { - if ("strict".equals(option)) { - return addStrict(); - } else if ("rigid".equals(option)) { - return addRigid(); - } else if ("list".equals(option)) { - return addList(); - } - - return false; + return switch (option) { + case "strict" -> addStrict(); + case "rigid" -> addRigid(); + case "list" -> addList(); + case "definitional" -> addDefinitional(); + case null, default -> false; + }; } public boolean addRigid() { @@ -72,6 +73,11 @@ public boolean addList() { return listEnabled(); } + public boolean addDefinitional() { + this.definitional = true; + return definitionalEnabled(); + } + public static class ProgramSV extends SchemaVariableModifierSet { protected boolean listEnabled() { return true; @@ -102,6 +108,9 @@ public static class VariableSV extends SchemaVariableModifierSet { } public static class SkolemTermSV extends SchemaVariableModifierSet { + protected boolean definitionalEnabled() { + return true; + } } public static class FreshProgVarSV extends SchemaVariableModifierSet { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index 95a716671d8..4a26e1b6ba7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java @@ -702,7 +702,10 @@ private PendingRuleApp(RuleApp ruleApp, NodeChangeJournal journal, Node original * @param ruleApp the rule application to perform * @return the pending application to be committed, or {@code null} if the rule aborted */ - public @Nullable PendingRuleApp computeRuleApp(final RuleApp ruleApp) { + public @Nullable PendingRuleApp computeRuleApp(final RuleApp p_ruleApp) { + final RuleApp ruleApp = p_ruleApp instanceof TacletApp tacletApp + ? tacletApp.createSkolemConstants(this) + : p_ruleApp; final Proof proof = proof(); final NodeChangeJournal journal = new NodeChangeJournal(proof, this); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java index 4531162a8e3..6783cf7a788 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java @@ -34,6 +34,8 @@ import org.key_project.util.collection.ImmutableSet; import org.key_project.util.java.ArrayUtil; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; + /** * A proof obligation for a {@link FunctionalBlockContract}. * @@ -85,7 +87,7 @@ protected static JTerm createLocalAnonUpdate( JTerm localAnonUpdate = null; for (LocationVariable pv : localOutVariables) { final Name anonFuncName = new Name(tb.newName(pv.name().toString())); - final Function anonFunc = new JFunction(anonFuncName, pv.sort(), true); + final Function anonFunc = new JFunction(anonFuncName, pv.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonFunc); final JTerm elemUpd = tb.elementary(pv, tb.func(anonFunc)); if (localAnonUpdate == null) { @@ -112,7 +114,7 @@ private static Map createAnonInHeaps( final String anonymisationName = tb.newName(AuxiliaryContractBuilders.ANON_IN_PREFIX + heap.name()); final Function anonymisationFunction = - new JFunction(new Name(anonymisationName), heap.sort(), true); + new JFunction(new Name(anonymisationName), heap.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonymisationFunction); anonHeaps.put(heap, anonymisationFunction); } @@ -136,7 +138,7 @@ private static Map createAnonOutHeaps( final String anonymisationName = tb.newName(AuxiliaryContractBuilders.ANON_OUT_PREFIX + heap.name()); final Function anonymisationFunction = - new JFunction(new Name(anonymisationName), heap.sort(), true); + new JFunction(new Name(anonymisationName), heap.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonymisationFunction); anonOutHeaps.put(heap, anonymisationFunction); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java index 544cd1da17d..b5875bacca0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java @@ -34,6 +34,8 @@ import org.key_project.util.collection.ImmutableSet; import org.key_project.util.java.ArrayUtil; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; + /** * A proof obligation for a {@link FunctionalLoopContract}. * @@ -322,7 +324,7 @@ private static Map createAnonInHeaps( final String anonymisationName = tb.newName(AuxiliaryContractBuilders.ANON_IN_PREFIX + heap.name()); final Function anonymisationFunction = - new JFunction(new Name(anonymisationName), heap.sort(), true); + new JFunction(new Name(anonymisationName), heap.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonymisationFunction); anonInHeaps.put(heap, anonymisationFunction); } @@ -346,7 +348,7 @@ private Map createAnonOutHeaps( final String anonymisationName = tb.newName(AuxiliaryContractBuilders.ANON_OUT_PREFIX + heap.name()); final Function anonymisationFunction = - new JFunction(new Name(anonymisationName), heap.sort(), true); + new JFunction(new Name(anonymisationName), heap.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonymisationFunction); anonOutHeaps.put(heap, anonymisationFunction); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java index f329e7ad3ef..428e3b32001 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java @@ -1075,7 +1075,7 @@ public static TacletApp parseSV2(TacletApp app, SchemaVariable sv, String value, final ProgramElement pe = app.getProgramElement(value, psv, services); result = app.addCheckedInstantiation(sv, pe, services, true); } else if (sv instanceof SkolemTermSV skolemSv) { - result = app.createSkolemConstant(value, skolemSv, true, services); + result = app.createSkolemConstant(value, skolemSv, true, targetGoal); } else if (sv instanceof ModalOperatorSV msv) { result = app.addInstantiation( app.instantiations().add(msv, JModality.JavaModalityKind.getKind(value), services), diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java index 790dafb48d8..bb631d68e8d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java @@ -27,6 +27,8 @@ import org.jspecify.annotations.NonNull; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; + /** *

* Rule for the application of {@link AuxiliaryContract}s. @@ -123,7 +125,7 @@ protected static JTerm createLocalAnonUpdate(ImmutableSet loca final TermBuilder tb = services.getTermBuilder(); for (LocationVariable pv : localOuts) { final Name anonFuncName = new Name(tb.newName(pv.name().toString())); - final Function anonFunc = new JFunction(anonFuncName, pv.sort(), true); + final Function anonFunc = new JFunction(anonFuncName, pv.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonFunc); final JTerm elemUpd = tb.elementary(pv, tb.func(anonFunc)); if (anonUpdate == null) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java index 856ccb44329..5436cbfca61 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java @@ -30,6 +30,8 @@ import org.jspecify.annotations.Nullable; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; + /** *

* Rule for the application of {@link BlockContract}s. @@ -167,7 +169,7 @@ protected static Map createAndRegisterAnonymisationV final String anonymisationName = tb.newName(AuxiliaryContractBuilders.ANON_OUT_PREFIX + variable.name()); final Function anonymisationFunction = - new JFunction(new Name(anonymisationName), variable.sort(), true); + new JFunction(new Name(anonymisationName), variable.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonymisationFunction); result.put(variable, anonymisationFunction); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java index 61f5663ba47..72913394b5c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java @@ -30,6 +30,8 @@ import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; + /** *

* Rule for the application of {@link LoopContract}s. @@ -135,8 +137,7 @@ protected boolean contractApplied(final LoopContract contract, final Goal goal) && selfOrParentNode.getChildNr(previousNode) == 0) { // prevent application of contract in its own check validity branch // but not in other branches, e.g., do-while loops might need to apply the same - // contract - // twice in its usage branch + // contract twice in its usage branch return true; } } @@ -213,7 +214,7 @@ protected Map createAndRegisterAnonymisationVariable final String anonymisationName = tb.newName(AuxiliaryContractBuilders.ANON_OUT_PREFIX + variable.name()); final Function anonymisationFunction = - new JFunction(new Name(anonymisationName), variable.sort(), true); + new JFunction(new Name(anonymisationName), variable.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonymisationFunction); result.put(variable, anonymisationFunction); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java index 950134bfca8..d9dc6fc8ca4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java @@ -34,6 +34,7 @@ import org.key_project.util.collection.Pair; import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; /** * An abstract super class for loop invariant rules. Extending rules should usually call @@ -219,7 +220,7 @@ protected static JTerm createLocalAnonUpdate(ImmutableSet loca return localOuts.stream().map(pv -> { final Function anonFunc = - new JFunction(new Name(tb.newName(pv.name().toString())), pv.sort(), true); + new JFunction(new Name(tb.newName(pv.name().toString())), pv.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonFunc); return tb.elementary(pv, tb.func(anonFunc)); @@ -432,7 +433,7 @@ protected static AnonUpdateData createAnonUpdate(LocationVariable heap, JTerm mo final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); final Name loopHeapName = new Name(tb.newName(heap + "_After_LOOP")); final Function loopHeapFunc = - new JFunction(loopHeapName, heapLDT.targetSort(), true); + new JFunction(loopHeapName, heapLDT.targetSort(), SKOLEM); services.getNamespaces().functions().addSafely(loopHeapFunc); final JTerm loopHeap = tb.func(loopHeapFunc); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java index ae5b3f0f1df..60213ad593c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java @@ -56,6 +56,7 @@ import org.jspecify.annotations.NonNull; import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; /** * This contains various builders used in building formulae and terms for block and loop contracts. @@ -720,7 +721,7 @@ private JTerm buildLocalVariablesAnonUpdate(Collection vars, for (LocationVariable variable : vars) { final String anonymisationName = newName(prefix + variable.name()); final Function anonymisationFunction = - new JFunction(new Name(anonymisationName), variable.sort(), true); + new JFunction(new Name(anonymisationName), variable.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonymisationFunction); final JTerm elementaryUpdate = elementary(variable, func(anonymisationFunction)); result = parallel(result, elementaryUpdate); @@ -1457,7 +1458,7 @@ public JTerm setUpLoopValidityGoal(final Goal goal, final LoopContract contract, final String anonymisationName = tb.newName("init_" + ANON_OUT_PREFIX + heap.name()); final Function anonymisationFunction = - new JFunction(new Name(anonymisationName), heap.sort(), true); + new JFunction(new Name(anonymisationName), heap.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonymisationFunction); anonOutHeaps2.put(heap, anonymisationFunction); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java index e2fbc3746ab..6d0e330e7ba 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java @@ -16,8 +16,10 @@ import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.ClashFreeSubst.VariableCollectVisitor; import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.logic.op.JFunction; import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.logic.sort.ProgramSVSort; +import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.VariableNameProposer; import de.uka.ilkd.key.rule.inst.GenericSortCondition; import de.uka.ilkd.key.rule.inst.GenericSortException; @@ -26,6 +28,7 @@ import org.key_project.logic.*; import org.key_project.logic.op.Function; +import org.key_project.logic.op.Function.FunctionKind; import org.key_project.logic.op.Operator; import org.key_project.logic.op.QuantifiableVariable; import org.key_project.logic.op.sv.SchemaVariable; @@ -38,6 +41,8 @@ import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; +import static org.key_project.logic.op.Function.FunctionKind.*; + /** * A TacletApp object contains information required for a concrete application. These information * may consist of @@ -524,7 +529,7 @@ public final TacletApp tryToInstantiateAsMuchAsPossible(Services services) { } } - if (!app.complete()) { + if (!app.completeExceptSkolemConstants()) { return null; } return app; @@ -576,20 +581,12 @@ private TacletApp instantiationHelper(boolean force, Services services) { } while (nameclash); } else if (operatorSv instanceof SkolemTermSV) { // if the sort of the schema variable is generic, - // ensure that it is instantiated + // ensure that it is instantiated; the constant itself is created when the + // rule is applied, see createSkolemConstants app = forceGenericSortInstantiation(app, operatorSv, services); if (app == null) { return null; } - - String proposal = - VariableNameProposer.DEFAULT.getProposal(app, operatorSv, services, null, - proposals); - - proposals = proposals.append(proposal); - - app = app.createSkolemConstant(proposal, operatorSv, true, services); - } else if (operatorSv instanceof VariableSV) { // if the sort of the schema variable is generic, // ensure that it is instantiated @@ -700,15 +697,20 @@ public Sort getRealSort(JOperatorSV p_sv, Services services) { * @param services the Services class allowing access to the type model */ public TacletApp createSkolemConstant(String instantiation, JOperatorSV sv, - boolean interesting, Services services) { - return createSkolemConstant(instantiation, sv, getRealSort(sv, services), interesting, - services); + boolean interesting, Goal goal) { + return createSkolemConstant(instantiation, sv, + getRealSort(sv, goal.getOverlayServices()), interesting, goal); } public TacletApp createSkolemConstant(String instantiation, SchemaVariable sv, Sort sort, - boolean interesting, Services services) { + boolean interesting, Goal goal) { + final FunctionKind kind = + sv instanceof SkolemTermSV skolemSV && skolemSV.isDefinitional() + ? DEFINITIONAL_SKOLEM + : SKOLEM; final Function c = - new JFunction(new Name(instantiation), sort, true, new Sort[0]); + new JFunction(new Name(instantiation), sort, kind, goal.appliedRuleApps().size()); + final Services services = goal.getOverlayServices(); return addInstantiation(sv, services.getTermBuilder().func(c), interesting, services); } @@ -742,6 +744,45 @@ && uninstantiatedGenericSorts().isEmpty() && assumesInstantionsComplete(); } + /** + * Whether this application can be applied: like {@link #complete()}, except skolem term + * schema variables, whose constants {@link #createSkolemConstants(Goal)} creates when the + * rule is applied. + */ + public final boolean completeExceptSkolemConstants() { + if (posInOccurrence() == null && !(taclet instanceof NoFindTaclet)) { + return false; + } + if (!uninstantiatedGenericSorts().isEmpty() || !assumesInstantionsComplete()) { + return false; + } + for (final SchemaVariable sv : uninstantiatedVars()) { + if (!(sv instanceof SkolemTermSV)) { + return false; + } + } + return true; + } + + /** + * Creates the skolem constants of the still uninstantiated skolem term schema variables. + * Called when the rule is applied, on the goal it is applied to, so every constant records + * the point of its introduction. + */ + public TacletApp createSkolemConstants(Goal goal) { + TacletApp app = this; + ImmutableList proposals = ImmutableList.nil(); + for (final SchemaVariable sv : uninstantiatedVars()) { + if (sv instanceof SkolemTermSV skolemSV) { + final String proposal = VariableNameProposer.DEFAULT.getProposal(app, skolemSV, + goal.getOverlayServices(), null, proposals); + proposals = proposals.append(proposal); + app = app.createSkolemConstant(proposal, skolemSV, true, goal); + } + } + return app; + } + /** * adds a new instantiation to this TacletApp. This method does not check (beside some very * rudimentary tests) if the instantiation is possible. If you cannot guarantee that adding the diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java index d3bd33a501e..b59386adf57 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java @@ -45,6 +45,7 @@ import org.jspecify.annotations.Nullable; import static de.uka.ilkd.key.java.ast.expression.BinaryAssignment.BinaryAssignmentKind.*; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; /** * Implements the rule which inserts operation contracts for a method call. @@ -276,7 +277,7 @@ private static AnonUpdateData createAnonUpdate(LocationVariable heap, IProgramMe final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); final Name methodHeapName = new Name(tb.newName(heap + "After_" + pm.getName())); final Function methodHeapFunc = - new JFunction(methodHeapName, heapLDT.targetSort(), true); + new JFunction(methodHeapName, heapLDT.targetSort(), SKOLEM); services.getNamespaces().functions().addSafely(methodHeapFunc); final JTerm methodHeap = tb.func(methodHeapFunc); final Name anonHeapName = new Name(tb.newName("anon_" + heap + "_" + pm.getName())); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java index ba6d0d0c1c2..fea1953edbc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java @@ -45,6 +45,7 @@ import org.jspecify.annotations.Nullable; import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; @NullMarked public class WhileInvariantRule implements BuiltInRule { @@ -447,7 +448,7 @@ private static JTerm createLocalAnonUpdate(ImmutableSet localO final TermBuilder tb = services.getTermBuilder(); for (LocationVariable pv : localOuts) { final Name anonFuncName = new Name(tb.newName(pv.name().toString())); - final Function anonFunc = new JFunction(anonFuncName, pv.sort(), true); + final Function anonFunc = new JFunction(anonFuncName, pv.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonFunc); final JTerm elemUpd = tb.elementary(pv, tb.func(anonFunc)); if (anonUpdate == null) { @@ -467,8 +468,7 @@ private static AnonUpdateData createAnonUpdate(LocationVariable heap, JTerm modi final TermBuilder tb = services.getTermBuilder(); final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); final Name loopHeapName = new Name(tb.newName(heap + "_After_LOOP")); - final Function loopHeapFunc = - new JFunction(loopHeapName, heapLDT.targetSort(), true); + final Function loopHeapFunc = new JFunction(loopHeapName, heapLDT.targetSort(), SKOLEM); services.getNamespaces().functions().addSafely(loopHeapFunc); final JTerm loopHeap = tb.func(loopHeapFunc); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateLocalAnonUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateLocalAnonUpdate.java index 0650c37a260..2853bc17afb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateLocalAnonUpdate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateLocalAnonUpdate.java @@ -17,6 +17,8 @@ import org.key_project.logic.op.Function; import org.key_project.util.collection.ImmutableSet; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; + /** * Expects a loop body and creates the anonymizing update * out_1:=anon_1||...||out_n:=anon_n, where anon_1, ..., anon_n are the written @@ -69,7 +71,8 @@ private static JTerm createLocalAnonUpdate(ImmutableSet localO private static Function anonConstForPV(ProgramVariable pv, Services services) { final TermBuilder tb = services.getTermBuilder(); final Name anonFuncName = new Name(tb.newName(pv.name().toString())); - final Function anonFunc = new JFunction(anonFuncName, pv.sort(), true); + final Function anonFunc = + new JFunction(anonFuncName, pv.sort(), SKOLEM); services.getNamespaces().functions().addSafely(anonFunc); return anonFunc; diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java index fde7a76fa9f..6c6c399a5b7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java @@ -65,7 +65,9 @@ public void execute(ScriptCommandAst command) throws ScriptException, Interrupte TacletApp app = completions.head(); app = app.tryToInstantiate(g.proof().getServices().getOverlay(g.getLocalNamespaces())); - if (app == null || !app.complete()) { + // the skolem constants of an application are created when the goal applies it, so an + // instantiated application is complete except for them + if (app == null || !app.completeExceptSkolemConstants()) { throw new ScriptException("Cannot complete the rule app"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java index dc7eb462f5c..01fb338176e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/ObtainCommand.java @@ -108,7 +108,7 @@ private JTerm executeFromGoal(LocationVariable var) throws ScriptException { SchemaVariable sk = getSV(app.uninstantiatedVars(), "sk"); String name = VariableNameProposer.DEFAULT.getNameProposal(var.name().toString(), services, null); - app = app.createSkolemConstant(name, sk, var.sort(), true, services); + app = app.createSkolemConstant(name, sk, var.sort(), true, goal); SchemaVariable b = getSV(app.uninstantiatedVars(), "b"); app = app.addCheckedInstantiation(b, formula.sub(0), services, true); @@ -156,7 +156,8 @@ private JTerm executeEquals(LocationVariable var, @Nullable JTerm equals) SchemaVariable t = getSV(app.uninstantiatedVars(), "t"); String name = VariableNameProposer.DEFAULT.getNameProposal(var.name().toString(), services, null); - app = app.createSkolemConstant(name, sk, var.sort(), true, services); + app = app.createSkolemConstant(name, sk, var.sort(), true, + state.getFirstOpenAutomaticGoal()); app = app.addCheckedInstantiation(t, equals, services, true); state.getFirstOpenAutomaticGoal().apply(app); return app.instantiations().getInstantiation(sk); diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/WitnessCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/WitnessCommand.java index 119d40e49f2..7ec38f85c40 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/WitnessCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/WitnessCommand.java @@ -101,10 +101,9 @@ public void execute(ScriptCommandAst ast) throws ScriptException, InterruptedExc true, services); app = app.addInstantiation(getSV(schemaVars, "b"), match.second.formula().sub(0), true, services); - app = app.createSkolemConstant(params.as, getSV(schemaVars, "sk"), - match.second.formula().boundVars().get(0).sort(), true, services); - Goal g = state.getFirstOpenAutomaticGoal(); + app = app.createSkolemConstant(params.as, getSV(schemaVars, "sk"), + match.second.formula().boundVars().get(0).sort(), true, g); g.apply(app); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractMonomialSmallerThanFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractMonomialSmallerThanFeature.java index 4b691663ede..f0f51ad7338 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractMonomialSmallerThanFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractMonomialSmallerThanFeature.java @@ -3,152 +3,40 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy.feature; -import java.util.Map; - import de.uka.ilkd.key.ldt.IntegerLDT; -import de.uka.ilkd.key.logic.op.SkolemTermSV; -import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.rule.TacletApp; -import org.key_project.logic.Name; import org.key_project.logic.Term; import org.key_project.logic.op.Function; import org.key_project.logic.op.Operator; -import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.rules.RuleSet; import org.key_project.util.collection.ImmutableList; public abstract class AbstractMonomialSmallerThanFeature extends SmallerThanFeature { - private static final Name newSymRuleSetName = new Name("polySimp_newSmallSym"); - private final Function add, mul, Z; - + private final Function mul; protected AbstractMonomialSmallerThanFeature(IntegerLDT numbers) { - this.add = numbers.getAdd(); this.mul = numbers.getMul(); - this.Z = numbers.getNumberSymbol(); } /** - * if {@code op} is a Skolem constant the returned introduction time is the number of taclets - * applied before and including the taclet by which it was introduced. For all other - * operators the returned value is -1 - * - *

- * Although this reads the goal, the value is a constant for every operator a cost evaluation - * can encounter, which is what makes features built on it {@code StableCost}-classifiable: - *

    - *
  1. The compared terms are instantiation terms of the taclet app, so an operator seen here - * either occurs in the goal's sequent or is the app's own fresh {@code SkolemTermSV} - * instantiation.
    2. - *
  2. A sequent operator with a {@code polySimp_newSmallSym} introducer: that application is - * already part of the goal's applied-rule sequence (a symbol cannot occur before the - * application that created it), and its position there never changes; every goal in which the - * symbol occurs lies below the introduction and so agrees on that position. The value is the - * same at every evaluation.
    3. - *
  3. A sequent operator without such an introducer answers {@code -1}, and stays {@code -1}: - * skolem instantiations are always fresh symbols ({@code TacletApp.createSkolemConstant}), so - * no later application can become the introducer of an already existing operator.
    4. - *
  4. An app's own fresh skolem symbol answers {@code -1} for as long as the app exists: its - * introducer would be the app itself, which is unapplied while the app is pending, and once - * applied the app is consumed, so no further evaluation of it takes place.
    5. - *
- * Case 4 is also the reason the {@code -1} answer must not be cached below: for that symbol - * the answer changes the moment the introducing taclet is applied, and a frozen {@code -1} - * would then leak into evaluations of other apps. - *

+ * The point at which the definitional skolem symbol {@code op} was introduced, counted in + * the rule applications its goal had seen, or -1 for every other operator. Such a symbol + * abbreviates a term through a defining equation ({@code \skolemTerm[definitional]}), and + * the ordering places it below all symbols that existed when it was made, newest lowest, so + * that applying a definition is a decrease, also in chains of definitions. Kind and time are + * constants of the symbol, which makes features built on this {@code StableCost}. * * @param op the Operator whose introduction time is queried - * @param goal the Goal whose state is queried - * @return the introduction time or -1 if not yet introduced or op is not a Skolem constant + * @return the introduction time, or -1 for an operator that is no definitional symbol */ - protected int introductionTime(Operator op, Goal goal) { - if (op == add || op == mul || op == Z) { - return -1; - } - - // A taclet with rule set "polySimp_newSmallSym" introduces its symbol as a SkolemTermSV - // instantiation, which is always a skolem-constant function - // (TacletApp.createSkolemConstant). - // So an op that is not a skolem-constant function can never have been introduced by one: - // its time is -1, with no need to scan the applied-rule history. This is what made the - // scan a hotspot -- the common monomial atoms (program variables, ordinary functions) are - // not skolem constants, yet walked the full O(history) on every compare and, never being - // "introduced", were never cached. (A skolem constant from some OTHER rule still walks and - // returns -1; only the structurally-impossible ops are short-circuited, so every result is - // unchanged.) - if (!(op instanceof Function func) || !func.isSkolemConstant()) { - return -1; - } - - final Map introductionTimeCache = - goal.proof().getServices().getCaches().getIntroductionTimeCache(); - - // ConcurrentLruCache: get/put are individually atomic, no external lock needed. - Integer res = introductionTimeCache.get(op); - - if (res == null) { - res = introductionTimeHelp(op, goal); - // Do NOT cache the "not introduced (yet)" answer (-1): op may be introduced by a later - // rule application, after which introductionTimeHelp would find a real time. Caching - // the -1 would freeze it, making the value depend on whether op happened to be first - // queried before or after its introduction -- i.e. on the access pattern (which - // features run, when). That makes term ordering, and hence OneStepSimplifier rewriting, - // subtly non-deterministic. A real introduction time, once found, is stable (the - // introducing rule stays in the applied-rule prefix), so it is safe to cache. - if (res != -1) { - introductionTimeCache.put(op, res); - } + protected int introductionTime(Operator op) { + if (op instanceof Function func && func.isDefinitionalSkolem()) { + final int time = func.introductionTime(); + return time < 0 ? -1 : time; } - - return res; - } - - private int introductionTimeHelp(Operator op, Goal goal) { - ImmutableList appliedRules = goal.appliedRuleApps(); - while (!appliedRules.isEmpty()) { - final RuleApp app = appliedRules.head(); - appliedRules = appliedRules.tail(); - - if (app instanceof TacletApp tapp) { - if (!inNewSmallSymRuleSet(tapp)) { - continue; - } - - if (introducesSkolemSymbol(tapp, op)) { - return appliedRules.size(); - } - } - } - return -1; } - private boolean introducesSkolemSymbol(TacletApp tapp, Operator op) { - for (final var entry : tapp.instantiations().getInstantiationMap()) { - if (!(entry.key() instanceof SkolemTermSV)) { - continue; - } - if (op == ((Term) entry.value().getInstantiation()).op()) { - return true; - } - } - return false; - } - - private boolean inNewSmallSymRuleSet(TacletApp tapp) { - ImmutableList ruleSets = tapp.taclet().getRuleSets(); - while (!ruleSets.isEmpty()) { - final RuleSet rs = ruleSets.head(); - ruleSets = ruleSets.tail(); - if (rs.name().equals(newSymRuleSetName)) { - return true; - } - } - return false; - } - protected ImmutableList collectAtoms(Term t) { final AtomCollector m = new AtomCollector(); m.collect(t); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AtomsSmallerThanFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AtomsSmallerThanFeature.java index 017c34d3874..f18a48c2fea 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AtomsSmallerThanFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AtomsSmallerThanFeature.java @@ -21,13 +21,12 @@ * a second monomial. * *

- * The value is determined by the compared instantiation terms alone: the atom ordering consists of - * the number-literal distinction, the term-only {@link de.uka.ilkd.key.logic.LexPathOrdering}, and - * the introduction time of basis symbols, which is a constant for every operator a cost evaluation - * can encounter (the argument is given at - * {@link AbstractMonomialSmallerThanFeature#introductionTime}). Hence {@link StableCost} -- the - * same classification, for the same reason, as {@link MonomialsSmallerThanFeature}, which orders - * whole monomials by the same ingredients. + * The value is determined by the compared instantiation terms alone: the atom ordering consists + * of the number-literal distinction, the term-only {@link de.uka.ilkd.key.logic.LexPathOrdering}, + * and the introduction time of definitional skolem symbols, which is a constant of the symbol + * (see {@link AbstractMonomialSmallerThanFeature#introductionTime}). Hence {@link StableCost} -- + * the same classification, for the same reason, as {@link MonomialsSmallerThanFeature}, which + * orders whole monomials by the same ingredients. *

*/ @StableCost @@ -73,7 +72,7 @@ protected boolean lessThan(Term t1, Term t2, PosInOccurrence focus, Goal goal) { } } - final int v = introductionTime(t2.op(), goal) - introductionTime(t1.op(), goal); + final int v = introductionTime(t2.op()) - introductionTime(t1.op()); if (v < 0) { return true; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java index 15c026541b0..028517641fa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java @@ -103,7 +103,7 @@ protected boolean lessThan(Term t1, Term t2, PosInOccurrence focus, Goal goal) { // transformation; such symbols are smaller than other symbols (and // the smaller the later they were introduced) - final int v = introductionTime(t2.op(), goal) - introductionTime(t1.op(), goal); + final int v = introductionTime(t2.op()) - introductionTime(t1.op()); if (v < 0) { return true; } @@ -141,7 +141,7 @@ private int compareLexNewSyms(ImmutableList atoms1, ImmutableList at atoms1 = atoms1.tail(); atoms2 = atoms2.tail(); - final int c = introductionTime(t2.op(), goal) - introductionTime(t1.op(), goal); + final int c = introductionTime(t2.op()) - introductionTime(t1.op()); if (c != 0) { return c; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/GenPolTieBreak.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/GenPolTieBreak.java index 1faa773d32e..8c77ab1213f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/GenPolTieBreak.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/GenPolTieBreak.java @@ -4,36 +4,21 @@ package de.uka.ilkd.key.strategy.quantifierHeuristics; import java.util.ArrayDeque; -import java.util.ArrayList; import java.util.HashMap; -import java.util.HashSet; import java.util.LinkedHashMap; -import java.util.List; import java.util.Map; -import java.util.Set; import java.util.TreeSet; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; -import de.uka.ilkd.key.logic.op.SkolemTermSV; -import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.rule.TacletApp; import org.key_project.logic.Term; import org.key_project.logic.op.Function; -import org.key_project.logic.op.Operator; -import org.key_project.prover.rules.RuleApp; -import org.key_project.util.collection.ImmutableList; /** * Orders tied instantiation candidates primarily by generation, that is by how late the * instance's newest skolem constant was introduced on the branch, and breaks a same-generation - * tie by the - * proving-polarity occurrence connection of {@link PolarityOccurrenceTieBreak}. The tie-break of - * the {@code Good} quantifier treatment. - * - * Generation-primary keeps the sequent walk to a secondary role: it only decides between candidates - * of the same generation, which for the input constants of generation zero is the one large group. + * tie by the proving-polarity occurrence connection of {@link PolarityOccurrenceTieBreak}. */ final class GenPolTieBreak extends PolarityOccurrenceTieBreak { @@ -67,69 +52,28 @@ private static long generationValue(Map ranks, Term inst) { } /** - * Ranks every candidate instance by the introduction step of its newest skolem constant. A - * candidate whose symbols all come from the problem input ranks 0, like a generation zero term - * of an SMT solver; the skolem-containing candidates follow in the order their newest symbol - * was - * introduced on the branch, capped by {@link #CAP}. All candidates' skolem constants are - * resolved in one walk over the branch's rule applications. + * Ranks every candidate instance by the introduction step of its newest skolem constant. * * @param view the instantiation view * @return the rank per candidate */ private static Map computeGenerationRanks(View view) { - // the skolem constants occurring in each candidate - final Map> skolems = new LinkedHashMap<>(); - final Set wanted = new HashSet<>(); + final Map intro = new LinkedHashMap<>(); + final TreeSet distinct = new TreeSet<>(); final ArrayDeque todo = new ArrayDeque<>(); for (final Term cand : view.candidates()) { - final List ops = new ArrayList<>(2); + int max = -1; todo.push(cand); while (!todo.isEmpty()) { final Term t = todo.pop(); if (t.op() instanceof Function f && f.isSkolemConstant()) { - ops.add(f); - wanted.add(f); + max = Math.max(max, f.introductionTime()); } for (int i = 0; i < t.arity(); i++) { todo.push(t.sub(i)); } } - skolems.put(cand, ops); - } - // one walk over the branch: the introduction step of every wanted skolem constant. Unlike - // the introduction time of the arithmetic ordering this considers every taclet, so the - // delta-rule skolems are found as well. - final Map steps = new HashMap<>(); - if (!wanted.isEmpty()) { - final Goal goal = view.goal(); - ImmutableList applied = goal.appliedRuleApps(); - while (!applied.isEmpty() && steps.size() < wanted.size()) { - final RuleApp app = applied.head(); - applied = applied.tail(); - if (!(app instanceof TacletApp tapp)) { - continue; - } - for (final var entry : tapp.instantiations().getInstantiationMap()) { - if (!(entry.key() instanceof SkolemTermSV)) { - continue; - } - final Operator op = ((Term) entry.value().getInstantiation()).op(); - if (wanted.contains(op)) { - steps.putIfAbsent(op, applied.size()); - } - } - } - } - // newest skolem decides a candidate's introduction step; -1 = generation zero - final Map intro = new LinkedHashMap<>(); - final TreeSet distinct = new TreeSet<>(); - for (final var e : skolems.entrySet()) { - int max = -1; - for (final Operator op : e.getValue()) { - max = Math.max(max, steps.getOrDefault(op, -1)); - } - intro.put(e.getKey(), max); + intro.put(cand, max); if (max >= 0) { distinct.add(max); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java b/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java index bd94d9ce13c..c40caa2a7df 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java @@ -161,7 +161,7 @@ private void renameSkolemConstant(JTerm term) { final Name newName = VariableNameProposer.DEFAULT.getNewName(services, new Name(f.name() + postfix)); final Function renamedF = new JFunction(newName, f.sort(), f.argSorts(), - f.whereToBind(), f.isUnique(), f.isSkolemConstant()); + f.whereToBind(), f.isUnique(), f.kind(), f.introductionTime()); services.getNamespaces().functions().addSafely(renamedF); final JTerm fTerm = label(func(renamedF), term.getLabels()); replaceMap.put(term, fTerm); diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java index 7ede7c532c3..0763d28c434 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java @@ -54,6 +54,7 @@ import org.slf4j.LoggerFactory; import static de.uka.ilkd.key.logic.equality.RenamingSourceElementProperty.RENAMING_SOURCE_ELEMENT_PROPERTY; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; /** * This class encapsulates static methods used in the MergeRule implementation. The methods are @@ -417,7 +418,7 @@ public static Function getNewSkolemConstantForPrefix(String prefix, Sort sort, do { newName = services.getTermBuilder().newName(prefix); - result = new JFunction(new Name(newName), sort, true); + result = new JFunction(new Name(newName), sort, SKOLEM); services.getNamespaces().functions().add(result); } while (newName.equals(prefix)); @@ -1381,7 +1382,7 @@ private static Pair> anonymizeProgramV */ private static Function rename(Name newName, Function old) { return new JFunction(newName, old.sort(), old.argSorts(), old.whereToBind(), - old.isUnique(), old.isSkolemConstant()); + old.isUnique(), old.kind(), old.introductionTime()); } /** diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/intDiv.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/intDiv.key index 56bfaf73989..b699aa002d0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/intDiv.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/intDiv.key @@ -14,7 +14,7 @@ \schemaVariables { \term int divNum, divDenom, polyDivCoeff; - \skolemTerm int l, quotient; + \skolemTerm[definitional] int quotient; } \rules { @@ -46,7 +46,7 @@ \if(divDenom >= 0) \then(mul(quotient, divDenom) >= 1 + divNum + (-1) * divDenom) \else(mul(quotient, divDenom) >= 1 + divNum + divDenom)) ==>) - \heuristics(defOps_div, polySimp_newSmallSym, notHumanReadable) + \heuristics(defOps_div, notHumanReadable) }; \lemma diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerSimplificationRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerSimplificationRules.key index 3e9bb56aaa2..9698ade08bd 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerSimplificationRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/integer/integerSimplificationRules.key @@ -50,7 +50,7 @@ \term int divNum, divDenom, polyDivCoeff; \term int modNumLeft, modNumRight, modDenom; \term int newSymLeft, newSymLeftCoeff, newSymRight, newSymDef; - \skolemTerm int l, quotient; + \skolemTerm[definitional] int l; \term int applyEqLeft, applyEqRight, applyEqOther; \term int tautLeft, tautRightBigger, tautRightSmaller; \term int weakenLeft, weakenRightSmaller, weakenRightBigger; @@ -2845,7 +2845,7 @@ \newDependingOn(l, newSymLeft)) \add(newSymLeft = l + newSymDef ==>) \heuristics(polySimp_leftNonUnit, - polySimp_newSym, polySimp_newSmallSym) + polySimp_newSym) }; } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key index cfd234be07b..ee4a0feb2a7 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key @@ -158,11 +158,6 @@ polySimp_newSym; polySimp_applyEqPseudo; - // the symbols introduced by rules of the following - // category will be considered as very small by the - // term ordering - polySimp_newSmallSym; - polyDivision; // primary categories for Omega diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java b/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java index e61c338a98c..70899b71216 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java @@ -199,6 +199,9 @@ public void testSuccTacletAllRight() { assertEquals(1, rApplist.size(), "Too many or zero rule applications."); TacletApp rApp = rApplist.head(); rApp = rApp.tryToInstantiate(TacletForTests.services()); + assertTrue(rApp.completeExceptSkolemConstants(), + "Rule App should be applicable, the skolem constants are created on application"); + rApp = rApp.createSkolemConstants(goal); assertTrue(rApp.complete(), "Rule App should be complete"); ImmutableList goals = rApp.rule().getExecutor().apply(goal, rApp); assertEquals(1, goals.size(), "Too many or zero goals for all-right."); diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index e2af31cd506..5703767ecb4 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -5988,7 +5988,7 @@ Choices: true} div_axiom { \find(div(divNum,divDenom)) \add [or(equals(divDenom,Z(0(#))),and(and(equals(div(divNum,divDenom),quotient),leq(mul(quotient,divDenom),divNum)),if-then-else(geq(divDenom,Z(0(#))),geq(mul(quotient,divDenom),add(add(Z(1(#)),divNum),mul(Z(neglit(1(#))),divDenom))),geq(mul(quotient,divDenom),add(add(Z(1(#)),divNum),divDenom)))))]==>[] -\heuristics(notHumanReadable, polySimp_newSmallSym, defOps_div) +\heuristics(notHumanReadable, defOps_div) Choices: true} ----------------------------------------------------- == div_cancel1 (div_cancel1) ========================================= @@ -13811,7 +13811,7 @@ Choices: true} newSym_eq { \find(equals(mul(newSymLeft,newSymLeftCoeff),newSymRight)==>) \add [equals(newSymLeft,add(l,newSymDef))]==>[] -\heuristics(polySimp_newSmallSym, polySimp_newSym, polySimp_leftNonUnit) +\heuristics(polySimp_newSym, polySimp_leftNonUnit) Choices: integerSimplificationRules:full} ----------------------------------------------------- == niceDouble (niceDouble) ========================================= diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Function.java b/key.ncore/src/main/java/org/key_project/logic/op/Function.java index d3206cd21d2..0bcc7b3451d 100644 --- a/key.ncore/src/main/java/org/key_project/logic/op/Function.java +++ b/key.ncore/src/main/java/org/key_project/logic/op/Function.java @@ -8,27 +8,59 @@ import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; +import static org.key_project.logic.op.Function.FunctionKind.DEFINITIONAL_SKOLEM; +import static org.key_project.logic.op.Function.FunctionKind.ORDINARY; +import static org.key_project.logic.op.Function.FunctionKind.SKOLEM; + /// Objects of this class represent function and predicate symbols. Note that program variables are -/// a -/// separate syntactic category, and not a type of function. +/// a separate syntactic category, and not a type of function. public abstract class Function extends AbstractSortedOperator { + /// Kinds of function symbols + public enum FunctionKind { + /// a normal logic function or predicate symbol + ORDINARY, + /// a skolem constant + SKOLEM, + /// a skolem constant introduced as a definitional equation + DEFINITIONAL_SKOLEM + } + + /// Value of [#introductionTime()] when no introduction time is available (e.g. not a Skolem + /// constant) + protected static final int UNRECORDED = -1; + + /// The point in a proof branch at which this skolem constant was introduced, counted in + /// rule applications, or [#UNRECORDED]. + private final int introductionTime; + protected Function(Name name, ImmutableArray argSorts, Sort sort, ImmutableArray whereToBind, boolean isRigid, boolean unique, - boolean isSkolemConstant) { - super(name, argSorts, sort, whereToBind, toModifier(isRigid, unique, isSkolemConstant)); + FunctionKind kind, int introductionTime) { + super(name, argSorts, sort, whereToBind, toModifier(isRigid, unique, kind)); + this.introductionTime = introductionTime; } - private static Modifier toModifier(boolean isRigid, boolean unique, boolean isSkolemConstant) { + private static Modifier toModifier(boolean isRigid, boolean unique, FunctionKind kind) { Modifier mod = Modifier.NONE; if (isRigid) mod = mod.combine(Modifier.RIGID); if (unique) mod = mod.combine(Modifier.UNIQUE); - if (isSkolemConstant) + if (kind != ORDINARY) mod = mod.combine(Modifier.SKOLEM); + if (kind == DEFINITIONAL_SKOLEM) + mod = mod.combine(Modifier.DEFINITIONAL_SKOLEM); return mod; } + /// @return the kind of this symbol + public final FunctionKind kind() { + if (hasModifier(Modifier.DEFINITIONAL_SKOLEM)) { + return DEFINITIONAL_SKOLEM; + } + return hasModifier(Modifier.SKOLEM) ? SKOLEM : ORDINARY; + } + // ------------------------------------------------------------------------- // public interface @@ -36,8 +68,7 @@ private static Modifier toModifier(boolean isRigid, boolean unique, boolean isSk /// Indicates whether the function or predicate symbol has the "uniqueness" property. For two /// unique symbols f1: A1 -> B1, f2: A2 -> B2 by definition we have (1) f1(x) != f1(y) for all - /// x, - /// y in A1 with x != y (i.e., injectivity), and (2) f1(x) != f2(y) for all x in A1, y in A2. + /// x, y in A1 with x != y (i.e., injectivity), and (2) f1(x) != f2(y) for all x in A1, y in A2. public final boolean isUnique() { return hasModifier(Modifier.UNIQUE); } @@ -46,6 +77,21 @@ public final boolean isSkolemConstant() { return hasModifier(Modifier.SKOLEM); } + /// Whether this symbol is a definitional skolem symbol, one that abbreviates a term + /// through a defining equation. A term ordering places such a symbol below all symbols + /// that existed when it was made, so that applying its definition is a decrease. + public final boolean isDefinitionalSkolem() { + return hasModifier(Modifier.DEFINITIONAL_SKOLEM); + } + + /// The point in a proof branch at which this skolem constant was introduced, counted in + /// rule applications. + /// + /// @return the introduction time, or a negative value if none is recorded + public final int introductionTime() { + return introductionTime; + } + @Override public final String toString() { return (name() + (whereToBind() == null ? "" : "{" + whereToBind() + "}")); diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Modifier.java b/key.ncore/src/main/java/org/key_project/logic/op/Modifier.java index d9bc2974eec..9ee3c4b8dbf 100644 --- a/key.ncore/src/main/java/org/key_project/logic/op/Modifier.java +++ b/key.ncore/src/main/java/org/key_project/logic/op/Modifier.java @@ -24,12 +24,15 @@ public class Modifier implements Named { /// A rigid (non-flexible) function. public static final Modifier RIGID = create("rigid", 1); - /// A skolem function. + /// A skolem symbol. public static final Modifier SKOLEM = create("skolem", 1 << 1); /// A unique function. public static final Modifier UNIQUE = create("unique", 1 << 2); + /// A skolem symbol that abbreviates a term through a defining equation. Implies [#SKOLEM]. + public static final Modifier DEFINITIONAL_SKOLEM = create("definitionalSkolem", 1 << 3); + static Modifier create(String name, int bitMask) { var mod = MODIFIERS.get(bitMask); if (mod != null) {