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/proof/init/Profile.java

@@ -17,6 +17,8 @@
 import de.uka.ilkd.key.rule.UseOperationContractRule;
 import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.strategy.StrategyFactory;
+import de.uka.ilkd.key.strategy.quantifierHeuristics.QuantifierTheorySupport;
+import de.uka.ilkd.key.strategy.quantifierHeuristics.QuantifierTheorySupports;
 
 import org.key_project.logic.Name;
 import org.key_project.prover.engine.GoalChooserFactory;
@@ -211,4 +213,13 @@ default List<String> prepareInitConfig(InitConfig baseConfig,
             @Nullable Configuration additionalProfileOptions) {
         return Collections.emptyList();
     }
+
+    /// The theories the quantifier heuristic consults for the terms of this profile, in the order
+    /// it consults them. A profile over other terms returns its own.
+    ///
+    /// @param classic whether the classic trigger selection is in effect
+    /// @return the theories, never empty
+    default List<QuantifierTheorySupport> getTheorySupports(boolean classic) {
+        return classic ? QuantifierTheorySupports.CLASSIC : QuantifierTheorySupports.JAVA_DL;
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/strategy/FOLStrategy.java

@@ -397,7 +397,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",
@@ -406,7 +406,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,
                                 CostBand.DEFAULT.at(10),
@@ -432,11 +432,11 @@ 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()),
-                    CostBand.DEFAULT.cost())));
+                    InstantiationCost.create(instOf("t"), triggerTreatment()),
+                    longConst(0))));
 
             final TermBuffer splitInst = new TermBuffer();
             bindRuleSet(d, "triggered",
@@ -628,9 +628,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/JavaCardDLCosts.java

@@ -125,4 +125,10 @@ private HeapSelectCost() {}
 
     /** {@code hide_auxiliary_eq_const}: same, for the constant-valued case. */
     static final long HIDE_AUXILIARY_EQ_CONST = -500;
+
+    /**
+     * {@code derive_inequality}: two objects whose reads of one field differ are different; the
+     * disequality feeds the assumes clauses of the select simplification rules.
+     */
+    static final long DERIVE_INEQUALITY = -2000;
 }

key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java

@@ -8,6 +8,7 @@
 import java.util.concurrent.atomic.AtomicLong;
 
 import de.uka.ilkd.key.ldt.HeapLDT;
+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;
@@ -184,6 +185,7 @@ private RuleSetDispatchFeature setupCostComputationF() {
         final int pullOutHeapSize = getHeapSizeBound();
         bindRuleSet(d, "pull_out_heap",
             pullOutHeapSize <= 0 ? inftyConst() : pullOutHeap(pullOutHeapSize));
+        bindRuleSet(d, "derive_inequality", longConst(DERIVE_INEQUALITY));
         bindRuleSet(d, "simplify_heap_high_costs", inftyConst());
 
         bindRuleSet(d, "javaIntegerSemantics",
@@ -493,6 +495,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";