Z3: support fp.to_ieee_bv internal decl (#140)

* Z3: support `fp.to_ieee_bv` internal decl * Upgrade ksmt version to 0.5.12
UnitTestBot · Oct 30, 2023 · 92add18 · 92add18
1 parent d110acf
commit 92add18
Show file tree

Hide file tree

Showing 6 changed files with 37 additions and 13 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.11)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.12)
 [![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.11")
+implementation("io.ksmt:ksmt-core:0.5.12")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.11")
+implementation("io.ksmt:ksmt-z3:0.5.12")
 ```
 
 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.11"
+version = "0.5.12"
 
 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.11")    
+    implementation("io.ksmt:ksmt-core:0.5.12")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.11")
+    implementation("io.ksmt:ksmt-z3:0.5.12")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.11")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.12")
 }
 ```
 

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.11")
+    implementation("io.ksmt:ksmt-core:0.5.12")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.11")
+    implementation("io.ksmt:ksmt-z3:0.5.12")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.11")
+    implementation("io.ksmt:ksmt-runner:0.5.12")
 }
 
 java {

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
@@ -410,9 +410,7 @@ open class KZ3ExprConverter(
                 throw KSolverUnsupportedFeatureException("Fp $declKind is not supported")
             }
 
-           Z3_decl_kind.Z3_OP_INTERNAL -> {
-                throw KSolverUnsupportedFeatureException("Z3 internal decl $declKind is not supported")
-            }
+            Z3_decl_kind.Z3_OP_INTERNAL -> tryConvertInternalAppExpr(expr, decl)
 
             Z3_decl_kind.Z3_OP_RECURSIVE -> {
                 throw KSolverUnsupportedFeatureException("Recursive decl $declKind is not supported")
@@ -586,6 +584,14 @@ open class KZ3ExprConverter(
         else -> convertApp(expr)
     }
 
+    private fun tryConvertInternalAppExpr(expr: Long, decl: Long): ExprConversionResult = with(ctx) {
+        val internalDeclName = convertNativeSymbol(Native.getDeclName(nCtx, decl))
+        when (internalDeclName) {
+            "fp.to_ieee_bv" -> expr.convert(::mkFpToIEEEBvExpr)
+            else -> throw KSolverUnsupportedFeatureException("Z3 internal decl $internalDeclName is not supported")
+        }
+    }
+
     @Suppress("MemberVisibilityCanBePrivate")
     fun convertFpRmNumeral(expr: Long): KFpRoundingModeExpr = with(ctx) {
         val decl = Native.getAppDecl(nCtx, expr)

diff --git a/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/FloatingPointTest.kt b/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/FloatingPointTest.kt
@@ -29,6 +29,7 @@ import io.ksmt.expr.KFp64Value
 import io.ksmt.expr.KFpRoundingMode
 import io.ksmt.expr.KFpRoundingModeExpr
 import io.ksmt.expr.KTrue
+import io.ksmt.solver.KSolverStatus
 import io.ksmt.sort.KBoolSort
 import io.ksmt.sort.KFp16Sort
 import io.ksmt.sort.KFp32Sort
@@ -739,6 +740,23 @@ class FloatingPointTest {
     @Test
     fun testIsInfinite() = testPredicate(context::mkFpIsInfiniteExpr) { value: Double -> value.isInfinite() }
 
+    @Test
+    fun testFpToIeeeModel() = with(context) {
+        val x by fp32Sort
+        val expr = mkFpToIEEEBvExpr(x)
+
+        solver.assert(expr eq mkBv(0, bv32Sort))
+        assertEquals(KSolverStatus.SAT, solver.check())
+
+        val model = solver.model()
+        val z3Value = model.eval(x)
+
+        val detachedModel = model.detach()
+        val detachedValue = detachedModel.eval(x)
+
+        assertEquals(z3Value, detachedValue)
+    }
+
     companion object {
         const val DELTA = 1e-15
     }