Add user-defined strategy presets to the strategy options pane

key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java

@@ -59,6 +59,7 @@ public class ProofIndependentSettings {
     private final ViewSettings viewSettings = new ViewSettings();
     private final TermLabelSettings termLabelSettings = new TermLabelSettings();
     private final FeatureSettings featureSettings = new FeatureSettings();
+    private final StrategyPresetsSettings strategyPresetsSettings = new StrategyPresetsSettings();
 
     private File filename;
 
@@ -75,6 +76,7 @@ private ProofIndependentSettings() {
         addSettings(generalSettings);
         addSettings(viewSettings);
         addSettings(featureSettings);
+        addSettings(strategyPresetsSettings);
     }
 
     private ProofIndependentSettings(File filename) {
@@ -193,6 +195,10 @@ public FeatureSettings getFeatureSettings() {
         return featureSettings;
     }
 
+    public StrategyPresetsSettings getStrategyPresetsSettings() {
+        return strategyPresetsSettings;
+    }
+
     /**
      * Checks if pretty printing is enabled or not.
      *

key.core/src/main/java/de/uka/ilkd/key/settings/StrategyPresetsSettings.java

@@ -0,0 +1,213 @@
+/* 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.settings;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Optional;
+import java.util.Properties;
+
+import de.uka.ilkd.key.strategy.StrategyProperties;
+
+import org.jspecify.annotations.NonNull;
+
+/**
+ * User-defined strategy presets shown in the strategy options combo box.
+ * <p>
+ * In addition to the built-in presets (defined in code by the profile's
+ * {@link de.uka.ilkd.key.strategy.definition.StrategySettingsDefinition}), the user may store the
+ * currently selected strategy options under a name and re-select them later. Each preset captures a
+ * complete {@link StrategyProperties} value set together with the maximal number of rule
+ * applications.
+ * <p>
+ * A single reserved preset named {@value #STASH_NAME} is used for the "stash current settings"
+ * quick action: stashing again simply overwrites it.
+ * <p>
+ * Presets are persisted as part of the proof-independent settings. Persistence uses the
+ * {@link Configuration} (JSON-like) format only; the deprecated flat {@link Properties} format is
+ * not supported for presets (KeY writes the {@link Configuration} format on every save anyway).
+ */
+public class StrategyPresetsSettings extends AbstractSettings {
+    /** Category / top-level key under which the presets are stored. */
+    public static final String CATEGORY = "StrategyPresets";
+
+    /** Name of the reserved single-slot stash preset. */
+    public static final String STASH_NAME = "Stash";
+
+    /** Property name fired whenever the set of presets changes. */
+    public static final String PROP_PRESETS = "presets";
+
+    /** Configuration key for a preset's display name. */
+    private static final String KEY_NAME = "name";
+
+    /** Configuration key for a preset's maximal rule applications. */
+    private static final String KEY_MAX_STEPS = "maxSteps";
+
+    /** Fallback max. rule applications if a stored preset lacks the entry. */
+    private static final int DEFAULT_MAX_STEPS = 10000;
+
+    /** The stored presets, in insertion order. */
+    private final List<StrategyPreset> presets = new ArrayList<>();
+
+    /**
+     * A single named strategy preset.
+     *
+     * @param name display name; unique among the stored presets
+     * @param maxSteps captured maximal number of rule applications
+     * @param properties captured (complete) strategy properties
+     */
+    public record StrategyPreset(String name, int maxSteps, StrategyProperties properties) {
+        public StrategyPreset {
+            properties = (StrategyProperties) properties.clone();
+        }
+
+        @Override
+        public StrategyProperties properties() {
+            return (StrategyProperties) properties.clone();
+        }
+    }
+
+    /**
+     * @return an unmodifiable snapshot of the stored presets in insertion order
+     */
+    public List<StrategyPreset> getPresets() {
+        return List.copyOf(presets);
+    }
+
+    /**
+     * Looks up a preset by name.
+     *
+     * @param name the preset name
+     * @return the preset, if present
+     */
+    public Optional<StrategyPreset> getPreset(String name) {
+        return presets.stream().filter(p -> p.name().equals(name)).findFirst();
+    }
+
+    /**
+     * @param name a preset name
+     * @return {@code true} if a preset with the given name is stored
+     */
+    public boolean contains(String name) {
+        return getPreset(name).isPresent();
+    }
+
+    /**
+     * Adds a new preset or replaces an existing one with the same name. The preset keeps its
+     * original position when replaced, otherwise it is appended.
+     *
+     * @param preset the preset to store
+     */
+    public void saveOrUpdate(StrategyPreset preset) {
+        for (int i = 0; i < presets.size(); i++) {
+            if (presets.get(i).name().equals(preset.name())) {
+                presets.set(i, preset);
+                firePropertyChange(PROP_PRESETS, null, preset.name());
+                return;
+            }
+        }
+        presets.add(preset);
+        firePropertyChange(PROP_PRESETS, null, preset.name());
+    }
+
+    /**
+     * Overwrites the reserved {@value #STASH_NAME} preset with the given settings.
+     *
+     * @param maxSteps the maximal number of rule applications to capture
+     * @param properties the strategy properties to capture
+     */
+    public void stash(int maxSteps, StrategyProperties properties) {
+        saveOrUpdate(new StrategyPreset(STASH_NAME, maxSteps, properties));
+    }
+
+    /**
+     * Removes the preset with the given name (if present).
+     *
+     * @param name the preset name
+     * @return {@code true} if a preset was removed
+     */
+    public boolean remove(String name) {
+        if (presets.removeIf(p -> p.name().equals(name))) {
+            firePropertyChange(PROP_PRESETS, name, null);
+            return true;
+        }
+        return false;
+    }
+
+    /**
+     * Renames a preset, keeping its position and captured settings.
+     *
+     * @param oldName the current name
+     * @param newName the new name; must not already be in use by a different preset
+     * @return {@code true} if the rename succeeded
+     */
+    public boolean rename(String oldName, String newName) {
+        if (oldName.equals(newName)) {
+            return true;
+        }
+        if (contains(newName)) {
+            return false;
+        }
+        for (int i = 0; i < presets.size(); i++) {
+            StrategyPreset p = presets.get(i);
+            if (p.name().equals(oldName)) {
+                presets.set(i, new StrategyPreset(newName, p.maxSteps(), p.properties()));
+                firePropertyChange(PROP_PRESETS, oldName, newName);
+                return true;
+            }
+        }
+        return false;
+    }
+
+    @Override
+    public void readSettings(@NonNull Configuration props) {
+        presets.clear();
+        List<Configuration> stored = props.getList(CATEGORY, Configuration.class);
+        if (stored == null) {
+            return;
+        }
+        for (Configuration entry : stored) {
+            String name = entry.getString(KEY_NAME);
+            if (name == null || name.isEmpty()) {
+                continue;
+            }
+            int maxSteps = entry.getInt(KEY_MAX_STEPS, DEFAULT_MAX_STEPS);
+            StrategyProperties properties = StrategyProperties.read(entry);
+            presets.add(new StrategyPreset(name, maxSteps, properties));
+        }
+    }
+
+    @Override
+    public void writeSettings(@NonNull Configuration props) {
+        List<Configuration> stored = new ArrayList<>(presets.size());
+        for (StrategyPreset preset : presets) {
+            Configuration entry = new Configuration();
+            entry.set(KEY_NAME, preset.name());
+            entry.set(KEY_MAX_STEPS, preset.maxSteps());
+            preset.properties().write(entry);
+            stored.add(entry);
+        }
+        props.set(CATEGORY, stored);
+    }
+
+    /**
+     * Presets are only persisted via the {@link Configuration} format; the deprecated flat
+     * {@link Properties} format cannot represent a list of presets and is intentionally not
+     * supported here.
+     */
+    @Override
+    public void readSettings(Properties props) {
+        // intentionally empty: see class documentation
+    }
+
+    /**
+     * Presets are only persisted via the {@link Configuration} format; the deprecated flat
+     * {@link Properties} format cannot represent a list of presets and is intentionally not
+     * supported here.
+     */
+    @Override
+    public void writeSettings(Properties props) {
+        // intentionally empty: see class documentation
+    }
+}

key.core/src/test/java/de/uka/ilkd/key/settings/StrategyPresetsSettingsTest.java

@@ -0,0 +1,134 @@
+/* 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.settings;
+
+import java.io.IOException;
+import java.io.StringWriter;
+
+import de.uka.ilkd.key.settings.StrategyPresetsSettings.StrategyPreset;
+import de.uka.ilkd.key.strategy.StrategyProperties;
+
+import org.antlr.v4.runtime.CharStreams;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+/**
+ * Tests for {@link StrategyPresetsSettings}: the in-memory bookkeeping (add / overwrite / stash /
+ * rename / remove) and the {@link Configuration} persistence round-trip.
+ */
+class StrategyPresetsSettingsTest {
+
+    private static StrategyProperties props(String splitting, String loop) {
+        StrategyProperties p = new StrategyProperties();
+        p.setProperty(StrategyProperties.SPLITTING_OPTIONS_KEY, splitting);
+        p.setProperty(StrategyProperties.LOOP_OPTIONS_KEY, loop);
+        return p;
+    }
+
+    @Test
+    void saveKeepsInsertionOrderAndOverwritesByName() {
+        StrategyPresetsSettings s = new StrategyPresetsSettings();
+        s.saveOrUpdate(new StrategyPreset("arith", 4000,
+            props(StrategyProperties.SPLITTING_OFF, StrategyProperties.LOOP_NONE)));
+        s.saveOrUpdate(new StrategyPreset("loops", 8000,
+            props(StrategyProperties.SPLITTING_NORMAL, StrategyProperties.LOOP_INVARIANT)));
+
+        assertEquals(2, s.getPresets().size());
+        assertEquals("arith", s.getPresets().get(0).name());
+        assertEquals("loops", s.getPresets().get(1).name());
+
+        // overwriting an existing name keeps its position but replaces the payload
+        s.saveOrUpdate(new StrategyPreset("arith", 1234,
+            props(StrategyProperties.SPLITTING_DELAYED, StrategyProperties.LOOP_EXPAND)));
+        assertEquals(2, s.getPresets().size());
+        assertEquals("arith", s.getPresets().get(0).name());
+        assertEquals(1234, s.getPreset("arith").orElseThrow().maxSteps());
+    }
+
+    @Test
+    void stashUsesReservedSingleSlot() {
+        StrategyPresetsSettings s = new StrategyPresetsSettings();
+        s.stash(5000, props(StrategyProperties.SPLITTING_OFF, StrategyProperties.LOOP_NONE));
+        s.stash(6000, props(StrategyProperties.SPLITTING_NORMAL, StrategyProperties.LOOP_EXPAND));
+
+        assertEquals(1, s.getPresets().size(), "stashing twice must not create a second slot");
+        StrategyPreset stash = s.getPreset(StrategyPresetsSettings.STASH_NAME).orElseThrow();
+        assertEquals(6000, stash.maxSteps());
+        assertEquals(StrategyProperties.SPLITTING_NORMAL,
+            stash.properties().getProperty(StrategyProperties.SPLITTING_OPTIONS_KEY));
+    }
+
+    @Test
+    void renameRejectsCollisionAndUpdatesOtherwise() {
+        StrategyPresetsSettings s = new StrategyPresetsSettings();
+        s.saveOrUpdate(new StrategyPreset("a", 1, props(StrategyProperties.SPLITTING_OFF,
+            StrategyProperties.LOOP_NONE)));
+        s.saveOrUpdate(new StrategyPreset("b", 2, props(StrategyProperties.SPLITTING_OFF,
+            StrategyProperties.LOOP_NONE)));
+
+        assertFalse(s.rename("a", "b"), "must not rename onto an existing name");
+        assertTrue(s.contains("a"));
+
+        assertTrue(s.rename("a", "c"));
+        assertFalse(s.contains("a"));
+        assertTrue(s.contains("c"));
+        assertEquals(1, s.getPreset("c").orElseThrow().maxSteps());
+    }
+
+    @Test
+    void removeDropsPreset() {
+        StrategyPresetsSettings s = new StrategyPresetsSettings();
+        s.saveOrUpdate(new StrategyPreset("a", 1, props(StrategyProperties.SPLITTING_OFF,
+            StrategyProperties.LOOP_NONE)));
+        assertTrue(s.remove("a"));
+        assertFalse(s.remove("a"));
+        assertTrue(s.getPresets().isEmpty());
+    }
+
+    @Test
+    void configurationRoundTripPreservesEverything() throws IOException {
+        StrategyPresetsSettings original = new StrategyPresetsSettings();
+        original.saveOrUpdate(new StrategyPreset("arith", 4000,
+            props(StrategyProperties.SPLITTING_OFF, StrategyProperties.LOOP_NONE)));
+        original.saveOrUpdate(new StrategyPreset("loops", 8000,
+            props(StrategyProperties.SPLITTING_NORMAL, StrategyProperties.LOOP_INVARIANT)));
+        original.stash(5000, props(StrategyProperties.SPLITTING_DELAYED,
+            StrategyProperties.LOOP_EXPAND));
+
+        // write -> serialize to text -> reparse -> read (mirrors the actual settings file path)
+        Configuration written = new Configuration();
+        original.writeSettings(written);
+        StringWriter out = new StringWriter();
+        written.save(out, "");
+        Configuration reparsed = Configuration.load(CharStreams.fromString(out.toString()));
+
+        StrategyPresetsSettings restored = new StrategyPresetsSettings();
+        restored.readSettings(reparsed);
+
+        assertEquals(3, restored.getPresets().size());
+        assertEquals("arith", restored.getPresets().get(0).name());
+        assertEquals("loops", restored.getPresets().get(1).name());
+        assertEquals(StrategyPresetsSettings.STASH_NAME, restored.getPresets().get(2).name());
+
+        StrategyPreset arith = restored.getPreset("arith").orElseThrow();
+        assertEquals(4000, arith.maxSteps());
+        assertEquals(StrategyProperties.SPLITTING_OFF,
+            arith.properties().getProperty(StrategyProperties.SPLITTING_OPTIONS_KEY));
+        assertEquals(StrategyProperties.LOOP_NONE,
+            arith.properties().getProperty(StrategyProperties.LOOP_OPTIONS_KEY));
+
+        StrategyPreset loops = restored.getPreset("loops").orElseThrow();
+        assertEquals(8000, loops.maxSteps());
+        assertEquals(StrategyProperties.LOOP_INVARIANT,
+            loops.properties().getProperty(StrategyProperties.LOOP_OPTIONS_KEY));
+    }
+
+    @Test
+    void readingEmptyConfigurationYieldsNoPresets() {
+        StrategyPresetsSettings s = new StrategyPresetsSettings();
+        s.readSettings(new Configuration());
+        assertTrue(s.getPresets().isEmpty());
+    }
+}