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")) } 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()), 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..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 @@ -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,10 +46,16 @@ 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") - .addString(WINDOWS, X64, "Win64") + .addString(WINDOWS, X64, "Win64.exe") .build() ); } @@ -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"; + } + } } 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( 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" 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"; 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",