Upgrade Z3 version to 4.12.2 (#132)

* Update z3 version to 4.12.2 * Custom z3 linux distribution * Update version to 0.5.9 * Add new Z3 kinds
UnitTestBot · Oct 14, 2023 · 3efd7a0 · 3efd7a0
1 parent 3c4efa7
commit 3efd7a0
Show file tree

Hide file tree

Showing 8 changed files with 61 additions and 31 deletions.
diff --git a/README.md b/README.md
@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.8)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.9)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.8")
+implementation("io.ksmt:ksmt-core:0.5.9")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.8")
+implementation("io.ksmt:ksmt-z3:0.5.9")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 

diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.8"
+version = "0.5.9"
 
 repositories {
     mavenCentral()

diff --git a/docs/getting-started.md b/docs/getting-started.md
@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.8")    
+    implementation("io.ksmt:ksmt-core:0.5.9")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.8")
+    implementation("io.ksmt:ksmt-z3:0.5.9")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.8")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.9")
 }
 ```
 

diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.8")
+    implementation("io.ksmt:ksmt-core:0.5.9")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.8")
+    implementation("io.ksmt:ksmt-z3:0.5.9")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.8")
+    implementation("io.ksmt:ksmt-runner:0.5.9")
 }
 
 java {

diff --git a/ksmt-z3/dist/z3-native-linux-x86-64-4.12.2.zip b/ksmt-z3/dist/z3-native-linux-x86-64-4.12.2.zip
diff --git a/ksmt-z3/ksmt-z3-core/build.gradle.kts b/ksmt-z3/ksmt-z3-core/build.gradle.kts
@@ -9,7 +9,7 @@ repositories {
     mavenCentral()
 }
 
-val z3Version = "4.11.2"
+val z3Version = "4.12.2"
 
 val z3JavaJar by lazy { mkZ3ReleaseDownloadTask(z3Version, "x64-win", "*.jar") }
 

diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt
@@ -23,6 +23,7 @@ import io.ksmt.expr.KIntNumExpr
 import io.ksmt.expr.KInterpretedValue
 import io.ksmt.expr.KRealNumExpr
 import io.ksmt.expr.rewrite.KExprUninterpretedDeclCollector
+import io.ksmt.solver.KSolverUnsupportedFeatureException
 import io.ksmt.solver.util.ExprConversionResult
 import io.ksmt.solver.util.KExprConverterUtils.argumentsConversionRequired
 import io.ksmt.solver.util.KExprLongConverterBase
@@ -200,6 +201,7 @@ open class KZ3ExprConverter(
             Z3_decl_kind.Z3_OP_XOR -> expr.convert(::mkXor)
             Z3_decl_kind.Z3_OP_NOT -> expr.convert(::mkNot)
             Z3_decl_kind.Z3_OP_IMPLIES -> expr.convert(::mkImplies)
+            Z3_decl_kind.Z3_OP_IFF,
             Z3_decl_kind.Z3_OP_EQ -> expr.convert(::mkEq)
             Z3_decl_kind.Z3_OP_DISTINCT -> expr.convertList(::mkDistinct)
             Z3_decl_kind.Z3_OP_ITE -> expr.convert(::mkIte)
@@ -220,6 +222,12 @@ open class KZ3ExprConverter(
             Z3_decl_kind.Z3_OP_TO_REAL -> expr.convert(::mkIntToReal)
             Z3_decl_kind.Z3_OP_TO_INT -> expr.convert(::mkRealToInt)
             Z3_decl_kind.Z3_OP_IS_INT -> expr.convert(::mkRealIsInt)
+            Z3_decl_kind.Z3_OP_ANUM -> {
+                error("Unexpected algebraic numeral in app converter")
+            }
+            Z3_decl_kind.Z3_OP_AGNUM -> {
+                throw KSolverUnsupportedFeatureException("Irrational algebraic numbers are not supported")
+            }
             Z3_decl_kind.Z3_OP_STORE -> convertArrayStore(expr)
             Z3_decl_kind.Z3_OP_SELECT -> convertArraySelect(expr)
             Z3_decl_kind.Z3_OP_CONST_ARRAY -> expr.convert { arg: KExpr<KSort> ->
@@ -399,9 +407,18 @@ open class KZ3ExprConverter(
                 }
             Z3_decl_kind.Z3_OP_FPA_BVWRAP,
             Z3_decl_kind.Z3_OP_FPA_BV2RM -> {
-                TODO("Fp $declKind is not supported")
+                throw KSolverUnsupportedFeatureException("Fp $declKind is not supported")
+            }
+
+           Z3_decl_kind.Z3_OP_INTERNAL -> {
+                throw KSolverUnsupportedFeatureException("Z3 internal decl $declKind is not supported")
             }
-            else -> TODO("$declKind is not supported")
+
+            Z3_decl_kind.Z3_OP_RECURSIVE -> {
+                throw KSolverUnsupportedFeatureException("Recursive decl $declKind is not supported")
+            }
+
+            else -> throw KSolverUnsupportedFeatureException("$declKind is not supported")
         }
     }
 

diff --git a/ksmt-z3/ksmt-z3-native/build.gradle.kts b/ksmt-z3/ksmt-z3-native/build.gradle.kts
@@ -2,43 +2,53 @@ plugins {
     id("io.ksmt.ksmt-base")
 }
 
+val distDir = projectDir.parentFile.resolve("dist")
+
 repositories {
     mavenCentral()
+    flatDir { dirs(distDir) }
 }
 
 val compileConfig by configurations.creating
+val z3NativeLinuxX64 by configurations.creating
 
 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 z3Version = "4.11.2"
+val z3Version = "4.12.2"
 
-val z3Binaries = mapOf(
-    `windows-x64` to mkZ3ReleaseDownloadTask(z3Version, "x64-win", "*.dll"),
-    `linux-x64` to mkZ3ReleaseDownloadTask(z3Version, "x64-glibc-2.31", "*.so"),
-    `mac-x64` to mkZ3ReleaseDownloadTask(z3Version, "x64-osx-10.16", "*.dylib"),
-    `mac-arm` to mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-11.0", "*.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-10.16", "*.dylib"), null),
+    Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-11.0", "*.dylib"), null),
 )
 
-z3Binaries.keys.forEach { it.compileClasspath = compileConfig }
+z3Binaries.forEach { it.first.compileClasspath = compileConfig }
 
 dependencies {
     compileConfig(project(":ksmt-core"))
     compileConfig(project(":ksmt-z3:ksmt-z3-core"))
+
+    z3NativeLinuxX64("z3", "z3-native-linux-x86-64", z3Version, ext = "zip")
 }
 
-z3Binaries.entries.forEach { (sourceSet, z3BinaryTask) ->
+z3Binaries.forEach { (sourceSet, z3BinaryTask, nativeConfig) ->
     val name = sourceSet.name
     val systemArch = name.replace('-', '/')
 
     val jarTask = tasks.register<Jar>("$name-jar") {
-        dependsOn(z3BinaryTask)
-
         from(sourceSet.output)
-        from(z3BinaryTask.outputFiles) {
-            into("lib/$systemArch/z3")
+
+        z3BinaryTask?.let {
+            dependsOn(it)
+            from(it.outputFiles) { into("lib/$systemArch/z3") }
+        }
+
+        nativeConfig?.let {
+            copyArtifactsIntoJar(it, this, "lib/$systemArch/z3")
         }
     }
 
@@ -62,13 +72,16 @@ z3Binaries.entries.forEach { (sourceSet, z3BinaryTask) ->
 }
 
 tasks.getByName<Jar>("jar") {
-    dependsOn.addAll(z3Binaries.values)
-
-    z3Binaries.forEach { (sourceSet, z3BinaryTask) ->
+    z3Binaries.forEach { (sourceSet, z3BinaryTask, nativeConfig) ->
         from(sourceSet.output)
-        from(z3BinaryTask.outputFiles) {
-            val systemArch = sourceSet.name.replace('-', '/')
-            into("lib/$systemArch/z3")
+
+        val systemArch = sourceSet.name.replace('-', '/')
+        z3BinaryTask?.let {
+            dependsOn(it)
+            from(it.outputFiles) { into("lib/$systemArch/z3") }
+        }
+        nativeConfig?.let {
+            copyArtifactsIntoJar(it, this, "lib/$systemArch/z3")
         }
     }
 }