Warn on missing SMT solvers if flag is set

key.core/src/test/java/de/uka/ilkd/key/smt/SmtTestUtils.java

@@ -0,0 +1,58 @@
+/* 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.smt;
+
+import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation;
+import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
+
+import org.junit.jupiter.api.Assertions;
+import org.junit.jupiter.api.Assumptions;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (5/5/25)
+ */
+public class SmtTestUtils {
+
+    /// Variable signals whether a missing SMT solver should result into a abortion of the test
+    /// cases or a failing of the test case.
+    /// Flag is triggered by the environment variable `failIfSmtSolverIsUnavailable` or
+    /// `GITHUB_ACTIONS`.
+    public static final boolean failIfSmtSolverIsUnavailable =
+        Boolean.parseBoolean(System.getenv("failIfSmtSolverIsUnavailable"))
+                || Boolean.parseBoolean(System.getenv("GITHUB_ACTIONS"));
+
+    private static final String REQUIRED_SMT_SOLVER_NOT_INSTALLED =
+        "required SMT solver not installed";
+
+
+    /// Return true if z3 is installed. This means an {@link
+    /// de.uka.ilkd.key.smt.solvertypes.SolverType}
+    /// for z3 is available and it returned true for being installed.
+    ///
+    /// @see de.uka.ilkd.key.smt.solvertypes.SolverType#isInstalled(boolean)
+    public static boolean z3Installed() {
+        return SolverTypes.getSolverTypes().stream()
+                .filter(it -> it.getClass().equals(SolverTypeImplementation.class)
+                        && it.getName().equals("Z3"))
+                .findFirst().map(x -> x.isInstalled(true)).orElse(false);
+    }
+
+    /// Assumes or assert that z3 is installed depending on [#failIfSmtSolverIsUnavailable]
+    public static void assumeZ3Installed() {
+        var isInstalled = z3Installed();
+        assumeSmtIsInstalled(isInstalled);
+    }
+
+    /// Assumes or assert that the SMT is not installed depending on [#failIfSmtSolverIsUnavailable]
+    public static void assumeSmtIsInstalled(boolean isInstalled) {
+        if (!isInstalled && !failIfSmtSolverIsUnavailable) {
+            Assumptions.abort(REQUIRED_SMT_SOLVER_NOT_INSTALLED);
+        }
+
+        if (!isInstalled && failIfSmtSolverIsUnavailable) {
+            Assertions.fail(REQUIRED_SMT_SOLVER_NOT_INSTALLED);
+        }
+    }
+}

key.core/src/test/java/de/uka/ilkd/key/smt/TestUnsatCore.java

@@ -12,8 +12,6 @@
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
-import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation;
-import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.helper.FindResources;
@@ -29,9 +27,7 @@ class TestUnsatCore {
 
     @Test
     void testUnsatCore() throws ProblemLoaderException {
-        if (!z3Installed()) {
-            return;
-        }
+        SmtTestUtils.assumeZ3Installed();
 
         KeYEnvironment<DefaultUserInterfaceControl> env =
             KeYEnvironment.load(new File(testCaseDirectory, "smt/unsatCore.proof"));
@@ -54,10 +50,4 @@ void testUnsatCore() throws ProblemLoaderException {
         Assertions.assertEquals(4, ifs.size());
     }
 
-    private static boolean z3Installed() {
-        return SolverTypes.getSolverTypes().stream()
-                .filter(it -> it.getClass().equals(SolverTypeImplementation.class)
-                        && it.getName().equals("Z3"))
-                .findFirst().map(x -> x.isInstalled(true)).orElse(false);
-    }
 }

key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java

@@ -3,11 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.smt.newsmt2;
 
-import java.io.BufferedReader;
-import java.io.FileNotFoundException;
-import java.io.IOException;
-import java.io.OutputStream;
-import java.io.StringReader;
+import java.io.*;
 import java.net.URISyntaxException;
 import java.net.URL;
 import java.nio.charset.StandardCharsets;
@@ -17,7 +13,6 @@
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Properties;
-import java.util.stream.Collectors;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.control.KeYEnvironment;
@@ -27,13 +22,15 @@
 import de.uka.ilkd.key.settings.DefaultSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.smt.SMTSettings;
+import de.uka.ilkd.key.smt.SmtTestUtils;
 import de.uka.ilkd.key.smt.solvertypes.SolverType;
 import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation;
 import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
 import de.uka.ilkd.key.util.LineProperties;
 
 import org.key_project.util.Streams;
 
+import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.api.Assumptions;
@@ -89,7 +86,7 @@ public static List<Arguments> data()
 
         List<Path> files;
         try (var s = Files.list(directory)) {
-            files = s.collect(Collectors.toList());
+            files = s.toList();
         }
         List<Arguments> result = new ArrayList<>(files.size());
         for (Path file : files) {
@@ -129,7 +126,7 @@ public record TestData(String name, Path path, LineProperties props, String tran
                 Path srcDir = Files.createTempDirectory("SMT_key_" + name);
                 Path tmpSrc = srcDir.resolve("src.java");
                 Files.write(tmpSrc, sources);
-                lines.add(0, "\\javaSource \"" + srcDir + "\";\n");
+                lines.addFirst("\\javaSource \"" + srcDir + "\";\n");
             }
 
             Path tmpKey = Files.createTempFile("SMT_key_" + name, ".key");
@@ -158,7 +155,7 @@ public record TestData(String name, Path path, LineProperties props, String tran
         }
 
         @Override
-        public String toString() {
+        public @NonNull String toString() {
             return name;
         }
     }
@@ -194,9 +191,9 @@ public static boolean containsModuloSpaces(String haystack, String needle) {
     @ParameterizedTest
     @MethodSource("data")
     public void testZ3(TestData data) throws Exception {
+        SmtTestUtils.assumeZ3Installed();
+
         Assumptions.assumeTrue(Z3_SOLVER != null);
-        Assumptions.assumeTrue(Z3_SOLVER.isInstalled(false),
-            "Z3 is not installed, this testcase is ignored.");
 
         String expectation = data.props.get("expected");
         Assumptions.assumeTrue(expectation != null, "No Z3 expectation.");

key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java

@@ -10,16 +10,14 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
-import de.uka.ilkd.key.smt.SMTProblem;
-import de.uka.ilkd.key.smt.SMTSolverResult;
-import de.uka.ilkd.key.smt.SMTTestSettings;
-import de.uka.ilkd.key.smt.SolverLauncher;
+import de.uka.ilkd.key.smt.*;
 import de.uka.ilkd.key.smt.solvertypes.SolverType;
 import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation;
 import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
 
 import org.key_project.util.helper.FindResources;
 
+import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.api.Test;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -68,13 +66,21 @@ public void testModSpec() throws ProblemLoaderException {
                 result = checkGoal(g, Z3_SOLVER);
                 assertSame(SMTSolverResult.ThreeValuedTruth.VALID, result.isValid());
             } else {
-                LOGGER.warn("Warning:Z3 solver not installed, tests skipped.");
+                if (SmtTestUtils.failIfSmtSolverIsUnavailable) {
+                    Assertions.fail("z3 solver not installed");
+                } else {
+                    LOGGER.warn("Warning:Z3 solver not installed, tests skipped.");
+                }
             }
             if (CVC5_SOLVER.isInstalled(true)) {
                 result = checkGoal(g, CVC5_SOLVER);
                 assertSame(SMTSolverResult.ThreeValuedTruth.VALID, result.isValid());
             } else {
-                LOGGER.warn("Warning:cvc5 solver not installed, tests skipped.");
+                if (SmtTestUtils.failIfSmtSolverIsUnavailable) {
+                    Assertions.fail("cvc4 solver not installed");
+                } else {
+                    LOGGER.warn("Warning:cvc5 solver not installed, tests skipped.");
+                }
             }
         } finally {
             env.dispose();

key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java

@@ -0,0 +1,98 @@
+/* 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.smt.test;
+
+import java.util.stream.Stream;
+
+import de.uka.ilkd.key.smt.solvertypes.SolverType;
+import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation;
+import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
+
+import org.junit.jupiter.params.provider.Arguments;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.UNKNOWN;
+import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID;
+
+/**
+ * Tests that some simple .key files are translated to SMT-LIB correctly and cvc5 has a specified
+ * behavior on them (returns unsat, sat, or unknown/timeout). The test uses the new modular SMT
+ * translation!
+ * <p>
+ * Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}!
+ */
+public class Cvc5Test extends SMTSolverTest {
+
+
+    public static final String SYSTEM_PROPERTY_SOLVER_PATH = "cvc5SolverPath";
+    private static final Logger LOGGER = LoggerFactory.getLogger(Cvc5Test.class);
+    private static final String SOLVER_NAME = "cvc5";
+
+    private static final SolverType CVC5_SOLVER = SolverTypes.getSolverTypes().stream()
+            .filter(it -> it.getClass().equals(SolverTypeImplementation.class)
+                    && it.getName().equals(SOLVER_NAME))
+            .findFirst().orElse(null);
+
+    @Override
+    protected Logger getLogger() {
+        return LOGGER;
+    }
+
+    @Override
+    protected String getSystemPropertySolverPath() {
+        return SYSTEM_PROPERTY_SOLVER_PATH;
+    }
+
+    @Override
+    protected String getSolverName() {
+        return SOLVER_NAME;
+    }
+
+    @Override
+    public SolverType getSolverType() {
+        SolverType type = CVC5_SOLVER;
+        String solverPathProperty = System.getProperty(SYSTEM_PROPERTY_SOLVER_PATH);
+        if (solverPathProperty != null && !solverPathProperty.isEmpty()) {
+            type.setSolverCommand(solverPathProperty);
+        }
+        return type;
+    }
+
+    @Override
+    protected final Stream<Arguments> provideTestData() {
+        return Stream.of(
+            Arguments.of(UNKNOWN, "andnot.key"), // timeout expected
+            Arguments.of(VALID, "ornot.key"),
+            Arguments.of(UNKNOWN, "andornot.key"), // timeout expected
+            Arguments.of(VALID, "andornot2.key"),
+            Arguments.of(VALID, "imply.key"),
+            Arguments.of(VALID, "imply2.key"),
+            Arguments.of(UNKNOWN, "imply3.key"), // timeout expected
+            Arguments.of(VALID, "equi1.key"),
+            Arguments.of(UNKNOWN, "equi2.key"), // timeout expected
+            Arguments.of(VALID, "allex1.key"),
+            Arguments.of(UNKNOWN, "allex2.key"), // timeout expected
+            Arguments.of(UNKNOWN, "allex3.key"),
+            Arguments.of(VALID, "logicalite1.key"),
+            Arguments.of(UNKNOWN, "logicalite2.key"), // timeout expected
+            Arguments.of(VALID, "equal1.key"),
+            Arguments.of(UNKNOWN, "equal2.key"), // timeout expected
+            Arguments.of(VALID, "subsort1.key"),
+            Arguments.of(UNKNOWN, "subsort2.key"), // timeout expected
+            Arguments.of(VALID, "add1.key"),
+            Arguments.of(VALID, "bsum1.key"),
+            Arguments.of(VALID, "bsum2.key"),
+            Arguments.of(UNKNOWN, "bsum3.key"), // timeout expected
+            Arguments.of(VALID, "bprod1.key"),
+            Arguments.of(VALID, "bprod2.key"),
+            Arguments.of(UNKNOWN, "bprod3.key"), // timeout expected
+            Arguments.of(UNKNOWN, "binder4.key"), // timeout expected
+            Arguments.of(UNKNOWN, "binder5.key"), // timeout expected
+            Arguments.of(VALID, "div1.key"),
+            Arguments.of(VALID, "div3.key"),
+            Arguments.of(UNKNOWN, "div5.key"),
+            Arguments.of(UNKNOWN, "div6.key"));
+    }
+}

key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java

@@ -17,7 +17,6 @@
 import de.uka.ilkd.key.util.HelperClassForTests;
 
 import org.jspecify.annotations.NonNull;
-import org.junit.jupiter.api.Assumptions;
 import org.junit.jupiter.api.Tag;
 
 import static org.junit.jupiter.api.Assertions.*;
@@ -52,7 +51,7 @@ protected TermServices getServices() {
     protected SMTSolverResult.ThreeValuedTruth getResult(SMTSolverResult.ThreeValuedTruth expected,
             String filepath)
             throws ProblemLoaderException {
-        Assumptions.assumeTrue(toolInstalled());
+        SmtTestUtils.assumeSmtIsInstalled(toolInstalled());
         return checkFile(expected, filepath).isValid();
     }
 

key.core/src/test/java/de/uka/ilkd/key/util/LineProperties.java

@@ -17,6 +17,8 @@
 import java.util.Map.Entry;
 import java.util.Set;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * An infrastructure to read string to string maps from files.
  *
@@ -70,7 +72,7 @@ public void read(Reader reader) throws IOException {
 
     }
 
-    public String get(String key) {
+    public @Nullable String get(String key) {
         return map.get(key);
     }