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/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 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 fe50d3cf0d5..cbbef494762 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); } @@ -57,7 +57,7 @@ public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOEx pipe.sendMessage("(exit)"); // pipe.close(); } else if (msg.contains("unknown")) { - sc.setFinalResult(SMTSolverResult.createUnknownResult(getName())); + sc.setFinalResult(SMTSolverResult.createUnknownResult(getName(), false)); sc.setState(FINISH); pipe.sendMessage("(exit)"); // pipe.close(); @@ -67,7 +67,7 @@ public void messageIncoming(@NonNull Pipe pipe, @NonNull String msg) throws IOEx @Override public AbstractSolverSocket copy() { - return new CVC5Socket(getName(), getQuery()); + return new Cvc5Socket(getName(), getQuery()); } } 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/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 1b3115d8c43..135c6e6bfcb 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 @@ -44,7 +44,7 @@ public class ModularSMTLib2Translator implements SMTTranslator { * Handler option. If provided, the translator will label translations of sequent formulas such * that {@link de.uka.ilkd.key.smt.SMTFocusResults} can interpret the unsat core. *

- * This option is currently only enabled for Z3 and CVC5 (needs 1.0.4+). + * This option is currently only enabled for Z3 and cvc5 (needs 1.0.4+). *

* Make sure to also send (get-unsat-core) in the respective socket class when adding this * option. 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 14407ad355d..7e5e1a0f490 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 --produce-models --no-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 d8d6a955237..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 @@ -1,9 +1,9 @@ -legacy=true +experimental=true params=--no-print-success --produce-models --no-interactive --lang smt2 timeout=-1 name=CVC4 (Legacy Translation) info=CVC4 solver command=cvc4 version=--version -socketClass=socketClass=de.uka.ilkd.key.smt.communication.CVC4Socket +socketClass=de.uka.ilkd.key.smt.communication.CVC4Socket translatorClass=de.uka.ilkd.key.smt.SmtLib2Translator 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 5dc0bef1d1c..760e4eb3caf 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=--no-interactive --produce-models --lang smt2 timeout=-1 -name=CVC5 -info=CVC5 solver (https://cvc5.github.io/). +name=cvc5 +info=cvc5 solver (https://cvc5.github.io/). command=cvc5 version=--version -socketClass=de.uka.ilkd.key.smt.communication.CVC5Socket +socketClass=de.uka.ilkd.key.smt.communication.Cvc5Socket handlers=de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler,\ de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler,\ de.uka.ilkd.key.smt.newsmt2.QuantifierHandler,\ 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/SMTTestSettings.java b/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java index a6cbba2a302..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 @@ -12,12 +12,15 @@ 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; - } + /* + * 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() { @@ -41,7 +44,17 @@ public Collection getTaclets() { @Override public long getTimeout() { - return 300000; + 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 @@ -136,6 +149,4 @@ public boolean invarianForall() { public NewSMTTranslationSettings getNewSettings() { return new NewSMTTranslationSettings(); } - - } 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/SMTSolverTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java new file mode 100644 index 00000000000..036c90f7722 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTSolverTest.java @@ -0,0 +1,79 @@ +/* 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.params.ParameterizedTest; +import org.junit.jupiter.params.provider.Arguments; +import org.junit.jupiter.params.provider.MethodSource; +import org.slf4j.Logger; + +/** + * 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}! + */ +@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 solver binary.", + 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 { + 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/TestCommons.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java similarity index 56% 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..a06abdec8fb 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 @@ -4,9 +4,6 @@ package de.uka.ilkd.key.smt.test; import java.io.File; -import java.util.Collection; -import java.util.HashSet; -import java.util.LinkedList; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.logic.TermServices; @@ -15,14 +12,11 @@ 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; -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; +import org.jspecify.annotations.NonNull; import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.api.Tag; @@ -33,21 +27,12 @@ * 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(); - - static Profile init() { - return new JavaProfile(); - } + protected static ProblemInitializer initializer = null; + protected static final Profile profile = new JavaProfile(); private TermServices services; @@ -62,96 +47,65 @@ protected TermServices getServices() { */ public abstract SolverType getSolverType(); - public abstract boolean toolNotInstalled(); + public abstract boolean toolInstalled(); - protected boolean correctResult(String filepath, boolean isValid) + protected SMTSolverResult.ThreeValuedTruth getResult(SMTSolverResult.ThreeValuedTruth expected, + String filepath) throws ProblemLoaderException { - Assumptions.assumeFalse(toolNotInstalled()); - SMTSolverResult result = checkFile(filepath); - // unknown is always allowed. But wrong answers are not allowed - return correctResult(isValid, result); - } - - protected boolean correctResult(Goal g, boolean isValid) { - return correctResult(isValid, checkGoal(g)); - } - - private boolean correctResult(boolean isValid, SMTSolverResult result) { - if (isValid && result != null) { - return result.isValid() != SMTSolverResult.ThreeValuedTruth.FALSIFIABLE; - } else { - return result.isValid() != SMTSolverResult.ThreeValuedTruth.VALID; - } + Assumptions.assumeTrue(toolInstalled()); + 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 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); } - /** - * 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); @@ -173,7 +127,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.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..e0abc62b10b --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3LegacyTest.java @@ -0,0 +1,96 @@ +/* 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 Z3 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 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"), // disabled because it takes too long in CI + Arguments.of(VALID, "subsort1.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"), + 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"), + 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..8e6da3e20c5 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Z3Test.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.*; +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, 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}! + */ +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; + } + + @Override + protected final Stream 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")); + } +} 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