Upgrade Z3 to 4.13.0 && support Z3 on linux/arm

UnitTestBot · Jul 1, 2024 · 3b4f6a2 · 3b4f6a2
1 parent af4a529
commit 3b4f6a2
Show file tree

Hide file tree

Showing 7 changed files with 54 additions and 15 deletions.
diff --git a/buildSrc/src/main/kotlin/Publications.kt b/buildSrc/src/main/kotlin/Publications.kt
@@ -73,18 +73,21 @@ fun MavenPublication.addEmptyArtifact(project: Project): Unit = with(project) {
     artifact(generateEmptyJar("javadoc"))
 }
 
-fun MavenPublication.addMavenDependencies(dependencies: DependencySet) {
+fun MavenPublication.addMavenDependencies(
+    dependencies: DependencySet,
+    dependencyFilter: (MavenPublication) -> Boolean = { true }
+) {
     pom.withXml {
         val dependenciesNode: Node = asNode().appendNode("dependencies")
         dependencies.forEach {
-            addDependencyPublications(dependenciesNode, it)
+            addDependencyPublications(dependenciesNode, it, dependencyFilter)
         }
     }
 }
 
-private fun addDependencyPublications(node: Node, dependency: Dependency) {
+private fun addDependencyPublications(node: Node, dependency: Dependency, dependencyFilter: (MavenPublication) -> Boolean) {
     val project = (dependency as? ProjectDependency)?.dependencyProject ?: return
-    project.publishing.publications.filterIsInstance<MavenPublication>().forEach {
+    project.publishing.publications.filterIsInstance<MavenPublication>().filter(dependencyFilter).forEach {
         val dependencyNode = node.appendNode("dependency")
         addMavenPublicationDependency(dependencyNode, it)
     }

diff --git a/buildSrc/src/main/kotlin/Z3ReleaseDownloadUtil.kt b/buildSrc/src/main/kotlin/Z3ReleaseDownloadUtil.kt
@@ -1,20 +1,24 @@
 import org.gradle.api.Project
 import org.gradle.api.Task
+import org.gradle.api.file.DuplicatesStrategy
 import org.gradle.api.tasks.TaskProvider
 
-fun Project.mkZ3ReleaseDownloadTask(z3Version: String, arch: String, artifactPattern: String): TaskProvider<Task> {
+fun Project.mkZ3ReleaseDownloadTask(z3Version: String, arch: String, requiredFiles: List<String>): TaskProvider<Task> {
     val z3ReleaseBaseUrl = "https://github.com/Z3Prover/z3/releases/download"
     val releaseName = "z3-${z3Version}"
     val packageName = "z3-${z3Version}-${arch}.zip"
     val packageDownloadTarget = buildDir.resolve("dist").resolve(releaseName).resolve(packageName)
     val downloadUrl = listOf(z3ReleaseBaseUrl, releaseName, packageName).joinToString("/")
-    val downloadTaskName = "z3-release-$releaseName-$arch-${artifactPattern.replace('*', '-')}"
+    val downloadTaskName = "z3-release-$releaseName-$arch"
     return tasks.register(downloadTaskName) {
         val outputDir = buildDir.resolve("dist").resolve(downloadTaskName)
         doLast {
             download(downloadUrl, packageDownloadTarget)
-            val files = zipTree(packageDownloadTarget).matching { include("**/$artifactPattern") }
+            val files = zipTree(packageDownloadTarget).matching {
+                include(requiredFiles)
+            }
             copy {
+                duplicatesStrategy = DuplicatesStrategy.EXCLUDE
                 from(files.files)
                 into(outputDir)
             }

diff --git a/ksmt-z3/build.gradle.kts b/ksmt-z3/build.gradle.kts
@@ -14,7 +14,12 @@ dependencies {
 publishing.publications {
     register<MavenPublication>("maven") {
         addKsmtPom()
-        addMavenDependencies(configurations.default.get().allDependencies)
+
+        addMavenDependencies(configurations.default.get().allDependencies) { dependency ->
+            // exclude linux arm from default ksmt-z3 configuration
+            dependency.artifactId.let { !it.endsWith("linux-arm") }
+        }
+
         addEmptyArtifact(project)
         signKsmtPublication(project)
     }

diff --git a/ksmt-z3/dist/z3-native-linux-x86-64-4.12.5.zip b/ksmt-z3/dist/z3-native-linux-x86-64-4.12.5.zip
diff --git a/ksmt-z3/ksmt-z3-core/build.gradle.kts b/ksmt-z3/ksmt-z3-core/build.gradle.kts
@@ -9,9 +9,9 @@ repositories {
     mavenCentral()
 }
 
-val z3Version = "4.12.5"
+val z3Version = "4.13.0"
 
-val z3JavaJar by lazy { mkZ3ReleaseDownloadTask(z3Version, "x64-win", "*.jar") }
+val z3JavaJar by lazy { mkZ3ReleaseDownloadTask(z3Version, "x64-win", listOf("**/com.microsoft.z3.jar")) }
 
 dependencies {
     implementation(project(":ksmt-core"))

diff --git a/ksmt-z3/ksmt-z3-native/build.gradle.kts b/ksmt-z3/ksmt-z3-native/build.gradle.kts
@@ -16,14 +16,21 @@ val `windows-x64` by sourceSets.creating
 val `linux-x64` by sourceSets.creating
 val `mac-x64` by sourceSets.creating
 val `mac-arm` by sourceSets.creating
+val `windows-arm` by sourceSets.creating
+val `linux-arm` by sourceSets.creating
 
-val z3Version = "4.12.5"
+val z3Version = "4.13.0"
+
+val winDllPath = listOf("**/vcruntime140.dll", "**/vcruntime140_1.dll", "**/libz3.dll", "**/libz3java.dll")
+val linuxSoPath = listOf("**/libz3.so", "**/libz3java.so")
+val macDylibPath = listOf("**/libz3.dylib", "**/libz3java.dylib")
 
 val z3Binaries = listOf(
-    Triple(`windows-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-win", "*.dll"), null),
-    Triple(`linux-x64`, null, z3NativeLinuxX64),
-    Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-11.7.10", "*.dylib"), null),
-    Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-11.0", "*.dylib"), null),
+    Triple(`windows-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-win", winDllPath), null),
+    Triple(`linux-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-glibc-2.31", linuxSoPath), null),
+    Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-11.7.10", macDylibPath), null),
+    Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-11.0", macDylibPath), null),
+    Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.35", linuxSoPath), null),
 )
 
 z3Binaries.forEach { it.first.compileClasspath = compileConfig }

diff --git a/...3/ksmt-z3-native/src/linux-arm/kotlin/io/ksmt/solver/z3/KZ3NativeLibraryLoaderLinuxArm.kt b/...3/ksmt-z3-native/src/linux-arm/kotlin/io/ksmt/solver/z3/KZ3NativeLibraryLoaderLinuxArm.kt
@@ -0,0 +1,20 @@
+package io.ksmt.solver.z3
+
+import io.ksmt.utils.library.NativeLibraryLoaderArm
+import io.ksmt.utils.library.NativeLibraryLoaderLinux
+import io.ksmt.utils.library.NativeLibraryLoaderUtils
+
+@Suppress("unused")
+class KZ3NativeLibraryLoaderLinuxArm :
+    KZ3NativeLibraryLoader,
+    NativeLibraryLoaderLinux,
+    NativeLibraryLoaderArm {
+
+    override fun load() {
+        NativeLibraryLoaderUtils.loadLibrariesFromResources(this, libraries)
+    }
+
+    companion object {
+        private val libraries = listOf("libz3", "libz3java")
+    }
+}