Fp review fixes

UnitTestBot · Sep 5, 2022 · a562b1f · a562b1f
1 parent 36c5be6
commit a562b1f
Show file tree

Hide file tree

Showing 8 changed files with 44 additions and 10 deletions.
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
@@ -470,7 +470,7 @@ open class KBitwuzlaExprInternalizer(
             throw KSolverUnsupportedFeatureException("Unsupported sort $sort")
 
         override fun <S : KFpSort> visit(sort: S): BitwuzlaSort =
-            throw KSolverUnsupportedFeatureException("Unsupported sort $sort")
+            TODO("We do not support KFP sort yet")
     }
 
     open class FunctionSortInternalizer(

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
@@ -224,7 +224,7 @@ import org.ksmt.expr.KFpValue
 import org.ksmt.expr.KFunctionAsArray
 import org.ksmt.utils.booleanSignBit
 import org.ksmt.utils.cast
-import org.ksmt.utils.extendWithZeros
+import org.ksmt.utils.extendWithLeadingZeros
 import org.ksmt.utils.extractExponent
 import org.ksmt.utils.extractSignificand
 import org.ksmt.utils.toBinary
@@ -1138,6 +1138,24 @@ open class KContext : AutoCloseable {
         }
     }
 
+    fun <T : KFpSort> mkFpCustomSize(
+        exponent: KBitVecValue<out KBvSort>,
+        significand: KBitVecValue<out KBvSort>,
+        signBit: Boolean
+    ): KFpValue<T> {
+        // TODO we should not use numbers and work with bitvectors. Change it later
+        val exponentLongValue = exponent.stringValue.toULong(radix = 2).toLong()
+        val significandLongValue = significand.stringValue.toULong(radix = 2).toLong()
+
+        return mkFpCustomSize(
+            exponent.sort.sizeBits,
+            significand.sort.sizeBits,
+            exponentLongValue,
+            significandLongValue,
+            signBit
+        )
+    }
+
     private fun constructFp16Number(exponent: Long, significand: Long, intSignBit: Int): Float {
         // get sign and `body` of the unbiased exponent
         val exponentSign = (exponent.toInt() shr 4) and 1
@@ -1175,10 +1193,10 @@ open class KContext : AutoCloseable {
 
     fun <T : KFpSort> mkFp(value: Float, sort: T): KExpr<T> {
         val significand = value.extractSignificand(sort)
-        val exponent = value.extractExponent(sort, isBiased = false).extendWithZeros()
+        val exponent = value.extractExponent(sort, isBiased = false).extendWithLeadingZeros()
         val sign = value.booleanSignBit
 
-        return mkFpCustomSize(sort.exponentBits, sort.significandBits, exponent, significand.extendWithZeros(), sign)
+        return mkFpCustomSize(sort.exponentBits, sort.significandBits, exponent, significand.extendWithLeadingZeros(), sign)
     }
 
     fun <T : KFpSort> mkFp(value: Double, sort: T): KExpr<T> {
@@ -1193,8 +1211,8 @@ open class KContext : AutoCloseable {
         mkFpCustomSize(
             sort.exponentBits,
             sort.significandBits,
-            exponent.extendWithZeros(),
-            significand.extendWithZeros(),
+            exponent.extendWithLeadingZeros(),
+            significand.extendWithLeadingZeros(),
             signBit
         )
 

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/decl/KFloatingPointDecl.kt b/ksmt-core/src/main/kotlin/org/ksmt/decl/KFloatingPointDecl.kt
@@ -12,7 +12,6 @@ import org.ksmt.utils.getHalfPrecisionExponent
 import org.ksmt.utils.booleanSignBit
 import org.ksmt.utils.getExponent
 import org.ksmt.utils.halfPrecisionSignificand
-import org.ksmt.utils.signBit
 import org.ksmt.utils.significand
 import org.ksmt.utils.toBinary
 
@@ -84,6 +83,7 @@ class KFp64Decl internal constructor(ctx: KContext, val value: Double) :
     override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
 }
 
+// TODO replace significand with bit vector and change KFpDecl accordingly
 class KFp128Decl internal constructor(
     ctx: KContext,
     significand: Long,

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt
@@ -10,16 +10,21 @@ import org.ksmt.sort.KBv64Sort
 import org.ksmt.sort.KBv8Sort
 import org.ksmt.sort.KBvSort
 import org.ksmt.sort.KIntSort
+import org.ksmt.utils.toBinary
 
 abstract class KBitVecValue<S : KBvSort>(
     ctx: KContext
 ) : KApp<S, KExpr<*>>(ctx) {
     override val args: List<KExpr<*>> = emptyList()
+
+    abstract val stringValue: String
 }
 
 class KBitVec1Value internal constructor(ctx: KContext, val value: Boolean) : KBitVecValue<KBv1Sort>(ctx) {
     override fun accept(transformer: KTransformer): KExpr<KBv1Sort> = transformer.transform(this)
 
+    override val stringValue: String = if (value) "1" else "0"
+
     override fun decl(): KDecl<KBv1Sort> = ctx.mkBvDecl(value)
 
     override fun sort(): KBv1Sort = ctx.mkBv1Sort()
@@ -28,7 +33,9 @@ class KBitVec1Value internal constructor(ctx: KContext, val value: Boolean) : KB
 abstract class KBitVecNumberValue<S : KBvSort, N : Number>(
     ctx: KContext,
     val numberValue: N
-) : KBitVecValue<S>(ctx)
+) : KBitVecValue<S>(ctx) {
+    override val stringValue: String = numberValue.toBinary()
+}
 
 class KBitVec8Value internal constructor(ctx: KContext, byteValue: Byte) :
     KBitVecNumberValue<KBv8Sort, Byte>(ctx, byteValue) {
@@ -80,6 +87,8 @@ class KBitVecCustomValue internal constructor(
 
     override fun accept(transformer: KTransformer): KExpr<KBvSort> = transformer.transform(this)
 
+    override val stringValue: String = binaryStringValue
+
     override fun decl(): KDecl<KBvSort> = ctx.mkBvDecl(binaryStringValue, sizeBits)
 
     override fun sort(): KBvSort = ctx.mkBvSort(sizeBits)

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt
@@ -123,6 +123,10 @@ class KFpCustomSizeValue internal constructor(
     exponent = with(ctx) { exponentValue.toBv(exponentSize) },
     signBit
 ) {
+    init {
+        require(exponentSize.toInt() <= 63) { "Maximum number of exponent bits is 63" }
+    }
+
     override fun decl(): KDecl<KFpSort> =
         ctx.mkFpCustomSizeDecl(significandSize, exponentSize, significandValue, exponentValue, signBit)
 

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt
@@ -97,7 +97,9 @@ class KUninterpretedSort internal constructor(val name: String, ctx: KContext) :
 }
 
 sealed class KFpSort(ctx: KContext, val exponentBits: UInt, val significandBits: UInt) : KSort(ctx) {
-    override fun print(): String = "FP (eBits: $exponentBits) (sBits: $significandBits)"
+    override fun print(builder: StringBuilder) {
+        builder.append("FP (eBits: $exponentBits) (sBits: $significandBits)")
+    }
     override fun <T> accept(visitor: KSortVisitor<T>): T = visitor.visit(this)
     abstract fun exponentShiftSize(): Int
 }

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt b/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt
@@ -113,7 +113,7 @@ fun Float.extractSignificand(sort: KFpSort): Int {
  * therefore we will have not a value of 32 zeros following by 32 ones, but 100...0011..11, that will change
  * the value of the bitvector we wanted to construct.
  */
-fun Int.extendWithZeros(): Long = toLong().let {
+fun Int.extendWithLeadingZeros(): Long = toLong().let {
     ((((it shr 63) and 1) shl 31) or it) and 0xffff_ffff
 }
 

diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt
@@ -268,6 +268,7 @@ open class KZ3ExprConverter(
 
                     // if we have sBits greater than long size bits, take it all, otherwise take last (sBits - 1) bits
                     val significandMask = if (sBits < fp64SizeBits) (1L shl (sBits - 1)) - 1 else -1
+                    // TODO it is not right if we have significand with number of bits greater than 64
                     val significand = significandUInt64 and significandMask
 
                     val exponentMask = (1L shl sort.exponentBits.toInt()) - 1