12 files changed, 463 insertions, 0 deletions

diff --git a/z3/subprojects/solver-darwin-aarch64/build.gradle.kts b/z3/subprojects/solver-darwin-aarch64/build.gradle.kts
new file mode 100644
index 00000000..21c9739c
--- /dev/null
+++ b/z3/subprojects/solver-darwin-aarch64/build.gradle.kts
@@ -0,0 +1,36 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-arm64-osx-11.0"
+val library = "z3java-darwin-aarch64"
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+}
+
+val extractZ3Libs by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                zipTree(zipFile).matching {
+                        include("${classifier}/bin/*.so")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(2).toTypedArray()
+                relativePath = RelativePath(true, library, *pathInBin)
+        }
+        into(layout.buildDirectory.dir("z3-extracted"))
+}
+
+sourceSets.main {
+        resources.srcDir(extractZ3Libs)
+}
diff --git a/z3/subprojects/solver-darwin-x86-64/build.gradle.kts b/z3/subprojects/solver-darwin-x86-64/build.gradle.kts
new file mode 100644
index 00000000..75e59267
--- /dev/null
+++ b/z3/subprojects/solver-darwin-x86-64/build.gradle.kts
@@ -0,0 +1,36 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-x64-osx-10.16"
+val library = "z3java-darwin-x86-64"
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+}
+
+val extractZ3Libs by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                zipTree(zipFile).matching {
+                        include("${classifier}/bin/*.so")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(2).toTypedArray()
+                relativePath = RelativePath(true, library, *pathInBin)
+        }
+        into(layout.buildDirectory.dir("z3-extracted"))
+}
+
+sourceSets.main {
+        resources.srcDir(extractZ3Libs)
+}
diff --git a/z3/subprojects/solver-linux-aarch64/build.gradle.kts b/z3/subprojects/solver-linux-aarch64/build.gradle.kts
new file mode 100644
index 00000000..a8e7e259
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/build.gradle.kts
@@ -0,0 +1,14 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+tasks.jar {
+        // License information is redundant here, since it already gets added to the POM.
+        exclude("**/*.license")
+}
diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so
new file mode 100755
index 00000000..574ee3ab
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so
diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license
new file mode 100644
index 00000000..0993dbf7
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3.so.license
@@ -0,0 +1,6 @@
+Copyright (c) Microsoft Corporations
+
+SPDX-License-Identifier: MIT
+
+This file was created from the Z3 4.12.6 release sources using the
+z3/docker/cross_build.sh script in this repository.
diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so
new file mode 100755
index 00000000..aace2c30
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so
diff --git a/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license
new file mode 100644
index 00000000..0993dbf7
--- /dev/null
+++ b/z3/subprojects/solver-linux-aarch64/src/main/resources/z3java-linux-aarch64/libz3java.so.license
@@ -0,0 +1,6 @@
+Copyright (c) Microsoft Corporations
+
+SPDX-License-Identifier: MIT
+
+This file was created from the Z3 4.12.6 release sources using the
+z3/docker/cross_build.sh script in this repository.
diff --git a/z3/subprojects/solver-linux-x86-64/build.gradle.kts b/z3/subprojects/solver-linux-x86-64/build.gradle.kts
new file mode 100644
index 00000000..89c737b6
--- /dev/null
+++ b/z3/subprojects/solver-linux-x86-64/build.gradle.kts
@@ -0,0 +1,36 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-x64-glibc-2.31"
+val library = "z3java-linux-x86-64"
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+}
+
+val extractZ3Libs by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                zipTree(zipFile).matching {
+                        include("${classifier}/bin/*.so")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(2).toTypedArray()
+                relativePath = RelativePath(true, library, *pathInBin)
+        }
+        into(layout.buildDirectory.dir("z3-extracted"))
+}
+
+sourceSets.main {
+        resources.srcDir(extractZ3Libs)
+}
diff --git a/z3/subprojects/solver-win32-x86-64/build.gradle.kts b/z3/subprojects/solver-win32-x86-64/build.gradle.kts
new file mode 100644
index 00000000..c5fa0421
--- /dev/null
+++ b/z3/subprojects/solver-win32-x86-64/build.gradle.kts
@@ -0,0 +1,38 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-x64-win"
+val library = "z3java-win32-x86-64"
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+}
+
+val extractZ3Libs by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                zipTree(zipFile).matching {
+                        include("${classifier}/bin/*.dll")
+                        // Do not include .NET assembly.
+                        exclude("${classifier}/bin/Microsoft.Z3.dll")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(2).toTypedArray()
+                relativePath = RelativePath(true, library, *pathInBin)
+        }
+        into(layout.buildDirectory.dir("z3-extracted"))
+}
+
+sourceSets.main {
+        resources.srcDir(extractZ3Libs)
+}
diff --git a/z3/subprojects/solver/build.gradle.kts b/z3/subprojects/solver/build.gradle.kts
new file mode 100644
index 00000000..7e898b3e
--- /dev/null
+++ b/z3/subprojects/solver/build.gradle.kts
@@ -0,0 +1,107 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+import tools.refinery.z3.gradle.ClassFilePatcher
+
+plugins {
+        id("tools.refinery.z3.gradle.java-library")
+}
+
+val classifier = "z3-${version}-x64-glibc-2.31"
+val extractedClassesDir = layout.buildDirectory.dir("z3-extracted")
+val extractedSourcesDir = layout.buildDirectory.dir("z3-sources")
+
+java {
+        withJavadocJar()
+        withSourcesJar()
+}
+
+val z3Source: Configuration by configurations.creating {
+        isCanBeConsumed = false
+        isCanBeResolved = true
+}
+
+val extractZ3Jar by tasks.registering(Sync::class) {
+        dependsOn(configurations.z3)
+        from({
+                val zipFile = configurations.z3.map { it.singleFile }
+                val jarFile = zipTree(zipFile).matching {
+                        include("${classifier}/bin/com.microsoft.z3.jar")
+                }.singleFile
+                zipTree(jarFile).matching {
+                        exclude("META-INF/MANIFEST.MF")
+                        includeEmptyDirs = false
+                }
+        })
+        into(extractedClassesDir)
+        doLast {
+                // The class initializer off {@see com.microsoft.z3.Native} will try to load the Z3 native libraries
+                // from the system default library path unless the {@code z3.skipLibraryLoad} system property is set.
+                // Since we don't control the library path or system properties, we remove the class initializer entirely.
+                val nativeClassFile = extractedClassesDir.get().file("com/microsoft/z3/Native.class").asFile
+                ClassFilePatcher.removeClassInitializer(nativeClassFile)
+        }
+}
+
+val extractZ3Source by tasks.registering(Sync::class) {
+        dependsOn(z3Source)
+        from({
+                val zipFile = z3Source.singleFile
+                zipTree(zipFile).matching {
+                        include("z3-z3-${version}/src/api/java/**/*")
+                        includeEmptyDirs = false
+                }
+        })
+        eachFile {
+                val pathInBin = relativePath.segments.drop(4).toTypedArray()
+                relativePath = RelativePath(true, "com", "microsoft", "z3", *pathInBin)
+        }
+        into(extractedSourcesDir)
+}
+
+tasks.jar {
+        // Add class files to our jar manually.
+        from(extractZ3Jar)
+}
+
+tasks.test {
+        useJUnitPlatform()
+}
+
+tasks.named<Jar>("sourcesJar") {
+        from(extractZ3Source)
+}
+
+tasks.named<Javadoc>("javadoc") {
+        source(sourceSets.main.map { it.allJava })
+        source(fileTree(extractedSourcesDir) {
+                builtBy(extractZ3Source)
+                include("**/*.java")
+        })
+        options {
+                this as StandardJavadocDocletOptions
+                addBooleanOption("Xdoclint:none", true)
+                // {@code -Xmaxwarns 0} will print all warnings, so we must keep at least one.
+                addStringOption("Xmaxwarns", "1")
+                quiet()
+        }
+}
+
+dependencies {
+        z3("Z3Prover:z3:${version}:${classifier}@zip")
+        z3Source("Z3Prover:z3:${version}@zip")
+        // This dependency doesn't get added to Maven metadata, so we have to add the class files to our jar manually.
+        api(files(extractZ3Jar))
+        implementation(libs.jna)
+        implementation(project(":refinery-z3-solver-darwin-aarch64"))
+        implementation(project(":refinery-z3-solver-darwin-x86-64"))
+        implementation(project(":refinery-z3-solver-linux-aarch64"))
+        implementation(project(":refinery-z3-solver-linux-x86-64"))
+        implementation(project(":refinery-z3-solver-win32-x86-64"))
+        testImplementation(libs.junit.api)
+        testRuntimeOnly(libs.junit.engine)
+        testRuntimeOnly("org.junit.platform:junit-platform-launcher")
+}
diff --git a/z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java b/z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java
new file mode 100644
index 00000000..84f99540
--- /dev/null
+++ b/z3/subprojects/solver/src/main/java/tools/refinery/z3/Z3SolverLoader.java
@@ -0,0 +1,154 @@
+/*
+ * Copyright 2010-2022 Google LLC
+ * Copyright 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ *
+ * This file is based on
+ * https://github.com/google/or-tools/blob/f3d1d5f6a67356ec38a7fd2ab607624eea8ad3a6/ortools/java/com/google/ortools/Loader.java
+ * We adapted the loader logic to extract the JNI libraries of Z3 and the corresponding dependencies instead of the
+ * Google OR-Tools JNI libraries.
+ */
+package tools.refinery.z3;
+
+import com.sun.jna.Platform;
+
+import java.io.IOException;
+import java.net.URI;
+import java.net.URISyntaxException;
+import java.nio.file.*;
+import java.nio.file.attribute.BasicFileAttributes;
+import java.util.Map;
+
+public final class Z3SolverLoader {
+        private static final String JNI_LIBRARY_NAME = "z3java";
+        private static final String SOLVER_LIBRARY_NAME = "z3";
+
+        private static boolean loaded;
+
+        private Z3SolverLoader() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static synchronized void loadNativeLibraries() {
+                if (loaded) {
+                        return;
+                }
+                try {
+                        System.loadLibrary(getOsSpecificLibraryName(JNI_LIBRARY_NAME));
+                        loaded = true;
+                        return;
+                } catch (UnsatisfiedLinkError e) {
+                        // Continue, we'll have to extract the libraries from the classpath.
+                }
+                try {
+                        extractAndLoad();
+                        loaded = true;
+                } catch (IOException e) {
+                        throw new IllegalStateException("Could not extract and load " + JNI_LIBRARY_NAME, e);
+                }
+        }
+
+        private static void extractAndLoad() throws IOException {
+                var resourceName = JNI_LIBRARY_NAME + "-" + Platform.RESOURCE_PREFIX;
+                var resource = Z3SolverLoader.class.getClassLoader().getResource(resourceName);
+                if (resource == null) {
+                        throw new IllegalStateException("Resource %s was not found".formatted(resourceName));
+                }
+                URI resourceUri;
+                try {
+                        resourceUri = resource.toURI();
+                } catch (URISyntaxException e) {
+                        throw new IllegalStateException("Invalid resource URI: " + resource);
+                }
+                FileSystem fileSystem = null;
+                boolean newFileSystem = false;
+                Path extractedPath;
+                try {
+                        try {
+                                fileSystem = FileSystems.newFileSystem(resourceUri, Map.of());
+                                newFileSystem = true;
+                        } catch (FileSystemAlreadyExistsException e) {
+                                fileSystem = FileSystems.getFileSystem(resourceUri);
+                        }
+                        var resourcePath = fileSystem.provider().getPath(resourceUri);
+                        if (fileSystem.equals(FileSystems.getDefault())) {
+                                extractedPath = resourcePath;
+                        } else {
+                                extractedPath = extract(resourcePath);
+                        }
+                } finally {
+                        if (newFileSystem) {
+                                fileSystem.close();
+                        }
+                }
+                // We can't rely on RPATH, so we load libraries in reverse dependency order manually.
+                try {
+                        loadFromPath(extractedPath, SOLVER_LIBRARY_NAME);
+                } catch (UnsatisfiedLinkError e) {
+                        if (Platform.isWindows()) {
+                                // Try again with our packaged msvcp140 if the system one is missing.
+                                loadFromPathExactName(extractedPath, "vcruntime140.dll");
+                                loadFromPathExactName(extractedPath, "vcruntime140_1.dll");
+                                loadFromPathExactName(extractedPath, "msvcp140.dll");
+                                loadFromPath(extractedPath, SOLVER_LIBRARY_NAME);
+                        } else {
+                                throw e;
+                        }
+                }
+                loadFromPath(extractedPath, JNI_LIBRARY_NAME);
+        }
+
+        private static Path extract(Path resourcePath) throws IOException {
+                var tempDir = Files.createTempDirectory(JNI_LIBRARY_NAME).toAbsolutePath();
+                tempDir.toFile().deleteOnExit();
+                Files.walkFileTree(resourcePath, new SimpleFileVisitor<>() {
+                        @Override
+                        public FileVisitResult preVisitDirectory(Path dir, BasicFileAttributes attrs) throws IOException {
+                                var result = super.preVisitDirectory(dir, attrs);
+                                var targetPath = getTargetPath(dir, resourcePath, tempDir);
+                                if (!Files.exists(targetPath)) {
+                                        Files.createDirectory(targetPath);
+                                        targetPath.toFile().deleteOnExit();
+                                }
+                                return result;
+                        }
+
+                        @Override
+                        public FileVisitResult visitFile(Path file, BasicFileAttributes attrs) throws IOException {
+                                var result = super.visitFile(file, attrs);
+                                var targetPath = getTargetPath(file, resourcePath, tempDir);
+                                Files.copy(file, targetPath);
+                                targetPath.toFile().deleteOnExit();
+                                return result;
+                        }
+                });
+                return tempDir;
+        }
+
+        private static Path getTargetPath(Path sourcePath, Path resourcePath, Path tempDir) {
+                var targetPath = tempDir.resolve(resourcePath.relativize(sourcePath).toString()).normalize();
+                if (!targetPath.startsWith(tempDir)) {
+                        throw new IllegalStateException("Target path '%s' for '%s' is outside '%s'"
+                                        .formatted(targetPath, sourcePath, tempDir));
+                }
+                return targetPath;
+        }
+
+        private static String getOsSpecificLibraryName(String libraryName) {
+                var osSpecificLibraryNamePrefix = Platform.isWindows() ? "lib" : "";
+                return osSpecificLibraryNamePrefix + libraryName;
+        }
+
+        private static void loadFromPath(Path extractedPath, String libraryName) {
+                var osSpecificLibraryName = getOsSpecificLibraryName(libraryName);
+                loadFromPathExactName(extractedPath, System.mapLibraryName(osSpecificLibraryName));
+        }
+
+        private static void loadFromPathExactName(Path extractedPath, String exactName) {
+                var library = extractedPath.resolve(exactName)
+                                .toAbsolutePath()
+                                .toString();
+                System.load(library);
+        }
+}
diff --git a/z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java b/z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java
new file mode 100644
index 00000000..df3139cc
--- /dev/null
+++ b/z3/subprojects/solver/src/test/java/tools/refinery/z3/Z3SolverLoaderTest.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+package tools.refinery.z3;
+
+import com.microsoft.z3.*;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertDoesNotThrow;
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+class Z3SolverLoaderTest {
+        @Test
+        void testLoad() {
+                assertDoesNotThrow(Z3SolverLoader::loadNativeLibraries);
+                try (var context = new Context()) {
+                        var solver = context.mkSolver();
+                        var a = context.mkConst("a", context.getIntSort());
+                        var b = context.mkConst("b", context.getIntSort());
+                        solver.add(context.mkEq(a, context.mkInt(3)));
+                        solver.add(context.mkEq(b, context.mkMul(context.mkInt(2), a)));
+                        assertEquals(Status.SATISFIABLE, solver.check());
+                        var model = solver.getModel();
+                        var bValue = (IntNum) model.getConstInterp(b);
+                        assertEquals(6, bValue.getInt());
+                }
+        }
+}