From 401ba171058345d40ef266359499da0c89b7f0c8 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 11 Aug 2026 13:38:03 +0200 Subject: [PATCH 1/4] Instantiate quantifiers over shifted array indices Improves treatment of quantified formulas involving arrays with affine integer indexes. Trigger matching compares the structure of two terms, so a fact about b[srcStart + t] cannot be used on a term about a[x]: the witness x - srcStart occurs nowhere in the proof. Re-indexing therefore had to be written as a lemma and discharged by SMT. A theory can now solve a trigger subterm against the term it should match, through a new method on QuantifierTheorySupport. Integer arithmetic solves k*t + rest = s for t by exact division, for a pattern affine in one unbound variable. A wrong solution costs one instantiation, since instantiating a universal with any term is sound. (created with AI tooling support) --- .../quantifierHeuristics/BasicMatching.java | 61 +++++++++++-- .../HeapArrayTheorySupport.java | 12 +++ .../IntegerTheorySupport.java | 87 +++++++++++++++++++ .../quantifierHeuristics/Matching.java | 5 +- .../QuantifierTheorySupport.java | 57 ++++++++++-- .../quantifierHeuristics/TriggersSet.java | 26 ++++-- .../quantifierHeuristics/UniTrigger.java | 2 +- 7 files changed, 224 insertions(+), 26 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java index 4d36ebde6a9..a846d4692a2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy.quantifierHeuristics; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.JModality; import de.uka.ilkd.key.logic.op.Quantifier; import de.uka.ilkd.key.logic.op.UpdateApplication; @@ -26,18 +28,27 @@ private BasicMatching() {} * @return all substitution found from this matching */ static ImmutableSet getSubstitutions(Term trigger, Term targetTerm) { + return getSubstitutions(trigger, targetTerm, null); + } + + /** + * As above, but with the theory supports consulted where syntactic matching fails. Passing no + * services keeps the match purely syntactic, which is what the trigger loop test wants. + */ + static ImmutableSet getSubstitutions(Term trigger, Term targetTerm, + Services services) { ImmutableSet allsubs = DefaultImmutableSet.nil(); if (targetTerm.freeVars().size() > 0 || targetTerm.op() instanceof Quantifier) { return allsubs; } - final Substitution subst = match(trigger, targetTerm); + final Substitution subst = match(trigger, targetTerm, services); if (subst != null) { allsubs = allsubs.add(subst); } final var op = targetTerm.op(); if (!(op instanceof JModality || op instanceof UpdateApplication)) { for (int i = 0; i < targetTerm.arity(); i++) { - allsubs = allsubs.union(getSubstitutions(trigger, targetTerm.sub(i))); + allsubs = allsubs.union(getSubstitutions(trigger, targetTerm.sub(i), services)); } } return allsubs; @@ -49,9 +60,9 @@ static ImmutableSet getSubstitutions(Term trigger, Term targetTerm * @return all substitution that a given pattern(ex: a term of a uniTrigger) match in the * instance. */ - private static Substitution match(Term pattern, Term instance) { + private static Substitution match(Term pattern, Term instance, Services services) { final ImmutableMap map = - matchRec(DefaultImmutableMap.nilMap(), pattern, instance); + matchRec(DefaultImmutableMap.nilMap(), pattern, instance, services, false); if (map == null) { return null; } @@ -62,7 +73,8 @@ private static Substitution match(Term pattern, Term instance) { * match the pattern to instance recursively. */ private static ImmutableMap matchRec( - ImmutableMap varMap, Term pattern, Term instance) { + ImmutableMap varMap, Term pattern, Term instance, + Services services, boolean nested) { final var patternOp = pattern.op(); if (patternOp instanceof QuantifiableVariable) { @@ -70,17 +82,48 @@ private static ImmutableMap matchRec( } if (patternOp != instance.op()) { - return null; + // Only inside an observation that has matched so far. Solving a bare coordinate + // against an arbitrary integer of the sequent says nothing: the shift is meaningful + // only once the read around it is known to be the same read. + return nested ? solveByTheory(varMap, pattern, instance, services) : null; } for (int i = 0; i < pattern.arity(); i++) { - varMap = matchRec(varMap, pattern.sub(i), instance.sub(i)); - if (varMap == null) { - return null; + final ImmutableMap matched = + matchRec(varMap, pattern.sub(i), instance.sub(i), services, true); + if (matched == null) { + // Shapes agree at the top and disagree below, which is what a coordinate written + // against a different offset looks like: both sides are sums, but their parts do + // not line up. Solving the two as one equation still succeeds. + return nested ? solveByTheory(varMap, pattern, instance, services) : null; } + varMap = matched; } return varMap; } + /** + * Last resort when the shapes disagree: ask the theories whether the pattern can be solved for + * one of its variables. A coordinate written relative to an offset never matches an absolute + * one by shape, so without this a fact stated over {@code base + t} is unreachable from a term + * about {@code x}. + */ + private static ImmutableMap solveByTheory( + ImmutableMap varMap, Term pattern, Term instance, + Services services) { + if (services == null || !(pattern instanceof JTerm patternTerm) + || !(instance instanceof JTerm instanceTerm)) { + return null; + } + for (QuantifierTheorySupport support : TriggersSet.THEORY_SUPPORTS) { + final ImmutableMap solved = + support.solveForVariable(patternTerm, instanceTerm, varMap, services); + if (solved != null) { + return solved; + } + } + return null; + } + /** * match a variable to a instance. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java index 199afb85e17..9e27a921e15 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java @@ -58,6 +58,18 @@ public boolean rejectsAsTrigger(JTerm candidate, Services services) { * @param services access to the heap theory operators and term construction * @return the generalized read triggers, possibly empty */ + /** + * An array index gives way to the read around it. Taking the index alone as a trigger matches + * it against every term of its sort on the sequent, while the read says which observation is + * meant; the read is registered as well, so an instantiation reachable through either one + * stays reachable. + */ + @Override + public boolean prefersEnclosingTrigger(JTerm candidate, JTerm enclosing, Services services) { + return enclosing != null + && enclosing.op() == services.getTypeConverter().getHeapLDT().getArr(); + } + @Override public List provideTriggers(JTerm term, ImmutableSet clauseVariables, Services services) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java index 76e6fb18dd5..e8ea09e466b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java @@ -3,14 +3,21 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy.quantifierHeuristics; +import java.math.BigInteger; import java.util.List; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.ldt.IntegerLDT; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial; +import de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial; +import org.key_project.logic.Term; import org.key_project.logic.op.Operator; import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.logic.sort.Sort; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableMap; import org.key_project.util.collection.ImmutableSet; /** @@ -114,6 +121,86 @@ public boolean allowsEqualityRewrite(JTerm from, JTerm to, Services services) { * @param integerLDT the integer theory operators * @return whether the top operator carries polynomial structure */ + /** + * Solves {@code pattern = instance} for the single variable the pattern is affine in. + * + * A trigger coordinate is typically written relative to an offset, as {@code base + t}, while + * the terms a proof produces are absolute. Decomposing both sides as polynomials turns the + * match into an equation: with the pattern {@code k*t + rest} and the instance {@code s}, the + * variable is {@code (s - rest) / k}. That division has to be exact, since a non-integer + * solution cannot reproduce the instance. + * + * Instantiating a universally quantified formula with any term is sound, so a solution that + * does not reproduce the instance costs one instantiation and nothing else. + * + * Declined when the pattern is affine in more than one variable, because the equation is then + * underdetermined; when a variable sits inside a product with another atom, because that is + * not linear; and when a variable of the pattern is already bound by this match, which would + * require substituting before solving. + */ + @Override + public ImmutableMap solveForVariable(JTerm pattern, JTerm instance, + ImmutableMap varMap, Services services) { + final Sort integerSort = services.getTypeConverter().getIntegerLDT().targetSort(); + if (pattern.sort() != integerSort || instance.sort() != integerSort + || !instance.freeVars().isEmpty() || pattern.freeVars().isEmpty()) { + return null; + } + for (var free : pattern.freeVars()) { + if (varMap.get(free) != null) { + return null; + } + } + + final Polynomial patternPoly = Polynomial.create(pattern, services); + Monomial linear = null; + QuantifiableVariable variable = null; + for (Monomial part : patternPoly.getParts()) { + final ImmutableList atoms = part.getParts(); + if (atoms.stream().allMatch(a -> a.freeVars().isEmpty())) { + continue; + } + if (atoms.size() != 1 || linear != null + || !(atoms.head().op() instanceof QuantifiableVariable qv)) { + return null; + } + linear = part; + variable = qv; + } + if (linear == null) { + return null; + } + + Polynomial rest = zero(services).add(patternPoly.getConstantTerm()); + for (Monomial part : patternPoly.getParts()) { + if (part != linear) { + rest = rest.add(part); + } + } + final Polynomial solution = divideExactly( + Polynomial.create(instance, services).sub(rest), linear.getCoefficient(), services); + return solution == null ? null : varMap.put(variable, solution.toTerm(services)); + } + + private static Polynomial zero(Services services) { + return Polynomial.create(services.getTermBuilder().zero(), services); + } + + /** Divides every coefficient by the divisor, or returns null when a division is not exact. */ + private static Polynomial divideExactly(Polynomial p, BigInteger divisor, Services services) { + if (divisor.signum() == 0 || p.getConstantTerm().remainder(divisor).signum() != 0) { + return null; + } + Polynomial result = zero(services).add(p.getConstantTerm().divide(divisor)); + for (Monomial part : p.getParts()) { + if (part.getCoefficient().remainder(divisor).signum() != 0) { + return null; + } + result = result.add(part.setCoefficient(part.getCoefficient().divide(divisor))); + } + return result; + } + private static boolean hasPolynomialStructure(JTerm t, IntegerLDT integerLDT) { final Operator op = t.op(); return op == integerLDT.getAdd() || op == integerLDT.getMul() diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Matching.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Matching.java index 3c556d14b9c..ad55b0460ff 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Matching.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Matching.java @@ -22,8 +22,9 @@ private Matching() {} * @param targetTerm a gound term * @return all substitution found from this matching */ - public static ImmutableSet basicMatching(Trigger trigger, Term targetTerm) { - return BasicMatching.getSubstitutions(trigger.getTriggerTerm(), targetTerm); + public static ImmutableSet basicMatching(Trigger trigger, Term targetTerm, + Services services) { + return BasicMatching.getSubstitutions(trigger.getTriggerTerm(), targetTerm, services); } public static ImmutableSet twoSidedMatching(UniTrigger trigger, Term targetTerm, diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java index 3c9a2ebe71b..0381e00126c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java @@ -9,19 +9,20 @@ import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.op.Junctor; +import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.util.collection.ImmutableMap; import org.key_project.util.collection.ImmutableSet; /** * A theory's contribution to quantifier instantiation. * * The instantiation heuristic needs knowledge that is specific to each theory at two points. When - * choosing triggers: what counts as coordinate or connective material rather than a meaningful - * observation (an array index, an integer comparison), and which derived triggers make an - * observation matchable against the terms a proof actually produces (a read generalized over the - * heaps of a symbolic execution). And when predicting the cost of an instantiation: whether a - * literal is proved true or false, from itself or from an assumed literal, by the theory's own - * reasoning (arithmetic comparisons, equality up to renaming). This interface isolates that + * choosing triggers: which subterms are unfit on their own (an array index, an integer + * comparison), and which further triggers to derive so that a read matches the terms a proof + * produces. And when predicting the cost of an instantiation: whether a literal is proved true or + * false, from itself or from an assumed literal, by the theory's own reasoning (arithmetic + * comparisons, equality up to renaming). This interface isolates that * knowledge. Registering a new support in {@link TriggersSet#THEORY_SUPPORTS} is the only change * needed to teach the heuristic about a further theory; {@link TriggersSet} and * {@link PredictCostProver} stay untouched. @@ -62,9 +63,51 @@ static LiteralDecision fromTruthTerm(JTerm t) { return LiteralDecision.UNKNOWN; } + /** + * Solves a trigger subterm against a ground instance when syntactic matching has failed. + * + * Basic matching compares the two structures, so a trigger whose array index is written + * against an offset never matches an instance written absolutely: a read of + * {@code base + t} does not match one of {@code x}, since {@code x - base} occurs nowhere in + * the proof. A theory that can invert its own index expressions solves the equation for the + * variable instead. + * + * Instantiating a universally quantified formula with any term is sound, so a solution that + * turns out not to reproduce the instance costs an instantiation and nothing else. + * + * @param pattern a trigger subterm, containing at least one variable not yet bound in + * {@code varMap} + * @param instance the ground term it should match + * @param varMap the bindings established so far + * @param services access to the theory's operators + * @return the extended bindings, or null when this theory cannot solve the equation + */ + default ImmutableMap solveForVariable(JTerm pattern, JTerm instance, + ImmutableMap varMap, Services services) { + return null; + } + + /** + * Whether a candidate should give way to the term enclosing it, when that term yields a + * trigger of its own. + * + * Unlike {@link #rejectsAsTrigger}, this is a preference and not a veto. An array index + * matches every integer term on the sequent, while the read around it says which access is + * meant. Where no enclosing term yields a trigger the candidate is used anyway, since a + * clause without a trigger is never instantiated. + * + * @param candidate a trigger candidate + * @param enclosing the term the candidate is an argument of, null at the top of a literal + * @param services access to the theory's operators + * @return whether an enclosing trigger is preferable to this candidate + */ + default boolean prefersEnclosingTrigger(JTerm candidate, JTerm enclosing, Services services) { + return false; + } + /** * Whether {@code candidate} must not be used as a standalone trigger, because for this theory - * it is coordinate or connective material rather than a meaningful observation. + * it is an array index or a connective rather than a read. * * @param candidate a subterm that contains the quantified variables and is a trigger candidate * @param services access to the theory operators diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java index 568c5438de4..bb243051796 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java @@ -230,7 +230,7 @@ public void createTriggers(Services services) { if (positive.op() == Junctor.NOT) { positive = positive.sub(0); } - addMaximalUniTriggers(positive, services); + addMaximalUniTriggers(positive, null, services); } } buildCoveringMultiTriggers(); @@ -244,7 +244,7 @@ public void createTriggers(Services services) { * @param services access to the theory operators and term construction * @return whether a trigger was found in the term or its subterms */ - private boolean addMaximalUniTriggers(JTerm term, Services services) { + private boolean addMaximalUniTriggers(JTerm term, JTerm enclosing, Services services) { if (!mightContainTriggers(term)) { return false; } @@ -255,7 +255,7 @@ private boolean addMaximalUniTriggers(JTerm term, Services services) { boolean foundSubtriggers = false; for (int i = 0; i < term.arity(); i++) { final JTerm subTerm = term.sub(i); - final boolean found = addMaximalUniTriggers(subTerm, services); + final boolean found = addMaximalUniTriggers(subTerm, term, services); if (found && uniVarsInTerm.subset(subTerm.freeVars())) { foundSubtriggers = true; @@ -266,7 +266,7 @@ private boolean addMaximalUniTriggers(JTerm term, Services services) { // whose candidates were all rejected (not acceptable as triggers) does not count, // so the next enclosing meaningful term gets its chance if (!foundSubtriggers) { - return addUniTrigger(term, services); + return addUniTrigger(term, enclosing, services); } return true; @@ -336,7 +336,7 @@ private boolean mightContainTriggers(JTerm term) { /** * A trigger candidate is acceptable unless some theory's {@link QuantifierTheorySupport} - * rejects it as coordinate or connective material. + * rejects it as an array index or connective material. */ private boolean isAcceptableTrigger(JTerm term, Services services) { for (final QuantifierTheorySupport support : supports) { @@ -347,13 +347,23 @@ private boolean isAcceptableTrigger(JTerm term, Services services) { return true; } + /** Whether some theory would rather trigger on the term enclosing this one. */ + private boolean prefersEnclosing(JTerm term, JTerm enclosing, Services services) { + for (final QuantifierTheorySupport support : supports) { + if (support.prefersEnclosingTrigger(term, enclosing, services)) { + return true; + } + } + return false; + } + /** * add a uni-trigger to triggers set or add an element of multi-triggers for this clause, * together with the derived triggers each theory's {@link QuantifierTheorySupport} provides * * @return whether a trigger was registered for {@code term} */ - private boolean addUniTrigger(JTerm term, Services services) { + private boolean addUniTrigger(JTerm term, JTerm enclosing, Services services) { if (!isAcceptableTrigger(term, services)) { return false; } @@ -369,7 +379,9 @@ private boolean addUniTrigger(JTerm term, Services services) { } } } - return true; + // An array index is registered like any other candidate, but does not stop the + // ascent: the read around it says which access is meant and becomes a trigger too. + return !prefersEnclosing(term, enclosing, services); } private void registerUniTrigger(JTerm term, boolean matchByUnification) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java index 765883d6510..966d2d79ae2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java @@ -89,7 +89,7 @@ private ImmutableSet computeSubstitutionsForTerm(Term target, Serv || matchByUnification) { subs = Matching.twoSidedMatching(this, target, services); } else if (!onlyUnify) { - subs = Matching.basicMatching(this, target); + subs = Matching.basicMatching(this, target, services); } return subs; } From da73533451efba4f7c069cabdda027f29028e61d Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 11 Aug 2026 21:55:11 +0200 Subject: [PATCH 2/4] Make a quantified property applicable across a method call Applying a method contract anonymises the heap. A quantified formula from before the call has its triggers over the old heap, so trigger matching finds no instance and the property cannot be used afterwards. For an array read select(h,a,arr(i)) the heap theory now adds the trigger select(H,a,arr(i)) with a metavariable H for the heap, which matches the read over any heap. Such a trigger is matched by unification and by basic matching. An instantiation that basic matching gets by solving a subterm costs 10000 more, so it is tried after the ones from ordinary matches. AdjacencyStore.storeValidList, added here, needs this across its call to storeList. runAllProofs: 101 of 672 proofs change, 793103 against 803745 nodes. (created with AI tooling supported) --- .../de/uka/ilkd/key/strategy/FOLStrategy.java | 14 +- .../key/strategy/JFOLStrategyFactory.java | 12 +- .../ilkd/key/strategy/StrategyProperties.java | 10 +- .../quantifierHeuristics/BasicMatching.java | 156 ++++++++++++------ .../EqualityTheorySupport.java | 3 +- .../HeapArrayTheorySupport.java | 85 ++++------ .../HeuristicInstantiation.java | 31 ++-- .../quantifierHeuristics/Instantiation.java | 152 ++++++++++------- .../InstantiationCost.java | 14 +- .../InstantiationTieBreakFeature.java | 4 +- .../IntegerTheorySupport.java | 33 ++-- .../quantifierHeuristics/MultiTrigger.java | 22 ++- .../QuantifierTheorySupport.java | 23 ++- .../quantifierHeuristics/Substitution.java | 20 ++- .../quantifierHeuristics/Trigger.java | 26 +++ .../TriggerTreatment.java | 47 ++++++ .../quantifierHeuristics/TriggersSet.java | 19 ++- .../quantifierHeuristics/UniTrigger.java | 58 +++++-- .../proof/runallproofs/ProofCollections.java | 2 + .../heap/Adjacency/AdjacencyStore.java | 53 ++++++ key.ui/examples/heap/Adjacency/distinct.key | 34 ++++ key.ui/examples/heap/Adjacency/project.key | 34 ++++ 22 files changed, 614 insertions(+), 238 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerTreatment.java create mode 100644 key.ui/examples/heap/Adjacency/AdjacencyStore.java create mode 100644 key.ui/examples/heap/Adjacency/distinct.key create mode 100644 key.ui/examples/heap/Adjacency/project.key diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java index c4cda4a412e..3b6dfee61c5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java @@ -385,7 +385,7 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) { if (quantifierInstantiatedEnabled()) { final TermBuffer varInst = new TermBuffer(); final Feature branchPrediction = InstantiationCostScalerFeature - .create(InstantiationCost.create(varInst, classicTriggers()), + .create(InstantiationCost.create(varInst, triggerTreatment()), allowQuantifierSplitting()); bindRuleSet(d, "gamma", @@ -394,7 +394,7 @@ private void setupQuantifierInstantiation(RuleSetDispatchFeature d) { add(ff.quantifiedClauseSet, instQuantifiersWithQueries() ? longTermConst(0) : ff.notContainsExecutable)), - forEach(varInst, HeuristicInstantiation.forOption(classicTriggers()), + forEach(varInst, HeuristicInstantiation.forOption(triggerTreatment()), add(instantiate("t", varInst), add(branchPrediction, longConst(10), // orders candidates of one predicted-cost band by their @@ -419,10 +419,10 @@ private void setupQuantifierInstantiationApproval(RuleSetDispatchFeature d) { final TermBuffer varInst = new TermBuffer(); bindRuleSet(d, "gamma", add(isInstantiated("t"), - not(sum(varInst, HeuristicInstantiation.forOption(classicTriggers()), + not(sum(varInst, HeuristicInstantiation.forOption(triggerTreatment()), not(eq(instOf("t"), varInst)))), InstantiationCostScalerFeature.create( - InstantiationCost.create(instOf("t"), classicTriggers()), + InstantiationCost.create(instOf("t"), triggerTreatment()), longConst(0)))); final TermBuffer splitInst = new TermBuffer(); @@ -610,9 +610,9 @@ private String triggersOption() { return strategyProperties.getProperty(StrategyProperties.TRIGGERS_OPTIONS_KEY); } - /** whether the classic trigger selection is in effect for this strategy */ - private boolean classicTriggers() { - return StrategyProperties.TRIGGERS_CLASSIC.equals(triggersOption()); + /** how much the quantifier heuristic is told about the theories in this strategy */ + private TriggerTreatment triggerTreatment() { + return TriggerTreatment.forOption(triggersOption()); } private boolean quantifierInstantiatedEnabled() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JFOLStrategyFactory.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JFOLStrategyFactory.java index 104acbd03fe..37c61e8a4cb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JFOLStrategyFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JFOLStrategyFactory.java @@ -36,13 +36,13 @@ public class JFOLStrategyFactory implements StrategyFactory { might cause proof splitting."""; public static final String TOOL_TIP_TRIGGERS_BEST = - "Instantiate quantified formulas using knowledge about arrays and the heap, with the" - + " most informative ordering of the instances to try. Recommended.
" - + "Adds a small per-step cost on very large proof states."; + "" + + "Uses advanced knowledge about heap theory (in particular arrays) to find good instantiations." + + "Can deal with reads over different heaps (e.g., anon)
" + + "Slightly slower per proof step on very large proofs."; public static final String TOOL_TIP_TRIGGERS_GOOD = - "Instantiate quantified formulas using knowledge about arrays and the heap, with a" - + " lighter-weight ordering of the instances.
" - + "Close to Best, with less per-step overhead on large proof states."; + "Similar to Best but does not consider different heaps.
" + + "Slightly faster per proof step on very large proofs."; public static final String TOOL_TIP_TRIGGERS_CLASSIC = "Instantiate quantified formulas without the knowledge about arrays and the heap, and" + " without ordering the instances.
" diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java index 872de37dbbc..b9a45c44fc5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java @@ -89,11 +89,11 @@ public final class StrategyProperties extends Properties { /** * The quantifier instantiation treatment. {@link #TRIGGERS_BEST} and {@link #TRIGGERS_GOOD} - * both use the theory-aware trigger selection (heap and array reads); they differ in how tied - * candidates are ordered, {@code BEST} by the proving-polarity connection to the sequent, - * {@code GOOD} by generation with a lighter ordering. {@link #TRIGGERS_CLASSIC} uses the plain - * equality-and-integer trigger selection with no candidate ordering, matching the previous - * behaviour. + * both select triggers with knowledge of the heap and of array reads, and order tied + * candidates, {@code BEST} by their connection to the sequent, {@code GOOD} more cheaply. Only + * {@code BEST} matches a trigger against reads over another heap, which is how a property + * established before a method call is used after it. {@link #TRIGGERS_CLASSIC} selects with + * equality and integer knowledge only and does not order candidates. */ public static final String TRIGGERS_OPTIONS_KEY = "TRIGGERS_OPTIONS_KEY"; public static final String TRIGGERS_BEST = "TRIGGERS_BEST"; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java index a846d4692a2..e876d98dbae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/BasicMatching.java @@ -16,24 +16,49 @@ import org.key_project.util.collection.ImmutableMap; import org.key_project.util.collection.ImmutableSet; +/** + * Matches a trigger against a ground term of the sequent by descending both in step, binding a + * quantified variable to whatever ground subterm stands at its position. Operators and arities + * have to agree at every position above the variables, so the trigger's structure is fixed and + * only the variables are open. The trigger {@code select(heap, a, arr(i))} with quantified + * {@code i} matches the sequent term {@code select(heap, a, arr(3))} and binds {@code i} to + * {@code 3}; it does not match {@code select(heap2, a, arr(3))}, whose heap differs, nor + * {@code select(heap, b, arr(3))}. + * + * This is the weaker of the two matchings the heuristic uses. Unification (see + * {@link TwoSidedMatching}) binds metavariables on the trigger's side as well, so the trigger + * {@code select(H, a, arr(i))}, whose metavariable {@code H} stands for any heap, matches + * {@code select(heap2, a, arr(3))}, which basic matching cannot do. What unification does not + * offer is a place to intervene: it answers for the two terms at once and does not report which + * pair of subterms defeated it. Basic matching descends position by position with the ground term + * fixed, so a failing comparison stays located at the position where it failed and can be handed + * to a theory there: where {@code arr(base + i)} meets {@code arr(x)} the integer theory solves + * {@code base + i = x} for {@code i} (see {@link QuantifierTheorySupport#solveForVariable}) and + * the match continues with {@code i = x - base}. + */ class BasicMatching { private BasicMatching() {} /** - * matching trigger to targetTerm recursively + * Matches trigger against targetTerm and its subterms, comparing + * the two structures alone. * * @param trigger a uni-trigger - * @param targetTerm a gound term - * @return all substitution found from this matching + * @param targetTerm a ground term + * @return all substitutions found */ - static ImmutableSet getSubstitutions(Term trigger, Term targetTerm) { + static ImmutableSet getSyntacticSubstitutions(Term trigger, Term targetTerm) { return getSubstitutions(trigger, targetTerm, null); } /** - * As above, but with the theory supports consulted where syntactic matching fails. Passing no - * services keeps the match purely syntactic, which is what the trigger loop test wants. + * As above, and where a comparison fails the theories are asked whether they can solve it. + * + * @param trigger a uni-trigger + * @param targetTerm a ground term + * @param services the theories' operators, or null to compare the structures alone + * @return all substitutions found */ static ImmutableSet getSubstitutions(Term trigger, Term targetTerm, Services services) { @@ -61,88 +86,111 @@ static ImmutableSet getSubstitutions(Term trigger, Term targetTerm * instance. */ private static Substitution match(Term pattern, Term instance, Services services) { - final ImmutableMap map = - matchRec(DefaultImmutableMap.nilMap(), pattern, instance, services, false); - if (map == null) { + final Bindings bindings = + matchRec(Bindings.EMPTY, pattern, instance, services, false); + if (bindings == null) { return null; } - return new Substitution(map); + return new Substitution(bindings.variables(), bindings.solvedArrayIndex()); + } + + /** + * What a match has bound so far. Only {@code variables} is the result. A metavariable may + * occur at more than one position of a trigger and has to stand for the same term at each, + * which is what {@code metavariables} checks; it is dropped when the match ends. + * + * @param variables the instantiation of the trigger's quantified variables + * @param metavariables the terms the trigger's metavariables stand for + */ + private record Bindings(ImmutableMap variables, + ImmutableMap metavariables, boolean solvedArrayIndex) { + + static final Bindings EMPTY = new Bindings(DefaultImmutableMap.nilMap(), + DefaultImmutableMap.nilMap(), false); + + Bindings withVariable(QuantifiableVariable var, Term instance) { + final Term bound = variables.get(var); + if (bound == null) { + return new Bindings(variables.put(var, instance), metavariables, solvedArrayIndex); + } + return bound.equals(instance) ? this : null; + } + + Bindings withMetavariable(Metavariable metavariable, Term instance) { + final Term bound = metavariables.get(metavariable); + if (bound == null) { + return new Bindings(variables, metavariables.put(metavariable, instance), + solvedArrayIndex); + } + return bound.equals(instance) ? this : null; + } + + Bindings withSolution(ImmutableMap solved) { + return new Bindings(solved, metavariables, true); + } } /** * match the pattern to instance recursively. */ - private static ImmutableMap matchRec( - ImmutableMap varMap, Term pattern, Term instance, + private static Bindings matchRec(Bindings bindings, Term pattern, Term instance, Services services, boolean nested) { final var patternOp = pattern.op(); - if (patternOp instanceof QuantifiableVariable) { - return mapVarWithCheck(varMap, (QuantifiableVariable) patternOp, instance); + if (patternOp instanceof QuantifiableVariable var) { + return bindings.withVariable(var, instance); + } + + // A metavariable stands for any term of its sort, so comparing it as a rigid symbol fails + // against every concrete heap. Bind it like a variable instead, but only when matching for + // instantiation: trigger selection matches too, and binding there would change which + // candidates become triggers. + if (services != null && patternOp instanceof Metavariable metavariable + && pattern.sort() == instance.sort()) { + return bindings.withMetavariable(metavariable, instance); } if (patternOp != instance.op()) { - // Only inside an observation that has matched so far. Solving a bare coordinate - // against an arbitrary integer of the sequent says nothing: the shift is meaningful - // only once the read around it is known to be the same read. - return nested ? solveByTheory(varMap, pattern, instance, services) : null; + // Only below a read that has matched so far. Solving a bare array index against an + // arbitrary integer says nothing until the read around it is known to be the same. + return nested ? solveByTheory(bindings, pattern, instance, services) : null; } for (int i = 0; i < pattern.arity(); i++) { - final ImmutableMap matched = - matchRec(varMap, pattern.sub(i), instance.sub(i), services, true); + final Bindings matched = + matchRec(bindings, pattern.sub(i), instance.sub(i), services, true); if (matched == null) { - // Shapes agree at the top and disagree below, which is what a coordinate written - // against a different offset looks like: both sides are sums, but their parts do - // not line up. Solving the two as one equation still succeeds. - return nested ? solveByTheory(varMap, pattern, instance, services) : null; + // The operators agree at the top and disagree below, which is what an array index + // written against a different offset looks like: both sides are sums, but their + // parts do not line up. Solving the two as one equation still succeeds. + return nested ? solveByTheory(bindings, pattern, instance, services) : null; } - varMap = matched; + bindings = matched; } - return varMap; + return bindings; } /** - * Last resort when the shapes disagree: ask the theories whether the pattern can be solved for - * one of its variables. A coordinate written relative to an offset never matches an absolute - * one by shape, so without this a fact stated over {@code base + t} is unreachable from a term - * about {@code x}. + * Last resort when the structures disagree: ask the theories to solve the pattern for one of + * its variables. An array index written against an offset never matches an absolute one, so + * without this a fact about {@code base + t} cannot be used on a term about {@code x}. */ - private static ImmutableMap solveByTheory( - ImmutableMap varMap, Term pattern, Term instance, + private static Bindings solveByTheory(Bindings bindings, Term pattern, Term instance, Services services) { + // No services means the caller asked to compare the structures alone. if (services == null || !(pattern instanceof JTerm patternTerm) || !(instance instanceof JTerm instanceTerm)) { return null; } for (QuantifierTheorySupport support : TriggersSet.THEORY_SUPPORTS) { - final ImmutableMap solved = - support.solveForVariable(patternTerm, instanceTerm, varMap, services); + final ImmutableMap solved = support + .solveForVariable(patternTerm, instanceTerm, bindings.variables(), services); if (solved != null) { - return solved; + return bindings.withSolution(solved); } } return null; } - /** - * match a variable to a instance. - * - * @return true if it is a new vaiable or the instance it matched is the same as that it matched - * before. - */ - private static ImmutableMap mapVarWithCheck( - ImmutableMap varMap, QuantifiableVariable var, - Term instance) { - final Term oldTerm = varMap.get(var); - if (oldTerm == null) { - return varMap.put(var, instance); - } - - if (oldTerm.equals(instance)) { - return varMap; - } - return null; - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityTheorySupport.java index 3442c475a1e..f2f54e346a8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityTheorySupport.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityTheorySupport.java @@ -48,7 +48,8 @@ public boolean rejectsAsTrigger(JTerm candidate, Services services) { */ @Override public List provideTriggers(JTerm term, - ImmutableSet clauseVariables, Services services) { + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { return List.of(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java index 9e27a921e15..df485b4a2a6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeapArrayTheorySupport.java @@ -13,7 +13,6 @@ import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.sort.ArraySort; -import org.key_project.logic.Name; import org.key_project.logic.op.QuantifiableVariable; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableSet; @@ -21,7 +20,7 @@ /** * Support for the heap theory and array reads. * - * Rejects the bare array-index constructor {@code arr(i)} (a coordinate, not a read) and reads of + * Rejects the bare array-index constructor {@code arr(i)} (an index, not a read) and reads of * the implicit {@code $created} field, and provides array-read triggers generalized over the heap * so that a read written for one heap in a quantified formula matches the reads a proof produces * over its many other heaps. @@ -44,25 +43,16 @@ public boolean rejectsAsTrigger(JTerm candidate, Services services) { .endsWith(PipelineConstants.IMPLICIT_CREATED)) { return true; } - // the array-index constructor arr(i) alone is a coordinate, not a read: matching on it + // the array-index constructor arr(i) alone is an index, not a read: matching on it // instantiates with every index literal of any array on any heap. The enclosing select is // the meaningful trigger (see the generalized variants provided below). return candidate.op() == heapLDT.getArr(); } /** - * Provides the heap-generalized array read triggers, one per array dimension of the read. - * - * @param term an accepted trigger term - * @param clauseVariables the quantified variables of the clause the trigger belongs to - * @param services access to the heap theory operators and term construction - * @return the generalized read triggers, possibly empty - */ - /** - * An array index gives way to the read around it. Taking the index alone as a trigger matches - * it against every term of its sort on the sequent, while the read says which observation is - * meant; the read is registered as well, so an instantiation reachable through either one - * stays reachable. + * An array index gives way to the read around it: alone it matches every integer term on the + * sequent, while the read says which access is meant. Both are registered, so no instantiation + * is lost. */ @Override public boolean prefersEnclosingTrigger(JTerm candidate, JTerm enclosing, Services services) { @@ -70,10 +60,19 @@ public boolean prefersEnclosingTrigger(JTerm candidate, JTerm enclosing, Service && enclosing.op() == services.getTypeConverter().getHeapLDT().getArr(); } + /** + * Provides the heap-generalized array read triggers, one per array dimension of the read. + * + * @param term an accepted trigger term + * @param clauseVariables the quantified variables of the clause the trigger belongs to + * @param services access to the heap theory operators and term construction + * @return the generalized read triggers, possibly empty + */ @Override public List provideTriggers(JTerm term, - ImmutableSet clauseVariables, Services services) { - return dimensionVariants(term, clauseVariables, services); + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { + return dimensionVariants(term, clauseVariables, services, metavariableFactory); } /** @@ -92,9 +91,11 @@ public List provideTriggers(JTerm term, * * For a select chain over an array-sorted base this method therefore rebuilds the access path * once per depth, with the component sort of the base's array type at that depth and a fresh - * heap wildcard per level: for {@code x[i][i_1]} the triggers {@code x[i]} and - * {@code x[i][i_1]}, each carrying the sorts a ground read of that depth actually has. Prefixes - * that bind only part of the clause variables enter the multi-trigger pool as usual. + * metavariable per level: for {@code x[i][i_1]} the triggers {@code select(H0, x, arr(i))} + * and {@code select(H1, select(H0, x, arr(i)), arr(i_1))}, whose metavariables {@code H0} and + * {@code H1} each stand for any heap, and each carrying the sorts a ground read of that depth + * actually has. Prefixes that bind only part of the clause variables enter the multi-trigger + * pool as usual. * * @param term an accepted array read trigger * @param clauseVariables the quantified variables of the clause the trigger belongs to @@ -102,23 +103,24 @@ public List provideTriggers(JTerm term, * @return one generalized read trigger per array dimension, possibly empty */ private List dimensionVariants(JTerm term, - ImmutableSet clauseVariables, Services services) { + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); final TermBuilder tb = services.getTermBuilder(); final List variants = new ArrayList<>(); // decompose the select chain: walk through the object position collecting the arr - // coordinates, innermost first - final List coordinates = new ArrayList<>(); + // array indices, innermost first + final List arrayIndices = new ArrayList<>(); JTerm base = term; while (heapLDT.isSelectOp(base.op()) && base.sub(2).op() == heapLDT.getArr()) { - coordinates.add(0, base.sub(2).sub(0)); + arrayIndices.add(0, base.sub(2).sub(0)); base = base.sub(1); } - if (coordinates.isEmpty() || !(base.sort() instanceof ArraySort)) { + if (arrayIndices.isEmpty() || !(base.sort() instanceof ArraySort)) { return variants; } boolean anyVar = false; - for (final JTerm c : coordinates) { + for (final JTerm c : arrayIndices) { if (!TriggerUtils.intersect(c.freeVars(), clauseVariables).isEmpty()) { anyVar = true; } @@ -129,14 +131,13 @@ private List dimensionVariants(JTerm term, // rebuild the path bottom-up with the array's component sorts Sort sort = base.sort(); JTerm read = base; - for (int depth = 0; depth < coordinates.size(); depth++) { + for (int depth = 0; depth < arrayIndices.size(); depth++) { if (!(sort instanceof ArraySort arraySort)) { break; } sort = arraySort.elementSort(); - final JTerm heapVar = - tb.var(heapWildcard(term, clauseVariables, heapLDT.targetSort(), "_d" + depth)); - final JTerm arrField = tb.func(heapLDT.getArr(), coordinates.get(depth)); + final JTerm heapVar = tb.var(metavariableFactory.fresh(heapLDT.targetSort())); + final JTerm arrField = tb.func(heapLDT.getArr(), arrayIndices.get(depth)); read = tb.select(sort, heapVar, read, arrField); if (!TriggerUtils.intersect(read.freeVars(), clauseVariables).isEmpty() && !read.equals(term)) { @@ -146,27 +147,5 @@ private List dimensionVariants(JTerm term, return variants; } - /** - * A fresh heap-sorted metavariable standing for "any heap" in a generalized trigger. Its name - * is derived from the quantified variables of the read (plus a caller-chosen suffix to keep - * several wildcards of one trigger apart) rather than from creation order, so that the - * metavariable ordering (and through it the unification result and the chosen instances) does - * not depend on which goal builds its trigger set first. - * - * @param select the read the wildcard is built for - * @param clauseVariables the quantified variables of the clause the read belongs to - * @param heapSort the sort of heaps - * @param suffix keeps several wildcards of one trigger apart - * @return a fresh heap-sorted metavariable - */ - private static Metavariable heapWildcard(JTerm select, - ImmutableSet clauseVariables, Sort heapSort, String suffix) { - final StringBuilder name = new StringBuilder("heapWildcard"); - for (final QuantifiableVariable v : TriggerUtils.intersect(select.freeVars(), - clauseVariables)) { - name.append('_').append(v.name()); - } - name.append(suffix); - return new Metavariable(new Name(name.toString()), heapSort); - } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java index 248e9a9c49b..60ecbef3af5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java @@ -3,7 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.strategy.quantifierHeuristics; +import java.util.Collections; +import java.util.EnumMap; import java.util.Iterator; +import java.util.Map; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; @@ -22,14 +25,22 @@ public class HeuristicInstantiation implements TermGenerator { - private static final HeuristicInstantiation THEORY = new HeuristicInstantiation(false); - private static final HeuristicInstantiation CLASSIC = new HeuristicInstantiation(true); + /** One generator per treatment, so the option costs no allocation per instantiation. */ + private static final Map> GENERATORS; + static { + final EnumMap> generators = + new EnumMap<>(TriggerTreatment.class); + for (final TriggerTreatment t : TriggerTreatment.values()) { + generators.put(t, new HeuristicInstantiation(t)); + } + GENERATORS = Collections.unmodifiableMap(generators); + } - /** whether instances are computed with the classic trigger selection */ - private final boolean classicTriggers; + /** how much the instance computation is told about the theories */ + private final TriggerTreatment treatment; - private HeuristicInstantiation(boolean classicTriggers) { - this.classicTriggers = classicTriggers; + private HeuristicInstantiation(TriggerTreatment treatment) { + this.treatment = treatment; } /** @@ -37,11 +48,11 @@ private HeuristicInstantiation(boolean classicTriggers) { * strategy construction, like every other strategy option; reading it per generated * instance would take a synchronized settings lookup in the middle of proof search. * - * @param classicTriggers whether the classic trigger selection is in effect + * @param treatment how much the heuristic is told about the theories * @return the generator */ - public static TermGenerator forOption(boolean classicTriggers) { - return classicTriggers ? CLASSIC : THEORY; + public static TermGenerator forOption(TriggerTreatment treatment) { + return GENERATORS.get(treatment); } @Override @@ -51,7 +62,7 @@ public Iterator generate(RuleApp app, PosInOccurrence pos, Goal goal, final Term qf = pos.sequentFormula().formula(); final Instantiation ia = - Instantiation.create(qf, goal.sequent(), goal.proof().getServices(), classicTriggers); + Instantiation.create(qf, goal.sequent(), goal.proof().getServices(), treatment); final QuantifiableVariable var = qf.varsBoundHere(0).last(); assert var != null; return new HIIterator(ia.getSubstitution().iterator(), var, goal.proof().getServices()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Instantiation.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Instantiation.java index cdd2f5dd3f4..bdbf4e0927a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Instantiation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Instantiation.java @@ -71,37 +71,40 @@ class Instantiation { /** The sequent, kept for the tie-break view. */ private final Sequent sequent; + /** How much this instantiation is told about the theories. */ + private final TriggerTreatment treatment; + /** The services, kept for the tie-break view. */ private final Services services; - private Instantiation(Term allterm, Sequent seq, Services services, boolean classic) { + private Instantiation(Term allterm, Sequent seq, Services services, + TriggerTreatment treatment) { this.sequent = seq; this.services = services; firstVar = allterm.varsBoundHere(0).get(0); matrix = TriggerUtils.discardQuantifiers(allterm); /* Terms bound in every formula on goal */ - triggersSet = TriggersSet.create((JTerm) allterm, services, classic); + this.treatment = treatment; + triggersSet = TriggersSet.create((JTerm) allterm, services, treatment.isClassic()); assumedLiterals = initAssertLiterals(seq, services); congruence = new Congruence(assumedLiterals, services); assumedLiterals = normalizeAll(assumedLiterals); addInstances(sequentToTerms(seq), services); - // write-coordinate candidates are part of the theory-aware selection, dropped in classic - if (!classic) { - addStoreCoordinateInstances((JTerm) matrix, services); + // written-array-index candidates are part of the theory-aware selection, dropped in classic + if (!treatment.isClassic()) { + addWrittenArrayIndexInstances((JTerm) matrix, services); } } /** - * Heap-aware instance candidates from write coordinates: where the matrix reads an array - * through a built-up heap, {@code select(... store(h, o, arr(c), v) ..., o, arr(j))} with - * quantified index {@code j}, the written index {@code c} is a candidate for {@code j}. - * Instantiating with it lets the select collapse by the select-over-store rules, which is - * how such a quantified formula speaks about the stored value. Trigger matching cannot - * produce these candidates: the store coordinate contains no quantified variable, so no - * trigger binds {@code j} to it. The candidates go through the same cost computation as - * matched ones, so useless coordinates are excluded or ranked down as usual. + * Instance candidates taken from written array indices. Where the matrix reads an array + * through a store chain, {@code select(... store(h, o, arr(c), v) ..., o, arr(j))}, the + * written index {@code c} is a candidate for the quantified {@code j}: instantiating with it + * collapses the select by the select-over-store rules. No trigger produces it, since {@code c} + * holds no quantified variable. The candidates are costed like matched ones, so useless ones + * are ranked down as usual. */ - private void addStoreCoordinateInstances(JTerm term, Services services) { + private void addWrittenArrayIndexInstances(JTerm term, Services services) { final var heapLDT = services.getTypeConverter().getHeapLDT(); // isSelectOp tests the operator directly. Do not build getSelect(term.sort()): that // constructs a select of the subterm's sort, which fails for e.g. the Null sort. @@ -112,11 +115,11 @@ private void addStoreCoordinateInstances(JTerm term, Services services) { } } for (int i = 0; i < term.arity(); i++) { - addStoreCoordinateInstances(term.sub(i), services); + addWrittenArrayIndexInstances(term.sub(i), services); } } - /** Adds every ground index written on {@code obj}'s array fields in {@code heap}. */ + /** Adds every ground array index written on {@code obj}'s array fields in {@code heap}. */ private void collectWrittenIndices(JTerm heap, JTerm obj, Services services) { final var heapLDT = services.getTypeConverter().getHeapLDT(); if (heap.sort() != heapLDT.targetSort()) { @@ -129,7 +132,7 @@ private void collectWrittenIndices(JTerm heap, JTerm obj, Services services) { final ImmutableMap varMap = DefaultImmutableMap.nilMap() .put(firstVar, field.sub(0)); - addInstance(new Substitution(varMap), services); + addInstance(new Substitution(varMap), services, 0); } } for (int i = 0; i < heap.arity(); i++) { @@ -137,26 +140,24 @@ private void collectWrittenIndices(JTerm heap, JTerm obj, Services services) { } } - private record Cached(Proof proof, Term qf, Sequent seq, boolean classic, + private record Cached(Proof proof, Term qf, Sequent seq, TriggerTreatment treatment, Instantiation result) { } /** * Per-thread single-entry cache for {@link #create}. The parallel prover computes quantifier - * cost concurrently, so a shared static cache would hand the same {@link Instantiation} (with - * its - * mutable {@code instancesWithCosts}) to several workers and race them. ThreadLocal confines - * the - * cache -- and thereby each returned Instantiation -- to one worker, and also drops the - * cross-proof class-level lock. + * cost concurrently, so a shared cache would hand the same {@link Instantiation}, with its + * mutable {@code instancesWithCosts}, to several workers at once. Confining it to one worker + * also drops the cross-proof lock the class used to take. */ private static final ThreadLocal lastCreate = new ThreadLocal<>(); - static Instantiation create(Term qf, Sequent seq, Services services, boolean classic) { + static Instantiation create(Term qf, Sequent seq, Services services, + TriggerTreatment treatment) { final Proof proof = services.getProof(); final Cached cached = lastCreate.get(); if (cached != null && qf == cached.qf() && seq == cached.seq() - && classic == cached.classic()) { + && treatment == cached.treatment()) { return cached.result(); } if (cached != null && proof != cached.proof()) { @@ -164,8 +165,8 @@ static Instantiation create(Term qf, Sequent seq, Services services, boolean cla // proof's sequent stays reachable only while this entry is in use. lastCreate.remove(); } - final Instantiation result = new Instantiation(qf, seq, services, classic); - lastCreate.set(new Cached(proof, qf, seq, classic, result)); + final Instantiation result = new Instantiation(qf, seq, services, treatment); + lastCreate.set(new Cached(proof, qf, seq, treatment, result)); return result; } @@ -184,29 +185,77 @@ private static ImmutableSet sequentToTerms(Sequent seq) { * @param terms the sequent terms the triggers are matched against */ private void addInstances(ImmutableSet terms, Services services) { + boolean matchedByOwnTerms = false; for (final Trigger t : triggersSet.getAllTriggers()) { + if (t.isTheoryProvided()) { + continue; + } for (final Substitution sub : t.getSubstitutionsFromTerms(terms, services)) { - addInstance(sub, services); + addInstance(sub, services, + sub.isSolvedByTheory() ? SOLVED_POSITION_SURCHARGE : 0); + matchedByOwnTerms = true; + } + } + // Basic matching binds the trigger's metavariable to a term the trigger never read, so + // the instance speaks about a state the formula does not name. Where none of the formula's + // own terms match the sequent it is all there is, and costs what it predicts. Where they + // do match, it is offered behind them, so the search takes it only if nothing cheaper + // closes the goal. Only the cheapest offer for an instance is recorded. + for (final Trigger t : triggersSet.getAllTriggers()) { + if (!t.isTheoryProvided()) { + continue; + } + final ImmutableSet unified = + t.getSubstitutionsFromTerms(terms, services, false); + for (final Substitution sub : unified) { + addInstance(sub, services, 0); + } + if (treatment.allowsBasicMatchingOfTheoryTriggers()) { + final long surcharge = matchedByOwnTerms ? THEORY_TRIGGER_SURCHARGE : 0; + for (final Substitution sub : t.getSubstitutionsFromTerms(terms, services, true)) { + if (!unified.contains(sub)) { + addInstance(sub, services, surcharge); + } + } } } } - private void addInstance(Substitution sub, Services services) { - final long cost = + /** + * What an instance costs on top of its prediction when only basic matching of a + * theory-provided trigger produces it, and the formula's own terms do match the sequent. + * + * A predicted cost is a product of clause sizes (see {@link PredictCostProver}), so any + * surcharge above that range puts such instances behind the supported ones; the exact value + * does not matter. + */ + private static final long THEORY_TRIGGER_SURCHARGE = 10000L; + + /** + * What an instance costs on top of its prediction when a theory solved a disagreeing position + * to obtain it. The instance is then a term the matched term does not contain, so it is + * offered behind those the two terms produced by agreeing throughout. + */ + private static final long SOLVED_POSITION_SURCHARGE = 10000L; + + + /** + * @param sub the instantiation found + * @param services access to the theories + * @param surcharge what the instance costs on top of its prediction, zero where one of the + * formula's own terms produced it + */ + private void addInstance(Substitution sub, Services services, long surcharge) { + long cost = PredictCostProver.computerInstanceCost(sub, (JTerm) getMatrix(), assumedLiterals, congruence, services); - if (cost != -1) { - addInstance(sub, cost); + if (cost == -1) { + return; } + addInstance(sub, cost + surcharge); } - /** - * Pre-normalises the assumed literals once through the congruence, so each candidate's cost - * prediction reuses the result instead of re-normalising them. - * - * @param lits the assumed literals - * @return the normalised literals, or {@code lits} unchanged when the congruence is trivial - */ + /** Normalizes every literal by the congruence, so equal atoms coincide. */ private ImmutableSet normalizeAll(ImmutableSet lits) { if (congruence.isTrivial()) { return lits; @@ -218,19 +267,6 @@ private ImmutableSet normalizeAll(ImmutableSet lits) { return res; } - /** - * Records the instance chosen by sub for the quantified variable with its - * predicted cost, keeping the least cost when the instance is recorded already. - * - * The same instance can be found through different triggers whose matches differ only in term - * labels: one match picks the term up with an origin label, another without. Term equality is - * label sensitive, so both variants would enter the table as separate candidates, and the - * labels would decide which of the two is enumerated first. The table keeps one entry per - * instance up to term labels: a later variant merges into the entry of the first one found. - * - * @param sub the substitution providing the instance - * @param cost the predicted cost of the instance - */ private void addInstance(Substitution sub, long cost) { final Term inst = sub.getSubstitutedTerm(firstVar); @@ -288,8 +324,8 @@ private ImmutableSet initAssertLiterals(Sequent seq, * Try to find the cost of an instance(inst) according its quantified formula and current goal. */ static RuleAppCost computeCost(Term inst, Term form, Sequent seq, Services services, - boolean classic) { - return create(form, seq, services, classic).computeCostHelp(inst); + TriggerTreatment treatment) { + return create(form, seq, services, treatment).computeCostHelp(inst); } private RuleAppCost computeCostHelp(Term inst) { @@ -320,14 +356,14 @@ private RuleAppCost computeCostHelp(Term inst) { * @param seq the sequent * @param goal the goal, for the branch history the generation signal needs * @param services access to the theory operators - * @param classic whether the classic trigger selection is active + * @param treatment how much the heuristic is told about the theories * @param strategy the tie-break strategy * @return the tie-break cost */ static RuleAppCost computeTieBreak(Term inst, Term form, Sequent seq, - Goal goal, Services services, boolean classic, + Goal goal, Services services, TriggerTreatment treatment, QuantifierInstantiationTieBreak strategy) { - return create(form, seq, services, classic).tieBreak(inst, goal, strategy); + return create(form, seq, services, treatment).tieBreak(inst, goal, strategy); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationCost.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationCost.java index d27163c8736..fabac75cfc7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationCost.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationCost.java @@ -24,16 +24,16 @@ public class InstantiationCost implements Feature { final private ProjectionToTerm varInst; - /** whether the prediction runs with the classic trigger selection */ - private final boolean classicTriggers; + /** how much the prediction is told about the theories */ + private final TriggerTreatment treatment; - private InstantiationCost(ProjectionToTerm var, boolean classicTriggers) { + private InstantiationCost(ProjectionToTerm var, TriggerTreatment treatment) { varInst = var; - this.classicTriggers = classicTriggers; + this.treatment = treatment; } - public static Feature create(ProjectionToTerm varInst, boolean classicTriggers) { - return new InstantiationCost(varInst, classicTriggers); + public static Feature create(ProjectionToTerm varInst, TriggerTreatment treatment) { + return new InstantiationCost(varInst, treatment); } /** @@ -49,6 +49,6 @@ public static Feature create(ProjectionToTerm varInst, boolean classicTrig final var instance = varInst.toTerm(app, pos, jgoal, mState); return Instantiation.computeCost(instance, formula, goal.sequent(), - (Services) goal.proof().getServices(), classicTriggers); + (Services) goal.proof().getServices(), treatment); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationTieBreakFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationTieBreakFeature.java index 2e34d5f271c..29058c02d6a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationTieBreakFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/InstantiationTieBreakFeature.java @@ -66,13 +66,13 @@ public static Feature create(ProjectionToTerm varInst, String triggersOpti final de.uka.ilkd.key.proof.Goal jgoal = (de.uka.ilkd.key.proof.Goal) goal; if (strategy == null) { - // classic orders instances by their position in the sequent alone + // the classic treatment orders instances by their position in the sequent alone return NumberRuleAppCost.getZeroCost(); } final Term formula = pos.sequentFormula().formula(); final Term instance = varInst.toTerm(app, pos, jgoal, mState); return Instantiation.computeTieBreak(instance, formula, goal.sequent(), jgoal, - (Services) goal.proof().getServices(), false, strategy); + (Services) goal.proof().getServices(), TriggerTreatment.BEST, strategy); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java index e8ea09e466b..5f5efb71fd8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/IntegerTheorySupport.java @@ -53,7 +53,8 @@ public boolean rejectsAsTrigger(JTerm candidate, Services services) { */ @Override public List provideTriggers(JTerm term, - ImmutableSet clauseVariables, Services services) { + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory) { return List.of(); } @@ -124,7 +125,7 @@ public boolean allowsEqualityRewrite(JTerm from, JTerm to, Services services) { /** * Solves {@code pattern = instance} for the single variable the pattern is affine in. * - * A trigger coordinate is typically written relative to an offset, as {@code base + t}, while + * A trigger array index is typically written relative to an offset, as {@code base + t}, while * the terms a proof produces are absolute. Decomposing both sides as polynomials turns the * match into an equation: with the pattern {@code k*t + rest} and the instance {@code s}, the * variable is {@code (s - rest) / k}. That division has to be exact, since a non-integer @@ -141,23 +142,29 @@ public boolean allowsEqualityRewrite(JTerm from, JTerm to, Services services) { @Override public ImmutableMap solveForVariable(JTerm pattern, JTerm instance, ImmutableMap varMap, Services services) { - final Sort integerSort = services.getTypeConverter().getIntegerLDT().targetSort(); + final IntegerLDT integerLDT = services.getTypeConverter().getIntegerLDT(); + final Sort integerSort = integerLDT.targetSort(); + // The decomposition below allocates, and matching asks after every failed comparison, so + // the cheap tests come first: only a term built by the polynomial operators can be affine. if (pattern.sort() != integerSort || instance.sort() != integerSort + || !hasPolynomialStructure(pattern, integerLDT) || !instance.freeVars().isEmpty() || pattern.freeVars().isEmpty()) { return null; } - for (var free : pattern.freeVars()) { + for (final QuantifiableVariable free : pattern.freeVars()) { if (varMap.get(free) != null) { return null; } } final Polynomial patternPoly = Polynomial.create(pattern, services); + Polynomial rest = Polynomial.ZERO.add(patternPoly.getConstantTerm()); Monomial linear = null; QuantifiableVariable variable = null; - for (Monomial part : patternPoly.getParts()) { + for (final Monomial part : patternPoly.getParts()) { final ImmutableList atoms = part.getParts(); if (atoms.stream().allMatch(a -> a.freeVars().isEmpty())) { + rest = rest.add(part); continue; } if (atoms.size() != 1 || linear != null @@ -171,27 +178,17 @@ public ImmutableMap solveForVariable(JTerm pattern, return null; } - Polynomial rest = zero(services).add(patternPoly.getConstantTerm()); - for (Monomial part : patternPoly.getParts()) { - if (part != linear) { - rest = rest.add(part); - } - } final Polynomial solution = divideExactly( - Polynomial.create(instance, services).sub(rest), linear.getCoefficient(), services); + Polynomial.create(instance, services).sub(rest), linear.getCoefficient()); return solution == null ? null : varMap.put(variable, solution.toTerm(services)); } - private static Polynomial zero(Services services) { - return Polynomial.create(services.getTermBuilder().zero(), services); - } - /** Divides every coefficient by the divisor, or returns null when a division is not exact. */ - private static Polynomial divideExactly(Polynomial p, BigInteger divisor, Services services) { + private static Polynomial divideExactly(Polynomial p, BigInteger divisor) { if (divisor.signum() == 0 || p.getConstantTerm().remainder(divisor).signum() != 0) { return null; } - Polynomial result = zero(services).add(p.getConstantTerm().divide(divisor)); + Polynomial result = Polynomial.ZERO.add(p.getConstantTerm().divide(divisor)); for (Monomial part : p.getParts()) { if (part.getCoefficient().remainder(divisor).signum() != 0) { return null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java index 7dfbe159404..cd5bc7bf694 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java @@ -45,10 +45,16 @@ ImmutableSet elements() { @Override public ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerms, Services services) { + return getSubstitutionsFromTerms(targetTerms, services, true); + } + + @Override + public ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerms, + Services services, boolean basicMatching) { ImmutableList total = ImmutableList.nil(); final ImmutableSet combined = - combineElementSubstitutions(elements.iterator(), targetTerms, services); + combineElementSubstitutions(elements.iterator(), targetTerms, services, basicMatching); for (Substitution sub : combined) { if (sub.isTotalOn(clauseVariables)) { @@ -66,13 +72,13 @@ public ImmutableSet getSubstitutionsFromTerms(ImmutableSet t */ private ImmutableSet combineElementSubstitutions( Iterator remainingElements, ImmutableSet terms, - Services services) { + Services services, boolean basicMatching) { ImmutableList result = ImmutableList.nil(); if (remainingElements.hasNext()) { ImmutableSet headSubs = remainingElements.next().getSubstitutionsFromTerms(terms, services); ImmutableSet tailSubs = - combineElementSubstitutions(remainingElements, terms, services); + combineElementSubstitutions(remainingElements, terms, services, basicMatching); if (tailSubs.isEmpty()) { return headSubs; } else if (headSubs.isEmpty()) { @@ -132,6 +138,16 @@ public String toString() { return String.valueOf(elements); } + @Override + public boolean isTheoryProvided() { + for (final Trigger element : elements) { + if (element.isTheoryProvided()) { + return true; + } + } + return false; + } + @Override public Term getTriggerTerm() { return clause; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java index 0381e00126c..3c1927d2989 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/QuantifierTheorySupport.java @@ -11,6 +11,7 @@ import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableMap; import org.key_project.util.collection.ImmutableSet; @@ -122,10 +123,30 @@ default boolean prefersEnclosingTrigger(JTerm candidate, JTerm enclosing, Servic * @param term an accepted trigger term * @param clauseVariables the quantified variables of the clause the trigger belongs to * @param services access to the theory operators + * @param metavariableFactory supplies the metavariables a derived trigger needs * @return derived triggers, possibly empty */ List provideTriggers(JTerm term, - ImmutableSet clauseVariables, Services services); + ImmutableSet clauseVariables, Services services, + MetavariableFactory metavariableFactory); + + /** + * Hands out the metavariables a derived trigger puts in place of a ground subterm. + * + * The names are counted within one {@link TriggersSet}, which is built from the quantified + * formula alone, so the same formula always yields the same names and no two derived triggers + * share one. That matters because two metavariables of equal name are still distinct and are + * then ordered by a creation counter shared across the whole prover, which would make the + * order, and through it the instances chosen, depend on which goal built its trigger set + * first. A support must therefore take its metavariables from here rather than name them. + */ + interface MetavariableFactory { + /** + * @param sort the sort the metavariable stands for + * @return a metavariable distinct from every other one of its trigger set + */ + Metavariable fresh(Sort sort); + } /** * Checks whether the literal holds on its own, for cost prediction. The literal is passed diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Substitution.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Substitution.java index 1ad926b728f..035b925eee7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Substitution.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Substitution.java @@ -31,8 +31,26 @@ public class Substitution { private final ImmutableMap varMap; + /** + * Whether a theory solved a position where the two terms disagreed to obtain this + * substitution. The instance is then a term the matched term does not contain. + */ + private final boolean solvedByTheory; + public Substitution(ImmutableMap map) { - varMap = map; + this(map, false); + } + + public Substitution(ImmutableMap map, boolean solvedByTheory) { + this.varMap = map; + this.solvedByTheory = solvedByTheory; + } + + /** + * @return whether a theory solved a disagreeing position to obtain this substitution + */ + public boolean isSolvedByTheory() { + return solvedByTheory; } public ImmutableMap getVarMap() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Trigger.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Trigger.java index 1aab1102f3b..1d967cf23b8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Trigger.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/Trigger.java @@ -17,5 +17,31 @@ public interface Trigger { ImmutableSet getSubstitutionsFromTerms( ImmutableSet targetTerm, Services services); + /** + * As above, and where {@code basicMatching} is set a theory-provided trigger is matched by + * {@link BasicMatching} as well as unified. Only that matching lets a theory solve a + * array index, and only it binds a metavariable to a term the trigger never read. + * + * @param targetTerm the terms to match against + * @param services access to the theory's operators + * @param basicMatching whether a theory-provided trigger is also matched by + * {@link BasicMatching} + * @return the substitutions found + */ + default ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerm, + Services services, boolean basicMatching) { + return getSubstitutionsFromTerms(targetTerm, services); + } + Term getTriggerTerm(); + + /** + * Whether this trigger is a theory's generalization of another one rather than a term of the + * formula itself. + * + * @return whether the trigger was derived + */ + default boolean isTheoryProvided() { + return false; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerTreatment.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerTreatment.java new file mode 100644 index 00000000000..551fcc84afb --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggerTreatment.java @@ -0,0 +1,47 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.strategy.quantifierHeuristics; + +import de.uka.ilkd.key.strategy.StrategyProperties; + +/** + * How much the quantifier instantiation heuristic is told about the theories, as the strategy's + * trigger option selects it. + */ +public enum TriggerTreatment { + + /** Everything the heuristic knows. */ + BEST, + + /** The theories' trigger selection, with theory-provided triggers unified only. */ + GOOD, + + /** Equality and integer rejection only, and no ordering of the candidates. */ + CLASSIC; + + public static TriggerTreatment forOption(String option) { + if (StrategyProperties.TRIGGERS_CLASSIC.equals(option)) { + return CLASSIC; + } + return StrategyProperties.TRIGGERS_GOOD.equals(option) ? GOOD : BEST; + } + + /** Whether only the classic supports are consulted, and candidates are left unordered. */ + public boolean isClassic() { + return this == CLASSIC; + } + + /** + * Whether a theory-provided trigger may also be matched by {@link BasicMatching}, and not only + * unified. + * + * Basic matching binds the trigger's metavariable to a term the trigger never read, so a + * trigger written for one heap matches a read over another, and a theory can solve an array + * index along the way. It is the one part of the heuristic that instantiates from a term the + * formula does not name, so it is left to the most informed treatment. + */ + public boolean allowsBasicMatchingOfTheoryTriggers() { + return this == BEST; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java index bb243051796..e263cc2afa9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java @@ -17,8 +17,10 @@ import de.uka.ilkd.key.logic.label.TermLabelManager; import de.uka.ilkd.key.logic.op.*; +import org.key_project.logic.Name; import org.key_project.logic.op.Operator; import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.logic.sort.Sort; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -70,6 +72,21 @@ public class TriggersSet { * register unequal copies of the same triggers. */ private final Set theoryTriggersProvidedFor = new HashSet<>(); + /** + * Hands the supports their metavariables, counted within this set. The set is built from the + * quantified formula alone, so the same formula always yields the same names, and no two + * derived triggers share one. See {@link QuantifierTheorySupport.MetavariableFactory}. + */ + private final QuantifierTheorySupport.MetavariableFactory metavariableFactory = + new QuantifierTheorySupport.MetavariableFactory() { + private int created; + + @Override + public Metavariable fresh(Sort sort) { + return new Metavariable(new Name("unifier_derived_" + created++), sort); + } + }; + /** All universal variables of the formula. */ private final ImmutableSet uniQuantifiedVariables; /** @@ -374,7 +391,7 @@ private boolean addUniTrigger(JTerm term, JTerm enclosing, Services services) { if (theoryTriggersProvidedFor.add(term)) { for (final QuantifierTheorySupport support : supports) { for (final JTerm derived : support.provideTriggers(term, clauseVariables, - services)) { + services, metavariableFactory)) { registerUniTrigger(derived, true); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java index 966d2d79ae2..4051e8215b5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java @@ -51,6 +51,16 @@ class UniTrigger implements Trigger { // run outside the lock); at worst two workers redundantly compute the same (pure) result. private final ConcurrentLruCache> matchResults = new ConcurrentLruCache<>(1000); + /** + * The results of the same matching with basic matching allowed. That matching produces + * substitutions unification alone does not, so which of the two ran is part of what was + * computed and + * has to be part of the key: sharing one cache would hand the caller whichever mode happened + * to fill the entry first. Only a generalized trigger tells the two apart, see + * {@link #computeSubstitutionsForTerm}. + */ + private final ConcurrentLruCache> matchResultsByBasicMatching = + new ConcurrentLruCache<>(1000); UniTrigger(Term trigger, ImmutableSet universalVariables, boolean onlyUnify, @@ -67,34 +77,60 @@ class UniTrigger implements Trigger { @Override public ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerms, Services services) { + return getSubstitutionsFromTerms(targetTerms, services, true); + } + + @Override + public ImmutableSet getSubstitutionsFromTerms(ImmutableSet targetTerms, + Services services, boolean basicMatching) { ImmutableSet allSubs = DefaultImmutableSet.nil(); for (Term target : targetTerms) { - allSubs = allSubs.union(cachedSubstitutionsForTerm(target, services)); + allSubs = allSubs.union(cachedSubstitutionsForTerm(target, services, basicMatching)); } return allSubs; } - private ImmutableSet cachedSubstitutionsForTerm(Term target, Services services) { - ImmutableSet subs = matchResults.get(target); + private ImmutableSet cachedSubstitutionsForTerm(Term target, Services services, + boolean basicMatching) { + // A plain trigger is matched basically whenever it is not unified, so the mode leaves its + // result untouched and both callers share the one cache. + final ConcurrentLruCache> cache = + basicMatching && matchByUnification ? matchResultsByBasicMatching : matchResults; + ImmutableSet subs = cache.get(target); if (subs == null) { - subs = computeSubstitutionsForTerm(target, services); - matchResults.put(target, subs); + subs = computeSubstitutionsForTerm(target, services, basicMatching); + cache.put(target, subs); } return subs; } - private ImmutableSet computeSubstitutionsForTerm(Term target, Services services) { + private ImmutableSet computeSubstitutionsForTerm(Term target, + Services services, boolean basicMatching) { ImmutableSet subs = DefaultImmutableSet.nil(); - if (target.freeVars().size() > 0 || target.op() instanceof Quantifier - || matchByUnification) { + final boolean groundTarget = + target.freeVars().isEmpty() && !(target.op() instanceof Quantifier); + if (!groundTarget || matchByUnification) { subs = Matching.twoSidedMatching(this, target, services); - } else if (!onlyUnify) { - subs = Matching.basicMatching(this, target, services); + } + // Against a ground target basic matching applies as well, and only it lets a + // theory solve an array index: unification decides a pair of terms as a whole and offers no + // point at which a failing array index could be solved. + if (groundTarget && !onlyUnify && (basicMatching || !matchByUnification)) { + final ImmutableSet basicSubs = + Matching.basicMatching(this, target, services); + if (!basicSubs.isEmpty()) { + subs = subs.union(basicSubs); + } } return subs; } + @Override + public boolean isTheoryProvided() { + return matchByUnification; + } + @Override public Term getTriggerTerm() { return trigger; @@ -132,7 +168,7 @@ public TriggersSet getTriggerSetThisBelongsTo() { */ public static boolean passedLoopTest(Term candidate, Term searchTerm) { final ImmutableSet substitutions = - BasicMatching.getSubstitutions(candidate, searchTerm); + BasicMatching.getSyntacticSubstitutions(candidate, searchTerm); for (Substitution substitution : substitutions) { if (containsCycle(substitution)) { diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index fd1d85147d9..6531efa1099 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -524,6 +524,8 @@ public static ProofCollection automaticJavaDL() throws IOException { g.provable("heap/BoyerMoore/BM.count.accessible.key"); g.provable("heap/BoyerMoore/BM.count.key"); g.provable("heap/BoyerMoore/BM.monoLemma.key"); + g.provable("heap/Adjacency/project.key"); + g.provable("heap/Adjacency/distinct.key"); g = c.group("quicksort"); g.setDirectory("heap/quicksort"); diff --git a/key.ui/examples/heap/Adjacency/AdjacencyStore.java b/key.ui/examples/heap/Adjacency/AdjacencyStore.java new file mode 100644 index 00000000000..326b4a368ac --- /dev/null +++ b/key.ui/examples/heap/Adjacency/AdjacencyStore.java @@ -0,0 +1,53 @@ +/** + * Storing one node's neighbour list into the flat edge array of an adjacency structure. + */ +public final class AdjacencyStore { + + /*@ public normal_behavior + @ requires edges != null && list != null && edges != list; + @ requires 0 <= at && 0 <= n; + @ requires at + n <= edges.length; + @ requires n <= list.length; + @ ensures (\forall int i; 0 <= i && i < n; edges[at + i] == list[i]); + @ assignable edges[at .. at + n - 1]; + @*/ + public static void storeList(int[] edges, int at, int[] list, int n) { + int i = 0; + /*@ loop_invariant 0 <= i && i <= n; + @ loop_invariant (\forall int t; 0 <= t && t < i; edges[at + t] == list[t]); + @ assignable edges[at .. at + n - 1]; + @ decreases n - i; + @*/ + while (i < n) { + edges[at + i] = list[i]; + i++; + } + } + + /*@ public normal_behavior + @ requires edges != null && list != null && edges != list; + @ requires 0 <= at && 0 <= n; + @ requires at + n <= edges.length; + @ requires n <= list.length; + @ requires (\forall int i; 0 <= i && i < n; 0 <= list[i] && list[i] < nodeCount); + @ ensures (\forall int p; at <= p && p < at + n; + @ 0 <= edges[p] && edges[p] < nodeCount); + @ assignable edges[at .. at + n - 1]; + @*/ + public static void storeValidList(int[] edges, int at, int[] list, int n, int nodeCount) { + storeList(edges, at, list, n); + } + + /*@ public normal_behavior + @ requires edges != null && list != null && edges != list; + @ requires 0 <= at && 0 <= n; + @ requires at + n <= edges.length; + @ requires n <= list.length; + @ requires (\forall int u, v; 0 <= u && u < v && v < n; list[u] != list[v]); + @ ensures (\forall int p, q; at <= p && p < q && q < at + n; edges[p] != edges[q]); + @ assignable edges[at .. at + n - 1]; + @*/ + public static void storeDistinctList(int[] edges, int at, int[] list, int n) { + storeList(edges, at, list, n); + } +} diff --git a/key.ui/examples/heap/Adjacency/distinct.key b/key.ui/examples/heap/Adjacency/distinct.key new file mode 100644 index 00000000000..bb71d214ff0 --- /dev/null +++ b/key.ui/examples/heap/Adjacency/distinct.key @@ -0,0 +1,34 @@ +\settings { +"#Proof-Settings-Config-File +#Mon Aug 03 16:58:18 CEST 2009 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND +[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS +[DecisionProcedure]Timeout=60 +[View]ShowWholeTaclet=false +[View]MaxTooltipLines=40 +[General]DnDDirectionSensitive=true +[General]StupidMode=true +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[Strategy]Timeout=-1 +[Strategy]MaximumNumberOfAutomaticApplications=50000 +[Choice]DefaultChoices=assertions-assertions\:on, intRules-intRules\:arithmeticSemanticsIgnoringOF,initialisation-initialisation\:disableStaticInitialisation,programRules-programRules\:Java,runtimeExceptions-runtimeExceptions\:ban,JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:showSatisfiability , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , optimisedSelectRules-optimisedSelectRules\\:on , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off +[DecisionProcedure]ActiveRule=_noname_ +[General]UseJML=true +[View]HideClosedSubtrees=false +[View]HideIntermediateProofsteps=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +" +} + +\javaSource "."; + +\chooseContract "AdjacencyStore[AdjacencyStore::storeDistinctList([I,int,[I,int)].JML normal_behavior operation contract.0"; diff --git a/key.ui/examples/heap/Adjacency/project.key b/key.ui/examples/heap/Adjacency/project.key new file mode 100644 index 00000000000..8b2eae56536 --- /dev/null +++ b/key.ui/examples/heap/Adjacency/project.key @@ -0,0 +1,34 @@ +\settings { +"#Proof-Settings-Config-File +#Mon Aug 03 16:58:18 CEST 2009 +[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT +[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND +[StrategyProperty]DEP_OPTIONS_KEY=DEP_OFF +[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF +[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INV_TACLET +[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF +[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF +[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS +[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_DEF_OPS +[DecisionProcedure]Timeout=60 +[View]ShowWholeTaclet=false +[View]MaxTooltipLines=40 +[General]DnDDirectionSensitive=true +[General]StupidMode=true +[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON +[Strategy]Timeout=-1 +[Strategy]MaximumNumberOfAutomaticApplications=50000 +[Choice]DefaultChoices=assertions-assertions\:on, intRules-intRules\:arithmeticSemanticsIgnoringOF,initialisation-initialisation\:disableStaticInitialisation,programRules-programRules\:Java,runtimeExceptions-runtimeExceptions\:ban,JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:showSatisfiability , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , optimisedSelectRules-optimisedSelectRules\\:on , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off +[DecisionProcedure]ActiveRule=_noname_ +[General]UseJML=true +[View]HideClosedSubtrees=false +[View]HideIntermediateProofsteps=false +[Strategy]ActiveStrategy=JavaCardDLStrategy +[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED +" +} + +\javaSource "."; + +\chooseContract "AdjacencyStore[AdjacencyStore::storeValidList([I,int,[I,int,int)].JML normal_behavior operation contract.0"; From ea1867fca81fb6c4e31fa1e1ae53135955c69a99 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Tue, 11 Aug 2026 13:14:06 +0200 Subject: [PATCH 3/4] If reading the value of two locations (o,f) and (u,f) has different values then o != u Some heap simplification rules rely in their assumes on the fact that two objects are different, i.e., \assumes (==> o = u). this change makes it more likely for that formula to be actually present --- .../ilkd/key/strategy/JavaCardDLStrategy.java | 15 +++ .../de/uka/ilkd/key/proof/rules/heapRules.key | 15 +++ .../key/proof/rules/ruleSetsDeclarations.key | 1 + ...ameHeapAndFieldImplyDifferentObjects.proof | 99 +++++++++++++++++++ 4 files changed, 130 insertions(+) create mode 100644 key.core/tacletProofs/heap/Taclet_differentValuesForSameHeapAndFieldImplyDifferentObjects.proof diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java index d3a856e7572..b9cae1d8584 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.ldt.LocSetLDT; +import de.uka.ilkd.key.logic.op.Equality; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.BuiltInRule; @@ -180,6 +181,7 @@ private RuleSetDispatchFeature setupCostComputationF() { final int pullOutHeapSize = getHeapSizeBound(); bindRuleSet(d, "pull_out_heap", pullOutHeapSize <= 0 ? inftyConst() : pullOutHeap(pullOutHeapSize)); + bindRuleSet(d, "derive_inequality", longConst(-2000)); bindRuleSet(d, "simplify_heap_high_costs", inftyConst()); bindRuleSet(d, "javaIntegerSemantics", @@ -491,6 +493,19 @@ protected Feature setupApprovalF() { private RuleSetDispatchFeature setupApprovalDispatcher() { final RuleSetDispatchFeature d = new RuleSetDispatchFeature(); + // Only derive a disequality that is not known yet. The same disequality follows from + // every location the two objects read differently, so a duplicate-application check does + // not recognise those derivations as duplicates: their instantiations differ while their + // conclusion does not. Comparing the conclusion against the succedent does. + final TermBuffer succedentFormula = new TermBuffer(); + final TermBuffer firstObject = new TermBuffer(); + final TermBuffer secondObject = new TermBuffer(); + bindRuleSet(d, "derive_inequality", + let(firstObject, instOf("o"), let(secondObject, instOf("o2"), + sum(succedentFormula, SequentFormulasGenerator.succedent(), + not(applyTF(succedentFormula, + or(opSub(Equality.EQUALS, eq(firstObject), eq(secondObject)), + opSub(Equality.EQUALS, eq(secondObject), eq(firstObject))))))))); bindRuleSet(d, "inReachableStateImplication", NonDuplicateAppModPositionFeature.INSTANCE); bindRuleSet(d, "limitObserver", NonDuplicateAppModPositionFeature.INSTANCE); bindRuleSet(d, "partialInvAxiom", NonDuplicateAppModPositionFeature.INSTANCE); diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key index b27fbe81135..4a17a76e85a 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key @@ -534,6 +534,21 @@ \heuristics(simplify_select_elim_store) }; + \lemma + differentValuesForSameHeapAndFieldImplyDifferentObjects { + \schemaVar \term Heap h; + \schemaVar \term Object o, o2; + \schemaVar \term Field f; + \schemaVar \term beta x; + + \assumes(select(h, o, f) = x ==>) + \find(==> select(h, o2, f) = x) + + \add(==> o = o2) + + \heuristics(derive_inequality) + }; + dismissNonSelectedField { \schemaVar \term Heap h; \schemaVar \term Object o, u; 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..1b3ad1c6be5 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 @@ -273,6 +273,7 @@ hide_auxiliary_eq; hide_auxiliary_eq_const; simplify_heap_high_costs; + derive_inequality; // chrisg: pattern-based automation rules auto_induction; diff --git a/key.core/tacletProofs/heap/Taclet_differentValuesForSameHeapAndFieldImplyDifferentObjects.proof b/key.core/tacletProofs/heap/Taclet_differentValuesForSameHeapAndFieldImplyDifferentObjects.proof new file mode 100644 index 00000000000..568098806ed --- /dev/null +++ b/key.core/tacletProofs/heap/Taclet_differentValuesForSameHeapAndFieldImplyDifferentObjects.proof @@ -0,0 +1,99 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:safe", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 20000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_ON", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + + +\proofObligation +// +{ + "class" : "de.uka.ilkd.key.taclettranslation.lemma.TacletProofObligationInput", + "name" : "differentValuesForSameHeapAndFieldImplyDifferentObjects" +} + +\proof { +(keyLog "0" (keyUser "bubel" ) (keyVersion "05e3502a91ab2e6abbe38d72dd4c959321fc29a5")) + +(autoModeTime "37") + +(branch "dummy ID" +(rule "impRight" (formula "1")) +(rule "orRight" (formula "2")) +(rule "notRight" (formula "3")) +(rule "eqSymm" (formula "2")) +(rule "applyEq" (formula "3") (term "1,0") (ifseqformula "2")) +(rule "close" (formula "3") (ifseqformula "1")) +) +} From a29d31b7197e70dd4d0531627c09482a67e9c65a Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 12 Aug 2026 13:41:23 +0200 Subject: [PATCH 4/4] Fix Filter Staregy approval check Approval should only be called on taclets whose assumes clause has been matched. --- .../java/de/uka/ilkd/key/macros/FilterStrategy.java | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/FilterStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/macros/FilterStrategy.java index c2f8d7a1794..92e3b7c5405 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/FilterStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/FilterStrategy.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.macros; import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.strategy.RuleAppCostCollector; import de.uka.ilkd.key.strategy.Strategy; @@ -34,12 +35,22 @@ public boolean isApprovedApp(RuleApp app, PosInOccurrence pio, public > RuleAppCost computeCost(RuleApp app, PosInOccurrence pio, G goal, MutableState mState) { - if (!isApprovedApp(app, pio, (de.uka.ilkd.key.proof.Goal) goal)) { + if (assumesMatched(app) && !isApprovedApp(app, pio, (de.uka.ilkd.key.proof.Goal) goal)) { return TopRuleAppCost.INSTANCE; } return delegate.computeCost(app, pio, goal, mState); } + /** + * Checks that the assumes clause of a taclet is empty or instantiated + * + * @param app the rule application being costed + * @return whether a taclet application has its assumes clause matched + */ + private static boolean assumesMatched(RuleApp app) { + return !(app instanceof TacletApp tacletApp) || tacletApp.assumesInstantionsComplete(); + } + @Override public void instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal, RuleAppCostCollector collector) {