Use solvermanager to avoid dangling solver processes in long tests

RipplB · Feb 25, 2024 · 2af9a58 · 2af9a58
1 parent 0e22535
commit 2af9a58
Show file tree

Hide file tree

Showing 2 changed files with 33 additions and 38 deletions.
diff --git a/...ava/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java b/...ava/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java
@@ -81,34 +81,23 @@ public SolverFactory getSolverFactory(final Path installDir, final String versio
 
     @Override
     public List<String> getSupportedVersions() {
-        return Arrays.asList("2.5-1256", "2.5-1230", "2.5-916", "2.5-663", "2.5-479", "2.5-7");
+        return Arrays.asList("2.5-1301", "2.5-1256", "2.5-1230", "2.5-916", "2.5-663", "2.5-479", "2.5-7");
     }
 
     private URL getDownloadUrl(final String version)
             throws SmtLibSolverInstallerException, MalformedURLException {
-        final String fileName;
-        switch (version) {
-            case "2.5-1256":
-                fileName = "2.5-1230-g55d6ba76";
-                break;
-            case "2.5-1230":
-                fileName = "2.5-1230-g3eafb46a";
-                break;
-            case "2.5-916":
-                fileName = "2.5-916-ga5843d8b";
-                break;
-            case "2.5-663":
-                fileName = "2.5-663-gf15aa217";
-                break;
-            case "2.5-479":
-                fileName = "2.5-479-ga49e50b1";
-                break;
-            case "2.5-7":
-                fileName = "2.5-7-g64ec65d";
-                break;
-            default:
-                throw new SmtLibSolverInstallerException("Unsupported solver version.");
-        }
+        final String fileName = switch (version) {
+            //TODO download won't work on this, switch to the latest on next release
+            case "2.5-1301" -> "2.5-1301-g2c871e40";
+
+            case "2.5-1256" -> "2.5-1230-g55d6ba76";
+            case "2.5-1230" -> "2.5-1230-g3eafb46a";
+            case "2.5-916" -> "2.5-916-ga5843d8b";
+            case "2.5-663" -> "2.5-663-gf15aa217";
+            case "2.5-479" -> "2.5-479-ga49e50b1";
+            case "2.5-7" -> "2.5-7-g64ec65d";
+            default -> throw new SmtLibSolverInstallerException("Unsupported solver version.");
+        };
 
         return URI.create(String.format(
                 "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-%s.jar",

diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java
@@ -19,7 +19,7 @@
 import hu.bme.mit.theta.common.logging.ConsoleLogger;
 import hu.bme.mit.theta.common.logging.Logger;
 import hu.bme.mit.theta.common.logging.Logger.Level;
-import hu.bme.mit.theta.solver.smtlib.impl.smtinterpol.SMTInterpolSmtLibSolverFactory;
+import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
 import hu.bme.mit.theta.xsts.XSTS;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfig;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfigBuilder;
@@ -355,23 +355,29 @@ public void test() throws IOException {
                 new FileInputStream(propPath))) {
             xsts = XstsDslManager.createXsts(inputStream);
         }
-        String[] args = {"-q"};
+//        String[] args = {"-q"};
 //        final var smtSolver = SMTInterpolSmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\smtinterpol-2.5-1256-g55d6ba76.jar"), args);
-        final var smtSolver = SMTInterpolSmtLibSolverFactory.create(Path.of("E:\\smt\\SMTInterpol-releases\\smtinterpol-2.5-1301-g2c871e40_datatype_interpolation.jar"), args);
+//        final var smtSolver = SMTInterpolSmtLibSolverFactory.create(Path.of("E:\\smt\\SMTInterpol-releases\\smtinterpol-2.5-1301-g2c871e40_datatype_interpolation.jar"), args);
 //        final var smtSolver = CVC5SmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\cvc5-Win64.exe"), new String[]{"--incremental"});
 //        final var smtSolver = CVC5SmtLibSolverFactory.create(Path.of("E:\\smt\\cvc5\\cvc5-2024-01-13-x86_64-win64-production.exe"), new String[]{"--incremental"});
 //        final var smtSolver = Z3SmtLibSolverFactory.create(Path.of("C:\\Users\\brippl\\Downloads\\z3-4.12.4-x64-win\\bin\\z3.exe"), new String[]{"-smt2", "-in"});
-        final XstsConfig<?, ?, ?> configuration = new XstsConfigBuilder(domain,
-                XstsConfigBuilder.Refinement.SEQ_ITP, smtSolver,
-                smtSolver).initPrec(XstsConfigBuilder.InitPrec.CTRL)
-                .optimizeStmts(XstsConfigBuilder.OptimizeStmts.ON)
-                .predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250)
-                .autoExpl(XstsConfigBuilder.AutoExpl.NEWOPERANDS).logger(logger).build(xsts);
-        final SafetyResult<?, ?> status = configuration.check();
-        if (safe) {
-            assertTrue(status.isSafe());
-        } else {
-            assertTrue(status.isUnsafe());
+        try (final var solverManager = SmtLibSolverManager.create(Path.of("E:\\smt"), logger)) {
+            final var smtSolver = solverManager.getSolverFactory("smtinterpol", "2.5-1301-g2c871e40");
+            final XstsConfig<?, ?, ?> configuration = new XstsConfigBuilder(domain,
+                    XstsConfigBuilder.Refinement.SEQ_ITP, smtSolver,
+                    smtSolver).initPrec(XstsConfigBuilder.InitPrec.CTRL)
+                    .optimizeStmts(XstsConfigBuilder.OptimizeStmts.ON)
+                    .predSplit(XstsConfigBuilder.PredSplit.CONJUNCTS).maxEnum(250)
+                    .autoExpl(XstsConfigBuilder.AutoExpl.NEWOPERANDS).logger(logger).build(xsts);
+            final SafetyResult<?, ?> status = configuration.check();
+
+            if (safe) {
+                assertTrue(status.isSafe());
+            } else {
+                assertTrue(status.isUnsafe());
+            }
+        } catch (Exception e) {
+            throw new RuntimeException(e);
         }
     }