Various fixes (#57)

* update windows binary * Fix bitwuzla Fp on windows * Handle empty test data * remove unsupported test cases * Fix test infrastructure * Fix function-as-array evaluation * Uninterpreted sort universe * Staged ITE simplifier * Uninterpreted sort values evaluation * Fix quantifiers evaluation * Use biased fp value constructor in Z3 * Fix Bv default value sampler * Fix ite simplifier * Filter out underspecified operations * Fix Bv shifts * Fix fp round * Detect Fp underspecified operations in tests * Test report merge * Test ignore utility * Fix bitwuzla fma internalizer * Guard solver API's with context match checks * Check function interpretation args in models * Check function interpretation args in models * Fix bitwuzla fp from bv converter * Update linux bitwuzla native * Fix Bitwuzla constants reverse cache * Fix bitwuzla native on Windows * Fix Bitwuzla Bv constants on Windows * Fix Bitwuzla Bv constants on Windows * Generate uninterpreted sorts cardinality constraints in one traverse * Upgrade version
UnitTestBot · Dec 30, 2022 · 5dbd7fc · 5dbd7fc
1 parent 654ece7
commit 5dbd7fc
Show file tree

Hide file tree

Showing 54 changed files with 1,673 additions and 318 deletions.
diff --git a/.github/workflows/run-long-tests.yml b/.github/workflows/run-long-tests.yml
@@ -167,4 +167,46 @@ jobs:
         if: always()
         with:
           name: ${{ format('ksmt-test-report-{0}-{1}-{2}', matrix.os, matrix.test, matrix.chunk) }}
-          path: ksmt-test/build/reports/tests/test/
+          path: ksmt-test/build/test-results/test/binary
+
+  merge_test_report:
+    name: Merge chunked test reports into a single one
+
+    needs: [ run_tests ]
+    runs-on: ubuntu-latest
+    if: ${{ always() }}
+
+    steps:
+      - uses: actions/checkout@v3
+
+      - uses: actions/download-artifact@v3
+        with:
+          path: reports
+
+      - name: Set up JDK 1.8
+        uses: actions/setup-java@v3
+        with:
+          java-version: 8
+          distribution: 'zulu'
+
+      - name: Merge test report [ubuntu-latest]
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: |
+            :ksmt-test:mergeTestReports
+            --no-daemon
+            -PtestReportMergePrefix=ksmt-test-report-ubuntu-latest
+
+      - name: Merge test report [windows-latest]
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: |
+            :ksmt-test:mergeTestReports
+            --no-daemon
+            -PtestReportMergePrefix=ksmt-test-report-windows-latest
+            
+      - name: Upload merged test reports
+        uses: actions/upload-artifact@v3
+        with:
+          name: ksmt-test-report
+          path: ksmt-test-report-*
diff --git a/README.md b/README.md
@@ -14,9 +14,9 @@ repositories {
 }
 
 // core 
-implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.0")
+implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.1")
 // z3 solver
-implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.0")
+implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.1")
 ```
 
 ## Usage

diff --git a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
@@ -9,7 +9,7 @@ plugins {
 }
 
 group = "org.ksmt"
-version = "0.3.0"
+version = "0.3.1"
 
 repositories {
     mavenCentral()

diff --git a/docs/getting-started.md b/docs/getting-started.md
@@ -18,17 +18,17 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.0")    
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.1")    
 }
 ```
 
 #### 3. Add one or more SMT solver dependencies:
 ```kotlin
 dependencies {
     // z3 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.1")
     // bitwuzla
-    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.3.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.3.1")
 }
 ```
 SMT solver specific packages are provided with solver native binaries. 

diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
@@ -10,9 +10,9 @@ repositories {
 
 dependencies {
     // core
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.1")
     // z3 solver
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.0")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.1")
 }
 
 java {

diff --git a/ksmt-bitwuzla/build.gradle.kts b/ksmt-bitwuzla/build.gradle.kts
@@ -9,30 +9,38 @@ repositories {
     flatDir { dirs("dist") }
 }
 
-val bitwuzlaNative by configurations.creating
+val bitwuzlaNativeJna by configurations.creating
+val bitwuzlaNativeDependency by configurations.creating
 
 dependencies {
     implementation(project(":ksmt-core"))
     api("net.java.dev.jna:jna:5.12.0")
     implementation("net.java.dev.jna:jna-platform:5.12.0")
 
-    bitwuzlaNative("bitwuzla", "bitwuzla-native-linux-x86-64", "1.0", ext = "zip")
-    bitwuzlaNative("bitwuzla", "bitwuzla-native-win32-x86-64", "1.0", ext = "zip")
+    bitwuzlaNativeJna("bitwuzla", "bitwuzla-native-linux-x86-64", "1.0", ext = "zip")
+    bitwuzlaNativeDependency("bitwuzla", "bitwuzla-native-dependency-linux-x86-64", "1.0", ext = "zip")
+    bitwuzlaNativeJna("bitwuzla", "bitwuzla-native-win32-x86-64", "1.0", ext = "zip")
+    bitwuzlaNativeDependency("bitwuzla", "bitwuzla-native-dependency-win32-x86-64", "1.0", ext = "zip")
 }
 
 tasks.withType<KotlinCompile> {
     kotlinOptions.freeCompilerArgs += "-opt-in=kotlin.RequiresOptIn"
 }
 
 tasks.withType<ProcessResources> {
-    bitwuzlaNative.resolvedConfiguration.resolvedArtifacts.forEach { artifact ->
+    bitwuzlaNativeJna.resolvedConfiguration.resolvedArtifacts.forEach { artifact ->
         // destination must be in format {OS}-{ARCH} according to JNA docs
         // https://github.com/java-native-access/jna/blob/master/www/GettingStarted.md
         val destination = artifact.name.removePrefix("bitwuzla-native-")
         from(zipTree(artifact.file)) {
             into(destination)
         }
     }
+    bitwuzlaNativeDependency.resolvedConfiguration.resolvedArtifacts.forEach { artifact ->
+        from(zipTree(artifact.file)) {
+            into("lib/x64")
+        }
+    }
 }
 
 publishing {

diff --git a/ksmt-bitwuzla/dist/bitwuzla-native-dependency-linux-x86-64-1.0.zip b/ksmt-bitwuzla/dist/bitwuzla-native-dependency-linux-x86-64-1.0.zip
diff --git a/ksmt-bitwuzla/dist/bitwuzla-native-dependency-win32-x86-64-1.0.zip b/ksmt-bitwuzla/dist/bitwuzla-native-dependency-win32-x86-64-1.0.zip
diff --git a/ksmt-bitwuzla/dist/bitwuzla-native-linux-x86-64-1.0.zip b/ksmt-bitwuzla/dist/bitwuzla-native-linux-x86-64-1.0.zip
diff --git a/ksmt-bitwuzla/dist/bitwuzla-native-win32-x86-64-1.0.zip b/ksmt-bitwuzla/dist/bitwuzla-native-win32-x86-64-1.0.zip
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt
@@ -23,6 +23,7 @@ import org.ksmt.sort.KFpRoundingModeSort
 import org.ksmt.sort.KFpSort
 import org.ksmt.sort.KSort
 import org.ksmt.utils.mkFreshConst
+import org.ksmt.utils.uncheckedCast
 
 @Suppress("LargeClass")
 open class KBitwuzlaExprConverter(
@@ -321,12 +322,23 @@ open class KBitwuzlaExprConverter(
 
             check(size == nativeBitsSize) { "Bv size mismatch, expr size $size, native size $nativeBitsSize " }
 
-            val bits = if (size <= Long.SIZE_BITS) {
+            val bits = when {
+                size <= Int.SIZE_BITS -> {
+                    val numericValue = Native.bitwuzlaBvBitsToUInt32(nativeBits).toUInt()
+                    numericValue.toString(radix = 2).padStart(size, '0')
+                }
+                /**
+                Disabled until [Native.bitwuzlaBvBitsToUInt64] will be fixed
+
+                size <= Long.SIZE_BITS -> {
                 val numericValue = Native.bitwuzlaBvBitsToUInt64(nativeBits).toULong()
                 numericValue.toString(radix = 2).padStart(size, '0')
-            } else {
-                val bits = BooleanArray(size) { nativeBits.getBit(it) }
-                bits.toReversedBinaryString()
+                }
+                 */
+                else -> {
+                    val bits = BooleanArray(size) { nativeBits.getBit(it) }
+                    bits.toReversedBinaryString()
+                }
             }
 
             mkBv(bits, size.toUInt())
@@ -353,13 +365,17 @@ open class KBitwuzlaExprConverter(
             }
 
             when (size) {
+                /**
+                Disabled until [Native.bitwuzlaBvBitsToUInt64] will be fixed
+
                 Double.SIZE_BITS -> {
-                    val numericValue = Native.bitwuzlaBvBitsToUInt64(nativeBits)
-                    mkFp(Double.fromBits(numericValue), sort)
+                val numericValue = Native.bitwuzlaBvBitsToUInt64(nativeBits)
+                mkFp(Double.fromBits(numericValue), sort)
                 }
+                 */
                 Float.SIZE_BITS -> {
-                    val numericValue = Native.bitwuzlaBvBitsToUInt64(nativeBits)
-                    mkFp(Float.fromBits(numericValue.toInt()), sort)
+                    val numericValue = Native.bitwuzlaBvBitsToUInt32(nativeBits)
+                    mkFp(Float.fromBits(numericValue), sort)
                 }
                 else -> {
                     val exponentSize = sort.exponentBits
@@ -565,39 +581,21 @@ open class KBitwuzlaExprConverter(
                 ctx.mkBvToFpExpr(sort, rm, value, signed = false)
             }
         BitwuzlaKind.BITWUZLA_KIND_FP_FP -> expr.convert(ctx::mkFpFromBvExpr)
-        BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_BV -> {
-            val indices = Native.bitwuzlaTermGetIndices(expr)
-            check(indices.size == 2) { "unexpected fp-from-bv indices: $indices" }
-            val (exponentSize, significandSize) = indices
-            val bvValue = Native.bitwuzlaTermGetChildren(expr).single()
-            val bvSize = Native.bitwuzlaTermBvGetSize(bvValue)
-            check(bvSize == exponentSize + significandSize) {
-                "unexpected bv size in fp-from-bv: bv-size $bvSize, exp $exponentSize, significand $significandSize"
+        BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_BV ->
+            expr.convert { bv: KExpr<KBvSort> ->
+                with(ctx) {
+                    val indices = Native.bitwuzlaTermGetIndices(expr)
+                    check(indices.size == 2) { "unexpected fp-from-bv indices: $indices" }
+                    val exponentSize = indices.first()
+                    val size = bv.sort.sizeBits.toInt()
+
+                    val sign = mkBvExtractExpr(size - 1, size - 1, bv)
+                    val exponent = mkBvExtractExpr(size - 2, size - exponentSize - 1, bv)
+                    val significand = mkBvExtractExpr(size - exponentSize - 2, 0, bv)
+
+                    mkFpFromBvExpr(sign.uncheckedCast(), exponent, significand)
+                }
             }
-
-            // rewrite expression as fp_fp
-            val signBv = Native.bitwuzlaMkTerm1Indexed2(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_EXTRACT,
-                bvValue,
-                bvSize - 1, bvSize - 1
-            )
-            val exponentBv = Native.bitwuzlaMkTerm1Indexed2(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_EXTRACT,
-                bvValue,
-                bvSize - 2, bvSize - 1 - exponentSize
-            )
-            val significandBv = Native.bitwuzlaMkTerm1Indexed2(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_EXTRACT,
-                bvValue,
-                significandSize - 2, 0
-            )
-            val rewritedExpr = Native.bitwuzlaMkTerm3(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_FP_FP,
-                signBv, exponentBv, significandBv
-            )
-
-            convertNativeExpr(rewritedExpr)
-        }
         BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_FP ->
             expr.convert { rm: KExpr<KFpRoundingModeSort>, value: KExpr<KFpSort> ->
                 val sort = Native.bitwuzlaTermGetSort(expr).convertSort() as KFpSort