From 7f1633af48ff581dee55f8e49eb9c9527476c00f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= <3751182+as3810t@users.noreply.github.com> Date: Thu, 5 Oct 2023 10:33:24 +0000 Subject: [PATCH] Update existing well-established solvers --- .../smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java | 4 +++- .../impl/mathsat/MathSATSmtLibSolverInstaller.java | 2 +- .../impl/princess/PrincessSmtLibSolverInstaller.java | 2 +- .../smtinterpol/SMTInterpolSmtLibSolverInstaller.java | 5 ++++- .../solver/smtlib/impl/z3/Z3SmtLibSolverInstaller.java | 9 ++++++++- 5 files changed, 17 insertions(+), 5 deletions(-) diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java index 1f22b1988e..877b830e53 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java @@ -96,7 +96,9 @@ public SolverFactory getSolverFactory(final Path installDir, final String versio @Override public List getSupportedVersions() { - return Arrays.asList("1.0.2", "1.0.1", "1.0.0"); + return Arrays.asList( + "1.0.8", "1.0.7", "1.0.6", "1.0.5", "1.0.4", "1.0.3", "1.0.2", "1.0.1", "1.0.0" + ); } private URL getDownloadUrl(final String version) throws SmtLibSolverInstallerException, MalformedURLException { diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibSolverInstaller.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibSolverInstaller.java index df073cb186..e067faf099 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibSolverInstaller.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/mathsat/MathSATSmtLibSolverInstaller.java @@ -170,7 +170,7 @@ public SolverFactory getSolverFactory(final Path installDir, final String versio @Override public List getSupportedVersions() { return Arrays.asList( - "5.6.8", "5.6.7", "5.6.6", "5.6.5", "5.6.4", "5.6.3", "5.6.2", "5.6.1", "5.6.0", + "5.6.10", "5.6.9", "5.6.8", "5.6.7", "5.6.6", "5.6.5", "5.6.4", "5.6.3", "5.6.2", "5.6.1", "5.6.0", "5.5.4", "5.5.3", "5.5.2", "5.5.1", "5.5.0", "5.4.1", "5.4.0", "5.3.14", "5.3.13", "5.3.12", "5.3.11", "5.3.10", "5.3.9", "5.3.8", "5.3.7", "5.3.6", diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibSolverInstaller.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibSolverInstaller.java index 40caafbe0e..4c1d124653 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibSolverInstaller.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibSolverInstaller.java @@ -90,7 +90,7 @@ public SolverFactory getSolverFactory(final Path installDir, final String versio @Override public List getSupportedVersions() { return Arrays.asList( - "2022-07-01", "2021-11-15", + "2023-06-19", "2023-04-07", "2022-11-03", "2022-07-01", "2021-11-15", "2021-05-10", "2021-03-10", "2020-03-12", "2019-10-02", "2019-07-24", "2018-10-26", "2018-05-25", "2018-01-27", "2017-12-06", "2017-07-17" ); diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java index 065664320f..ed4d0bba13 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java @@ -81,13 +81,16 @@ public SolverFactory getSolverFactory(final Path installDir, final String versio @Override public List getSupportedVersions() { - return Arrays.asList("2.5-1230", "2.5-916", "2.5-663", "2.5-479", "2.5-7"); + return Arrays.asList("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; diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/z3/Z3SmtLibSolverInstaller.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/z3/Z3SmtLibSolverInstaller.java index 2d9a8bdce4..12443a2c8b 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/z3/Z3SmtLibSolverInstaller.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/z3/Z3SmtLibSolverInstaller.java @@ -44,6 +44,13 @@ public Z3SmtLibSolverInstaller(final Logger logger) { super(logger); versions = new ArrayList<>(); + versions.add(SemVer.VersionDecoder.create(SemVer.of("4.12.0")) + .addString(LINUX, X64, "x64-glibc-2.35") + .addString(WINDOWS, X64, "x64-win") + .addString(WINDOWS, X86, "x86-win") + .addString(MAC, X64, "x64-osx-10.16") + .build() + ); versions.add(SemVer.VersionDecoder.create(SemVer.of("4.8.12")) .addString(LINUX, X64, "x64-glibc-2.31") .addString(WINDOWS, X64, "x64-win") @@ -185,7 +192,7 @@ public SolverFactory getSolverFactory(final Path installDir, final String versio @Override public List getSupportedVersions() { return Arrays.asList( - "4.11.2", "4.11.0", "4.10.2", "4.10.1", "4.10.0", "4.9.1", "4.9.0", + "4.12.2", "4.12.1", "4.12.0", "4.11.2", "4.11.0", "4.10.2", "4.10.1", "4.10.0", "4.9.1", "4.9.0", "4.8.17", "4.8.16", "4.8.15", "4.8.14", "4.8.13", "4.8.12", "4.8.11", "4.8.10", "4.8.9", "4.8.8", "4.8.7", "4.8.6", "4.8.5", "4.8.4", "4.8.3", "4.8.2", "4.8.1", "4.7.1", "4.6.0", "4.5.0",