From ad575b728ad466bfedf2c261847eb52e0a0dad84 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 12 Aug 2026 09:11:13 +0200 Subject: [PATCH] Create skolem constants at rule application and read their introduction time from the constant itself Make definitional Skolem constants aware of their introduction time (removes need for caches) and formalizes the notion of definitional formerly known as small constants. Definitional Skolem constants are smaller then most terms in termordering. A PR with a rework of term orderings is coming "A skolem constant was created while a taclet application was instantiated, so its name and its introduction time depended on when the strategy considered the application, not on when the proof used it, and the introduction time had to be remembered in a cache of its own. The constant now carries its kind and the number of rule applications the goal had performed when it was created, and the goal creates the constants when it applies the rule. The function kind also distinguishes the constants a definition introduces, which the term ordering can then place below the term they name." (created with AI tooling support) --- .../InfFlowBlockContractInternalRule.java | 7 +- .../rule/InfFlowWhileInvariantRule.java | 4 +- .../instantiation_model/TacletFindModel.java | 3 +- .../de/uka/ilkd/key/java/ServiceCaches.java | 23 +-- .../de/uka/ilkd/key/logic/op/JFunction.java | 71 ++++++--- .../logic/op/ParametricFunctionInstance.java | 7 +- .../key/logic/op/SchemaVariableFactory.java | 9 +- .../uka/ilkd/key/logic/op/SkolemTermSV.java | 13 +- .../builder/FunctionPredicateBuilder.java | 5 +- .../key/nparser/builder/TacletPBuilder.java | 3 +- .../key/parser/SchemaVariableModifierSet.java | 39 +++-- .../main/java/de/uka/ilkd/key/proof/Goal.java | 5 +- .../proof/init/FunctionalBlockContractPO.java | 8 +- .../proof/init/FunctionalLoopContractPO.java | 6 +- .../proof/io/IntermediateProofReplayer.java | 2 +- .../rule/AbstractAuxiliaryContractRule.java | 4 +- .../key/rule/AbstractBlockContractRule.java | 4 +- .../key/rule/AbstractLoopContractRule.java | 7 +- .../key/rule/AbstractLoopInvariantRule.java | 5 +- .../key/rule/AuxiliaryContractBuilders.java | 5 +- .../java/de/uka/ilkd/key/rule/TacletApp.java | 73 +++++++--- .../key/rule/UseOperationContractRule.java | 3 +- .../uka/ilkd/key/rule/WhileInvariantRule.java | 6 +- .../metaconstruct/CreateLocalAnonUpdate.java | 5 +- .../ilkd/key/scripts/ExpandDefCommand.java | 4 +- .../uka/ilkd/key/scripts/ObtainCommand.java | 5 +- .../uka/ilkd/key/scripts/WitnessCommand.java | 5 +- .../AbstractMonomialSmallerThanFeature.java | 136 ++---------------- .../feature/AtomsSmallerThanFeature.java | 15 +- .../feature/MonomialsSmallerThanFeature.java | 4 +- .../quantifierHeuristics/GenPolTieBreak.java | 70 +-------- .../ilkd/key/util/InfFlowProgVarRenamer.java | 2 +- .../key/util/mergerule/MergeRuleUtils.java | 5 +- .../ilkd/key/proof/rules/integer/intDiv.key | 4 +- .../integer/integerSimplificationRules.key | 4 +- .../key/proof/rules/ruleSetsDeclarations.key | 5 - .../de/uka/ilkd/key/rule/TestApplyTaclet.java | 3 + .../de/uka/ilkd/key/nparser/taclets.old.txt | 4 +- .../org/key_project/logic/op/Function.java | 62 ++++++-- .../org/key_project/logic/op/Modifier.java | 5 +- 40 files changed, 314 insertions(+), 336 deletions(-) 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) {