From 715fadfc54e8570ce151b0d9824c58abba0281af Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 20 Jun 2024 14:10:35 +0200 Subject: [PATCH 01/14] Fixed Windows filename for cvc5 --- .../solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 e6f8978892..9b36e25867 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 @@ -48,7 +48,7 @@ public CVC5SmtLibSolverInstaller(final Logger logger) { versions.add(SemVer.VersionDecoder.create(SemVer.of("1.0.0")) .addString(LINUX, X64, "Linux") .addString(MAC, X64, "macOS") - .addString(WINDOWS, X64, "Win64") + .addString(WINDOWS, X64, "Win64.exe") .build() ); } From 47b796c93100ad98cbbfef8fb5f6254c5983aca4 Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 20 Jun 2024 14:11:25 +0200 Subject: [PATCH 02/14] Add dummy assertion to formula A for interpolation in cvc5 --- .../solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java index 69fe6fb906..707a80735c 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java @@ -17,6 +17,7 @@ import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.decl.Decls; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.solver.*; @@ -44,6 +45,7 @@ import static com.google.common.base.Preconditions.*; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; public class CVC5SmtLibItpSolver extends SmtLibItpSolver { @@ -55,6 +57,8 @@ public CVC5SmtLibItpSolver(final SmtLibSymbolTable symbolTable, final Supplier itpSolverBinaryFactory) { super(symbolTable, transformationManager, termTransformer, solverBinary); this.itpSolverBinaryFactory = itpSolverBinaryFactory; + final var tmp = Decls.Const("shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh", Int()); +// symbolTable.put(tmp, "shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh", "(declare-fun shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh () Int)"); } @Override @@ -106,11 +110,15 @@ public Interpolant getInterpolant(ItpPattern pattern) { final var bTerm = B.stream() .flatMap(m -> m.getTerms().stream().map(Tuple2::get2)); + itpSolverBinary.issueCommand("(push)"); + itpSolverBinary.issueCommand("(declare-fun shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh () Int)"); + itpSolverBinary.issueCommand("(assert (= shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh 0))"); itpSolverBinary.issueCommand( String.format("(assert (and %s))", aTerm.collect(Collectors.joining(" ")))); itpSolverBinary.issueCommand( String.format("(get-interpolant _cvc5_interpolant%d (not (and %s)))", interpolantCount++, bTerm.collect(Collectors.joining(" ")))); + itpSolverBinary.issueCommand("(pop)"); itpMap.put(marker, termTransformer.toExpr(parseItpResponse(itpSolverBinary.readResponse()), From 978ab04d828b8c4050af253d4050df76d435190f Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 20 Jun 2024 16:59:52 +0200 Subject: [PATCH 03/14] Add support for cvc5 1.1.1 and 1.1.2 --- .../impl/cvc5/CVC5SmtLibSolverInstaller.java | 45 ++++++++++++++----- 1 file changed, 35 insertions(+), 10 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 9b36e25867..6e506f60e3 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 @@ -20,6 +20,7 @@ import hu.bme.mit.theta.solver.SolverFactory; import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstaller; import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstallerException; +import hu.bme.mit.theta.solver.smtlib.utils.Compress; import hu.bme.mit.theta.solver.smtlib.utils.SemVer; import java.io.FileOutputStream; @@ -45,6 +46,12 @@ public CVC5SmtLibSolverInstaller(final Logger logger) { super(logger); versions = new ArrayList<>(); + versions.add(SemVer.VersionDecoder.create(SemVer.of("1.1.1")) + .addString(LINUX, X64, "Linux-static.zip") + .addString(MAC, X64, "macOS-arm64-static.zip") + .addString(WINDOWS, X64, "Win64-static.zip") + .build() + ); versions.add(SemVer.VersionDecoder.create(SemVer.of("1.0.0")) .addString(LINUX, X64, "Linux") .addString(MAC, X64, "macOS") @@ -60,13 +67,21 @@ protected String getSolverName() { @Override protected void installSolver(final Path installDir, final String version) throws SmtLibSolverInstallerException { - try ( - final var inputChannel = Channels.newChannel(getDownloadUrl(version).openStream()); - final var outputChannel = new FileOutputStream(installDir.resolve(getSolverBinaryName(version)).toAbsolutePath().toString()).getChannel() - ) { + try (final var inputStream = getDownloadUrl(version).openStream()) { logger.write(Logger.Level.MAINSTEP, "Starting download (%s)...\n", getDownloadUrl(version).toString()); - outputChannel.transferFrom(inputChannel, 0, Long.MAX_VALUE); - installDir.resolve(getSolverBinaryName(version)).toFile().setExecutable(true, true); + if (SemVer.of(version).compareTo(SemVer.of("1.1.1")) < 0) { + try ( + final var inputChannel = Channels.newChannel(inputStream); + final var outputChannel = new FileOutputStream(installDir.resolve(getSolverBinaryName(version)).toAbsolutePath().toString()).getChannel() + ) { + outputChannel.transferFrom(inputChannel, 0, Long.MAX_VALUE); + installDir.resolve(getSolverBinaryName(version)).toFile().setExecutable(true, true); + } + } else { + Compress.extract(inputStream, installDir, Compress.CompressionType.ZIP); + installDir.resolve("bin").resolve(getSolverBinaryName(version)).toFile().setExecutable(true, true); + } + } catch (IOException e) { throw new SmtLibSolverInstallerException(e); } @@ -101,14 +116,19 @@ protected String[] getDefaultSolverArgs(String version) { @Override public SolverFactory getSolverFactory(final Path installDir, final String version, final Path solverPath, final String[] solverArgs) throws SmtLibSolverInstallerException { - final var solverFilePath = solverPath != null ? solverPath : installDir.resolve(getSolverBinaryName(version)); + final Path solverFilePath; + if (SemVer.of(version).compareTo(SemVer.of("1.1.1")) < 0) { + solverFilePath = solverPath != null ? solverPath : installDir.resolve(getSolverBinaryName(version)); + } else { + solverFilePath = solverPath != null ? solverPath : installDir.resolve("bin").resolve(getSolverBinaryName(version)); + } return CVC5SmtLibSolverFactory.create(solverFilePath, solverArgs); } @Override public List getSupportedVersions() { 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" + "1.1.2", "1.1.1", "1.1.0", "1.0.9", "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" ); } @@ -134,13 +154,18 @@ private String getArchString(final String version) throws SmtLibSolverInstallerE } } if (archStr == null) { - throw new SmtLibSolverInstallerException(String.format("MathSAT on operating system %s and architecture %s is not supported", OsHelper.getOs(), OsHelper.getArch())); + throw new SmtLibSolverInstallerException(String.format("CVC5 on operating system %s and architecture %s is not supported", OsHelper.getOs(), OsHelper.getArch())); } return archStr; } private String getSolverBinaryName(final String version) throws SmtLibSolverInstallerException { - return String.format("cvc5-%s", getArchString(version)); + if (SemVer.of(version).compareTo(SemVer.of("1.1.1")) < 0) { + return String.format("cvc5-%s", getArchString(version)); + } else { + return OsHelper.getOs() == WINDOWS ? "cvc5.exe" : "cvc5"; + } + } } From 169495d7503162623670b2a880bb9abdd9b2c2d7 Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 20 Jun 2024 18:08:21 +0200 Subject: [PATCH 04/14] Fixed a typo in an SMTInterpol url --- .../impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 1edfb39281..3fbdc13376 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 @@ -89,7 +89,7 @@ private URL getDownloadUrl(final String version) final String fileName; switch (version) { case "2.5-1256": - fileName = "2.5-1230-g55d6ba76"; + fileName = "2.5-1256-g55d6ba76"; break; case "2.5-1230": fileName = "2.5-1230-g3eafb46a"; From 213ce46f9fffd9b68857992a3dfd91f19ff09e9e Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Thu, 20 Jun 2024 16:18:15 +0000 Subject: [PATCH 05/14] Reformatted code --- .../solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java | 4 ++-- 1 file changed, 2 insertions(+), 2 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 6e506f60e3..a338f437cf 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 @@ -71,8 +71,8 @@ protected void installSolver(final Path installDir, final String version) throws logger.write(Logger.Level.MAINSTEP, "Starting download (%s)...\n", getDownloadUrl(version).toString()); if (SemVer.of(version).compareTo(SemVer.of("1.1.1")) < 0) { try ( - final var inputChannel = Channels.newChannel(inputStream); - final var outputChannel = new FileOutputStream(installDir.resolve(getSolverBinaryName(version)).toAbsolutePath().toString()).getChannel() + final var inputChannel = Channels.newChannel(inputStream); + final var outputChannel = new FileOutputStream(installDir.resolve(getSolverBinaryName(version)).toAbsolutePath().toString()).getChannel() ) { outputChannel.transferFrom(inputChannel, 0, Long.MAX_VALUE); installDir.resolve(getSolverBinaryName(version)).toFile().setExecutable(true, true); From b253b5a987f6b3624d7fd3adbdd433a5c048eded Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 20 Jun 2024 14:10:35 +0200 Subject: [PATCH 06/14] Fixed Windows filename for cvc5 --- .../solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 e6f8978892..9b36e25867 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 @@ -48,7 +48,7 @@ public CVC5SmtLibSolverInstaller(final Logger logger) { versions.add(SemVer.VersionDecoder.create(SemVer.of("1.0.0")) .addString(LINUX, X64, "Linux") .addString(MAC, X64, "macOS") - .addString(WINDOWS, X64, "Win64") + .addString(WINDOWS, X64, "Win64.exe") .build() ); } From 90426038841a1772e57239971ef4085b5d1dd953 Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 20 Jun 2024 14:11:25 +0200 Subject: [PATCH 07/14] Add dummy assertion to formula A for interpolation in cvc5 --- .../solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java index 69fe6fb906..707a80735c 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java @@ -17,6 +17,7 @@ import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.decl.Decls; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.solver.*; @@ -44,6 +45,7 @@ import static com.google.common.base.Preconditions.*; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; public class CVC5SmtLibItpSolver extends SmtLibItpSolver { @@ -55,6 +57,8 @@ public CVC5SmtLibItpSolver(final SmtLibSymbolTable symbolTable, final Supplier itpSolverBinaryFactory) { super(symbolTable, transformationManager, termTransformer, solverBinary); this.itpSolverBinaryFactory = itpSolverBinaryFactory; + final var tmp = Decls.Const("shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh", Int()); +// symbolTable.put(tmp, "shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh", "(declare-fun shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh () Int)"); } @Override @@ -106,11 +110,15 @@ public Interpolant getInterpolant(ItpPattern pattern) { final var bTerm = B.stream() .flatMap(m -> m.getTerms().stream().map(Tuple2::get2)); + itpSolverBinary.issueCommand("(push)"); + itpSolverBinary.issueCommand("(declare-fun shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh () Int)"); + itpSolverBinary.issueCommand("(assert (= shevgcrjhsdfzgrjbms2dhrbcshdmrgcsh 0))"); itpSolverBinary.issueCommand( String.format("(assert (and %s))", aTerm.collect(Collectors.joining(" ")))); itpSolverBinary.issueCommand( String.format("(get-interpolant _cvc5_interpolant%d (not (and %s)))", interpolantCount++, bTerm.collect(Collectors.joining(" ")))); + itpSolverBinary.issueCommand("(pop)"); itpMap.put(marker, termTransformer.toExpr(parseItpResponse(itpSolverBinary.readResponse()), From bd09d19eb06f12e8028c1cf039448fd99c93ac57 Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 20 Jun 2024 16:59:52 +0200 Subject: [PATCH 08/14] Add support for cvc5 1.1.1 and 1.1.2 --- .../impl/cvc5/CVC5SmtLibSolverInstaller.java | 45 ++++++++++++++----- 1 file changed, 35 insertions(+), 10 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 9b36e25867..6e506f60e3 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 @@ -20,6 +20,7 @@ import hu.bme.mit.theta.solver.SolverFactory; import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstaller; import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstallerException; +import hu.bme.mit.theta.solver.smtlib.utils.Compress; import hu.bme.mit.theta.solver.smtlib.utils.SemVer; import java.io.FileOutputStream; @@ -45,6 +46,12 @@ public CVC5SmtLibSolverInstaller(final Logger logger) { super(logger); versions = new ArrayList<>(); + versions.add(SemVer.VersionDecoder.create(SemVer.of("1.1.1")) + .addString(LINUX, X64, "Linux-static.zip") + .addString(MAC, X64, "macOS-arm64-static.zip") + .addString(WINDOWS, X64, "Win64-static.zip") + .build() + ); versions.add(SemVer.VersionDecoder.create(SemVer.of("1.0.0")) .addString(LINUX, X64, "Linux") .addString(MAC, X64, "macOS") @@ -60,13 +67,21 @@ protected String getSolverName() { @Override protected void installSolver(final Path installDir, final String version) throws SmtLibSolverInstallerException { - try ( - final var inputChannel = Channels.newChannel(getDownloadUrl(version).openStream()); - final var outputChannel = new FileOutputStream(installDir.resolve(getSolverBinaryName(version)).toAbsolutePath().toString()).getChannel() - ) { + try (final var inputStream = getDownloadUrl(version).openStream()) { logger.write(Logger.Level.MAINSTEP, "Starting download (%s)...\n", getDownloadUrl(version).toString()); - outputChannel.transferFrom(inputChannel, 0, Long.MAX_VALUE); - installDir.resolve(getSolverBinaryName(version)).toFile().setExecutable(true, true); + if (SemVer.of(version).compareTo(SemVer.of("1.1.1")) < 0) { + try ( + final var inputChannel = Channels.newChannel(inputStream); + final var outputChannel = new FileOutputStream(installDir.resolve(getSolverBinaryName(version)).toAbsolutePath().toString()).getChannel() + ) { + outputChannel.transferFrom(inputChannel, 0, Long.MAX_VALUE); + installDir.resolve(getSolverBinaryName(version)).toFile().setExecutable(true, true); + } + } else { + Compress.extract(inputStream, installDir, Compress.CompressionType.ZIP); + installDir.resolve("bin").resolve(getSolverBinaryName(version)).toFile().setExecutable(true, true); + } + } catch (IOException e) { throw new SmtLibSolverInstallerException(e); } @@ -101,14 +116,19 @@ protected String[] getDefaultSolverArgs(String version) { @Override public SolverFactory getSolverFactory(final Path installDir, final String version, final Path solverPath, final String[] solverArgs) throws SmtLibSolverInstallerException { - final var solverFilePath = solverPath != null ? solverPath : installDir.resolve(getSolverBinaryName(version)); + final Path solverFilePath; + if (SemVer.of(version).compareTo(SemVer.of("1.1.1")) < 0) { + solverFilePath = solverPath != null ? solverPath : installDir.resolve(getSolverBinaryName(version)); + } else { + solverFilePath = solverPath != null ? solverPath : installDir.resolve("bin").resolve(getSolverBinaryName(version)); + } return CVC5SmtLibSolverFactory.create(solverFilePath, solverArgs); } @Override public List getSupportedVersions() { 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" + "1.1.2", "1.1.1", "1.1.0", "1.0.9", "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" ); } @@ -134,13 +154,18 @@ private String getArchString(final String version) throws SmtLibSolverInstallerE } } if (archStr == null) { - throw new SmtLibSolverInstallerException(String.format("MathSAT on operating system %s and architecture %s is not supported", OsHelper.getOs(), OsHelper.getArch())); + throw new SmtLibSolverInstallerException(String.format("CVC5 on operating system %s and architecture %s is not supported", OsHelper.getOs(), OsHelper.getArch())); } return archStr; } private String getSolverBinaryName(final String version) throws SmtLibSolverInstallerException { - return String.format("cvc5-%s", getArchString(version)); + if (SemVer.of(version).compareTo(SemVer.of("1.1.1")) < 0) { + return String.format("cvc5-%s", getArchString(version)); + } else { + return OsHelper.getOs() == WINDOWS ? "cvc5.exe" : "cvc5"; + } + } } From 1d8c8d5e0f853a0bad0b5e4027da483502b6da5e Mon Sep 17 00:00:00 2001 From: mondokm Date: Thu, 20 Jun 2024 18:08:21 +0200 Subject: [PATCH 09/14] Fixed a typo in an SMTInterpol url --- .../impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 1edfb39281..3fbdc13376 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 @@ -89,7 +89,7 @@ private URL getDownloadUrl(final String version) final String fileName; switch (version) { case "2.5-1256": - fileName = "2.5-1230-g55d6ba76"; + fileName = "2.5-1256-g55d6ba76"; break; case "2.5-1230": fileName = "2.5-1230-g3eafb46a"; From a6893681e24379d98cd232054eb9392f206a9a09 Mon Sep 17 00:00:00 2001 From: "ThetaBotMaintainer[bot]" <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> Date: Thu, 20 Jun 2024 16:18:15 +0000 Subject: [PATCH 10/14] Reformatted code --- .../solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java | 4 ++-- 1 file changed, 2 insertions(+), 2 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 6e506f60e3..a338f437cf 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 @@ -71,8 +71,8 @@ protected void installSolver(final Path installDir, final String version) throws logger.write(Logger.Level.MAINSTEP, "Starting download (%s)...\n", getDownloadUrl(version).toString()); if (SemVer.of(version).compareTo(SemVer.of("1.1.1")) < 0) { try ( - final var inputChannel = Channels.newChannel(inputStream); - final var outputChannel = new FileOutputStream(installDir.resolve(getSolverBinaryName(version)).toAbsolutePath().toString()).getChannel() + final var inputChannel = Channels.newChannel(inputStream); + final var outputChannel = new FileOutputStream(installDir.resolve(getSolverBinaryName(version)).toAbsolutePath().toString()).getChannel() ) { outputChannel.transferFrom(inputChannel, 0, Long.MAX_VALUE); installDir.resolve(getSolverBinaryName(version)).toFile().setExecutable(true, true); From 533a5406609b00521837294e256b943094ba358a Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 24 Jun 2024 12:21:00 +0200 Subject: [PATCH 11/14] Add new z3 versions --- .../mit/theta/solver/smtlib/impl/z3/Z3SmtLibSolverInstaller.java | 1 + 1 file changed, 1 insertion(+) 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 cd291f31e5..e8abed63aa 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 @@ -192,6 +192,7 @@ public SolverFactory getSolverFactory(final Path installDir, final String versio @Override public List getSupportedVersions() { return Arrays.asList( + "4.13.0", "4.12.6", "4.12.5", "4.12.4", "4.12.3", "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", From a0d73559144a057304d0b03c80284768b4ffb6ea Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 24 Jun 2024 12:24:17 +0200 Subject: [PATCH 12/14] Add new princess version --- .../smtlib/impl/princess/PrincessSmtLibSolverInstaller.java | 1 + 1 file changed, 1 insertion(+) 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 8d9b86a3f0..ce95aa9ff6 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,6 +90,7 @@ public SolverFactory getSolverFactory(final Path installDir, final String versio @Override public List getSupportedVersions() { return Arrays.asList( + "2024-01-12", "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" From d9560726976f9e592ad283a45e17136562c8678d Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 24 Jun 2024 14:59:28 +0200 Subject: [PATCH 13/14] Fix princess interpolation issue --- .../impl/princess/PrincessSmtLibItpSolver.java | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibItpSolver.java b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibItpSolver.java index 9b0fa954e2..8ab0bc7590 100644 --- a/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibItpSolver.java +++ b/subprojects/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibItpSolver.java @@ -41,13 +41,7 @@ import org.antlr.v4.runtime.ParserRuleContext; import org.antlr.v4.runtime.misc.Interval; -import java.util.ArrayList; -import java.util.Collections; -import java.util.HashMap; -import java.util.LinkedList; -import java.util.List; -import java.util.Map; -import java.util.Set; +import java.util.*; import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkArgument; @@ -57,8 +51,8 @@ public final class PrincessSmtLibItpSolver extends SmtLibItpSolver { - private final Map, String> assertionNames = new HashMap<>(); - private static final String assertionNamePattern = "_smtinterpol_assertion_%d"; + private final Map, String> assertionNames = new IdentityHashMap<>(); + private static final String assertionNamePattern = "_princess_assertion_%d"; private static long assertionCount = 0; public PrincessSmtLibItpSolver( From b5b2792c52d942b5247c5afea0939d40b361e29f Mon Sep 17 00:00:00 2001 From: mondokm Date: Mon, 24 Jun 2024 15:15:05 +0200 Subject: [PATCH 14/14] Bump version --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index d9240fe242..da4081e007 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -28,7 +28,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "5.2.0" + version = "5.2.1" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) }