SMT test cases rework

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

@@ -92,7 +92,7 @@ private ProofIndependentSMTSettings(ProofIndependentSMTSettings data) {
      */
     private ProofIndependentSMTSettings() {
         // load solver props from standard directory, see PathConfig
-        Collection<SolverType> legacyTypes = SolverTypes.getLegacySolvers();
+        Collection<SolverType> legacyTypes = SolverTypes.getExperimentalSolvers();
         Collection<SolverType> nonLegacyTypes = SolverTypes.getSolverTypes();
         solverTypes.addAll(nonLegacyTypes);
         nonLegacyTypes.removeAll(legacyTypes);

key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java

@@ -132,7 +132,7 @@ public static ImmutableList<PosInOccurrence> getUnsatCore(SMTProblem problem) {
             // Z3 unsat core format: all labels on one line
             numbers = parseZ3Format(lastLine);
         } else if (lastLine.equals(")")) {
-            // CVC5 unsat core format: each label on a separate line
+            // cvc5 unsat core format: each label on a separate line
             numbers = parseCVC5Format(lines);
         } else {
             // unknown format / no unsat core produced
@@ -184,7 +184,7 @@ static Integer[] parseZ3Format(String lastLine) {
     }
 
     /**
-     * Parse CVC5-style unsat core output:
+     * Parse cvc5-style unsat core output:
      *
      * <pre>
      *     (
@@ -193,7 +193,7 @@ static Integer[] parseZ3Format(String lastLine) {
      *     )
      * </pre>
      *
-     * @param lines CVC5 output
+     * @param lines cvc5 output
      * @return list of labels referenced in unsat core
      */
     static Integer[] parseCVC5Format(String[] lines) {

key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverResult.java

@@ -9,23 +9,30 @@
 public class SMTSolverResult {
 
     /**
-     * In the context of proving nodes/sequents these values mean the following: TRUE iff negation
-     * of the sequent is unsatisfiable, FALSIFIABLE iff negation of the sequent is satisfiable (i.e.
-     * it has a counterexample), UNKNOWN otherwise (I'm not sure if this holds if an error occurs)
-     * Note: Currently (1.12.'09) the SMT Solvers do not check if a node is FALSE.
+     * This enum represents the three possible outcomes of an external SMT solver call.
      */
     public enum ThreeValuedTruth {
+        /**
+         * The sequent is valid, i.e. the negation of the sequent is unsatisfiable.
+         */
         VALID {
             @Override
             public String toString() {
                 return "valid";
             }
         },
+        /**
+         * The sequent is falsifiable, i.e. the negation of the sequent is satisfiable (it has a
+         * counterexample).
+         */
         FALSIFIABLE {
             public String toString() {
                 return "there is a counter example";
             }
         },
+        /**
+         * The solver could not determine the validity of the sequent.
+         */
         UNKNOWN {
             public String toString() {
                 return "unknown";
@@ -36,21 +43,24 @@ public String toString() {
     // We should get rid of this constant because it does not track the source (the solver) of the
     // result.
     public static final SMTSolverResult NO_IDEA =
-        new SMTSolverResult(ThreeValuedTruth.UNKNOWN, "?");
-
-
+        new SMTSolverResult(ThreeValuedTruth.UNKNOWN, "?", false);
 
     private final ThreeValuedTruth isValid;
     private static int idCounter = 0;
     private final int id = ++idCounter;
 
     /** This is to identify where the result comes from. E.g. for user feedback. */
-    public final String solverName;
+    private final String solverName;
 
-    private SMTSolverResult(ThreeValuedTruth isValid, String solverName) {
-        this.solverName = solverName;
+    /**
+     * Indicates that the solver timed out. Should only be used in combination with unknown result.
+     */
+    private final boolean timeout;
 
+    private SMTSolverResult(ThreeValuedTruth isValid, String solverName, boolean timeout) {
+        this.solverName = solverName;
         this.isValid = isValid;
+        this.timeout = timeout;
     }
 
     public int getID() {
@@ -59,21 +69,19 @@ public int getID() {
 
 
     public static SMTSolverResult createValidResult(String name) {
-        return new SMTSolverResult(ThreeValuedTruth.VALID, name);
+        return new SMTSolverResult(ThreeValuedTruth.VALID, name, false);
     }
 
 
     public static SMTSolverResult createInvalidResult(String name) {
-        return new SMTSolverResult(ThreeValuedTruth.FALSIFIABLE, name);
+        return new SMTSolverResult(ThreeValuedTruth.FALSIFIABLE, name, false);
     }
 
 
-    public static SMTSolverResult createUnknownResult(String name) {
-        return new SMTSolverResult(ThreeValuedTruth.UNKNOWN, name);
+    public static SMTSolverResult createUnknownResult(String name, boolean timeout) {
+        return new SMTSolverResult(ThreeValuedTruth.UNKNOWN, name, timeout);
     }
 
-
-
     public ThreeValuedTruth isValid() {
         return isValid;
     }

key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC4Socket.java

@@ -48,7 +48,7 @@ public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOEx
                 pipe.sendMessage("(exit)");
                 // pipe.close();
             } else if (msg.equals("unknown")) {
-                sc.setFinalResult(SMTSolverResult.createUnknownResult(getName()));
+                sc.setFinalResult(SMTSolverResult.createUnknownResult(getName(), false));
                 sc.setState(FINISH);
                 pipe.sendMessage("(exit)");
                 // pipe.close();

key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java → key.core/src/main/java/de/uka/ilkd/key/smt/communication/Cvc5Socket.java

@@ -11,17 +11,17 @@
 import org.jspecify.annotations.NonNull;
 
 /**
- * Socket for CVC5 (<a href="https://cvc5.github.io/">...</a>).
+ * Socket for cvc5 (<a href="https://cvc5.github.io/">...</a>).
  */
-public class CVC5Socket extends AbstractSolverSocket {
+public class Cvc5Socket extends AbstractSolverSocket {
 
     /**
-     * Create a new CVC5Socket.
+     * Create a new Cvc5Socket.
      *
      * @param name the socket's name (usually "CVC5", but other solvers might also use it).
      * @param query the ModelExtractor for model interpretation (currently not used by this socket)
      */
-    public CVC5Socket(String name, ModelExtractor query) {
+    public Cvc5Socket(String name, ModelExtractor query) {
         super(name, query);
     }
 
@@ -57,7 +57,7 @@ public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOEx
                 pipe.sendMessage("(exit)");
                 // pipe.close();
             } else if (msg.contains("unknown")) {
-                sc.setFinalResult(SMTSolverResult.createUnknownResult(getName()));
+                sc.setFinalResult(SMTSolverResult.createUnknownResult(getName(), false));
                 sc.setState(FINISH);
                 pipe.sendMessage("(exit)");
                 // pipe.close();
@@ -67,7 +67,7 @@ public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOEx
 
     @Override
     public AbstractSolverSocket copy() {
-        return new CVC5Socket(getName(), getQuery());
+        return new Cvc5Socket(getName(), getQuery());
     }
 
 }

key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java

@@ -47,7 +47,7 @@ public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOEx
                 sc.setState(WAIT_FOR_MODEL);
             }
             if (msg.equals("unknown")) {
-                sc.setFinalResult(SMTSolverResult.createUnknownResult(getName()));
+                sc.setFinalResult(SMTSolverResult.createUnknownResult(getName(), false));
                 sc.setState(WAIT_FOR_DETAILS);
                 pipe.sendMessage("(exit)");
             }

key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java

@@ -52,7 +52,7 @@ public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOEx
 
             }
             if (msg.equals("unknown")) {
-                sc.setFinalResult(SMTSolverResult.createUnknownResult(getName()));
+                sc.setFinalResult(SMTSolverResult.createUnknownResult(getName(), false));
                 pipe.sendMessage("(exit)\n");
                 sc.setState(WAIT_FOR_DETAILS);
             }

key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java

@@ -44,7 +44,7 @@ public class ModularSMTLib2Translator implements SMTTranslator {
      * Handler option. If provided, the translator will label translations of sequent formulas such
      * that {@link de.uka.ilkd.key.smt.SMTFocusResults} can interpret the unsat core.
      * <p>
-     * This option is currently only enabled for Z3 and CVC5 (needs 1.0.4+).
+     * This option is currently only enabled for Z3 and cvc5 (needs 1.0.4+).
      * </p>
      * Make sure to also send (get-unsat-core) in the respective socket class when adding this
      * option.

key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java

@@ -48,9 +48,9 @@ public class SolverPropertiesLoader {
      */
     private static final Collection<SolverType> SOLVERS = new ArrayList<>(5);
     /**
-     * The LEGACY solvers loaded by this loader.
+     * The EXPERIMENTAL solvers loaded by this loader.
      */
-    private static final Collection<SolverType> LEGACY_SOLVERS = new ArrayList<>(2);
+    private static final Collection<SolverType> EXPERIMENTAL_SOLVERS = new ArrayList<>(2);
 
     /**
      * String used to SPLIT list properties such as the delimiter list or the handler list.
@@ -135,10 +135,10 @@ public class SolverPropertiesLoader {
      */
     private static final String MIN_VERSION = "minVersion";
     /**
-     * The .props key for signalling whether the solver is a LEGACY solver (only used in
+     * The .props key for signalling whether the solver is an EXPERIMENTAL solver (only used in
      * experimental mode). Default value is false.
      */
-    private static final String LEGACY = "legacy";
+    private static final String EXPERIMENTAL = "experimental";
     /**
      * The .props key for the solver's
      * {@link de.uka.ilkd.key.smt.communication.AbstractSolverSocket}. Default socket is
@@ -170,7 +170,7 @@ public class SolverPropertiesLoader {
      * All supported keys for solver props files.
      */
     private static final String[] SUPPORTED_KEYS = { NAME, VERSION, COMMAND, PARAMS, DELIMITERS,
-        INFO, MIN_VERSION, LEGACY, TIMEOUT, SOLVER_SOCKET_CLASS, TRANSLATOR_CLASS,
+        INFO, MIN_VERSION, EXPERIMENTAL, TIMEOUT, SOLVER_SOCKET_CLASS, TRANSLATOR_CLASS,
         HANDLER_NAMES, HANDLER_OPTIONS, PREAMBLE_FILE };
 
     /**
@@ -211,22 +211,24 @@ public Collection<SolverType> getSolvers() {
             for (Properties solverProp : loadSolvers()) {
                 SolverType createdType = makeSolver(solverProp);
                 SOLVERS.add(createdType);
-                // If the solver is a LEGACY solver (only available in experimental mode),
-                // add it to the separate list:
-                if (SettingsConverter.read(solverProp, LEGACY, false)) {
-                    LEGACY_SOLVERS.add(createdType);
+                /*
+                 * If the solver is an EXPERIMENTAL solver (only available in experimental mode),
+                 * add it to the separate list:
+                 */
+                if (SettingsConverter.read(solverProp, EXPERIMENTAL, false)) {
+                    EXPERIMENTAL_SOLVERS.add(createdType);
                 }
             }
         }
         return new ArrayList<>(SOLVERS);
     }
 
     /**
-     * @return a copy of the created list of legacy solvers
+     * @return a copy of the created list of experimental solvers
      */
-    public Collection<SolverType> getLegacySolvers() {
+    public Collection<SolverType> getExperimentalSolvers() {
         getSolvers();
-        return new ArrayList<>(LEGACY_SOLVERS);
+        return new ArrayList<>(EXPERIMENTAL_SOLVERS);
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypes.java

@@ -19,15 +19,15 @@
 public final class SolverTypes {
 
     /**
-     * All available solver types, including legacy solvers. The objects in this map are identically
-     * returned whenever {@link #getSolverTypes()} is called.
+     * All available solver types, including experimental solvers. The objects in this map are
+     * identically returned whenever {@link #getSolverTypes()} is called.
      */
     private static final Collection<SolverType> SOLVERS = new ArrayList<>(5);
     /**
-     * The available legacy solvers out of the {@link #SOLVERS} list. The objects in this map are
-     * identically returned whenever {@link #getLegacySolvers()} is called.
+     * The available experimental solvers out of the {@link #SOLVERS} list. The objects in this map
+     * are identically returned whenever {@link #getExperimentalSolvers()} is called.
      */
-    private static final Collection<SolverType> LEGACY_SOLVERS = new ArrayList<>(1);
+    private static final Collection<SolverType> EXPERIMENTAL_SOLVERS = new ArrayList<>(1);
 
     private SolverTypes() {
 
@@ -37,27 +37,28 @@ private SolverTypes() {
      * Loads and returns the available solver types using the {@link SolverPropertiesLoader}. The
      * returned SolverType objects don't change (singletons).
      *
-     * @return the available solver types, including legacy solvers
+     * @return the available solver types, including experimental solvers
      */
     public static @NonNull Collection<SolverType> getSolverTypes() {
         if (SOLVERS.isEmpty()) {
             SolverPropertiesLoader solverLoader = new SolverPropertiesLoader();
             SOLVERS.addAll(solverLoader.getSolvers());
-            LEGACY_SOLVERS.addAll(solverLoader.getLegacySolvers());
+            EXPERIMENTAL_SOLVERS.addAll(solverLoader.getExperimentalSolvers());
         }
         return new ArrayList<>(SOLVERS);
     }
 
     /**
-     * Returns the available legacy solver types according to the {@link SolverPropertiesLoader}.
+     * Returns the available experimental solver types according to the
+     * {@link SolverPropertiesLoader}.
      *
-     * @return the available legacy solver types
+     * @return the available experimental solver types
      */
-    public static @NonNull Collection<SolverType> getLegacySolvers() {
+    public static @NonNull Collection<SolverType> getExperimentalSolvers() {
         if (SOLVERS.isEmpty()) {
             getSolverTypes();
         }
-        return new ArrayList<>(LEGACY_SOLVERS);
+        return new ArrayList<>(EXPERIMENTAL_SOLVERS);
     }
 
     /**

key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/AddingSMTSolvers.md

@@ -109,7 +109,7 @@ If you want to use another, more solver-specific preamble, the file should be pu
 preamble = specialPreamble.smt2
 ```
 
-If this is true, the solver is only usable in experimental mode. Generally, those are the solvers that still use the SmtLib2Translator instead of the ModularSMTLib2Translator. The property is false by default, if not specified.
+If this is true, the solver is only usable in experimental mode. The property is false by default, if not specified. Generally, it is a good idea to set this to true for solvers that still use the SmtLib2Translator (legacy translation) instead of the ModularSMTLib2Translator.
 ```properties
-legacy=true/false
+experimental=true/false
 ```

key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4.props

@@ -1,3 +1,4 @@
+experimental=true
 params=--no-print-success --produce-models --no-interactive --lang smt2
 timeout=-1
 name=CVC4

key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props

@@ -1,9 +1,9 @@
-legacy=true
+experimental=true
 params=--no-print-success --produce-models --no-interactive --lang smt2
 timeout=-1
 name=CVC4 (Legacy Translation)
 info=CVC4 solver
 command=cvc4
 version=--version
-socketClass=socketClass=de.uka.ilkd.key.smt.communication.CVC4Socket
+socketClass=de.uka.ilkd.key.smt.communication.CVC4Socket
 translatorClass=de.uka.ilkd.key.smt.SmtLib2Translator

key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props

@@ -1,10 +1,10 @@
 params=--no-interactive --produce-models --lang smt2
 timeout=-1
-name=CVC5
-info=CVC5 solver (https://cvc5.github.io/).
+name=cvc5
+info=cvc5 solver (https://cvc5.github.io/).
 command=cvc5
 version=--version
-socketClass=de.uka.ilkd.key.smt.communication.CVC5Socket
+socketClass=de.uka.ilkd.key.smt.communication.Cvc5Socket
 handlers=de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler,\
 de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler,\
 de.uka.ilkd.key.smt.newsmt2.QuantifierHandler,\

key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_legacy.props

@@ -1,4 +1,4 @@
-legacy=true
+experimental=true
 params=-in -smt2
 timeout=-1
 name=Z3 (Legacy Translation)