Quantifier and Heap Reasoning Improvements

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 <G extends ProofGoal<@NonNull G>> 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) {

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() {

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.</html>""";
 
     public static final String TOOL_TIP_TRIGGERS_BEST =
-        "<html>Instantiate quantified formulas using knowledge about arrays and the heap, with the"
-            + " most informative ordering of the instances to try. Recommended.<br>"
-            + "Adds a small per-step cost on very large proof states.</html>";
+        "<html>"
+            + "Uses advanced knowledge about heap theory (in particular arrays) to find good instantiations."
+            + "Can deal with reads over different heaps (e.g., anon)<br>"
+            + "Slightly slower per proof step on very large proofs.</html>";
     public static final String TOOL_TIP_TRIGGERS_GOOD =
-        "<html>Instantiate quantified formulas using knowledge about arrays and the heap, with a"
-            + " lighter-weight ordering of the instances.<br>"
-            + "Close to <i>Best</i>, with less per-step overhead on large proof states.</html>";
+        "<html>Similar to Best but does not consider different heaps.<br>"
+            + "Slightly faster per proof step on very large proofs.</html>";
     public static final String TOOL_TIP_TRIGGERS_CLASSIC =
         "<html>Instantiate quantified formulas without the knowledge about arrays and the heap, and"
             + " without ordering the instances.<br>"

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);

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";

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;
@@ -14,30 +16,64 @@
 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 <code>trigger</code> to <code>targetTerm</code> recursively
+     * Matches <code>trigger</code> against <code>targetTerm</code> 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<Substitution> getSubstitutions(Term trigger, Term targetTerm) {
+    static ImmutableSet<Substitution> getSyntacticSubstitutions(Term trigger, Term targetTerm) {
+        return getSubstitutions(trigger, targetTerm, null);
+    }
+
+    /**
+     * 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<Substitution> getSubstitutions(Term trigger, Term targetTerm,
+            Services services) {
         ImmutableSet<Substitution> 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,57 +85,112 @@ static ImmutableSet<Substitution> 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) {
-        final ImmutableMap<QuantifiableVariable, Term> map =
-            matchRec(DefaultImmutableMap.nilMap(), pattern, instance);
-        if (map == null) {
+    private static Substitution match(Term pattern, Term instance, Services services) {
+        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<QuantifiableVariable, Term> variables,
+            ImmutableMap<Metavariable, Term> 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<QuantifiableVariable, Term> solved) {
+            return new Bindings(solved, metavariables, true);
+        }
     }
 
     /**
      * match the pattern to instance recursively.
      */
-    private static ImmutableMap<QuantifiableVariable, Term> matchRec(
-            ImmutableMap<QuantifiableVariable, Term> 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()) {
-            return 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++) {
-            varMap = matchRec(varMap, pattern.sub(i), instance.sub(i));
-            if (varMap == null) {
-                return null;
+            final Bindings matched =
+                matchRec(bindings, pattern.sub(i), instance.sub(i), services, true);
+            if (matched == 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;
             }
+            bindings = matched;
         }
-        return varMap;
+        return bindings;
     }
 
     /**
-     * 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.
+     * 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<QuantifiableVariable, Term> mapVarWithCheck(
-            ImmutableMap<QuantifiableVariable, Term> varMap, QuantifiableVariable var,
-            Term instance) {
-        final Term oldTerm = varMap.get(var);
-        if (oldTerm == null) {
-            return varMap.put(var, 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;
         }
-
-        if (oldTerm.equals(instance)) {
-            return varMap;
+        for (QuantifierTheorySupport support : TriggersSet.THEORY_SUPPORTS) {
+            final ImmutableMap<QuantifiableVariable, Term> solved = support
+                    .solveForVariable(patternTerm, instanceTerm, bindings.variables(), services);
+            if (solved != null) {
+                return bindings.withSolution(solved);
+            }
         }
         return null;
     }
 
 
+
 }

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<JTerm> provideTriggers(JTerm term,
-            ImmutableSet<QuantifiableVariable> clauseVariables, Services services) {
+            ImmutableSet<QuantifiableVariable> clauseVariables, Services services,
+            MetavariableFactory metavariableFactory) {
         return List.of();
     }