Get rid of experimental flag using more fine-grained flags

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

@@ -111,7 +111,7 @@ public void readSettings(Configuration props) {
         if (cat == null)
             return;
         propertyEntries.forEach(it -> {
-            final var value = cat.get(it.getKey());
+            final var value = it.fromObject(cat.get(it.getKey()));
             if (value != null) {
                 properties.put(it.getKey(), value);
             }
@@ -127,39 +127,45 @@ public void writeSettings(Configuration props) {
     }
 
     protected PropertyEntry<Double> createDoubleProperty(String key, double defValue) {
-        PropertyEntry<Double> pe = new DefaultPropertyEntry<>(key, defValue, parseDouble);
+        PropertyEntry<Double> pe =
+            new DefaultPropertyEntry<>(key, defValue, parseDouble, (it) -> (double) it);
         propertyEntries.add(pe);
         return pe;
     }
 
     protected PropertyEntry<Integer> createIntegerProperty(String key, int defValue) {
-        PropertyEntry<Integer> pe = new DefaultPropertyEntry<>(key, defValue, parseInt);
+        PropertyEntry<Integer> pe = new DefaultPropertyEntry<>(key, defValue, parseInt,
+            (it) -> Math.toIntExact((Long) it));
         propertyEntries.add(pe);
         return pe;
     }
 
     protected PropertyEntry<Float> createFloatProperty(String key, float defValue) {
-        PropertyEntry<Float> pe = new DefaultPropertyEntry<>(key, defValue, parseFloat);
+        PropertyEntry<Float> pe =
+            new DefaultPropertyEntry<>(key, defValue, parseFloat, (it) -> (float) (double) it);
         propertyEntries.add(pe);
         return pe;
     }
 
     protected PropertyEntry<String> createStringProperty(String key, String defValue) {
-        PropertyEntry<String> pe = new DefaultPropertyEntry<>(key, defValue, id -> id);
+        PropertyEntry<String> pe =
+            new DefaultPropertyEntry<>(key, defValue, id -> id, Object::toString);
         propertyEntries.add(pe);
         return pe;
     }
 
     protected PropertyEntry<Boolean> createBooleanProperty(String key, boolean defValue) {
-        PropertyEntry<Boolean> pe = new DefaultPropertyEntry<>(key, defValue, parseBoolean);
+        PropertyEntry<Boolean> pe =
+            new DefaultPropertyEntry<>(key, defValue, parseBoolean, (it) -> (Boolean) it);
         propertyEntries.add(pe);
         return pe;
     }
 
     protected PropertyEntry<Set<String>> createStringSetProperty(String key, String defValue) {
         PropertyEntry<Set<String>> pe = new DefaultPropertyEntry<>(key, parseStringSet(defValue),
             AbstractPropertiesSettings::parseStringSet,
-            AbstractPropertiesSettings::stringSetToString);
+            AbstractPropertiesSettings::stringSetToString,
+            (it) -> new LinkedHashSet<>((Collection<String>) it));
         propertyEntries.add(pe);
         return pe;
     }
@@ -175,7 +181,7 @@ protected PropertyEntry<List<String>> createStringListProperty(@NonNull String k
             @Nullable String defValue) {
         PropertyEntry<List<String>> pe = new DefaultPropertyEntry<>(key, parseStringList(defValue),
             AbstractPropertiesSettings::parseStringList,
-            AbstractPropertiesSettings::stringListToString);
+            AbstractPropertiesSettings::stringListToString, it -> (List<String>) it);
         propertyEntries.add(pe);
         return pe;
     }
@@ -195,6 +201,8 @@ default void update() {
         }
 
         String value();
+
+        T fromObject(@Nullable Object o);
     }
 
 
@@ -204,16 +212,20 @@ class DefaultPropertyEntry<T> implements PropertyEntry<T> {
         private final Function<String, T> convert;
         private final Function<T, String> toString;
 
-        private DefaultPropertyEntry(String key, T defaultValue, Function<String, T> convert) {
-            this(key, defaultValue, convert, Objects::toString);
+        private final Function<Object, T> fromObject;
+
+        private DefaultPropertyEntry(String key, T defaultValue, Function<String, T> convert,
+                Function<Object, T> fromObject) {
+            this(key, defaultValue, convert, Objects::toString, fromObject);
         }
 
         private DefaultPropertyEntry(String key, T defaultValue, Function<String, T> convert,
-                Function<T, String> toString) {
+                Function<T, String> toString, Function<Object, T> fromObject) {
             this.key = key;
             this.defaultValue = defaultValue;
             this.convert = convert;
             this.toString = toString;
+            this.fromObject = fromObject;
         }
 
         @Override
@@ -255,5 +267,10 @@ public String value() {
                 return toString.apply(v);
             }
         }
+
+        @Override
+        public T fromObject(@Nullable Object o) {
+            return fromObject.apply(o);
+        }
     }
 }

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

@@ -0,0 +1,206 @@
+/* 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.*;
+import java.util.function.Consumer;
+
+import org.jspecify.annotations.NonNull;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+/**
+ * Feature flags for the selected and deselected of experimental features.
+ * <p>
+ * In the old days of KeY, we used to have {@code --experimental} flag, which was a bad idea.
+ * You cannot control which feature you want to activate.
+ * Instead, you are getting the full load of fun(ctionality). This class allows you to have more
+ * fine-grained feature flags by defining feature flags which are controllable by the user.
+ *
+ * @author Alexander Weigl
+ * @version 1 (04.12.23)
+ */
+public class FeatureSettings extends AbstractSettings {
+    private static final Logger LOGGER = LoggerFactory.getLogger(FeatureSettings.class);
+    private static final String CATEGORY = "Feature";
+
+    /**
+     * unstored, set by {@code --experimental}
+     */
+    private boolean activateAll = false;
+
+    /**
+     * persistent list of activated features
+     */
+    private final Set<String> activatedFeatures = new TreeSet<>();
+
+    public FeatureSettings() {
+        readFromSystemProperties();
+    }
+
+    public static boolean isFeatureActivated(Feature f) {
+        return ProofIndependentSettings.DEFAULT_INSTANCE.getFeatureSettings().isActivated(f);
+    }
+
+    public static boolean isFeatureActivated(String s) {
+        return ProofIndependentSettings.DEFAULT_INSTANCE.getFeatureSettings().isActivated(s);
+    }
+
+    /**
+     * Helper function for notification on feature flag changes.
+     *
+     * @param feature the feature to be listening on
+     * @param update a callback function which gets informed on changes with the new value
+     */
+    public static void on(Feature feature, Consumer<Boolean> update) {
+        ProofIndependentSettings.DEFAULT_INSTANCE.getFeatureSettings().addPropertyChangeListener(
+            feature.id, evt -> update.accept((Boolean) evt.getNewValue()));
+    }
+
+    /**
+     * Helper function for notification on feature flag changes which also calls the consumer.
+     *
+     * @param feature the feature to be listening on
+     * @param update a callback function which gets informed on changes with the new value
+     */
+    public static void onAndActivate(Feature feature, Consumer<Boolean> update) {
+        on(feature, update);
+        update.accept(isFeatureActivated(feature));
+    }
+
+    /**
+     * Use the system properties ({@code -P FEATURE:XXX=true} to activate a feature from the command
+     * line.
+     */
+    private void readFromSystemProperties() {
+        var prefix = CATEGORY.toUpperCase() + ":";
+        for (Map.Entry<Object, Object> entries : System.getProperties().entrySet()) {
+            final var s = entries.getKey().toString();
+            if (s.startsWith(prefix) && isTrue(entries.getValue())) {
+                final var feature = s.substring(prefix.length());
+                activate(feature);
+                LOGGER.info("Activate feature: {}", feature);
+            }
+        }
+    }
+
+    /**
+     * Checks if the given {@code value} represents something like to true.
+     *
+     * @return true, if {@code value} feels like a feature activation.
+     */
+    private boolean isTrue(Object value) {
+        return switch (value.toString().toLowerCase()) {
+        case "true", "yes", "on" -> true;
+        default -> false;
+        };
+    }
+
+    @Override
+    public void readSettings(Properties props) {
+        activatedFeatures.clear();
+        var prefix = "[" + CATEGORY + "]";
+        for (Map.Entry<Object, Object> entries : props.entrySet()) {
+            final var s = entries.getKey().toString();
+            if (s.startsWith(prefix) && isTrue(entries.getValue())) {
+                final var feature = s.substring(prefix.length());
+                activate(feature);
+                LOGGER.info("Activate feature: {}", feature);
+            }
+        }
+    }
+
+    @Override
+    public void writeSettings(Properties props) {
+        var prefix = "[" + CATEGORY + "]";
+        for (String activatedFeature : activatedFeatures) {
+            props.put(prefix + activatedFeature, "true");
+        }
+    }
+
+    @Override
+    public void readSettings(@NonNull Configuration props) {
+        activatedFeatures.clear();
+        for (String s : props.getStringList(CATEGORY)) {
+            activate(s);
+        }
+    }
+
+    @Override
+    public void writeSettings(@NonNull Configuration props) {
+        props.set(CATEGORY, activatedFeatures.stream().toList());
+    }
+
+    public boolean isActivated(Feature f) {
+        return isActivated(f.id);
+    }
+
+    private boolean isActivated(String id) {
+        if (activateAll)
+            return true;
+        return activatedFeatures.contains(id);
+    }
+
+    /**
+     * Activates the given feature {@code f}.
+     */
+    public void activate(Feature f) {
+        activate(f.id);
+    }
+
+    /**
+     * Activates the given feature by {@code id}.
+     */
+    private void activate(String id) {
+        if (!isActivated(id)) {
+            activatedFeatures.add(id);
+            firePropertyChange(id, false, isActivated(id));
+        }
+    }
+
+    /**
+     * Deactivates the given feature {@code f}.
+     */
+    public void deactivate(Feature f) {
+        deactivate(f.id);
+    }
+
+    /**
+     * Deactivates the given feature by {@code id}.
+     */
+    private void deactivate(String id) {
+        if (isActivated(id)) {
+            firePropertyChange(id, true, isActivated(id));
+            activatedFeatures.remove(id);
+        }
+    }
+
+    public void setActivateAll(boolean b) {
+        activateAll = b;
+    }
+
+    public boolean isActivateAll() {
+        return activateAll;
+    }
+
+    public static Feature createFeature(String id) {
+        return createFeature(id, "", true);
+    }
+
+    public static Feature createFeature(String id, String doc) {
+        return new Feature(id, doc, true);
+    }
+
+    public static Feature createFeature(String id, String doc, boolean restartRequired) {
+        return new Feature(id, doc, restartRequired);
+    }
+
+    public record Feature(String id, String documentation, boolean restartRequired) {
+        public static final List<Feature> FEATURES = new ArrayList<>();
+
+        public Feature {
+            FEATURES.add(this);
+        }
+    }
+}

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

@@ -12,6 +12,8 @@
 import de.uka.ilkd.key.smt.solvertypes.SolverType;
 import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
 
+import static de.uka.ilkd.key.settings.FeatureSettings.createFeature;
+
 public final class ProofIndependentSMTSettings extends AbstractSettings {
     private static final String CATEGORY = "SMTSettings";
     public static final String ACTIVE_SOLVER = "ActiveSolver";
@@ -49,6 +51,9 @@ public final class ProofIndependentSMTSettings extends AbstractSettings {
     public static final String PROP_STORE_TACLET_TRANSLATION_FILE =
         "PROP_STORE_TACLET_TRANSLATION_FILE";
 
+    private static final FeatureSettings.Feature FEATURE_EXPERIMENTAL_SMT_SOLVERS =
+        createFeature("EXPERIMENTAL_SMT_SOLVERS", "Activate experimental SMT solvers");
+
     private final Collection<SolverType> solverTypes = new LinkedList<>();
     private boolean showResultsAfterExecution = false;
     private boolean storeSMTTranslationToFile = false;
@@ -497,6 +502,11 @@ public SolverTypeCollection computeActiveSolverUnion() {
     }
 
 
+    public Collection<SolverTypeCollection> getUsableSolverUnions() {
+        return getUsableSolverUnions(
+            FeatureSettings.isFeatureActivated(FEATURE_EXPERIMENTAL_SMT_SOLVERS));
+    }
+
     public Collection<SolverTypeCollection> getUsableSolverUnions(boolean experimental) {
         LinkedList<SolverTypeCollection> unions = new LinkedList<>();
         for (SolverTypeCollection union : getSolverUnions(experimental)) {
@@ -507,6 +517,11 @@ public Collection<SolverTypeCollection> getUsableSolverUnions(boolean experiment
         return unions;
     }
 
+    public Collection<SolverTypeCollection> getSolverUnions() {
+        return getSolverUnions(
+            FeatureSettings.isFeatureActivated(FEATURE_EXPERIMENTAL_SMT_SOLVERS));
+    }
+
     public Collection<SolverTypeCollection> getSolverUnions(boolean experimental) {
         LinkedList<SolverTypeCollection> res = new LinkedList<>(solverUnions);
         if (experimental) {