Merge pull request #271 from ftsrg/smtlib-fixes

SMTLIB integration fixes
ftsrg · Jun 25, 2024 · 928c853 · 928c853
2 parents c4e24fa + b5b2792
commit 928c853
Show file tree

Hide file tree

Showing 7 changed files with 51 additions and 22 deletions.
diff --git 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/...er-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java b/...er-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<CVC5SmtLibItpMarker> {
 
@@ -55,6 +57,8 @@ public CVC5SmtLibItpSolver(final SmtLibSymbolTable symbolTable,
                                final Supplier<? extends SmtLibSolverBinary> 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/...lib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibSolverInstaller.java b/...lib/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<String> 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/...b/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibItpSolver.java b/...b/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<PrincessSmtLibItpMarker> {
 
-    private final Map<Expr<BoolType>, String> assertionNames = new HashMap<>();
-    private static final String assertionNamePattern = "_smtinterpol_assertion_%d";
+    private final Map<Expr<BoolType>, String> assertionNames = new IdentityHashMap<>();
+    private static final String assertionNamePattern = "_princess_assertion_%d";
     private static long assertionCount = 0;
 
     public PrincessSmtLibItpSolver(

diff --git a/...main/java/hu/bme/mit/theta/solver/smtlib/impl/princess/PrincessSmtLibSolverInstaller.java b/...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<String> 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/...ava/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java b/...ava/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/...-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/z3/Z3SmtLibSolverInstaller.java b/...-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<String> 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",