Fix wellFormedEQ* taclets and some improvements for large heaps

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

@@ -63,9 +63,6 @@ public FormulaTermFeatures(ArithTermFeatures tf) {
                 ifZero(tf.eqF, longTermConst(100), longTermConst(200))),
             rec(any(), longTermConst(1)));
         // directCutAllowed = add ( tf.intInEquation, notContainsQuery );
-
-
-
     }
 
     final TermFeature forF;

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

@@ -20,6 +20,8 @@
 import de.uka.ilkd.key.strategy.termgenerator.HeapGenerator;
 
 import org.key_project.logic.Name;
+import org.key_project.logic.Term;
+import org.key_project.logic.op.Function;
 import org.key_project.prover.proof.ProofGoal;
 import org.key_project.prover.proof.rulefilter.SetRuleFilter;
 import org.key_project.prover.rules.RuleApp;
@@ -30,6 +32,9 @@
 import org.key_project.prover.strategy.costbased.TopRuleAppCost;
 import org.key_project.prover.strategy.costbased.feature.*;
 import org.key_project.prover.strategy.costbased.feature.instantiator.ChoicePoint;
+import org.key_project.prover.strategy.costbased.termfeature.TermFeature;
+import org.key_project.prover.strategy.costbased.termfeature.TermPredicateTermFeature;
+import org.key_project.prover.strategy.costbased.termgenerator.SequentFormulasGenerator;
 
 import org.jspecify.annotations.NonNull;
 
@@ -64,7 +69,7 @@ protected JavaCardDLStrategy(Proof proof, StrategyProperties strategyProperties)
         super(proof);
         heapLDT = getServices().getTypeConverter().getHeapLDT();
 
-        this.strategyProperties = (StrategyProperties) strategyProperties.clone();
+        this.strategyProperties = strategyProperties.clone();
 
         this.tf = new ArithTermFeatures(getServices().getTypeConverter().getIntegerLDT());
         this.ff = new FormulaTermFeatures(this.tf);
@@ -151,10 +156,30 @@ protected Feature setupGlobalF(@NonNull Feature dispatcher) {
     // //////////////////////////////////////////////////////////////////////////
     // //////////////////////////////////////////////////////////////////////////
 
+    /**
+     * @return the minimal length before the heap term is pulled out in an eequation
+     *         length <code>0</code> means no pull out happens at all
+     */
+    private int getHeapSizeBound() {
+        return switch (strategyProperties.getProperty(
+            StrategyProperties.HEAP_REDUCTION_OPTIONS_KEY,
+            StrategyProperties.HEAP_REDUCTION_NORMAL)) {
+            case StrategyProperties.HEAP_REDUCTION_NORMAL ->
+                StrategyProperties.HEAP_REDUCTION_NORMAL_BOUND;
+            case StrategyProperties.HEAP_REDUCTION_DELAYED ->
+                StrategyProperties.HEAP_REDUCTION_DELAYED_BOUND;
+            default -> 0;
+        };
+    }
+
     private RuleSetDispatchFeature setupCostComputationF() {
         final RuleSetDispatchFeature d = new RuleSetDispatchFeature();
 
         bindRuleSet(d, "semantics_blasting", inftyConst());
+
+        final int pullOutHeapSize = getHeapSizeBound();
+        bindRuleSet(d, "pull_out_heap",
+            pullOutHeapSize <= 0 ? inftyConst() : pullOutHeap(pullOutHeapSize));
         bindRuleSet(d, "simplify_heap_high_costs", inftyConst());
 
         bindRuleSet(d, "javaIntegerSemantics",
@@ -301,20 +326,26 @@ private void setupSelectSimplification(final RuleSetDispatchFeature d) {
         bindRuleSet(d, "simplify_select_concrete", longConst(-6000));
         bindRuleSet(d, "simplify_select_elim_store", longConst(-7000));
         bindRuleSet(d, "apply_auxiliary_eq",
-            // replace skolem constant by it's computed value
+            // replace a skolem constant by its computed value
             add(isSelectSkolemConstantTerm("t1"), longConst(-5500)));
+        // hide an auxiliary equation once the skolem constant has been replaced by its value
+        final Feature hideReplacedAuxiliaryEq = add(isSelectSkolemConstantTerm("auxiliarySK"),
+            applyTF("result",
+                rec(any(),
+                    add(SimplifiedSelectTermFeature.create(heapLDT), not(ff.ifThenElse)))),
+            not(ContainsTermFeature.create(instOf("result"), instOf("auxiliarySK"))));
+
+        final int pullOutHeapBound = getHeapSizeBound();
         bindRuleSet(d, "hide_auxiliary_eq",
-            // hide auxiliary equation after the skolem constants have
-            // been replaced by it's computed value
-            add(isSelectSkolemConstantTerm("auxiliarySK"),
-                applyTF("result",
-                    rec(any(),
-                        add(SimplifiedSelectTermFeature.create(heapLDT), not(ff.ifThenElse)))),
-                not(ContainsTermFeature.create(instOf("result"), instOf("auxiliarySK"))),
-                longConst(-5400)));
+            pullOutHeapBound <= 0 ? add(hideReplacedAuxiliaryEq, longConst(-5400))
+                    : ifZero(hideReplacedAuxiliaryEq, longConst(-5400),
+                        ifZero(isTermAPulledOutHeap(),
+                            ifZero(isSkolemConstantUsedElsewhereInSequent(), longConst(-5400),
+                                longConst(HIDE_DEFERRAL_COST)),
+                            inftyConst())));
         bindRuleSet(d, "hide_auxiliary_eq_const",
-            // hide auxiliary equation after the skolem constatns have
-            // been replaced by it's computed value
+            // hide an auxiliary equation once the skolem constant has been replaced by its
+            // value
             add(isSelectSkolemConstantTerm("auxiliarySK"), longConst(-500)));
     }
 
@@ -332,6 +363,65 @@ private void setupUserTaclets(RuleSetDispatchFeature d) {
         }
     }
 
+    private Feature pullOutHeap(int minHeapSizeForPullout) {
+        final TermFeature chain =
+            TermPredicateTermFeature.create(
+                t -> getHeapTermSize(t, minHeapSizeForPullout) >= minHeapSizeForPullout);
+        final Feature updateValue = applyTF(FocusProjection.create(1), ff.elemUpdate);
+        return add(applyTF(FocusProjection.INSTANCE, chain), updateValue, longConst(-30000));
+    }
+
+
+    /**
+     * @param t a term describing a heap
+     * @param bound the heap length at which a pullout will be performed (and we can stop counting)
+     * @return the number of nested heap operations (max value is that of <code>bound</code>)
+     */
+    private int getHeapTermSize(Term t, int bound) {
+        int length = 0;
+        while (length < bound && t.arity() > 0
+                && (t.op() == heapLDT.getStore() || t.op() == heapLDT.getCreate()
+                        || t.op() == heapLDT.getAnon())) {
+            length++;
+            t = t.sub(0);
+        }
+        return length;
+    }
+
+    /**
+     * Defers application of hiding equations. It is realised as a finite cost so that
+     * the rule is deferred and not abandoned in the approval stage.
+     */
+    private static final long HIDE_DEFERRAL_COST = 30000;
+
+    /**
+     * cheap check if the equation to be hidden is of the required shape
+     * this check is cheap and run before the more expensive check whether the skolem constant still
+     * occurs in the sequent
+     *
+     * @return we only want to hid equations that describe a heap and were the result of a former
+     *         pullout
+     */
+    private Feature isTermAPulledOutHeap() {
+        return add(applyTF("result", op(heapLDT.getStore())),
+            applyTF("auxiliarySK", add(constantTermFeature(),
+                TermPredicateTermFeature.create(t -> t.op() instanceof Function f
+                        && f.isSkolemConstant()))));
+    }
+
+    /**
+     * expensive check ensuring that the Skolem constant of teh equation to be hidden is no longer
+     * in the
+     * sequent
+     */
+    private Feature isSkolemConstantUsedElsewhereInSequent() {
+        final TermBuffer sf = new TermBuffer();
+        return add(sequentContainsNoPrograms(),
+            sum(sf, SequentFormulasGenerator.sequent(),
+                or(eq(sf, FocusFormulaProjection.INSTANCE),
+                    not(ContainsTermFeature.create(sf, instOf("auxiliarySK"))))));
+    }
+
     private void setupSystemInvariantSimp(RuleSetDispatchFeature d) {
         bindRuleSet(d, "system_invariant",
             ifZero(MatchedAssumesFeature.INSTANCE, add(applyTF("negLit", tf.negLiteral),
@@ -405,6 +495,13 @@ private RuleSetDispatchFeature setupApprovalDispatcher() {
         bindRuleSet(d, "limitObserver", NonDuplicateAppModPositionFeature.INSTANCE);
         bindRuleSet(d, "partialInvAxiom", NonDuplicateAppModPositionFeature.INSTANCE);
 
+        final int pullOutHeapBound = getHeapSizeBound();
+        if (pullOutHeapBound > 0) {
+            bindRuleSet(d, "hide_auxiliary_eq",
+                ifZero(isSelectSkolemConstantTerm("auxiliarySK"), longConst(0),
+                    isSkolemConstantUsedElsewhereInSequent()));
+        }
+
         setupClassAxiomApproval(d);
 
         bindRuleSet(d, "apply_select_eq",

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

@@ -54,6 +54,12 @@ public class JavaCardDLStrategyFactory implements StrategyFactory {
         + "proofs even for simple problems. This option can,<br>"
         + "nevertheless, be meaningful to keep the complexity<br>"
         + "of proofs small and support interactive proving." + "</html>";
+    public static final String TOOL_TIP_HEAP_REDUCTION_NORMAL = "<html>"
+        + "Keep heap size in updates small." + "</html>";
+    public static final String TOOL_TIP_HEAP_REDUCTION_DELAYED = "<html>"
+        + "Keep heap size in updates at a medium size." + "</html>";
+    public static final String TOOL_TIP_HEAP_REDUCTION_OFF =
+        "<html>Keep the heap in an update as it is.</html>";
     public static final String TOOL_TIP_CLASSAXIOM_FREE =
         "<html>Expand class axioms (such as invariants) freely.</html>";
     public static final String TOOL_TIP_CLASSAXIOM_DELAYED =
@@ -161,6 +167,18 @@ private static OneOfStrategyPropertyDefinition getProofSplitting() {
                 TOOL_TIP_PROOF_SPLITTING_OFF));
     }
 
+    private static OneOfStrategyPropertyDefinition getHeapReduction() {
+        return new OneOfStrategyPropertyDefinition(StrategyProperties.HEAP_REDUCTION_OPTIONS_KEY,
+            "Heap reduction",
+            new StrategyPropertyValueDefinition(StrategyProperties.HEAP_REDUCTION_NORMAL, "Normal",
+                TOOL_TIP_HEAP_REDUCTION_NORMAL),
+            new StrategyPropertyValueDefinition(StrategyProperties.HEAP_REDUCTION_DELAYED,
+                "Delayed",
+                TOOL_TIP_HEAP_REDUCTION_DELAYED),
+            new StrategyPropertyValueDefinition(StrategyProperties.HEAP_REDUCTION_OFF, "Off",
+                TOOL_TIP_HEAP_REDUCTION_OFF));
+    }
+
     private static OneOfStrategyPropertyDefinition getDependencyContracts() {
         return new OneOfStrategyPropertyDefinition(StrategyProperties.DEP_OPTIONS_KEY,
             "Dependency contracts",
@@ -226,11 +244,12 @@ public StrategySettingsDefinition getSettingsDefinition() {
         final OneOfStrategyPropertyDefinition ossUsage = getOssUsage();
         final OneOfStrategyPropertyDefinition proofSplitting = getProofSplitting();
         final OneOfStrategyPropertyDefinition dependencyContracts = getDependencyContracts();
+        final OneOfStrategyPropertyDefinition heapReduction = getHeapReduction();
         final OneOfStrategyPropertyDefinition queryTreatment = getQueryTreatment();
         final OneOfStrategyPropertyDefinition classAxiom = getClassAxiom();
         final OneOfStrategyPropertyDefinition autoInduction = getAutoInduction();
         // Model
         return new StrategySettingsDefinition("Java DL Options", ossUsage, proofSplitting,
-            dependencyContracts, queryTreatment, classAxiom, autoInduction);
+            dependencyContracts, heapReduction, queryTreatment, classAxiom, autoInduction);
     }
 }

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

@@ -54,6 +54,14 @@ public final class StrategyProperties extends Properties {
     public static final String DEP_ON = "DEP_ON";
     public static final String DEP_OFF = "DEP_OFF";
 
+    public static final String HEAP_REDUCTION_OPTIONS_KEY = "HEAP_REDUCTION_OPTIONS_KEY";
+    public static final String HEAP_REDUCTION_NORMAL = "HEAP_REDUCTION_NORMAL";
+    public static final int HEAP_REDUCTION_NORMAL_BOUND = 8;
+    public static final String HEAP_REDUCTION_DELAYED = "HEAP_REDUCTION_DELAYED";
+    public static final int HEAP_REDUCTION_DELAYED_BOUND = 16;
+    public static final String HEAP_REDUCTION_OFF = "HEAP_REDUCTION_OFF";
+
+
     public static final String QUERY_OPTIONS_KEY = "QUERY_NEW_OPTIONS_KEY";
     public static final String QUERY_ON = "QUERY_ON";
     public static final String QUERY_RESTRICTED = "QUERY_RESTRICTED";
@@ -178,7 +186,9 @@ public final class StrategyProperties extends Properties {
         LOOP_SCOPE_INV_TACLET, LOOP_SCOPE_EXPAND, LOOP_NONE, BLOCK_OPTIONS_KEY,
         BLOCK_CONTRACT_INTERNAL, BLOCK_CONTRACT_EXTERNAL, BLOCK_EXPAND, BLOCK_NONE,
         METHOD_OPTIONS_KEY, METHOD_EXPAND, METHOD_CONTRACT, METHOD_NONE, MPS_OPTIONS_KEY, MPS_MERGE,
-        MPS_SKIP, MPS_NONE, DEP_OPTIONS_KEY, DEP_ON, DEP_OFF, QUERY_OPTIONS_KEY, QUERY_ON,
+        MPS_SKIP, MPS_NONE, DEP_OPTIONS_KEY, DEP_ON, DEP_OFF, HEAP_REDUCTION_OPTIONS_KEY,
+        HEAP_REDUCTION_NORMAL, HEAP_REDUCTION_DELAYED, HEAP_REDUCTION_OFF, QUERY_OPTIONS_KEY,
+        QUERY_ON,
         QUERY_RESTRICTED, QUERY_OFF, QUERYAXIOM_OPTIONS_KEY, QUERYAXIOM_ON, QUERYAXIOM_OFF,
         NON_LIN_ARITH_OPTIONS_KEY, NON_LIN_ARITH_NONE, NON_LIN_ARITH_DEF_OPS,
         NON_LIN_ARITH_COMPLETION, OSS_OPTIONS_KEY, OSS_ON, OSS_OFF, QUANTIFIERS_OPTIONS_KEY,
@@ -207,6 +217,7 @@ public final class StrategyProperties extends Properties {
         DEFAULT_MAP.setProperty(MPS_OPTIONS_KEY, MPS_MERGE);
         DEFAULT_MAP.setProperty(OSS_OPTIONS_KEY, OSS_ON);
         DEFAULT_MAP.setProperty(DEP_OPTIONS_KEY, DEP_ON);
+        DEFAULT_MAP.setProperty(HEAP_REDUCTION_OPTIONS_KEY, HEAP_REDUCTION_NORMAL);
         DEFAULT_MAP.setProperty(QUERY_OPTIONS_KEY, QUERY_OFF);
         DEFAULT_MAP.setProperty(QUERYAXIOM_OPTIONS_KEY, QUERYAXIOM_ON);
         DEFAULT_MAP.setProperty(NON_LIN_ARITH_OPTIONS_KEY, NON_LIN_ARITH_NONE);
@@ -233,6 +244,7 @@ public StrategyProperties() {
         put(METHOD_OPTIONS_KEY, DEFAULT_MAP.get(METHOD_OPTIONS_KEY));
         put(MPS_OPTIONS_KEY, DEFAULT_MAP.get(MPS_OPTIONS_KEY));
         put(DEP_OPTIONS_KEY, DEFAULT_MAP.get(DEP_OPTIONS_KEY));
+        put(HEAP_REDUCTION_OPTIONS_KEY, DEFAULT_MAP.get(HEAP_REDUCTION_OPTIONS_KEY));
         put(QUERY_OPTIONS_KEY, DEFAULT_MAP.get(QUERY_OPTIONS_KEY));
         put(QUERYAXIOM_OPTIONS_KEY, DEFAULT_MAP.get(QUERYAXIOM_OPTIONS_KEY));
         put(NON_LIN_ARITH_OPTIONS_KEY, DEFAULT_MAP.get(NON_LIN_ARITH_OPTIONS_KEY));
@@ -266,6 +278,7 @@ public static StrategyProperties read(Properties p) {
         sp.put(METHOD_OPTIONS_KEY, readSingleOption(p, METHOD_OPTIONS_KEY));
         sp.put(MPS_OPTIONS_KEY, readSingleOption(p, MPS_OPTIONS_KEY));
         sp.put(DEP_OPTIONS_KEY, readSingleOption(p, DEP_OPTIONS_KEY));
+        sp.put(HEAP_REDUCTION_OPTIONS_KEY, readSingleOption(p, HEAP_REDUCTION_OPTIONS_KEY));
         sp.put(QUERY_OPTIONS_KEY, readSingleOption(p, QUERY_OPTIONS_KEY));
         sp.put(QUERYAXIOM_OPTIONS_KEY, readSingleOption(p, QUERYAXIOM_OPTIONS_KEY));
         sp.put(NON_LIN_ARITH_OPTIONS_KEY, readSingleOption(p, NON_LIN_ARITH_OPTIONS_KEY));
@@ -426,6 +439,7 @@ public void write(Properties p) {
         p.put(STRATEGY_PROPERTY + METHOD_OPTIONS_KEY, get(METHOD_OPTIONS_KEY));
         p.put(STRATEGY_PROPERTY + MPS_OPTIONS_KEY, get(MPS_OPTIONS_KEY));
         p.put(STRATEGY_PROPERTY + DEP_OPTIONS_KEY, get(DEP_OPTIONS_KEY));
+        p.put(STRATEGY_PROPERTY + HEAP_REDUCTION_OPTIONS_KEY, get(HEAP_REDUCTION_OPTIONS_KEY));
         p.put(STRATEGY_PROPERTY + QUERY_OPTIONS_KEY, get(QUERY_OPTIONS_KEY));
         p.put(STRATEGY_PROPERTY + QUERYAXIOM_OPTIONS_KEY, get(QUERYAXIOM_OPTIONS_KEY));
         p.put(STRATEGY_PROPERTY + NON_LIN_ARITH_OPTIONS_KEY, get(NON_LIN_ARITH_OPTIONS_KEY));

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/classicalLogic/firstOrderRules.key

@@ -209,7 +209,7 @@
         \varcond(\newDependingOn(sk, t))
         \replacewith(sk)
         \add(t = sk ==>)
-        \heuristics(semantics_blasting)
+        \heuristics(pull_out_heap)
     };
 
     intro {