From 8e8737ddef4f90ea863f87dcc8ea15b30ab380ed Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 11 Apr 2025 12:50:44 +0200 Subject: [PATCH 1/9] changed expected results to ThreeValuedTruth, separate tests for legacy and new modular translation --- .../de/uka/ilkd/key/smt/SMTSolverResult.java | 40 +++-- .../key/smt/communication/CVC4Socket.java | 2 +- .../key/smt/communication/CVC5Socket.java | 2 +- .../key/smt/communication/Z3CESocket.java | 2 +- .../ilkd/key/smt/communication/Z3Socket.java | 2 +- .../de/uka/ilkd/key/smt/SMTTestSettings.java | 16 +- .../uka/ilkd/key/smt/test/Cvc4LegacyTest.java | 100 +++++++++++ .../uka/ilkd/key/smt/test/SMTSolverTest.java | 81 +++++++++ .../{TestCommons.java => SMTTestCommons.java} | 67 ++------ .../de/uka/ilkd/key/smt/test/TestCvc4.java | 60 ------- .../uka/ilkd/key/smt/test/TestSMTSolver.java | 162 ------------------ .../java/de/uka/ilkd/key/smt/test/TestZ3.java | 91 ---------- .../uka/ilkd/key/smt/test/Z3LegacyTest.java | 97 +++++++++++ .../java/de/uka/ilkd/key/smt/test/Z3Test.java | 112 ++++++++++++ 14 files changed, 443 insertions(+), 391 deletions(-) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java create mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java rename key.core/src/test/java/de/uka/ilkd/key/smt/test/{TestCommons.java => SMTTestCommons.java} (69%) delete mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCvc4.java delete mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/test/TestSMTSolver.java delete mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/test/TestZ3.java create mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java create mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverResult.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverResult.java index cca321c766c..ee9ce11bdc8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverResult.java +++ b/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; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC4Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC4Socket.java index a459b33378e..69aa3c5868d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC4Socket.java +++ b/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(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java index 6d7c47cf2d3..d4957b9270c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java @@ -56,7 +56,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(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java index 648c4968109..9572396ff31 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3CESocket.java +++ b/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)"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java index 1ff6deac753..1ccbbf2c214 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Z3Socket.java +++ b/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); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java index a6cbba2a302..b1aa88fe02c 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java @@ -12,13 +12,11 @@ import de.uka.ilkd.key.settings.ProofDependentSMTSettings; import de.uka.ilkd.key.smt.solvertypes.SolverType; +/** + * Special settings for the SMT solvers tests. + */ public class SMTTestSettings implements de.uka.ilkd.key.smt.SMTSettings { - - public long getGlobalBound() { - return 0; - } - @Override public int getMaxConcurrentProcesses() { return 1; @@ -41,7 +39,11 @@ public Collection getTaclets() { @Override public long getTimeout() { - return 300000; + /* 20s should be sufficient, and since we have a few examples that are expected to run into + * a timeout (because the file is intentionally not provable), we want to have it as low as + * possible. + */ + return 20000; } @Override @@ -136,6 +138,4 @@ public boolean invarianForall() { public NewSMTTranslationSettings getNewSettings() { return new NewSMTTranslationSettings(); } - - } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java new file mode 100644 index 00000000000..9893382f1b5 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java @@ -0,0 +1,100 @@ +/* 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 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 java.util.stream.Stream; + +import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.*; +import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID; + +/** + * Tests that some simple .key files are translated to SMT-LIB correctly and CVC4 has a specified + * behavior on them (returns unsat, or sat/unknown). The test uses the old and non-modular SMT + * translation! + *

+ * Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! + */ +public class Cvc4LegacyTest extends SMTSolverTest { + private static final String SYSTEM_PROPERTY_SOLVER_PATH = "cvc4SolverPath"; + private static final Logger LOGGER = LoggerFactory.getLogger(Cvc4LegacyTest.class); + private static final String SOLVER_NAME = "CVC4 (Legacy Translation)"; + + public static final SolverType CVC4_LEGACY_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 = CVC4_LEGACY_SOLVER; + String solverPathProperty = System.getProperty(SYSTEM_PROPERTY_SOLVER_PATH); + if (solverPathProperty != null && !solverPathProperty.isEmpty()) { + type.setSolverCommand(solverPathProperty); + } + return type; + } + + @Override + protected final Stream provideTestData() { + return Stream.of( + Arguments.of(FALSIFIABLE, "andnot.key"), + Arguments.of(VALID, "ornot.key"), + Arguments.of(FALSIFIABLE, "andornot.key"), + Arguments.of(VALID, "andornot2.key"), + Arguments.of(VALID, "imply.key"), + Arguments.of(VALID, "imply2.key"), + Arguments.of(FALSIFIABLE, "imply3.key"), + Arguments.of(VALID, "equi1.key"), + Arguments.of(FALSIFIABLE, "equi2.key"), + Arguments.of(VALID, "allex1.key"), + Arguments.of(FALSIFIABLE, "allex2.key"), + Arguments.of(VALID, "allex3.key"), + Arguments.of(VALID, "logicalite1.key"), + Arguments.of(FALSIFIABLE, "logicalite2.key"), + Arguments.of(VALID, "equal1.key"), + Arguments.of(UNKNOWN, "equal2.key"), + Arguments.of(VALID, "subsort1.key"), + Arguments.of(UNKNOWN, "subsort2.key"), + Arguments.of(VALID, "add1.key"), + Arguments.of(VALID, "bsum1.key"), + Arguments.of(VALID, "bsum2.key"), + Arguments.of(UNKNOWN, "bsum3.key"), + Arguments.of(VALID, "bprod1.key"), + Arguments.of(VALID, "bprod2.key"), + Arguments.of(UNKNOWN, "bprod3.key"), + Arguments.of(VALID, "binder4.key"), + Arguments.of(VALID, "binder5.key"), + // These testcases are z3 specific, because other solvers don't support integer division + Arguments.of(VALID, "div1.key"), + Arguments.of(VALID, "div3.key"), + Arguments.of(UNKNOWN, "div5.key"), + Arguments.of(UNKNOWN, "div6.key") + ); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java new file mode 100644 index 00000000000..be7d1ca5955 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java @@ -0,0 +1,81 @@ +/* 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.io.File; +import java.util.stream.Stream; + +import de.uka.ilkd.key.proof.io.ProblemLoaderException; +import de.uka.ilkd.key.smt.SMTSolverResult; +import de.uka.ilkd.key.smt.solvertypes.SolverType; +import de.uka.ilkd.key.util.HelperClassForTests; + +import org.junit.jupiter.api.*; +import org.junit.jupiter.api.condition.DisabledIf; +import org.junit.jupiter.api.condition.EnabledIf; +import org.junit.jupiter.api.extension.ConditionEvaluationResult; +import org.junit.jupiter.api.extension.ExecutionCondition; +import org.junit.jupiter.api.extension.ExtensionContext; +import org.junit.jupiter.params.ParameterizedTest; +import org.junit.jupiter.params.provider.Arguments; +import org.junit.jupiter.params.provider.MethodSource; +import org.slf4j.Logger; + +/** + * Concrete instance of this class test that some .key files are translated to SMT-LIB correctly and + * the SMT solver has a specified behavior on them (returns unsat, or sat/unknown). + *

+ * Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! + */ +@TestInstance(TestInstance.Lifecycle.PER_CLASS) +public abstract class SMTSolverTest extends SMTTestCommons { + public static final String TEST_DIR = + HelperClassForTests.TESTCASE_DIRECTORY + File.separator + "smt" + File.separator; + + protected boolean isInstalled = false; + protected boolean installChecked = false; + + protected abstract Logger getLogger(); + + protected abstract String getSystemPropertySolverPath(); + + protected abstract String getSolverName(); + + @Override + public boolean toolInstalled() { + if (!installChecked) { + SolverType solverType = getSolverType(); + isInstalled = solverType != null && solverType.isInstalled(true); + installChecked = true; + if (!isInstalled) { + getLogger().warn("Warning: {} is not installed, tests skipped.", + getSolverName()); + getLogger().warn( + "Maybe use JVM system property \"{}\" to define the path to the CVC4 command.", + getSystemPropertySolverPath()); + } else if (!solverType.supportHasBeenChecked()) { + if (!solverType.checkForSupport()) { + getLogger().warn("Warning: The version of the solver {}" + + " used for the following tests may not be supported.", + getSolverName()); + } + } + } + return isInstalled; + } + + /** + * Provides arguments for the parameterized test + * {@link #test(SMTSolverResult.ThreeValuedTruth, String)}. + * @return the stream of arguments + */ + protected abstract Stream provideTestData(); + + @MethodSource("provideTestData") + @ParameterizedTest(name = "test {1}") + public void test(SMTSolverResult.ThreeValuedTruth expected, String filename) + throws ProblemLoaderException { + Assertions.assertSame(expected, getResult(TEST_DIR + filename)); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCommons.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java similarity index 69% rename from key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCommons.java rename to key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java index da1a0422122..8931e99ccd4 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCommons.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java @@ -5,7 +5,6 @@ import java.io.File; import java.util.Collection; -import java.util.HashSet; import java.util.LinkedList; import de.uka.ilkd.key.control.KeYEnvironment; @@ -23,6 +22,7 @@ import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.util.HelperClassForTests; +import org.jspecify.annotations.NonNull; import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.api.Tag; @@ -33,14 +33,10 @@ * this class directly but derive subclasses to implement tests. */ @Tag("slow") -public abstract class TestCommons { - protected static final String folder = +public abstract class SMTTestCommons { + protected static final String FOLDER = HelperClassForTests.TESTCASE_DIRECTORY + File.separator + "smt" + File.separator + "tacletTranslation" + File.separator; - /** - * The set of taclets - */ - private final Collection taclets = new LinkedList<>(); InitConfig initConfig = null; static protected ProblemInitializer initializer = null; static protected final Profile profile = init(); @@ -62,26 +58,24 @@ protected TermServices getServices() { */ public abstract SolverType getSolverType(); - public abstract boolean toolNotInstalled(); + public abstract boolean toolInstalled(); - protected boolean correctResult(String filepath, boolean isValid) + protected boolean correctResult(String filepath, SMTSolverResult.ThreeValuedTruth expected) throws ProblemLoaderException { - Assumptions.assumeFalse(toolNotInstalled()); + Assumptions.assumeTrue(toolInstalled()); SMTSolverResult result = checkFile(filepath); - // unknown is always allowed. But wrong answers are not allowed - return correctResult(isValid, result); + return correctResult(expected, result); } - protected boolean correctResult(Goal g, boolean isValid) { - return correctResult(isValid, checkGoal(g)); + protected SMTSolverResult.ThreeValuedTruth getResult(String filepath) + throws ProblemLoaderException { + Assumptions.assumeTrue(toolInstalled()); + return checkFile(filepath).isValid(); } - private boolean correctResult(boolean isValid, SMTSolverResult result) { - if (isValid && result != null) { - return result.isValid() != SMTSolverResult.ThreeValuedTruth.FALSIFIABLE; - } else { - return result.isValid() != SMTSolverResult.ThreeValuedTruth.VALID; - } + private boolean correctResult(SMTSolverResult.ThreeValuedTruth expected, + @NonNull SMTSolverResult result) { + return result.isValid() == expected; } /** @@ -104,7 +98,7 @@ protected SMTSolverResult checkFile(String filepath) throws ProblemLoaderExcepti } } - private SMTSolverResult checkGoal(Goal g) { + private @NonNull SMTSolverResult checkGoal(Goal g) { SolverLauncher launcher = new SolverLauncher(new SMTTestSettings()); SMTProblem problem = new SMTProblem(g); launcher.launch(problem, g.proof().getServices(), getSolverType()); @@ -116,42 +110,15 @@ protected KeYEnvironment loadProof(String filepath) throws ProblemLoaderExcep return KeYEnvironment.load(new File(filepath), null, null, null); } - /** - * Returns a set of taclets that can be used for tests. REMARK: First you have to call - * parse to instantiate the set of taclets. - * - * @return set of taclets. - */ - protected Collection getTaclets() { - if (taclets.isEmpty()) { - if (initConfig == null) { - parse(); - } - for (Taclet t : initConfig.getTaclets()) { - taclets.add(t); - } - } - return taclets; - } - - protected HashSet getTacletNames() { - Collection set = getTaclets(); - HashSet names = new HashSet<>(); - for (Taclet taclet : set) { - names.add(taclet.name().toString()); - } - return names; - } - /** * Use this method if you only need taclets for testing. */ protected ProofAggregate parse() { - return parse(new File(folder + "dummyFile.key")); + return parse(new File(FOLDER + "dummyFile.key")); } /** - * Calls parse(File file, Profile profile) with the standard profile for testing. + * Calls parse(File file, Profile profile) with the standard profile for testing. */ protected ProofAggregate parse(File file) { return parse(file, profile); diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCvc4.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCvc4.java deleted file mode 100644 index 572ce23bf97..00000000000 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCvc4.java +++ /dev/null @@ -1,60 +0,0 @@ -/* 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 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.slf4j.Logger; -import org.slf4j.LoggerFactory; - -public class TestCvc4 extends TestSMTSolver { - private static final String SYSTEM_PROPERTY_SOLVER_PATH = "cvc4SolverPath"; - private static final Logger LOGGER = LoggerFactory.getLogger(TestCvc4.class); - - private static boolean isInstalled = false; - private static boolean installChecked = false; - - public static final SolverType CVC4_SOLVER = - SolverTypes.getSolverTypes().stream() - .filter(it -> it.getClass().equals(SolverTypeImplementation.class) - && it.getName().equals("CVC4 (Legacy Translation)")) - .findFirst().orElse(null); - - @Override - public boolean toolNotInstalled() { - if (!installChecked) { - isInstalled = getSolverType().isInstalled(true); - installChecked = true; - if (!isInstalled) { - LOGGER.warn("Warning: {} is not installed, tests skipped.", - getSolverType().getName()); - LOGGER.warn( - "Maybe use JVM system property \"{}\" to define the path to the CVC4 command.", - SYSTEM_PROPERTY_SOLVER_PATH); - } - if (isInstalled && !getSolverType().supportHasBeenChecked()) { - if (!getSolverType().checkForSupport()) { - LOGGER.warn( - "Warning: The version of the solver {}" - + " used for the following tests may not be supported.", - getSolverType().getName()); - } - } - } - return !isInstalled; - } - - @Override - public SolverType getSolverType() { - SolverType type = CVC4_SOLVER; - String solverPathProperty = System.getProperty(SYSTEM_PROPERTY_SOLVER_PATH); - if (solverPathProperty != null && !solverPathProperty.isEmpty()) { - type.setSolverCommand(solverPathProperty); - } - return type; - } -} diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestSMTSolver.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestSMTSolver.java deleted file mode 100644 index 3b6aecf0f7b..00000000000 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestSMTSolver.java +++ /dev/null @@ -1,162 +0,0 @@ -/* 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.io.File; - -import de.uka.ilkd.key.util.HelperClassForTests; - -import org.junit.jupiter.api.AfterEach; -import org.junit.jupiter.api.Assertions; -import org.junit.jupiter.api.BeforeEach; -import org.junit.jupiter.api.Test; - -public abstract class TestSMTSolver extends TestCommons { - public static final String testFile = - HelperClassForTests.TESTCASE_DIRECTORY + File.separator + "smt" + File.separator; - - @BeforeEach - public void setUp() { - } - - @AfterEach - public void tearDown() throws Exception { - } - - @Test - public void testAndnot() throws Exception { - Assertions.assertTrue(correctResult(testFile + "andnot.key", false)); - } - - @Test - public void testOrnot() throws Exception { - Assertions.assertTrue(correctResult(testFile + "ornot.key", true)); - } - - @Test - public void testAndornot() throws Exception { - Assertions.assertTrue(correctResult(testFile + "andornot.key", false)); - } - - @Test - public void testAndornot2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "andornot2.key", true)); - } - - @Test - public void testImply() throws Exception { - Assertions.assertTrue(correctResult(testFile + "imply.key", true)); - } - - @Test - public void testImply2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "imply2.key", true)); - } - - @Test - public void testImply3() throws Exception { - Assertions.assertTrue(correctResult(testFile + "imply3.key", false)); - } - - @Test - public void testEqui1() throws Exception { - Assertions.assertTrue(correctResult(testFile + "equi1.key", true)); - } - - @Test - public void testEqui2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "equi2.key", false)); - } - - @Test - public void testAllex1() throws Exception { - Assertions.assertTrue(correctResult(testFile + "allex1.key", true)); - } - - // LONG runtime with CVC3 (~300s) - @Test - public void testAllex2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "allex2.key", false)); - } - - @Test - public void testAllex3() throws Exception { - Assertions.assertTrue(correctResult(testFile + "allex3.key", true)); - } - - @Test - public void testLogicalIte1() throws Exception { - Assertions.assertTrue(correctResult(testFile + "logicalite1.key", true)); - } - - @Test - public void testLogicalIte2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "logicalite2.key", false)); - } - - @Test - public void testEqual1() throws Exception { - Assertions.assertTrue(correctResult(testFile + "equal1.key", true)); - } - - @Test - public void testEqual2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "equal2.key", false)); - } - - @Test - public void testSubsort1() throws Exception { - Assertions.assertTrue(correctResult(testFile + "subsort1.key", true)); - } - - @Test - public void testSubsort2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "subsort2.key", false)); - } - - @Test - public void testAdd1() throws Exception { - Assertions.assertTrue(correctResult(testFile + "add1.key", true)); - } - - @Test - public void testBSum1() throws Exception { - Assertions.assertTrue(correctResult(testFile + "bsum1.key", true)); - } - - @Test - public void testBSum2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "bsum2.key", true)); - } - - @Test - public void testBSum3() throws Exception { - Assertions.assertTrue(correctResult(testFile + "bsum3.key", false)); - } - - @Test - public void testBProd1() throws Exception { - Assertions.assertTrue(correctResult(testFile + "bprod1.key", true)); - } - - @Test - public void testBProd2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "bprod2.key", true)); - } - - @Test - public void testBProd3() throws Exception { - Assertions.assertTrue(correctResult(testFile + "bprod3.key", false)); - } - - @Test - public void testBinderPred2() throws Exception { - Assertions.assertTrue(correctResult(testFile + "binder4.key", true)); - } - - @Test - public void testBinderPred3() throws Exception { - Assertions.assertTrue(correctResult(testFile + "binder5.key", true)); - } -} diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestZ3.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestZ3.java deleted file mode 100644 index 972bfdde083..00000000000 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestZ3.java +++ /dev/null @@ -1,91 +0,0 @@ -/* 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 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.api.Disabled; -import org.junit.jupiter.api.Test; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import static org.junit.jupiter.api.Assertions.assertTrue; - - -public class TestZ3 extends TestSMTSolver { - - - public static final String SYSTEM_PROPERTY_SOLVER_PATH = "z3SolverPath"; - private static final Logger LOGGER = LoggerFactory.getLogger(TestZ3.class); - - private static boolean isInstalled = false; - private static boolean installChecked = false; - - private static final SolverType Z3_SOLVER = SolverTypes.getSolverTypes().stream() - .filter(it -> it.getClass().equals(SolverTypeImplementation.class) - && it.getName().equals("Z3 (Legacy Translation)")) - .findFirst().orElse(null); - - @Override - public boolean toolNotInstalled() { - if (!installChecked) { - isInstalled = getSolverType().isInstalled(true); - installChecked = true; - if (!isInstalled) { - LOGGER.warn("Warning: {} is not installed, tests skipped.", - getSolverType().getName()); - LOGGER.warn( - "Maybe use JVM system property \"{}\" to define the path to the Z3 command.", - SYSTEM_PROPERTY_SOLVER_PATH); - } - - if (isInstalled && !getSolverType().supportHasBeenChecked()) { - if (!getSolverType().checkForSupport()) { - LOGGER.warn("Warning: " + "The version of the solver {} used for the " - + "following tests may not be supported.", getSolverType().getName()); - } - } - } - - - - return !isInstalled; - } - - @Override - public SolverType getSolverType() { - SolverType type = Z3_SOLVER; - String solverPathProperty = System.getProperty(SYSTEM_PROPERTY_SOLVER_PATH); - if (solverPathProperty != null && !solverPathProperty.isEmpty()) { - type.setSolverCommand(solverPathProperty); - } - return type; - } - - // These testcases are z3 specific, because other solvers don't support integer division. - @Test - public void testDiv1() throws Exception { - assertTrue(correctResult(testFile + "div1.key", true)); - } - - @Test - public void testDiv3() throws Exception { - assertTrue(correctResult(testFile + "div3.key", true)); - } - - @Test - @Disabled("weigl: due to performance issues") - public void testDiv5() throws Exception { - assertTrue(correctResult(testFile + "div5.key", false)); - } - - @Test - @Disabled("weigl: due to performance issues") - public void testDiv6() throws Exception { - assertTrue(correctResult(testFile + "div6.key", false)); - } - -} diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java new file mode 100644 index 00000000000..ba1bbead92a --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java @@ -0,0 +1,97 @@ +/* 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 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 java.util.stream.Stream; + +import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.*; +import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID; + +/** + * Tests that some simple .key files are translated to SMT-LIB correctly and Z3 has a specified + * behavior on them (returns unsat, or sat/unknown). The test uses the old and non-modular SMT + * translation! + *

+ * Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! + */ +public class Z3LegacyTest extends SMTSolverTest { + private static final String SYSTEM_PROPERTY_SOLVER_PATH = "z3SolverPath"; + private static final Logger LOGGER = LoggerFactory.getLogger(Z3LegacyTest.class); + private static final String SOLVER_NAME = "Z3 (Legacy Translation)"; + private static final SolverType Z3_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 = Z3_SOLVER; + String solverPathProperty = System.getProperty(SYSTEM_PROPERTY_SOLVER_PATH); + if (solverPathProperty != null && !solverPathProperty.isEmpty()) { + type.setSolverCommand(solverPathProperty); + } + return type; + } + + @Override + protected Stream provideTestData() { + return Stream.of( + Arguments.of(FALSIFIABLE, "andnot.key"), + Arguments.of(VALID, "ornot.key"), + Arguments.of(FALSIFIABLE, "andornot.key"), + Arguments.of(VALID, "andornot2.key"), + Arguments.of(VALID, "imply.key"), + Arguments.of(VALID, "imply2.key"), + Arguments.of(FALSIFIABLE, "imply3.key"), + Arguments.of(VALID, "equi1.key"), + Arguments.of(FALSIFIABLE, "equi2.key"), + Arguments.of(VALID, "allex1.key"), + Arguments.of(FALSIFIABLE, "allex2.key"), + Arguments.of(VALID, "allex3.key"), + Arguments.of(VALID, "logicalite1.key"), + Arguments.of(FALSIFIABLE, "logicalite2.key"), + Arguments.of(VALID, "equal1.key"), + Arguments.of(FALSIFIABLE, "equal2.key"), + Arguments.of(VALID, "subsort1.key"), + Arguments.of(FALSIFIABLE, "subsort2.key"), + 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(VALID, "binder4.key"), + Arguments.of(VALID, "binder5.key"), + // These testcases are z3 specific, because other solvers don't support integer division + Arguments.of(VALID, "div1.key"), + Arguments.of(VALID, "div3.key"), + Arguments.of(UNKNOWN, "div5.key"), // timeout expected + Arguments.of(UNKNOWN, "div6.key") // timeout expected + ); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java new file mode 100644 index 00000000000..9b3fa8c806b --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java @@ -0,0 +1,112 @@ +/* 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 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 java.util.stream.Stream; + +import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.*; +import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID; + +/** + * Tests that some simple .key files are translated to SMT-LIB correctly and Z3 has a specified + * behavior on them (returns unsat, or sat/unknown). The test uses the new modular SMT translation! + *

+ * Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! + */ +public class Z3Test extends SMTSolverTest { + + + public static final String SYSTEM_PROPERTY_SOLVER_PATH = "z3SolverPath"; + private static final Logger LOGGER = LoggerFactory.getLogger(Z3Test.class); + private static final String SOLVER_NAME = "Z3"; + + private static final SolverType Z3_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 = Z3_SOLVER; + String solverPathProperty = System.getProperty(SYSTEM_PROPERTY_SOLVER_PATH); + if (solverPathProperty != null && !solverPathProperty.isEmpty()) { + type.setSolverCommand(solverPathProperty); + } + return type; + } + + /* + @Test + @Disabled("weigl: due to performance issues") + public void testDiv5() throws Exception { + assertTrue(correctResult(TEST_DIR + "div5.key", ThreeValuedTruth.FALSIFIABLE)); + } + + @Test + @Disabled("weigl: due to performance issues") + public void testDiv6() throws Exception { + assertTrue(correctResult(TEST_DIR + "div6.key", ThreeValuedTruth.FALSIFIABLE)); + }*/ + + @Override + protected final Stream provideTestData() { + return Stream.of( + Arguments.of(UNKNOWN, "andnot.key"), + Arguments.of(VALID, "ornot.key"), + Arguments.of(UNKNOWN, "andornot.key"), + Arguments.of(VALID, "andornot2.key"), + Arguments.of(VALID, "imply.key"), + Arguments.of(VALID, "imply2.key"), + Arguments.of(UNKNOWN, "imply3.key"), + Arguments.of(VALID, "equi1.key"), + Arguments.of(UNKNOWN, "equi2.key"), + Arguments.of(VALID, "allex1.key"), + Arguments.of(UNKNOWN, "allex2.key"), + Arguments.of(UNKNOWN, "allex3.key"), + Arguments.of(VALID, "logicalite1.key"), + Arguments.of(UNKNOWN, "logicalite2.key"), + Arguments.of(VALID, "equal1.key"), + Arguments.of(UNKNOWN, "equal2.key"), + Arguments.of(VALID, "subsort1.key"), + Arguments.of(UNKNOWN, "subsort2.key"), + Arguments.of(VALID, "add1.key"), + Arguments.of(VALID, "bsum1.key"), + Arguments.of(VALID, "bsum2.key"), + Arguments.of(UNKNOWN, "bsum3.key"), + Arguments.of(VALID, "bprod1.key"), + Arguments.of(VALID, "bprod2.key"), + Arguments.of(UNKNOWN, "bprod3.key"), + Arguments.of(UNKNOWN, "binder4.key"), + Arguments.of(UNKNOWN, "binder5.key"), + // These testcases are z3 specific, because other solvers don't support integer division + Arguments.of(VALID, "div1.key"), + Arguments.of(VALID, "div3.key"), + Arguments.of(UNKNOWN, "div5.key"), + Arguments.of(UNKNOWN, "div6.key") + ); + } +} From 33d93c46f994504e3decbd8cf24ccf89774742dd Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 11 Apr 2025 13:52:51 +0200 Subject: [PATCH 2/9] minor comment changes --- .../test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java | 4 ++-- .../src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java | 2 +- .../src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java | 4 ++-- key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java | 3 ++- 4 files changed, 7 insertions(+), 6 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java index 9893382f1b5..fb4a874a1f0 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java @@ -19,8 +19,8 @@ /** * Tests that some simple .key files are translated to SMT-LIB correctly and CVC4 has a specified - * behavior on them (returns unsat, or sat/unknown). The test uses the old and non-modular SMT - * translation! + * behavior on them (returns unsat, sat, or unknown/timeout). The test uses the old and non-modular + * SMT translation! *

* Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! */ diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java index be7d1ca5955..43703aa8292 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java @@ -24,7 +24,7 @@ /** * Concrete instance of this class test that some .key files are translated to SMT-LIB correctly and - * the SMT solver has a specified behavior on them (returns unsat, or sat/unknown). + * the SMT solver has a specified behavior on them (returns unsat, sat, or unknown/timeout). *

* Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! */ diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java index ba1bbead92a..0fd8d7a52ea 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java @@ -18,8 +18,8 @@ /** * Tests that some simple .key files are translated to SMT-LIB correctly and Z3 has a specified - * behavior on them (returns unsat, or sat/unknown). The test uses the old and non-modular SMT - * translation! + * behavior on them (returns unsat, sat, or unknown/timeout). The test uses the old and non-modular + * SMT translation! *

* Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! */ diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java index 9b3fa8c806b..dad5062aee1 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java @@ -18,7 +18,8 @@ /** * Tests that some simple .key files are translated to SMT-LIB correctly and Z3 has a specified - * behavior on them (returns unsat, or sat/unknown). The test uses the new modular SMT translation! + * behavior on them (returns unsat, sat, or unknown/timeout). The test uses the new modular SMT + * translation! *

* Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! */ From 76d496ef4310e77cf77c20dfad8089663517147c Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 11 Apr 2025 13:56:03 +0200 Subject: [PATCH 3/9] spotless --- .../de/uka/ilkd/key/smt/SMTTestSettings.java | 3 +- .../uka/ilkd/key/smt/test/Cvc4LegacyTest.java | 7 ++-- .../uka/ilkd/key/smt/test/SMTSolverTest.java | 10 ++---- .../uka/ilkd/key/smt/test/SMTTestCommons.java | 5 +-- .../uka/ilkd/key/smt/test/Z3LegacyTest.java | 12 +++---- .../java/de/uka/ilkd/key/smt/test/Z3Test.java | 32 ++++++++++--------- 6 files changed, 32 insertions(+), 37 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java index b1aa88fe02c..08e76577290 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java @@ -39,7 +39,8 @@ public Collection getTaclets() { @Override public long getTimeout() { - /* 20s should be sufficient, and since we have a few examples that are expected to run into + /* + * 20s should be sufficient, and since we have a few examples that are expected to run into * a timeout (because the file is intentionally not provable), we want to have it as low as * possible. */ diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java index fb4a874a1f0..e0448b70f0e 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java @@ -4,6 +4,8 @@ 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; @@ -12,8 +14,6 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.stream.Stream; - import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.*; import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID; @@ -94,7 +94,6 @@ protected final Stream provideTestData() { Arguments.of(VALID, "div1.key"), Arguments.of(VALID, "div3.key"), Arguments.of(UNKNOWN, "div5.key"), - Arguments.of(UNKNOWN, "div6.key") - ); + Arguments.of(UNKNOWN, "div6.key")); } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java index 43703aa8292..8c2e83dbbee 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java @@ -12,11 +12,6 @@ import de.uka.ilkd.key.util.HelperClassForTests; import org.junit.jupiter.api.*; -import org.junit.jupiter.api.condition.DisabledIf; -import org.junit.jupiter.api.condition.EnabledIf; -import org.junit.jupiter.api.extension.ConditionEvaluationResult; -import org.junit.jupiter.api.extension.ExecutionCondition; -import org.junit.jupiter.api.extension.ExtensionContext; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.Arguments; import org.junit.jupiter.params.provider.MethodSource; @@ -57,7 +52,7 @@ public boolean toolInstalled() { } else if (!solverType.supportHasBeenChecked()) { if (!solverType.checkForSupport()) { getLogger().warn("Warning: The version of the solver {}" - + " used for the following tests may not be supported.", + + " used for the following tests may not be supported.", getSolverName()); } } @@ -68,6 +63,7 @@ public boolean toolInstalled() { /** * Provides arguments for the parameterized test * {@link #test(SMTSolverResult.ThreeValuedTruth, String)}. + * * @return the stream of arguments */ protected abstract Stream provideTestData(); @@ -75,7 +71,7 @@ public boolean toolInstalled() { @MethodSource("provideTestData") @ParameterizedTest(name = "test {1}") public void test(SMTSolverResult.ThreeValuedTruth expected, String filename) - throws ProblemLoaderException { + throws ProblemLoaderException { Assertions.assertSame(expected, getResult(TEST_DIR + filename)); } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java index 8931e99ccd4..2459b7ecebd 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java @@ -4,8 +4,6 @@ package de.uka.ilkd.key.smt.test; import java.io.File; -import java.util.Collection; -import java.util.LinkedList; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.logic.TermServices; @@ -14,7 +12,6 @@ import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.init.*; import de.uka.ilkd.key.proof.io.ProblemLoaderException; -import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.smt.SMTProblem; import de.uka.ilkd.key.smt.SMTSolverResult; import de.uka.ilkd.key.smt.SMTTestSettings; @@ -74,7 +71,7 @@ protected SMTSolverResult.ThreeValuedTruth getResult(String filepath) } private boolean correctResult(SMTSolverResult.ThreeValuedTruth expected, - @NonNull SMTSolverResult result) { + @NonNull SMTSolverResult result) { return result.isValid() == expected; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java index 0fd8d7a52ea..bf3d90a9cac 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java @@ -3,6 +3,8 @@ * 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; @@ -11,8 +13,6 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.stream.Stream; - import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.*; import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID; @@ -81,17 +81,17 @@ protected Stream provideTestData() { Arguments.of(VALID, "add1.key"), Arguments.of(VALID, "bsum1.key"), Arguments.of(VALID, "bsum2.key"), - Arguments.of(UNKNOWN, "bsum3.key"), // timeout expected + 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, "bprod3.key"), // timeout expected Arguments.of(VALID, "binder4.key"), Arguments.of(VALID, "binder5.key"), // These testcases are z3 specific, because other solvers don't support integer division Arguments.of(VALID, "div1.key"), Arguments.of(VALID, "div3.key"), - Arguments.of(UNKNOWN, "div5.key"), // timeout expected - Arguments.of(UNKNOWN, "div6.key") // timeout expected + Arguments.of(UNKNOWN, "div5.key"), // timeout expected + Arguments.of(UNKNOWN, "div6.key") // timeout expected ); } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java index dad5062aee1..3249f76f557 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java @@ -3,6 +3,8 @@ * 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; @@ -11,8 +13,6 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.stream.Stream; - import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.*; import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID; @@ -61,17 +61,20 @@ public SolverType getSolverType() { } /* - @Test - @Disabled("weigl: due to performance issues") - public void testDiv5() throws Exception { - assertTrue(correctResult(TEST_DIR + "div5.key", ThreeValuedTruth.FALSIFIABLE)); - } - - @Test - @Disabled("weigl: due to performance issues") - public void testDiv6() throws Exception { - assertTrue(correctResult(TEST_DIR + "div6.key", ThreeValuedTruth.FALSIFIABLE)); - }*/ + * @Test + * + * @Disabled("weigl: due to performance issues") + * public void testDiv5() throws Exception { + * assertTrue(correctResult(TEST_DIR + "div5.key", ThreeValuedTruth.FALSIFIABLE)); + * } + * + * @Test + * + * @Disabled("weigl: due to performance issues") + * public void testDiv6() throws Exception { + * assertTrue(correctResult(TEST_DIR + "div6.key", ThreeValuedTruth.FALSIFIABLE)); + * } + */ @Override protected final Stream provideTestData() { @@ -107,7 +110,6 @@ protected final Stream provideTestData() { Arguments.of(VALID, "div1.key"), Arguments.of(VALID, "div3.key"), Arguments.of(UNKNOWN, "div5.key"), - Arguments.of(UNKNOWN, "div6.key") - ); + Arguments.of(UNKNOWN, "div6.key")); } } From 20fee792641a8cebb813b80b2d2f85402248411a Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 11 Apr 2025 16:50:23 +0200 Subject: [PATCH 4/9] cleanup --- .../uka/ilkd/key/smt/test/Cvc4LegacyTest.java | 2 +- .../uka/ilkd/key/smt/test/SMTSolverTest.java | 4 +- .../uka/ilkd/key/smt/test/Z3LegacyTest.java | 1 - .../java/de/uka/ilkd/key/smt/test/Z3Test.java | 41 ++++++------------- 4 files changed, 15 insertions(+), 33 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java index e0448b70f0e..756cd8e17f7 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java @@ -62,6 +62,7 @@ public SolverType getSolverType() { @Override protected final Stream provideTestData() { + // no timeouts at all, either sat, unsat, or explicit unknown return Stream.of( Arguments.of(FALSIFIABLE, "andnot.key"), Arguments.of(VALID, "ornot.key"), @@ -90,7 +91,6 @@ protected final Stream provideTestData() { Arguments.of(UNKNOWN, "bprod3.key"), Arguments.of(VALID, "binder4.key"), Arguments.of(VALID, "binder5.key"), - // These testcases are z3 specific, because other solvers don't support integer division Arguments.of(VALID, "div1.key"), Arguments.of(VALID, "div3.key"), Arguments.of(UNKNOWN, "div5.key"), diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java index 8c2e83dbbee..76b0f34be69 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java @@ -18,8 +18,8 @@ import org.slf4j.Logger; /** - * Concrete instance of this class test that some .key files are translated to SMT-LIB correctly and - * the SMT solver has a specified behavior on them (returns unsat, sat, or unknown/timeout). + * Concrete instances of this class test that some .key files are translated to SMT-LIB correctly + * and the SMT solver has a specified behavior on them (returns unsat, sat, or unknown/timeout). *

* Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! */ diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java index bf3d90a9cac..c93a688be27 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java @@ -87,7 +87,6 @@ protected Stream provideTestData() { Arguments.of(UNKNOWN, "bprod3.key"), // timeout expected Arguments.of(VALID, "binder4.key"), Arguments.of(VALID, "binder5.key"), - // These testcases are z3 specific, because other solvers don't support integer division Arguments.of(VALID, "div1.key"), Arguments.of(VALID, "div3.key"), Arguments.of(UNKNOWN, "div5.key"), // timeout expected diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java index 3249f76f557..8e6da3e20c5 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.java @@ -60,53 +60,36 @@ public SolverType getSolverType() { return type; } - /* - * @Test - * - * @Disabled("weigl: due to performance issues") - * public void testDiv5() throws Exception { - * assertTrue(correctResult(TEST_DIR + "div5.key", ThreeValuedTruth.FALSIFIABLE)); - * } - * - * @Test - * - * @Disabled("weigl: due to performance issues") - * public void testDiv6() throws Exception { - * assertTrue(correctResult(TEST_DIR + "div6.key", ThreeValuedTruth.FALSIFIABLE)); - * } - */ - @Override protected final Stream provideTestData() { return Stream.of( - Arguments.of(UNKNOWN, "andnot.key"), + Arguments.of(UNKNOWN, "andnot.key"), // timeout expected Arguments.of(VALID, "ornot.key"), - Arguments.of(UNKNOWN, "andornot.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"), + Arguments.of(UNKNOWN, "imply3.key"), // timeout expected Arguments.of(VALID, "equi1.key"), - Arguments.of(UNKNOWN, "equi2.key"), + Arguments.of(UNKNOWN, "equi2.key"), // timeout expected Arguments.of(VALID, "allex1.key"), - Arguments.of(UNKNOWN, "allex2.key"), + Arguments.of(UNKNOWN, "allex2.key"), // timeout expected Arguments.of(UNKNOWN, "allex3.key"), Arguments.of(VALID, "logicalite1.key"), - Arguments.of(UNKNOWN, "logicalite2.key"), + Arguments.of(UNKNOWN, "logicalite2.key"), // timeout expected Arguments.of(VALID, "equal1.key"), - Arguments.of(UNKNOWN, "equal2.key"), + Arguments.of(UNKNOWN, "equal2.key"), // timeout expected Arguments.of(VALID, "subsort1.key"), - Arguments.of(UNKNOWN, "subsort2.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"), + Arguments.of(UNKNOWN, "bsum3.key"), // timeout expected Arguments.of(VALID, "bprod1.key"), Arguments.of(VALID, "bprod2.key"), - Arguments.of(UNKNOWN, "bprod3.key"), - Arguments.of(UNKNOWN, "binder4.key"), - Arguments.of(UNKNOWN, "binder5.key"), - // These testcases are z3 specific, because other solvers don't support integer division + 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"), From 9fd95048bf7f36fcf334e3bcfb214f7670c3a1c2 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 11 Apr 2025 17:21:18 +0200 Subject: [PATCH 5/9] 20sec timeout was not enough, increased to 30sec --- .../src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java index 08e76577290..1de96cc5776 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java @@ -40,11 +40,11 @@ public Collection getTaclets() { @Override public long getTimeout() { /* - * 20s should be sufficient, and since we have a few examples that are expected to run into + * 30s should be sufficient, and since we have a few examples that are expected to run into * a timeout (because the file is intentionally not provable), we want to have it as low as * possible. */ - return 20000; + return 30000; } @Override From 80bd8fd4793a21b2ed7e213b00e012be77597763 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 11 Apr 2025 17:56:22 +0200 Subject: [PATCH 6/9] removed all test cases for CVC4, make CVC4 experimental, minor refactoring --- .../settings/ProofIndependentSMTSettings.java | 2 +- .../de/uka/ilkd/key/smt/SMTFocusResults.java | 6 +- .../{CVC5Socket.java => Cvc5Socket.java} | 10 +- .../smt/newsmt2/ModularSMTLib2Translator.java | 2 +- .../solvertypes/SolverPropertiesLoader.java | 26 ++--- .../ilkd/key/smt/solvertypes/SolverTypes.java | 23 ++--- .../key/smt/solvertypes/AddingSMTSolvers.md | 4 +- .../uka/ilkd/key/smt/solvertypes/CVC4.props | 1 + .../key/smt/solvertypes/CVC4_legacy.props | 2 +- .../uka/ilkd/key/smt/solvertypes/CVC5.props | 6 +- .../ilkd/key/smt/solvertypes/Z3_legacy.props | 2 +- .../uka/ilkd/key/smt/newsmt2/TestSMTMod.java | 12 +-- .../uka/ilkd/key/smt/test/Cvc4LegacyTest.java | 99 ------------------- .../uka/ilkd/key/smt/test/SMTSolverTest.java | 2 +- .../uka/ilkd/key/smt/test/SMTTestCommons.java | 28 +----- .../gui/smt/settings/SMTSettingsProvider.java | 2 +- 16 files changed, 56 insertions(+), 171 deletions(-) rename key.core/src/main/java/de/uka/ilkd/key/smt/communication/{CVC5Socket.java => Cvc5Socket.java} (89%) delete mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java index 1e2c91fd504..306603355a5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java +++ b/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 legacyTypes = SolverTypes.getLegacySolvers(); + Collection legacyTypes = SolverTypes.getExperimentalSolvers(); Collection nonLegacyTypes = SolverTypes.getSolverTypes(); solverTypes.addAll(nonLegacyTypes); nonLegacyTypes.removeAll(legacyTypes); diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java index 4a20c0867c4..f30ac6ec0f2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java @@ -132,7 +132,7 @@ public static ImmutableList 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: * * 

      *     (
@@ -193,7 +193,7 @@ static Integer[] parseZ3Format(String lastLine) {
      *     )
      *
* - * @param lines CVC5 output + * @param lines cvc5 output * @return list of labels referenced in unsat core */ static Integer[] parseCVC5Format(String[] lines) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java b/key.core/src/main/java/de/uka/ilkd/key/smt/communication/Cvc5Socket.java similarity index 89% rename from key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java rename to key.core/src/main/java/de/uka/ilkd/key/smt/communication/Cvc5Socket.java index d4957b9270c..37e57a6e1f1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/communication/CVC5Socket.java +++ b/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 (...). + * Socket for cvc5 (...). */ -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); } @@ -66,7 +66,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()); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java index fc459866dd8..10677ec1faf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java @@ -45,7 +45,7 @@ public class ModularSMTLib2Translator implements SMTTranslator { * that {@link de.uka.ilkd.key.smt.SMTFocusResults} can interpret the unsat core. *

* This option is currently only enabled for Z3. - * Currently, this option only works with a CVC5 dev build. + * Currently, this option only works with a cvc5 dev build. * Once the fix is included in a release, * add this handler option to the .props file. *

diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java index 012cb6138a3..5b697bb940b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java @@ -48,9 +48,9 @@ public class SolverPropertiesLoader { */ private static final Collection SOLVERS = new ArrayList<>(5); /** - * The LEGACY solvers loaded by this loader. + * The EXPERIMENTAL solvers loaded by this loader. */ - private static final Collection LEGACY_SOLVERS = new ArrayList<>(2); + private static final Collection 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,10 +211,12 @@ public Collection 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); } } } @@ -222,11 +224,11 @@ public Collection getSolvers() { } /** - * @return a copy of the created list of legacy solvers + * @return a copy of the created list of experimental solvers */ - public Collection getLegacySolvers() { + public Collection getExperimentalSolvers() { getSolvers(); - return new ArrayList<>(LEGACY_SOLVERS); + return new ArrayList<>(EXPERIMENTAL_SOLVERS); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypes.java b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypes.java index b32eb79cfb2..9f6708e4e7e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypes.java +++ b/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 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 LEGACY_SOLVERS = new ArrayList<>(1); + private static final Collection 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 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 getLegacySolvers() { + public static @NonNull Collection getExperimentalSolvers() { if (SOLVERS.isEmpty()) { getSolverTypes(); } - return new ArrayList<>(LEGACY_SOLVERS); + return new ArrayList<>(EXPERIMENTAL_SOLVERS); } /** diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/AddingSMTSolvers.md b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/AddingSMTSolvers.md index cca3956585e..aa3fb1928dd 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/AddingSMTSolvers.md +++ b/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 ``` diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4.props index 156a8eaa2c5..524c345cd1d 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4.props +++ b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4.props @@ -1,3 +1,4 @@ +experimental=true params=--no-print-success -m --interactive --lang smt2 timeout=-1 name=CVC4 diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props index d52ff473927..99c861f8fc5 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props +++ b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props @@ -1,4 +1,4 @@ -legacy=true +experimental=true params=--no-print-success -m --interactive --lang smt2 timeout=-1 name=CVC4 (Legacy Translation) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props index 3e057ccb853..5dbc0c62ad0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props +++ b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props @@ -1,10 +1,10 @@ params=--interactive -m --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,\ diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_legacy.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_legacy.props index c2404f38b92..bd63ac4b0c0 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_legacy.props +++ b/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) diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java index 8c84069e5e4..047a14785c1 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java @@ -42,15 +42,15 @@ public class TestSMTMod { && it.getName().equals("Z3")) .findFirst().orElse(null); - private static final SolverType CVC4_SOLVER = SolverTypes.getSolverTypes().stream() + private static final SolverType CVC5_SOLVER = SolverTypes.getSolverTypes().stream() .filter(it -> it.getClass().equals(SolverTypeImplementation.class) - && it.getName().equals("CVC4")) + && it.getName().equals("cvc5")) .findFirst().orElse(null); /** * This tests if x mod y is non-negative and x mod y < |y| for y != 0 * thus satisfying the definition of euclidean modulo - * Tests for Z3 and CVC4 + * Tests for Z3 and cvc5 * * @throws ProblemLoaderException Occured Exception during load of problem file */ @@ -70,11 +70,11 @@ public void testModSpec() throws ProblemLoaderException { } else { LOGGER.warn("Warning:Z3 solver not installed, tests skipped."); } - if (CVC4_SOLVER.isInstalled(true)) { - result = checkGoal(g, CVC4_SOLVER); + if (CVC5_SOLVER.isInstalled(true)) { + result = checkGoal(g, CVC5_SOLVER); assertSame(SMTSolverResult.ThreeValuedTruth.VALID, result.isValid()); } else { - LOGGER.warn("Warning:CVC4 solver not installed, tests skipped."); + LOGGER.warn("Warning:cvc5 solver not installed, tests skipped."); } } finally { env.dispose(); diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java deleted file mode 100644 index 756cd8e17f7..00000000000 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc4LegacyTest.java +++ /dev/null @@ -1,99 +0,0 @@ -/* 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.*; -import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID; - -/** - * Tests that some simple .key files are translated to SMT-LIB correctly and CVC4 has a specified - * behavior on them (returns unsat, sat, or unknown/timeout). The test uses the old and non-modular - * SMT translation! - *

- * Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! - */ -public class Cvc4LegacyTest extends SMTSolverTest { - private static final String SYSTEM_PROPERTY_SOLVER_PATH = "cvc4SolverPath"; - private static final Logger LOGGER = LoggerFactory.getLogger(Cvc4LegacyTest.class); - private static final String SOLVER_NAME = "CVC4 (Legacy Translation)"; - - public static final SolverType CVC4_LEGACY_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 = CVC4_LEGACY_SOLVER; - String solverPathProperty = System.getProperty(SYSTEM_PROPERTY_SOLVER_PATH); - if (solverPathProperty != null && !solverPathProperty.isEmpty()) { - type.setSolverCommand(solverPathProperty); - } - return type; - } - - @Override - protected final Stream provideTestData() { - // no timeouts at all, either sat, unsat, or explicit unknown - return Stream.of( - Arguments.of(FALSIFIABLE, "andnot.key"), - Arguments.of(VALID, "ornot.key"), - Arguments.of(FALSIFIABLE, "andornot.key"), - Arguments.of(VALID, "andornot2.key"), - Arguments.of(VALID, "imply.key"), - Arguments.of(VALID, "imply2.key"), - Arguments.of(FALSIFIABLE, "imply3.key"), - Arguments.of(VALID, "equi1.key"), - Arguments.of(FALSIFIABLE, "equi2.key"), - Arguments.of(VALID, "allex1.key"), - Arguments.of(FALSIFIABLE, "allex2.key"), - Arguments.of(VALID, "allex3.key"), - Arguments.of(VALID, "logicalite1.key"), - Arguments.of(FALSIFIABLE, "logicalite2.key"), - Arguments.of(VALID, "equal1.key"), - Arguments.of(UNKNOWN, "equal2.key"), - Arguments.of(VALID, "subsort1.key"), - Arguments.of(UNKNOWN, "subsort2.key"), - Arguments.of(VALID, "add1.key"), - Arguments.of(VALID, "bsum1.key"), - Arguments.of(VALID, "bsum2.key"), - Arguments.of(UNKNOWN, "bsum3.key"), - Arguments.of(VALID, "bprod1.key"), - Arguments.of(VALID, "bprod2.key"), - Arguments.of(UNKNOWN, "bprod3.key"), - Arguments.of(VALID, "binder4.key"), - Arguments.of(VALID, "binder5.key"), - Arguments.of(VALID, "div1.key"), - Arguments.of(VALID, "div3.key"), - Arguments.of(UNKNOWN, "div5.key"), - Arguments.of(UNKNOWN, "div6.key")); - } -} diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java index 76b0f34be69..d2980bb7b82 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java @@ -47,7 +47,7 @@ public boolean toolInstalled() { getLogger().warn("Warning: {} is not installed, tests skipped.", getSolverName()); getLogger().warn( - "Maybe use JVM system property \"{}\" to define the path to the CVC4 command.", + "Maybe use JVM system property \"{}\" to define the path to the solver binary.", getSystemPropertySolverPath()); } else if (!solverType.supportHasBeenChecked()) { if (!solverType.checkForSupport()) { diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java index 2459b7ecebd..afd63a8001d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java @@ -12,10 +12,7 @@ import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.init.*; 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.util.HelperClassForTests; @@ -34,13 +31,8 @@ public abstract class SMTTestCommons { protected static final String FOLDER = HelperClassForTests.TESTCASE_DIRECTORY + File.separator + "smt" + File.separator + "tacletTranslation" + File.separator; - InitConfig initConfig = null; - static protected ProblemInitializer initializer = null; - static protected final Profile profile = init(); - - static Profile init() { - return new JavaProfile(); - } + protected static ProblemInitializer initializer = null; + protected static final Profile profile = new JavaProfile(); private TermServices services; @@ -57,24 +49,12 @@ protected TermServices getServices() { public abstract boolean toolInstalled(); - protected boolean correctResult(String filepath, SMTSolverResult.ThreeValuedTruth expected) - throws ProblemLoaderException { - Assumptions.assumeTrue(toolInstalled()); - SMTSolverResult result = checkFile(filepath); - return correctResult(expected, result); - } - protected SMTSolverResult.ThreeValuedTruth getResult(String filepath) throws ProblemLoaderException { Assumptions.assumeTrue(toolInstalled()); return checkFile(filepath).isValid(); } - private boolean correctResult(SMTSolverResult.ThreeValuedTruth expected, - @NonNull SMTSolverResult result) { - return result.isValid() == expected; - } - /** * check a problem file * @@ -137,7 +117,7 @@ protected ProofAggregate parse(File file, Profile pro) { if (initializer == null) { initializer = new ProblemInitializer(po.getProfile()); } - initConfig = initializer.prepare(po); + InitConfig initConfig = initializer.prepare(po); result = initializer.startProver(initConfig, po); services = initConfig.getServices(); // po.close(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java index 1cb00ad3d75..d5b9af61bf6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java @@ -142,7 +142,7 @@ public SMTSettingsProvider() { if (FeatureSettings.isFeatureActivated(FEATURE_SMT_TRANSLATION_OPTIONS)) { getChildren().add(new TranslationOptions()); } else { - solverTypes.removeAll(SolverTypes.getLegacySolvers()); + solverTypes.removeAll(SolverTypes.getExperimentalSolvers()); } /* * Only add options for those solvers that are actually theoretically available, according From 4300de5a2ba7170d3be86196d7329e438fc28928 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 25 Apr 2025 13:14:10 +0200 Subject: [PATCH 7/9] fix typo --- .../resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props index a91eec82ee4..e7e3247b88d 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props +++ b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props @@ -5,5 +5,5 @@ 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 From 745348fd368bdfc2170d44bc9f9c4206c56282dc Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 25 Apr 2025 16:37:56 +0200 Subject: [PATCH 8/9] better error message for failed tests, default timeout to 50s for sat/unsat and 2s for timeout/unknown cases --- .../de/uka/ilkd/key/smt/SMTTestSettings.java | 22 ++++++++++++----- .../uka/ilkd/key/smt/test/SMTSolverTest.java | 4 +++- .../uka/ilkd/key/smt/test/SMTTestCommons.java | 24 +++++++++++++------ 3 files changed, 36 insertions(+), 14 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java index 1de96cc5776..b93b7975ccb 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java @@ -16,6 +16,11 @@ * Special settings for the SMT solvers tests. */ public class SMTTestSettings implements de.uka.ilkd.key.smt.SMTSettings { + /* + * We set the default timeout to 50s. This should be sufficient for the unsat/sat cases which we + * have currently. For the unknown/timeout cases, we set a shorter timeout via setTimeout(). + */ + private long timeout = 50000; @Override public int getMaxConcurrentProcesses() { @@ -39,12 +44,17 @@ public Collection getTaclets() { @Override public long getTimeout() { - /* - * 30s should be sufficient, and since we have a few examples that are expected to run into - * a timeout (because the file is intentionally not provable), we want to have it as low as - * possible. - */ - return 30000; + return timeout; + } + + /** + * This is needed as a quick fix, so we can set a shorter timeout for test cases with expected + * unknown results, while keeping the default timeout for all other cases. + * + * @param timeout the timeout in milliseconds + */ + public void setTimeout(long timeout) { + this.timeout = timeout; } @Override diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java index d2980bb7b82..036c90f7722 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java @@ -72,6 +72,8 @@ public boolean toolInstalled() { @ParameterizedTest(name = "test {1}") public void test(SMTSolverResult.ThreeValuedTruth expected, String filename) throws ProblemLoaderException { - Assertions.assertSame(expected, getResult(TEST_DIR + filename)); + SMTSolverResult.ThreeValuedTruth actual = getResult(expected, TEST_DIR + filename); + Assertions.assertSame(expected, actual, "Expected \"" + expected.name() + "\" for " + + filename + ", but result was \"" + actual.name() + "\"!"); } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java index afd63a8001d..a06abdec8fb 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java @@ -49,40 +49,50 @@ protected TermServices getServices() { public abstract boolean toolInstalled(); - protected SMTSolverResult.ThreeValuedTruth getResult(String filepath) + protected SMTSolverResult.ThreeValuedTruth getResult(SMTSolverResult.ThreeValuedTruth expected, + String filepath) throws ProblemLoaderException { Assumptions.assumeTrue(toolInstalled()); - return checkFile(filepath).isValid(); + return checkFile(expected, filepath).isValid(); } /** * check a problem file * + * @param expected the expected result. Needed for setting a shorter timeout for unknown cases * @param filepath the path to the file * @return the resulttype of the external solver * @throws ProblemLoaderException */ - protected SMTSolverResult checkFile(String filepath) throws ProblemLoaderException { + protected SMTSolverResult checkFile(SMTSolverResult.ThreeValuedTruth expected, String filepath) + throws ProblemLoaderException { KeYEnvironment p = loadProof(filepath); try { Proof proof = p.getLoadedProof(); assertNotNull(proof); assertEquals(1, proof.openGoals().size()); Goal g = proof.openGoals().iterator().next(); - return checkGoal(g); + return checkGoal(expected, g); } finally { p.dispose(); } } - private @NonNull SMTSolverResult checkGoal(Goal g) { - SolverLauncher launcher = new SolverLauncher(new SMTTestSettings()); + private @NonNull SMTSolverResult checkGoal(SMTSolverResult.ThreeValuedTruth expected, Goal g) { + SMTTestSettings settings = new SMTTestSettings(); + if (expected == SMTSolverResult.ThreeValuedTruth.UNKNOWN) { + /* + * Hack: For test cases with unknown/timeout as expected result, we do not want to hold + * up the test unnecessarily long, so we set a short SMT timeout. + */ + settings.setTimeout(2000); + } + SolverLauncher launcher = new SolverLauncher(settings); SMTProblem problem = new SMTProblem(g); launcher.launch(problem, g.proof().getServices(), getSolverType()); return problem.getFinalResult(); } - protected KeYEnvironment loadProof(String filepath) throws ProblemLoaderException { return KeYEnvironment.load(new File(filepath), null, null, null); } From 8e7666d55e21a13837106b500811efa82030f0f8 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 25 Apr 2025 17:29:13 +0200 Subject: [PATCH 9/9] disabled two test cases that show strange behavior between Z3 versions and CI --- .../src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java index c93a688be27..e0abc62b10b 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java @@ -75,9 +75,9 @@ protected Stream provideTestData() { Arguments.of(VALID, "logicalite1.key"), Arguments.of(FALSIFIABLE, "logicalite2.key"), Arguments.of(VALID, "equal1.key"), - Arguments.of(FALSIFIABLE, "equal2.key"), + // Arguments.of(FALSIFIABLE, "equal2.key"), // disabled because it takes too long in CI Arguments.of(VALID, "subsort1.key"), - Arguments.of(FALSIFIABLE, "subsort2.key"), + // Arguments.of(FALSIFIABLE, "subsort2.key"), // only with old z3 versions (e.g. 4.9.x) Arguments.of(VALID, "add1.key"), Arguments.of(VALID, "bsum1.key"), Arguments.of(VALID, "bsum2.key"),