diff --git a/detekt.yml b/detekt.yml index 55a11a5f5..456f7cb9d 100644 --- a/detekt.yml +++ b/detekt.yml @@ -594,7 +594,7 @@ style: RedundantVisibilityModifierRule: active: false ReturnCount: - active: true + active: false max: 2 excludedFunctions: 'equals' excludeLabeled: false 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 index 395b1a797..a92cf00da 100644 --- a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt +++ b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt @@ -91,6 +91,8 @@ import org.ksmt.sort.KBv32Sort import org.ksmt.sort.KBv64Sort import org.ksmt.sort.KBv8Sort import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFpRoundingModeSort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KIntSort import org.ksmt.sort.KRealSort import org.ksmt.sort.KSort @@ -587,6 +589,13 @@ open class KBitwuzlaExprInternalizer( override fun visit(sort: KUninterpretedSort): BitwuzlaSort = throw KSolverUnsupportedFeatureException("Unsupported sort $sort") + + override fun visit(sort: S): BitwuzlaSort = + TODO("We do not support KFP sort yet") + + override fun visit(sort: KFpRoundingModeSort): BitwuzlaSort { + TODO("We do not support KFpRoundingModeSort 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 index 7e4b33e74..3464840d7 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt @@ -1,9 +1,13 @@ package org.ksmt +import java.lang.Double.longBitsToDouble +import java.lang.Float.intBitsToFloat import org.ksmt.cache.Cache0 import org.ksmt.cache.Cache1 import org.ksmt.cache.Cache2 import org.ksmt.cache.Cache3 +import org.ksmt.cache.Cache4 +import org.ksmt.cache.Cache5 import org.ksmt.cache.mkCache import org.ksmt.decl.KAndDecl import org.ksmt.decl.KArithAddDecl @@ -183,6 +187,12 @@ import org.ksmt.sort.KBv8Sort import org.ksmt.sort.KBvCustomSizeSort import org.ksmt.sort.KBvSort import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpCustomSizeSort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KIntSort import org.ksmt.sort.KRealSort import org.ksmt.sort.KSort @@ -192,6 +202,44 @@ import kotlin.reflect.KProperty import org.ksmt.decl.KBvRotateLeftIndexedDecl import org.ksmt.decl.KBvRotateRightIndexedDecl import org.ksmt.decl.KBvSubNoUnderflowDecl +import org.ksmt.decl.KBvToFpDecl +import org.ksmt.decl.KFp128Decl +import org.ksmt.decl.KFp16Decl +import org.ksmt.decl.KFp32Decl +import org.ksmt.decl.KFp64Decl +import org.ksmt.decl.KFpAbsDecl +import org.ksmt.decl.KFpAddDecl +import org.ksmt.decl.KFpCustomSizeDecl +import org.ksmt.decl.KFpDecl +import org.ksmt.decl.KFpDivDecl +import org.ksmt.decl.KFpEqualDecl +import org.ksmt.decl.KFpFromBvDecl +import org.ksmt.decl.KFpFusedMulAddDecl +import org.ksmt.decl.KFpGreaterDecl +import org.ksmt.decl.KFpGreaterOrEqualDecl +import org.ksmt.decl.KFpIsInfiniteDecl +import org.ksmt.decl.KFpIsNaNDecl +import org.ksmt.decl.KFpIsNegativeDecl +import org.ksmt.decl.KFpIsNormalDecl +import org.ksmt.decl.KFpIsPositiveDecl +import org.ksmt.decl.KFpIsSubnormalDecl +import org.ksmt.decl.KFpIsZeroDecl +import org.ksmt.decl.KFpLessDecl +import org.ksmt.decl.KFpLessOrEqualDecl +import org.ksmt.decl.KFpMaxDecl +import org.ksmt.decl.KFpMinDecl +import org.ksmt.decl.KFpMulDecl +import org.ksmt.decl.KFpNegationDecl +import org.ksmt.decl.KFpRemDecl +import org.ksmt.decl.KFpRoundToIntegralDecl +import org.ksmt.decl.KFpRoundingModeDecl +import org.ksmt.decl.KFpSqrtDecl +import org.ksmt.decl.KFpSubDecl +import org.ksmt.decl.KFpToBvDecl +import org.ksmt.decl.KFpToFpDecl +import org.ksmt.decl.KFpToIEEEBvDecl +import org.ksmt.decl.KFpToRealDecl +import org.ksmt.decl.KRealToFpDecl import org.ksmt.expr.KBitVec16Value import org.ksmt.expr.KBitVec1Value import org.ksmt.expr.KBitVec32Value @@ -201,8 +249,54 @@ import org.ksmt.expr.KBitVecCustomValue import org.ksmt.expr.KBvRotateLeftIndexedExpr import org.ksmt.expr.KBvRotateRightIndexedExpr import org.ksmt.expr.KBvSubNoUnderflowExpr +import org.ksmt.expr.KBvToFpExpr +import org.ksmt.expr.KFp128Value +import org.ksmt.expr.KFp16Value +import org.ksmt.expr.KFp32Value +import org.ksmt.expr.KFp64Value +import org.ksmt.expr.KFpAbsExpr +import org.ksmt.expr.KFpAddExpr +import org.ksmt.expr.KFpCustomSizeValue +import org.ksmt.expr.KFpDivExpr +import org.ksmt.expr.KFpEqualExpr +import org.ksmt.expr.KFpFromBvExpr +import org.ksmt.expr.KFpFusedMulAddExpr +import org.ksmt.expr.KFpGreaterExpr +import org.ksmt.expr.KFpGreaterOrEqualExpr +import org.ksmt.expr.KFpIsInfiniteExpr +import org.ksmt.expr.KFpIsNaNExpr +import org.ksmt.expr.KFpIsNegativeExpr +import org.ksmt.expr.KFpIsNormalExpr +import org.ksmt.expr.KFpIsPositiveExpr +import org.ksmt.expr.KFpIsSubnormalExpr +import org.ksmt.expr.KFpIsZeroExpr +import org.ksmt.expr.KFpLessExpr +import org.ksmt.expr.KFpLessOrEqualExpr +import org.ksmt.expr.KFpMaxExpr +import org.ksmt.expr.KFpMinExpr +import org.ksmt.expr.KFpMulExpr +import org.ksmt.expr.KFpNegationExpr +import org.ksmt.expr.KFpRemExpr +import org.ksmt.expr.KFpRoundToIntegralExpr +import org.ksmt.expr.KFpRoundingMode +import org.ksmt.expr.KFpRoundingModeExpr +import org.ksmt.expr.KFpSqrtExpr +import org.ksmt.expr.KFpSubExpr +import org.ksmt.expr.KFpToBvExpr +import org.ksmt.expr.KFpToFpExpr +import org.ksmt.expr.KFpToIEEEBvExpr +import org.ksmt.expr.KFpToRealExpr +import org.ksmt.expr.KFpValue import org.ksmt.expr.KFunctionAsArray +import org.ksmt.expr.KRealToFpExpr +import org.ksmt.sort.KFpRoundingModeSort +import org.ksmt.utils.booleanSignBit import org.ksmt.utils.cast +import org.ksmt.utils.extendWithLeadingZeros +import org.ksmt.utils.extractExponent +import org.ksmt.utils.extractSignificand +import org.ksmt.utils.getExponent +import org.ksmt.utils.getHalfPrecisionExponent import org.ksmt.utils.toBinary import org.ksmt.utils.uncheckedCast @@ -266,6 +360,39 @@ open class KContext : AutoCloseable { private val uninterpretedSortCache = mkClosableCache { name: String -> KUninterpretedSort(name, this) } fun mkUninterpretedSort(name: String): KUninterpretedSort = uninterpretedSortCache.createIfContextActive(name) + // floating point + private val fpSortCache = mkClosableCache { exponentBits: UInt, significandBits: UInt -> + when { + exponentBits == KFp16Sort.exponentBits && significandBits == KFp16Sort.significandBits -> KFp16Sort(this) + exponentBits == KFp32Sort.exponentBits && significandBits == KFp32Sort.significandBits -> KFp32Sort(this) + exponentBits == KFp64Sort.exponentBits && significandBits == KFp64Sort.significandBits -> KFp64Sort(this) + exponentBits == KFp128Sort.exponentBits && significandBits == KFp128Sort.significandBits -> KFp128Sort(this) + else -> KFpCustomSizeSort(this, exponentBits, significandBits) + } + } + + fun mkFp16Sort(): KFp16Sort = fpSortCache.createIfContextActive( + KFp16Sort.exponentBits, KFp16Sort.significandBits + ).cast() + + fun mkFp32Sort(): KFp32Sort = fpSortCache.createIfContextActive( + KFp32Sort.exponentBits, KFp32Sort.significandBits + ).cast() + + fun mkFp64Sort(): KFp64Sort = fpSortCache.createIfContextActive( + KFp64Sort.exponentBits, KFp64Sort.significandBits + ).cast() + + fun mkFp128Sort(): KFp128Sort = fpSortCache.createIfContextActive( + KFp128Sort.exponentBits, KFp128Sort.significandBits + ).cast() + + fun mkFpSort(exponentBits: UInt, significandBits: UInt): KFpSort = + fpSortCache.createIfContextActive(exponentBits, significandBits) + + private val roundingModeSortCache = mkClosableCache { KFpRoundingModeSort(this) } + fun mkFpRoundingModeSort(): KFpRoundingModeSort = roundingModeSortCache.createIfContextActive() + // utils val boolSort: KBoolSort get() = mkBoolSort() @@ -627,33 +754,53 @@ open class KContext : AutoCloseable { private val bvCache = mkClosableCache { value: String, sizeBits: UInt -> KBitVecCustomValue(this, value, sizeBits) } fun mkBv(value: Boolean): KBitVec1Value = bv1Cache.createIfContextActive(value) + fun mkBv(value: Boolean, sizeBits: UInt): KBitVecValue = mkBv((if (value) 1 else 0) as Number, sizeBits) fun Boolean.toBv(): KBitVec1Value = mkBv(this) + fun Boolean.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) + + fun mkBv(value: Byte): KBitVec8Value = bv8Cache.createIfContextActive(value) + fun mkBv(value: Byte, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) fun Byte.toBv(): KBitVec8Value = mkBv(this) + fun Byte.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun UByte.toBv(): KBitVec8Value = mkBv(toByte()) + fun mkBv(value: Short): KBitVec16Value = bv16Cache.createIfContextActive(value) + fun mkBv(value: Short, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) fun Short.toBv(): KBitVec16Value = mkBv(this) + fun Short.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun UShort.toBv(): KBitVec16Value = mkBv(toShort()) + fun mkBv(value: Int): KBitVec32Value = bv32Cache.createIfContextActive(value) + fun mkBv(value: Int, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) fun Int.toBv(): KBitVec32Value = mkBv(this) + fun Int.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun UInt.toBv(): KBitVec32Value = mkBv(toInt()) + fun mkBv(value: Long): KBitVec64Value = bv64Cache.createIfContextActive(value) + fun mkBv(value: Long, sizeBits: UInt): KBitVecValue = mkBv(value as Number, sizeBits) fun Long.toBv(): KBitVec64Value = mkBv(this) + fun Long.toBv(sizeBits: UInt): KBitVecValue = mkBv(this, sizeBits) fun ULong.toBv(): KBitVec64Value = mkBv(toLong()) - fun mkBv(value: Number, sizeBits: UInt): KBitVecValue { - val binaryString = value.toBinary() - - require(binaryString.length <= sizeBits.toInt()) { - "Cannot create a bitvector of size $sizeBits from the given number $value" + - " since its binary representation requires at least ${binaryString.length} bits" - } + /** + * Constructs a bit vector from the given [value] containing of [sizeBits] bits. + * + * Note: if [sizeBits] is less than is required to represent the [value], + * the last [sizeBits] bits of the [value] will be taken. + * + * At the same time, if [sizeBits] is greater than it is required, + * binary representation of the [value] will be padded from the start with its sign bit. + */ + private fun mkBv(value: Number, sizeBits: UInt): KBitVecValue { + val binaryString = value.toBinary().takeLast(sizeBits.toInt()) val paddedString = binaryString.padStart(sizeBits.toInt(), binaryString.first()) return mkBv(paddedString, sizeBits) } - fun Number.toBv(sizeBits: UInt) = mkBv(this, sizeBits) + private fun Number.toBv(sizeBits: UInt) = mkBv(this, sizeBits) + fun mkBv(value: String, sizeBits: UInt): KBitVecValue = when (sizeBits.toInt()) { 1 -> mkBv(value.toUInt(radix = 2).toInt() != 0).cast() Byte.SIZE_BITS -> mkBv(value.toUByte(radix = 2).toByte()).cast() @@ -983,6 +1130,7 @@ open class KContext : AutoCloseable { private val bvNegNoOverflowExprCache = mkClosableCache { value: KExpr -> KBvNegNoOverflowExpr(this, value) } + fun mkBvNegationNoOverflowExpr(value: KExpr): KBvNegNoOverflowExpr = bvNegNoOverflowExprCache.createIfContextActive(value.cast()).cast() @@ -1015,6 +1163,471 @@ open class KContext : AutoCloseable { fun mkBvMulNoUnderflowExpr(arg0: KExpr, arg1: KExpr): KBvMulNoUnderflowExpr = bvMulNoUnderflowExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + // fp values + private val fp16Cache = mkClosableCache { value: Float -> KFp16Value(this, value) } + private val fp32Cache = mkClosableCache { value: Float -> KFp32Value(this, value) } + private val fp64Cache = mkClosableCache { value: Double -> KFp64Value(this, value) } + private val fp128Cache = mkClosableCache { significand: Long, exponent: Long, signBit: Boolean -> + KFp128Value(this, significand, exponent, signBit) + } + private val fpCustomSizeCache = + mkClosableCache { significandSize: UInt, + exponentSize: UInt, + significand: Long, + exponent: Long, + signBit: Boolean -> + KFpCustomSizeValue(this, significandSize, exponentSize, significand, exponent, signBit) + } + + /** + * Creates FP16 from the [value]. + * + * Important: we suppose that [value] has biased exponent, but FP16 will be created from the unbiased one. + * So, at first, we'll subtract [KFp16Sort.exponentShiftSize] from the [value]'s exponent, + * take required for FP16 bits, and this will be **unbiased** FP16 exponent. + * The same is true for other methods but [mkFpCustomSize]. + * */ + fun mkFp16(value: Float): KFp16Value = fp16Cache.createIfContextActive(value) + fun mkFp32(value: Float): KFp32Value = fp32Cache.createIfContextActive(value) + fun mkFp64(value: Double): KFp64Value = fp64Cache.createIfContextActive(value) + fun mkFp128(significand: Long, exponent: Long, signBit: Boolean): KFp128Value = + fp128Cache.createIfContextActive(significand, exponent, signBit) + + /** + * Creates FP with a custom size. + * Important: [exponent] here is an **unbiased** value. + */ + fun mkFpCustomSize( + exponentSize: UInt, + significandSize: UInt, + exponent: Long, + significand: Long, + signBit: Boolean + ): KFpValue { + val intSignBit = if (signBit) 1 else 0 + + return when (mkFpSort(exponentSize, significandSize)) { + is KFp16Sort -> { + val number = constructFp16Number(exponent, significand, intSignBit) + + mkFp16(number).cast() + } + is KFp32Sort -> { + val number = constructFp32Number(exponent, significand, intSignBit) + + mkFp32(number).cast() + } + is KFp64Sort -> { + val number = constructFp64Number(exponent, significand, intSignBit) + + mkFp64(number).cast() + } + is KFp128Sort -> mkFp128(significand, exponent, signBit).cast() + else -> fpCustomSizeCache.createIfContextActive( + significandSize, exponentSize, significand, exponent, signBit + ).cast() + } + } + + fun mkFpCustomSize( + exponent: KBitVecValue, + significand: KBitVecValue, + signBit: Boolean + ): KFpValue { + // 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 + ) + } + + @Suppress("MagicNumber") + 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 + val otherExponent = exponent.toInt() and 0b1111 + + // get fp16 significand part -- last teb bits (eleventh stored implicitly) + val significandBits = significand.toInt() and 0b1111_1111_11 + + // Transform fp16 exponent into fp32 exponent adding three zeroes between the sign and the body + // Then add the bias for fp32 and apply the mask to avoid overflow of the eight bits + val biasedFloatExponent = (((exponentSign shl 7) or otherExponent) + KFp32Sort.exponentShiftSize) and 0xff + + val bits = (intSignBit shl 31) or (biasedFloatExponent shl 23) or (significandBits shl 13) + + return intBitsToFloat(bits) + } + + @Suppress("MagicNumber") + private fun constructFp32Number(exponent: Long, significand: Long, intSignBit: Int): Float { + // `and 0xff` here is to avoid overloading when we have a number greater than 255, + // and the result of the addition will affect the sign bit + val biasedExponent = (exponent.toInt() + KFp32Sort.exponentShiftSize) and 0xff + val intValue = (intSignBit shl 31) or (biasedExponent shl 23) or significand.toInt() + + return intBitsToFloat(intValue) + } + + @Suppress("MagicNumber") + private fun constructFp64Number(exponent: Long, significand: Long, intSignBit: Int): Double { + // `and 0b111_1111_1111` here is to avoid overloading when we have a number greater than 255, + // and the result of the addition will affect the sign bit + val biasedExponent = (exponent + KFp64Sort.exponentShiftSize) and 0b111_1111_1111 + val longValue = (intSignBit.toLong() shl 63) or (biasedExponent shl 52) or significand + + return longBitsToDouble(longValue) + } + + fun mkFp(value: Float, sort: T): KExpr { + val significand = value.extractSignificand(sort) + val exponent = value.extractExponent(sort, isBiased = false).extendWithLeadingZeros() + val sign = value.booleanSignBit + + return mkFpCustomSize( + sort.exponentBits, + sort.significandBits, + exponent, + significand.extendWithLeadingZeros(), + sign + ) + } + + fun mkFp(value: Double, sort: T): KExpr { + val significand = value.extractSignificand(sort) + val exponent = value.extractExponent(sort, isBiased = false) + val sign = value.booleanSignBit + + return mkFpCustomSize(sort.exponentBits, sort.significandBits, exponent, significand, sign) + } + + fun Double.toFp(sort: KFpSort = mkFp64Sort()): KExpr = mkFp(this, sort) + + fun Float.toFp(sort: KFpSort = mkFp32Sort()): KExpr = mkFp(this, sort) + + fun mkFp(significand: Int, exponent: Int, signBit: Boolean, sort: T): KExpr = + mkFpCustomSize( + sort.exponentBits, + sort.significandBits, + exponent.extendWithLeadingZeros(), + significand.extendWithLeadingZeros(), + signBit + ) + + fun mkFp(significand: Long, exponent: Long, signBit: Boolean, sort: T): KExpr = + mkFpCustomSize(sort.exponentBits, sort.significandBits, exponent, significand, signBit) + + /** + * Special Fp values + * */ + fun mkFpZero(signBit: Boolean, sort: T): KExpr = + mkFpCustomSize( + sort.exponentBits, + sort.significandBits, + exponent = fpZeroExponentUnbiased(sort), + significand = 0L, + signBit = signBit + ) + + fun mkFpInf(signBit: Boolean, sort: T): KExpr = + mkFpCustomSize( + sort.exponentBits, + sort.significandBits, + exponent = fpTopExponentUnbiased(sort), + significand = 0L, + signBit + ) + + fun mkFpNan(sort: T): KExpr = + mkFpCustomSize( + sort.exponentBits, + sort.significandBits, + exponent = fpTopExponentUnbiased(sort), + significand = 1L, + signBit = false + ) + + private fun fpTopExponentUnbiased(sort: KFpSort): Long = when (sort) { + is KFp16Sort -> Float.POSITIVE_INFINITY.getHalfPrecisionExponent(isBiased = false).toLong() + is KFp32Sort -> Float.POSITIVE_INFINITY.getExponent(isBiased = false).toLong() + is KFp64Sort -> Double.POSITIVE_INFINITY.getExponent(isBiased = false) + is KFp128Sort -> TODO("fp 128 top exponent") + is KFpCustomSizeSort -> TODO("custom fp top exponent") + } + + private fun fpZeroExponentUnbiased(sort: KFpSort): Long = when (sort) { + is KFp16Sort -> 0.0f.getHalfPrecisionExponent(isBiased = false).toLong() + is KFp32Sort -> 0.0f.getExponent(isBiased = false).toLong() + is KFp64Sort -> 0.0.getExponent(isBiased = false) + is KFp128Sort -> TODO("fp 128 zero exponent") + is KFpCustomSizeSort -> TODO("custom fp zero exponent") + } + + private val roundingModeCache = mkClosableCache { value: KFpRoundingMode -> KFpRoundingModeExpr(this, value) } + fun mkFpRoundingModeExpr(value: KFpRoundingMode): KFpRoundingModeExpr = + roundingModeCache.createIfContextActive(value) + + private val fpAbsExprCache = mkClosableCache { value: KExpr -> KFpAbsExpr(this, value) } + fun mkFpAbsExpr(value: KExpr): KFpAbsExpr = + fpAbsExprCache.createIfContextActive(value.cast()).cast() + + private val fpNegationExprCache = mkClosableCache { value: KExpr -> KFpNegationExpr(this, value) } + fun mkFpNegationExpr(value: KExpr): KFpNegationExpr = + fpNegationExprCache.createIfContextActive(value.cast()).cast() + + private val fpAddExprCache = mkClosableCache { roundingMode: KExpr, + arg0: KExpr, + arg1: KExpr -> + KFpAddExpr(this, roundingMode, arg0, arg1) + } + + fun mkFpAddExpr( + roundingMode: KExpr, + arg0: KExpr, + arg1: KExpr + ): KFpAddExpr = fpAddExprCache.createIfContextActive(roundingMode.cast(), arg0.cast(), arg1.cast()).cast() + + + private val fpSubExprCache = mkClosableCache { roundingMode: KExpr, + arg0: KExpr, + arg1: KExpr -> + KFpSubExpr(this, roundingMode, arg0, arg1) + } + + fun mkFpSubExpr( + roundingMode: KExpr, + arg0: KExpr, + arg1: KExpr + ): KFpSubExpr = fpSubExprCache.createIfContextActive(roundingMode.cast(), arg0.cast(), arg1.cast()).cast() + + private val fpMulExprCache = + mkClosableCache { roundingMode: KExpr, arg0: KExpr, arg1: KExpr -> + KFpMulExpr(this, roundingMode, arg0, arg1) + } + + fun mkFpMulExpr( + roundingMode: KExpr, + arg0: KExpr, + arg1: KExpr + ): KFpMulExpr = fpMulExprCache.createIfContextActive(roundingMode.cast(), arg0.cast(), arg1.cast()).cast() + + private val fpDivExprCache = + mkClosableCache { roundingMode: KExpr, arg0: KExpr, arg1: KExpr -> + KFpDivExpr(this, roundingMode, arg0, arg1) + } + + fun mkFpDivExpr( + roundingMode: KExpr, + arg0: KExpr, + arg1: KExpr + ): KFpDivExpr = fpDivExprCache.createIfContextActive(roundingMode.cast(), arg0.cast(), arg1.cast()).cast() + + private val fpFusedMulAddExprCache = mkClosableCache { roundingMode: KExpr, + arg0: KExpr, + arg1: KExpr, + arg2: KExpr -> + KFpFusedMulAddExpr(this, roundingMode, arg0, arg1, arg2) + } + + fun mkFpFusedMulAddExpr( + roundingMode: KExpr, + arg0: KExpr, + arg1: KExpr, + arg2: KExpr + ): KFpFusedMulAddExpr = + fpFusedMulAddExprCache.createIfContextActive(roundingMode.cast(), arg0.cast(), arg1.cast(), arg2.cast()).cast() + + private val fpSqrtExprCache = mkClosableCache { roundingMode: KExpr, value: KExpr -> + KFpSqrtExpr(this, roundingMode, value) + } + + fun mkFpSqrtExpr( + roundingMode: KExpr, + value: KExpr + ): KFpSqrtExpr = + fpSqrtExprCache.createIfContextActive(roundingMode.cast(), value.cast()).cast() + + private val fpRemExprCache = mkClosableCache { arg0: KExpr, arg1: KExpr -> + KFpRemExpr(this, arg0, arg1) + } + + fun mkFpRemExpr(arg0: KExpr, arg1: KExpr): KFpRemExpr = + fpRemExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + + private val fpRoundToIntegralExprCache = + mkClosableCache { roundingMode: KExpr, value: KExpr -> + KFpRoundToIntegralExpr(this, roundingMode, value) + } + + fun mkFpRoundToIntegralExpr( + roundingMode: KExpr, + value: KExpr + ): KFpRoundToIntegralExpr = + fpRoundToIntegralExprCache.createIfContextActive(roundingMode.cast(), value.cast()).cast() + + private val fpMinExprCache = mkClosableCache { arg0: KExpr, arg1: KExpr -> + KFpMinExpr(this, arg0, arg1) + } + + fun mkFpMinExpr(arg0: KExpr, arg1: KExpr): KFpMinExpr = + fpMinExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + + private val fpMaxExprCache = mkClosableCache { arg0: KExpr, arg1: KExpr -> + KFpMaxExpr(this, arg0, arg1) + } + + fun mkFpMaxExpr(arg0: KExpr, arg1: KExpr): KFpMaxExpr = + fpMaxExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + + private val fpLessOrEqualExprCache = mkClosableCache { arg0: KExpr, arg1: KExpr -> + KFpLessOrEqualExpr(this, arg0, arg1) + } + + fun mkFpLessOrEqualExpr(arg0: KExpr, arg1: KExpr): KFpLessOrEqualExpr = + fpLessOrEqualExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + + private val fpLessExprCache = mkClosableCache { arg0: KExpr, arg1: KExpr -> + KFpLessExpr(this, arg0, arg1) + } + + fun mkFpLessExpr(arg0: KExpr, arg1: KExpr): KFpLessExpr = + fpLessExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + + private val fpGreaterOrEqualExprCache = mkClosableCache { arg0: KExpr, arg1: KExpr -> + KFpGreaterOrEqualExpr(this, arg0, arg1) + } + + fun mkFpGreaterOrEqualExpr(arg0: KExpr, arg1: KExpr): KFpGreaterOrEqualExpr = + fpGreaterOrEqualExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + + private val fpGreaterExprCache = mkClosableCache { arg0: KExpr, arg1: KExpr -> + KFpGreaterExpr(this, arg0, arg1) + } + + fun mkFpGreaterExpr(arg0: KExpr, arg1: KExpr): KFpGreaterExpr = + fpGreaterExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + + private val fpEqualExprCache = mkClosableCache { arg0: KExpr, arg1: KExpr -> + KFpEqualExpr(this, arg0, arg1) + } + + fun mkFpEqualExpr(arg0: KExpr, arg1: KExpr): KFpEqualExpr = + fpEqualExprCache.createIfContextActive(arg0.cast(), arg1.cast()).cast() + + private val fpIsNormalExprCache = mkClosableCache { value: KExpr -> KFpIsNormalExpr(this, value) } + + fun mkFpIsNormalExpr(value: KExpr): KFpIsNormalExpr = + fpIsNormalExprCache.createIfContextActive(value.cast()).cast() + + private val fpIsSubnormalExprCache = mkClosableCache { value: KExpr -> KFpIsSubnormalExpr(this, value) } + + fun mkFpIsSubnormalExpr(value: KExpr): KFpIsSubnormalExpr = + fpIsSubnormalExprCache.createIfContextActive(value.cast()).cast() + + private val fpIsZeroExprCache = mkClosableCache { value: KExpr -> KFpIsZeroExpr(this, value) } + + fun mkFpIsZeroExpr(value: KExpr): KFpIsZeroExpr = + fpIsZeroExprCache.createIfContextActive(value.cast()).cast() + + private val fpIsInfiniteExprCache = mkClosableCache { value: KExpr -> KFpIsInfiniteExpr(this, value) } + + fun mkFpIsInfiniteExpr(value: KExpr): KFpIsInfiniteExpr = + fpIsInfiniteExprCache.createIfContextActive(value.cast()).cast() + + private val fpIsNaNExprCache = mkClosableCache { value: KExpr -> KFpIsNaNExpr(this, value) } + + fun mkFpIsNaNExpr(value: KExpr): KFpIsNaNExpr = + fpIsNaNExprCache.createIfContextActive(value.cast()).cast() + + private val fpIsNegativeExprCache = mkClosableCache { value: KExpr -> KFpIsNegativeExpr(this, value) } + + fun mkFpIsNegativeExpr(value: KExpr): KFpIsNegativeExpr = + fpIsNegativeExprCache.createIfContextActive(value.cast()).cast() + + private val fpIsPositiveExprCache = mkClosableCache { value: KExpr -> KFpIsPositiveExpr(this, value) } + + fun mkFpIsPositiveExpr(value: KExpr): KFpIsPositiveExpr = + fpIsPositiveExprCache.createIfContextActive(value.cast()).cast() + + private val fpToBvExprCache = mkClosableCache { roundingMode: KExpr, + value: KExpr, + bvSize: Int, + isSigned: Boolean -> + KFpToBvExpr(this, roundingMode, value, bvSize, isSigned) + } + + fun mkFpToBvExpr( + roundingMode: KExpr, + value: KExpr, + bvSize: Int, + isSigned: Boolean + ): KFpToBvExpr = + fpToBvExprCache.createIfContextActive(roundingMode.cast(), value.cast(), bvSize, isSigned).cast() + + private val fpToRealExprCache = mkClosableCache { value: KExpr -> KFpToRealExpr(this, value) } + + fun mkFpToRealExpr(value: KExpr): KFpToRealExpr = + fpToRealExprCache.createIfContextActive(value.cast()).cast() + + private val fpToIEEEBvExprCache = mkClosableCache { value: KExpr -> KFpToIEEEBvExpr(this, value) } + + fun mkFpToIEEEBvExpr(value: KExpr): KFpToIEEEBvExpr = + fpToIEEEBvExprCache.createIfContextActive(value.cast()).cast() + + private val fpFromBvExprCache = mkClosableCache { sign: KExpr, + exponent: KExpr, + significand: KExpr -> + val sort = mkFpSort(exponent.sort.sizeBits, significand.sort.sizeBits + 1u) + KFpFromBvExpr(this, sort, sign, exponent, significand) + } + fun mkFpFromBvExpr( + sign: KExpr, + exponent: KExpr, + significand: KExpr, + ): KFpFromBvExpr = fpFromBvExprCache.createIfContextActive(sign, exponent, significand).cast() + + private val fpToFpExprCache = mkClosableCache { sort: KFpSort, + rm: KExpr, + value: KExpr -> + KFpToFpExpr(this, sort, rm, value) + } + private val realToFpExprCache = mkClosableCache { sort: KFpSort, + rm: KExpr, + value: KExpr -> + KRealToFpExpr(this, sort, rm, value) + } + private val bvToFpExprCache = mkClosableCache { sort: KFpSort, + rm: KExpr, + value: KExpr, + signed: Boolean -> + KBvToFpExpr(this, sort, rm, value, signed) + } + + fun mkFpToFpExpr( + sort: T, + roundingMode: KExpr, + value: KExpr + ): KFpToFpExpr = fpToFpExprCache.createIfContextActive(sort, roundingMode, value).cast() + + fun mkRealToFpExpr( + sort: T, + roundingMode: KExpr, + value: KExpr + ): KRealToFpExpr = realToFpExprCache.createIfContextActive(sort, roundingMode, value).cast() + + fun mkBvToFpExpr( + sort: T, + roundingMode: KExpr, + value: KExpr, + signed: Boolean + ): KBvToFpExpr = bvToFpExprCache.createIfContextActive(sort, roundingMode, value, signed).cast() + // quantifiers private val existentialQuantifierCache = mkClosableCache { body: KExpr, bounds: List> -> ensureContextMatch(body) @@ -1335,11 +1948,13 @@ open class KContext : AutoCloseable { private val bvSignedRemDeclCache = mkClosableCache { arg0: KBvSort, arg1: KBvSort -> KBvSignedRemDecl(this, arg0, arg1) } + fun mkBvSignedRemDecl(arg0: T, arg1: T): KBvSignedRemDecl = bvSignedRemDeclCache.createIfContextActive(arg0, arg1).cast() private val bvSignedModDeclCache = mkClosableCache { arg0: KBvSort, arg1: KBvSort -> KBvSignedModDecl(this, arg0, arg1) } + fun mkBvSignedModDecl(arg0: T, arg1: T): KBvSignedModDecl = bvSignedModDeclCache.createIfContextActive(arg0, arg1).cast() @@ -1351,6 +1966,7 @@ open class KContext : AutoCloseable { private val bvSignedLessDeclCache = mkClosableCache { arg0: KBvSort, arg1: KBvSort -> KBvSignedLessDecl(this, arg0, arg1) } + fun mkBvSignedLessDecl(arg0: T, arg1: T): KBvSignedLessDecl = bvSignedLessDeclCache.createIfContextActive(arg0, arg1).cast() @@ -1390,7 +2006,9 @@ open class KContext : AutoCloseable { fun mkBvSignedGreaterDecl(arg0: T, arg1: T): KBvSignedGreaterDecl = bvSignedGreaterDeclCache.createIfContextActive(arg0, arg1).cast() - private val concatDeclCache = mkClosableCache { arg0: KBvSort, arg1: KBvSort -> KBvConcatDecl(this, arg0, arg1) } + private val concatDeclCache = + mkClosableCache { arg0: KBvSort, arg1: KBvSort -> KBvConcatDecl(this, arg0, arg1) } + fun mkBvConcatDecl(arg0: KBvSort, arg1: KBvSort): KBvConcatDecl = concatDeclCache.createIfContextActive(arg0, arg1) private val extractDeclCache = mkClosableCache { high: Int, low: Int, value: KExpr -> @@ -1521,7 +2139,8 @@ open class KContext : AutoCloseable { fun mkBvDivNoOverflowDecl(arg0: T, arg1: T): KBvDivNoOverflowDecl = bvDivNoOverflowDeclCache.createIfContextActive(arg0, arg1).cast() - private val bvNegationNoOverflowDeclCache = mkClosableCache { value: KBvSort -> KBvNegNoOverflowDecl(this, value) } + private val bvNegationNoOverflowDeclCache = + mkClosableCache { value: KBvSort -> KBvNegNoOverflowDecl(this, value) } fun mkBvNegationNoOverflowDecl(value: T): KBvNegNoOverflowDecl = bvNegationNoOverflowDeclCache.createIfContextActive(value).cast() @@ -1551,6 +2170,319 @@ open class KContext : AutoCloseable { fun mkBvMulNoUnderflowDecl(arg0: T, arg1: T): KBvMulNoUnderflowDecl = bvMulNoUnderflowDeclCache.createIfContextActive(arg0, arg1).cast() + // FP + private val fp16DeclCache = mkClosableCache { value: Float -> KFp16Decl(this, value) } + fun mkFp16Decl(value: Float): KFp16Decl = fp16DeclCache.createIfContextActive(value) + + private val fp32DeclCache = mkClosableCache { value: Float -> KFp32Decl(this, value) } + fun mkFp32Decl(value: Float): KFp32Decl = fp32DeclCache.createIfContextActive(value) + + private val fp64DeclCache = mkClosableCache { value: Double -> KFp64Decl(this, value) } + fun mkFp64Decl(value: Double): KFp64Decl = fp64DeclCache.createIfContextActive(value) + + private val fp128DeclCache = mkClosableCache { significand: Long, exponent: Long, signBit: Boolean -> + KFp128Decl(this, significand, exponent, signBit) + } + + fun mkFp128Decl(significandBits: Long, exponent: Long, signBit: Boolean): KFp128Decl = + fp128DeclCache.createIfContextActive(significandBits, exponent, signBit) + + private val fpCustomSizeDeclCache = + mkClosableCache { significandSize: UInt, + exponentSize: UInt, + significand: Long, + exponent: Long, + signBit: Boolean -> + KFpCustomSizeDecl(this, significandSize, exponentSize, significand, exponent, signBit) + } + + fun mkFpCustomSizeDecl( + significandSize: UInt, + exponentSize: UInt, + significand: Long, + exponent: Long, + signBit: Boolean + ): KFpDecl { + val sort = mkFpSort(exponentSize, significandSize) + + if (sort is KFpCustomSizeSort) { + return fpCustomSizeDeclCache.createIfContextActive( + significandSize, exponentSize, significand, exponent, signBit + ).cast() + } + + if (sort is KFp128Sort) { + return fp128DeclCache.createIfContextActive(significand, exponent, signBit).cast() + } + + val intSignBit = if (signBit) 1 else 0 + + return when (sort) { + is KFp16Sort -> { + val fp16Number = constructFp16Number(exponent, significand, intSignBit) + + mkFp16Decl(fp16Number).cast() + } + is KFp32Sort -> { + val fp32Number = constructFp32Number(exponent, significand, intSignBit) + + mkFp32Decl(fp32Number).cast() + } + is KFp64Sort -> { + val fp64Number = constructFp64Number(exponent, significand, intSignBit) + + mkFp64Decl(fp64Number).cast() + } + else -> error("Sort declaration for an unknown $sort") + } + } + + private val roundingModeDeclCache = + mkClosableCache { value: KFpRoundingMode -> KFpRoundingModeDecl(this, value) } + + fun mkFpRoundingModeDecl(value: KFpRoundingMode) = roundingModeDeclCache.createIfContextActive(value) + + private val fpAbsDeclCache = mkClosableCache { valueSort: KFpSort -> KFpAbsDecl(this, valueSort) } + + fun mkFpAbsDecl(valueSort: T): KFpAbsDecl = + fpAbsDeclCache.createIfContextActive(valueSort).cast() + + private val fpNegationDeclCache = mkClosableCache { valueSort: KFpSort -> KFpNegationDecl(this, valueSort) } + + fun mkFpNegationDecl(valueSort: T): KFpNegationDecl = + fpNegationDeclCache.createIfContextActive(valueSort).cast() + + private val fpAddDeclCache = + mkClosableCache { roundingMode: KFpRoundingModeSort, arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpAddDecl(this, roundingMode, arg0Sort, arg1Sort) + } + + fun mkFpAddDecl( + roundingMode: KFpRoundingModeSort, + arg0Sort: T, + arg1Sort: T + ): KFpAddDecl = fpAddDeclCache.createIfContextActive(roundingMode, arg0Sort, arg1Sort).cast() + + private val fpSubDeclCache = + mkClosableCache { roundingMode: KFpRoundingModeSort, arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpSubDecl(this, roundingMode, arg0Sort, arg1Sort) + } + + fun mkFpSubDecl( + roundingMode: KFpRoundingModeSort, + arg0Sort: T, + arg1Sort: T + ): KFpSubDecl = fpSubDeclCache.createIfContextActive(roundingMode, arg0Sort, arg1Sort).cast() + + private val fpMulDeclCache = + mkClosableCache { roundingMode: KFpRoundingModeSort, arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpMulDecl(this, roundingMode, arg0Sort, arg1Sort) + } + + fun mkFpMulDecl( + roundingMode: KFpRoundingModeSort, + arg0Sort: T, + arg1Sort: T + ): KFpMulDecl = fpMulDeclCache.createIfContextActive(roundingMode, arg0Sort, arg1Sort).cast() + + private val fpDivDeclCache = + mkClosableCache { roundingMode: KFpRoundingModeSort, arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpDivDecl(this, roundingMode, arg0Sort, arg1Sort) + } + + fun mkFpDivDecl( + roundingMode: KFpRoundingModeSort, + arg0Sort: T, + arg1Sort: T + ): KFpDivDecl = fpDivDeclCache.createIfContextActive(roundingMode, arg0Sort, arg1Sort).cast() + + private val fpFusedMulAddDeclCache = + mkClosableCache { roundingMode: KFpRoundingModeSort, arg0sort: KFpSort, arg1Sort: KFpSort, arg2Sort: KFpSort -> + KFpFusedMulAddDecl(this, roundingMode, arg0sort, arg1Sort, arg2Sort) + } + + fun mkFpFusedMulAddDecl( + roundingMode: KFpRoundingModeSort, + arg0Sort: T, + arg1Sort: T, + arg2Sort: T + ): KFpFusedMulAddDecl = + fpFusedMulAddDeclCache.createIfContextActive(roundingMode, arg0Sort, arg1Sort, arg2Sort).cast() + + private val fpSqrtDeclCache = mkClosableCache { roundingMode: KFpRoundingModeSort, valueSort: KFpSort -> + KFpSqrtDecl(this, roundingMode, valueSort) + } + + fun mkFpSqrtDecl(roundingMode: KFpRoundingModeSort, valueSort: T): KFpSqrtDecl = + fpSqrtDeclCache.createIfContextActive(roundingMode, valueSort).cast() + + private val fpRemDeclCache = mkClosableCache { arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpRemDecl(this, arg0Sort, arg1Sort) + } + + fun mkFpRemDecl(arg0Sort: T, arg1Sort: T): KFpRemDecl = + fpRemDeclCache.createIfContextActive(arg0Sort, arg1Sort).cast() + + private val roundToIntegralDeclCache = + mkClosableCache { roundingMode: KFpRoundingModeSort, valueSort: KFpSort -> + KFpRoundToIntegralDecl(this, roundingMode, valueSort) + } + + fun mkFpRoundToIntegralDecl( + roundingMode: KFpRoundingModeSort, + valueSort: T + ): KFpRoundToIntegralDecl = roundToIntegralDeclCache.createIfContextActive(roundingMode, valueSort).cast() + + private val fpMinDeclCache = mkClosableCache { arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpMinDecl(this, arg0Sort, arg1Sort) + } + + fun mkFpMinDecl(arg0Sort: T, arg1Sort: T): KFpMinDecl = + fpMinDeclCache.createIfContextActive(arg0Sort, arg1Sort).cast() + + private val fpMaxDeclCache = mkClosableCache { arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpMaxDecl(this, arg0Sort, arg1Sort) + } + + fun mkFpMaxDecl(arg0Sort: T, arg1Sort: T): KFpMaxDecl = + fpMaxDeclCache.createIfContextActive(arg0Sort, arg1Sort).cast() + + private val fpLessOrEqualDeclCache = mkClosableCache { arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpLessOrEqualDecl(this, arg0Sort, arg1Sort) + } + + fun mkFpLessOrEqualDecl(arg0Sort: T, arg1Sort: T): KFpLessOrEqualDecl = + fpLessOrEqualDeclCache.createIfContextActive(arg0Sort, arg1Sort).cast() + + private val fpLessDeclCache = mkClosableCache { arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpLessDecl(this, arg0Sort, arg1Sort) + } + + fun mkFpLessDecl(arg0Sort: T, arg1Sort: T): KFpLessDecl = + fpLessDeclCache.createIfContextActive(arg0Sort, arg1Sort).cast() + + private val fpGreaterOrEqualDeclCache = mkClosableCache { arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpGreaterOrEqualDecl(this, arg0Sort, arg1Sort) + } + + fun mkFpGreaterOrEqualDecl(arg0Sort: T, arg1Sort: T): KFpGreaterOrEqualDecl = + fpGreaterOrEqualDeclCache.createIfContextActive(arg0Sort, arg1Sort).cast() + + private val fpGreaterDeclCache = mkClosableCache { arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpGreaterDecl(this, arg0Sort, arg1Sort) + } + + fun mkFpGreaterDecl(arg0Sort: T, arg1Sort: T): KFpGreaterDecl = + fpGreaterDeclCache.createIfContextActive(arg0Sort, arg1Sort).cast() + + private val fpEqualDeclCache = mkClosableCache { arg0Sort: KFpSort, arg1Sort: KFpSort -> + KFpEqualDecl(this, arg0Sort, arg1Sort) + } + + fun mkFpEqualDecl(arg0Sort: T, arg1Sort: T): KFpEqualDecl = + fpEqualDeclCache.createIfContextActive(arg0Sort, arg1Sort).cast() + + private val fpIsNormalDeclCache = mkClosableCache { valueSort: KFpSort -> + KFpIsNormalDecl(this, valueSort) + } + + fun mkFpIsNormalDecl(valueSort: T): KFpIsNormalDecl = + fpIsNormalDeclCache.createIfContextActive(valueSort).cast() + + private val fpIsSubnormalDeclCache = mkClosableCache { valueSort: KFpSort -> + KFpIsSubnormalDecl(this, valueSort) + } + + fun mkFpIsSubnormalDecl(valueSort: T): KFpIsSubnormalDecl = + fpIsSubnormalDeclCache.createIfContextActive(valueSort).cast() + + private val fpIsZeroDeclCache = mkClosableCache { valueSort: KFpSort -> + KFpIsZeroDecl(this, valueSort) + } + + fun mkFpIsZeroDecl(valueSort: T): KFpIsZeroDecl = + fpIsZeroDeclCache.createIfContextActive(valueSort).cast() + + private val fpIsInfiniteDeclCache = mkClosableCache { valueSort: KFpSort -> + KFpIsInfiniteDecl(this, valueSort) + } + + fun mkFpIsInfiniteDecl(valueSort: T): KFpIsInfiniteDecl = + fpIsInfiniteDeclCache.createIfContextActive(valueSort).cast() + + private val fpIsNaNDecl = mkClosableCache { valueSort: KFpSort -> + KFpIsNaNDecl(this, valueSort) + } + + fun mkFpIsNaNDecl(valueSort: T): KFpIsNaNDecl = + fpIsNaNDecl.createIfContextActive(valueSort).cast() + + private val fpIsNegativeDecl = mkClosableCache { valueSort: KFpSort -> + KFpIsNegativeDecl(this, valueSort) + } + + fun mkFpIsNegativeDecl(valueSort: T): KFpIsNegativeDecl = + fpIsNegativeDecl.createIfContextActive(valueSort).cast() + + private val fpIsPositiveDecl = mkClosableCache { valueSort: KFpSort -> + KFpIsPositiveDecl(this, valueSort) + } + + fun mkFpIsPositiveDecl(valueSort: T): KFpIsPositiveDecl = + fpIsPositiveDecl.createIfContextActive(valueSort).cast() + + private val fpToBvDeclCache = + mkClosableCache { roundingMode: KFpRoundingModeSort, valueSort: KFpSort, bvSize: Int, isSigned: Boolean -> + KFpToBvDecl(this, roundingMode, valueSort, bvSize, isSigned) + } + + fun mkFpToBvDecl( + roundingMode: KFpRoundingModeSort, + valueSort: T, + bvSize: Int, + isSigned: Boolean + ): KFpToBvDecl = fpToBvDeclCache.createIfContextActive(roundingMode, valueSort, bvSize, isSigned).cast() + + private val fpToRealDeclCache = mkClosableCache { valueSort: KFpSort -> KFpToRealDecl(this, valueSort) } + + fun mkFpToRealDecl(valueSort: T): KFpToRealDecl = + fpToRealDeclCache.createIfContextActive(valueSort).cast() + + private val fpToIEEEBvDeclCache = mkClosableCache { valueSort: KFpSort -> KFpToIEEEBvDecl(this, valueSort) } + + fun mkFpToIEEEBvDecl(valueSort: T): KFpToIEEEBvDecl = + fpToIEEEBvDeclCache.createIfContextActive(valueSort).cast() + + private val fpFromBvDeclCache = mkClosableCache { signSort: KBv1Sort, expSort: KBvSort, significandSort: KBvSort -> + val sort = mkFpSort(expSort.sizeBits, significandSort.sizeBits + 1u) + KFpFromBvDecl(this, sort, signSort, expSort, significandSort) + } + + fun mkFpFromBvDecl(signSort: KBv1Sort, expSort: KBvSort, significandSort: KBvSort): KFpFromBvDecl = + fpFromBvDeclCache.createIfContextActive(signSort, expSort, significandSort).cast() + + private val fpToFpDeclCache = mkClosableCache { sort: KFpSort, rm: KFpRoundingModeSort, value: KFpSort -> + KFpToFpDecl(this, sort, rm, value) + } + + private val realToFpDeclCache = mkClosableCache { sort: KFpSort, rm: KFpRoundingModeSort, value: KRealSort -> + KRealToFpDecl(this, sort, rm, value) + } + + private val bvToFpDeclCache = + mkClosableCache { sort: KFpSort, rm: KFpRoundingModeSort, value: KBvSort, signed: Boolean -> + KBvToFpDecl(this, sort, rm, value, signed) + } + + fun mkFpToFpDecl(sort: T, rm: KFpRoundingModeSort, value: KFpSort): KFpToFpDecl = + fpToFpDeclCache.createIfContextActive(sort, rm, value).cast() + + fun mkRealToFpDecl(sort: T, rm: KFpRoundingModeSort, value: KRealSort): KRealToFpDecl = + realToFpDeclCache.createIfContextActive(sort, rm, value).cast() + + fun mkBvToFpDecl(sort: T, rm: KFpRoundingModeSort, value: KBvSort, signed: Boolean): KBvToFpDecl = + bvToFpDeclCache.createIfContextActive(sort, rm, value, signed).cast() + /* * KAst * */ @@ -1610,6 +2542,9 @@ open class KContext : AutoCloseable { private fun mkClosableCache(builder: (A0) -> T) = ensureClosed { mkCache(builder) } private fun mkClosableCache(builder: (A0, A1) -> T) = ensureClosed { mkCache(builder) } private fun mkClosableCache(builder: (A0, A1, A2) -> T) = ensureClosed { mkCache(builder) } + private fun mkClosableCache(builder: (A0, A1, A2, A3) -> T) = ensureClosed { mkCache(builder) } + private fun mkClosableCache(builder: (A0, A1, A2, A3, A4) -> T) = + ensureClosed { mkCache(builder) } private fun Cache0.createIfContextActive(): T = ensureContextActive { create() } @@ -1623,4 +2558,10 @@ open class KContext : AutoCloseable { private fun Cache3.createIfContextActive(a0: A0, a1: A1, a2: A2): T = ensureContextActive { create(a0, a1, a2) } + private fun Cache4.createIfContextActive(a0: A0, a1: A1, a2: A2, a3: A3): T = + ensureContextActive { create(a0, a1, a2, a3) } + + private fun Cache5.createIfContextActive( + a0: A0, a1: A1, a2: A2, a3: A3, a4: A4 + ): T = ensureContextActive { create(a0, a1, a2, a3, a4) } } diff --git a/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt b/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt index 6af903d55..2ecf4b99b 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt @@ -55,6 +55,18 @@ class Cache4(val builder: (A0, A1, A2, A3) -> T) : AutoClosea } } +class Cache5(val builder: (A0, A1, A2, A3, A4) -> T) : AutoCloseable { + private val cache = HashMap, T>() + + @Suppress("unused") + fun create(a0: A0, a1: A1, a2: A2, a3: A3, a4: A4): T = + cache.getOrPut(listOf(a0, a1, a2, a3, a4)) { builder(a0, a1, a2, a3, a4) } + + override fun close() { + cache.clear() + } +} + fun mkCache(builder: () -> T) = Cache0(builder) fun mkCache(builder: (A0) -> T) = Cache1(builder) fun mkCache(builder: (A0, A1) -> T) = Cache2(builder) @@ -62,3 +74,4 @@ fun mkCache(builder: (A0, A1, A2) -> T) = Cache3(builder) @Suppress("unused") fun mkCache(builder: (A0, A1, A2, A3) -> T) = Cache4(builder) +fun mkCache(builder: (A0, A1, A2, A3, A4) -> T) = Cache5(builder) diff --git a/ksmt-core/src/main/kotlin/org/ksmt/decl/KFloatingPointDecl.kt b/ksmt-core/src/main/kotlin/org/ksmt/decl/KFloatingPointDecl.kt new file mode 100644 index 000000000..43f23ac1b --- /dev/null +++ b/ksmt-core/src/main/kotlin/org/ksmt/decl/KFloatingPointDecl.kt @@ -0,0 +1,426 @@ +package org.ksmt.decl + +import org.ksmt.KContext +import org.ksmt.expr.KApp +import org.ksmt.expr.KExpr +import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KBv1Sort +import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpRoundingModeSort +import org.ksmt.sort.KFpSort +import org.ksmt.sort.KRealSort +import org.ksmt.sort.KSort +import org.ksmt.utils.getHalfPrecisionExponent +import org.ksmt.utils.booleanSignBit +import org.ksmt.utils.getExponent +import org.ksmt.utils.halfPrecisionSignificand +import org.ksmt.utils.significand +import org.ksmt.utils.toBinary + +abstract class KFpDecl internal constructor( + ctx: KContext, + sort: T, + val sign: Boolean, + val significand: N, + val exponent: N +) : KConstDecl( + ctx, + constructNameForDeclaration(sign, sort, exponent, significand), + sort +) + +private fun constructNameForDeclaration( + sign: Boolean, + sort: T, + exponent: N, + significand: N +): String { + val exponentBits = sort.exponentBits + val binaryExponent = exponent.toBinary().takeLast(exponentBits.toInt()) + val significandBits = sort.significandBits + val binarySignificand = significand + .toBinary() + .takeLast(significandBits.toInt() - 1) + .let { it.padStart(significandBits.toInt() - 1, it[0]) } + + return "FP (sign $sign) ($exponentBits $binaryExponent) ($significandBits $binarySignificand)" +} + +class KFp16Decl internal constructor(ctx: KContext, val value: Float) : + KFpDecl( + ctx, + ctx.mkFp16Sort(), + value.booleanSignBit, + value.halfPrecisionSignificand, + value.getHalfPrecisionExponent(isBiased = false) + ) { + override fun apply(args: List>): KApp = ctx.mkFp16(value) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KFp32Decl internal constructor(ctx: KContext, val value: Float) : + KFpDecl( + ctx, + ctx.mkFp32Sort(), + value.booleanSignBit, + value.significand, + value.getExponent(isBiased = false) + ) { + override fun apply(args: List>): KApp = ctx.mkFp32(value) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KFp64Decl internal constructor(ctx: KContext, val value: Double) : + KFpDecl( + ctx, + ctx.mkFp64Sort(), + value.booleanSignBit, + value.significand, + value.getExponent(isBiased = false) + ) { + override fun apply(args: List>): KApp = ctx.mkFp64(value) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +// TODO replace significand with bit vector and change KFpDecl accordingly +class KFp128Decl internal constructor( + ctx: KContext, + significand: Long, + exponent: Long, + signBit: Boolean +) : KFpDecl(ctx, ctx.mkFp128Sort(), signBit, significand, exponent) { + override fun apply(args: List>): KApp = ctx.mkFp128(significand, exponent, sign) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KFpCustomSizeDecl internal constructor( + ctx: KContext, + significandSize: UInt, + exponentSize: UInt, + significand: Long, + exponent: Long, + signBit: Boolean +) : KFpDecl(ctx, ctx.mkFpSort(exponentSize, significandSize), signBit, significand, exponent) { + override fun apply(args: List>): KApp = + ctx.mkFpCustomSize( + sort.exponentBits, + sort.significandBits, + exponent, + significand, + sign + ) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KFpAbsDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.abs", valueSort, valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpAbsExpr(arg) +} + +class KFpNegationDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.neg", valueSort, valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpNegationExpr(arg) +} + +class KFpAddDecl internal constructor( + ctx: KContext, + roundingModeSort: KFpRoundingModeSort, + arg0Sort: T, + arg1Sort: T +) : KFuncDecl3(ctx, "fp.add", arg0Sort, roundingModeSort, arg0Sort, arg1Sort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + override fun KContext.apply(arg0: KExpr, arg1: KExpr, arg2: KExpr): KApp = + ctx.mkFpAddExpr(arg0, arg1, arg2) +} + +class KFpSubDecl internal constructor( + ctx: KContext, + roundingModeSort: KFpRoundingModeSort, + arg0Sort: T, + arg1Sort: T +) : KFuncDecl3( + ctx, "fp.sub", resultSort = arg0Sort, roundingModeSort, arg0Sort, arg1Sort +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + override fun KContext.apply(arg0: KExpr, arg1: KExpr, arg2: KExpr): KApp = + ctx.mkFpSubExpr(arg0, arg1, arg2) +} + +class KFpMulDecl internal constructor( + ctx: KContext, + roundingModeSort: KFpRoundingModeSort, + arg0Sort: T, + arg1Sort: T +) : KFuncDecl3( + ctx, "fp.mul", resultSort = arg0Sort, roundingModeSort, arg0Sort, arg1Sort +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr, arg2: KExpr): KApp = + ctx.mkFpMulExpr(arg0, arg1, arg2) +} + +class KFpDivDecl internal constructor( + ctx: KContext, + roundingModeSort: KFpRoundingModeSort, + arg0Sort: T, + arg1Sort: T +) : KFuncDecl3( + ctx, "fp.div", resultSort = arg0Sort, roundingModeSort, arg0Sort, arg1Sort +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + override fun KContext.apply(arg0: KExpr, arg1: KExpr, arg2: KExpr): KApp = + ctx.mkFpDivExpr(arg0, arg1, arg2) +} + +class KFpFusedMulAddDecl internal constructor( + ctx: KContext, + roundingModeSort: KFpRoundingModeSort, + arg0Sort: T, arg1Sort: T, arg2Sort: T +) : KFuncDecl4( + ctx, "fp.fma", resultSort = arg0Sort, roundingModeSort, arg0Sort, arg1Sort, arg2Sort +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr, + arg3: KExpr + ): KApp = ctx.mkFpFusedMulAddExpr(arg0, arg1, arg2, arg3) +} + +class KFpSqrtDecl internal constructor( + ctx: KContext, + roundingModeSort: KFpRoundingModeSort, + valueSort: T +) : KFuncDecl2(ctx, "fp.sqrt", resultSort = valueSort, roundingModeSort, valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = + ctx.mkFpSqrtExpr(arg0, arg1) +} + +class KFpRemDecl internal constructor(ctx: KContext, arg0Sort: T, arg1Sort: T) : + KFuncDecl2(ctx, "fp.rem", arg0Sort, arg0Sort, arg1Sort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = ctx.mkFpRemExpr(arg0, arg1) +} + +class KFpRoundToIntegralDecl internal constructor( + ctx: KContext, + roundingModeSort: KFpRoundingModeSort, + valueSort: T +) : KFuncDecl2( + ctx, "fp.roundToIntegral", resultSort = valueSort, roundingModeSort, valueSort +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = + ctx.mkFpRoundToIntegralExpr(arg0, arg1) +} + +class KFpMinDecl internal constructor(ctx: KContext, arg0Sort: T, arg1Sort: T) : + KFuncDecl2(ctx, "fp.min", arg0Sort, arg0Sort, arg1Sort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = ctx.mkFpMinExpr(arg0, arg1) +} + +class KFpMaxDecl internal constructor(ctx: KContext, arg0Sort: T, arg1Sort: T) : + KFuncDecl2(ctx, "fp.max", arg0Sort, arg0Sort, arg1Sort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = ctx.mkFpMaxExpr(arg0, arg1) +} + +class KFpLessOrEqualDecl internal constructor(ctx: KContext, arg0Sort: T, arg1Sort: T) : + KFuncDecl2(ctx, "fp.leq", ctx.mkBoolSort(), arg0Sort, arg1Sort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = + ctx.mkFpLessOrEqualExpr(arg0, arg1) +} + +class KFpLessDecl internal constructor(ctx: KContext, arg0Sort: T, arg1Sort: T) : + KFuncDecl2(ctx, "fp.lt", ctx.mkBoolSort(), arg0Sort, arg1Sort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = ctx.mkFpLessExpr(arg0, arg1) +} + +class KFpGreaterOrEqualDecl internal constructor(ctx: KContext, arg0Sort: T, arg1Sort: T) : + KFuncDecl2(ctx, "fp.geq", ctx.mkBoolSort(), arg0Sort, arg1Sort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = + ctx.mkFpGreaterOrEqualExpr(arg0, arg1) +} + +class KFpGreaterDecl internal constructor(ctx: KContext, arg0Sort: T, arg1Sort: T) : + KFuncDecl2(ctx, "fp.gt", ctx.mkBoolSort(), arg0Sort, arg1Sort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = ctx.mkFpGreaterExpr(arg0, arg1) +} + +class KFpEqualDecl internal constructor(ctx: KContext, arg0Sort: T, arg1Sort: T) : + KFuncDecl2(ctx, "fp.eq", ctx.mkBoolSort(), arg0Sort, arg1Sort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = ctx.mkFpEqualExpr(arg0, arg1) +} + +class KFpIsNormalDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.isNormal", ctx.mkBoolSort(), valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpIsNormalExpr(arg) +} + +class KFpIsSubnormalDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.isSubnormal", ctx.mkBoolSort(), valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpIsSubnormalExpr(arg) +} + +class KFpIsZeroDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.isZero", ctx.mkBoolSort(), valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpIsZeroExpr(arg) +} + +class KFpIsInfiniteDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.isInfinite", ctx.mkBoolSort(), valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpIsInfiniteExpr(arg) +} + +class KFpIsNaNDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.isNaN", ctx.mkBoolSort(), valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpIsNaNExpr(arg) +} + +class KFpIsNegativeDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.isNegative", ctx.mkBoolSort(), valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpIsNegativeExpr(arg) +} + +class KFpIsPositiveDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.isPositive", ctx.mkBoolSort(), valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpIsPositiveExpr(arg) +} + +class KFpToBvDecl internal constructor( + ctx: KContext, + roundingModeSort: KFpRoundingModeSort, + valueSort: T, + val bvSize: Int, + val isSigned: Boolean +) : KFuncDecl2( + ctx, + "fp.to_${if (isSigned) "s" else "u"}bv", + ctx.mkBvSort(bvSize.toUInt()), + roundingModeSort, + valueSort +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = + ctx.mkFpToBvExpr(arg0, arg1, bvSize, isSigned) +} + +class KFpToRealDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1(ctx, "fp.to_real", ctx.mkRealSort(), valueSort) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpToRealExpr(arg) +} + +class KFpToIEEEBvDecl internal constructor(ctx: KContext, valueSort: T) : + KFuncDecl1( + ctx, + "fp.to_ieee_bv", + ctx.mkBvSort(valueSort.significandBits + valueSort.exponentBits), + valueSort + ) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp> = ctx.mkFpToIEEEBvExpr(arg) +} + +class KFpFromBvDecl internal constructor( + ctx: KContext, + sort: T, + signSort: KBv1Sort, + expSort: KBvSort, + significandSort: KBvSort +) : KFuncDecl3(ctx, "fp.to_fp", sort, signSort, expSort, significandSort) { + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg0: KExpr, arg1: KExpr, arg2: KExpr): KApp = + ctx.mkFpFromBvExpr(arg0, arg1, arg2) +} + +abstract class KToFpDecl internal constructor( + ctx: KContext, + sort: T, + roundingModeSort: KFpRoundingModeSort, + valueSort: S +) : KFuncDecl2(ctx, "fp.to_fp", resultSort = sort, roundingModeSort, valueSort) { + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KFpToFpDecl internal constructor( + ctx: KContext, + sort: T, + roundingModeSort: KFpRoundingModeSort, + valueSort: KFpSort +) : KToFpDecl(ctx, sort, roundingModeSort, valueSort) { + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = + ctx.mkFpToFpExpr(sort, arg0, arg1) +} + +class KRealToFpDecl internal constructor( + ctx: KContext, + sort: T, + roundingModeSort: KFpRoundingModeSort, + valueSort: KRealSort +) : KToFpDecl(ctx, sort, roundingModeSort, valueSort) { + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = + ctx.mkRealToFpExpr(sort, arg0, arg1) +} + +class KBvToFpDecl internal constructor( + ctx: KContext, + sort: T, + roundingModeSort: KFpRoundingModeSort, + valueSort: KBvSort, + val signed: Boolean +) : KToFpDecl(ctx, sort, roundingModeSort, valueSort) { + override fun KContext.apply(arg0: KExpr, arg1: KExpr): KApp = + ctx.mkBvToFpExpr(sort, arg0, arg1, signed) +} diff --git a/ksmt-core/src/main/kotlin/org/ksmt/decl/KFpRoundingModeDecl.kt b/ksmt-core/src/main/kotlin/org/ksmt/decl/KFpRoundingModeDecl.kt new file mode 100644 index 000000000..95eec74bf --- /dev/null +++ b/ksmt-core/src/main/kotlin/org/ksmt/decl/KFpRoundingModeDecl.kt @@ -0,0 +1,14 @@ +package org.ksmt.decl + +import org.ksmt.KContext +import org.ksmt.expr.KApp +import org.ksmt.expr.KExpr +import org.ksmt.expr.KFpRoundingMode +import org.ksmt.sort.KFpRoundingModeSort + +class KFpRoundingModeDecl(ctx: KContext, val value: KFpRoundingMode) : + KConstDecl(ctx, value.modeName, ctx.mkFpRoundingModeSort()) { + override fun apply(args: List>): KApp = ctx.mkFpRoundingModeExpr(value) + + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} diff --git a/ksmt-core/src/main/kotlin/org/ksmt/decl/KFuncDecl.kt b/ksmt-core/src/main/kotlin/org/ksmt/decl/KFuncDecl.kt index c0cb68e4b..824d1b94a 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/decl/KFuncDecl.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/decl/KFuncDecl.kt @@ -95,6 +95,26 @@ abstract class KFuncDecl3( } } +@Suppress("LongParameterList") +abstract class KFuncDecl4( + ctx: KContext, + name: String, + resultSort: T, + val arg0Sort: A0, + val arg1Sort: A1, + val arg2Sort: A2, + val arg3Sort: A3 +) : KFuncDecl(ctx, name, resultSort, listOf(arg0Sort, arg1Sort, arg2Sort, arg3Sort)) { + abstract fun KContext.apply(arg0: KExpr, arg1: KExpr, arg2: KExpr, arg3: KExpr): KApp + + @Suppress("UNCHECKED_CAST") + override fun apply(args: List>): KApp = with(ctx) { + checkArgSorts(args) + val (arg0, arg1, arg2, arg3) = args + return apply(arg0 as KExpr, arg1 as KExpr, arg2 as KExpr, arg3 as KExpr) + } +} + interface KParameterizedFuncDecl { val parameters: List } diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt index c51b4be29..adc9eddd0 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/KBitVecExprs.kt @@ -11,16 +11,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( ctx: KContext ) : KApp>(ctx) { override val args: List> = emptyList() + + abstract val stringValue: String } class KBitVec1Value internal constructor(ctx: KContext, val value: Boolean) : KBitVecValue(ctx) { override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) + override val stringValue: String = if (value) "1" else "0" + override fun decl(): KDecl = ctx.mkBvDecl(value) override fun sort(): KBv1Sort = ctx.mkBv1Sort() @@ -29,7 +34,9 @@ class KBitVec1Value internal constructor(ctx: KContext, val value: Boolean) : KB abstract class KBitVecNumberValue( ctx: KContext, val numberValue: N -) : KBitVecValue(ctx) +) : KBitVecValue(ctx) { + override val stringValue: String = numberValue.toBinary() +} class KBitVec8Value internal constructor(ctx: KContext, byteValue: Byte) : KBitVecNumberValue(ctx, byteValue) { @@ -81,6 +88,8 @@ class KBitVecCustomValue internal constructor( override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) + override val stringValue: String = binaryStringValue + override fun decl(): KDecl = 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 new file mode 100644 index 000000000..779519263 --- /dev/null +++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/KFloatingPointExpr.kt @@ -0,0 +1,640 @@ +package org.ksmt.expr + +import org.ksmt.KContext +import org.ksmt.decl.KDecl +import org.ksmt.expr.transformer.KTransformer +import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KBv1Sort +import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpRoundingModeSort +import org.ksmt.sort.KFpSort +import org.ksmt.sort.KRealSort +import org.ksmt.utils.booleanSignBit +import org.ksmt.utils.getExponent +import org.ksmt.utils.getHalfPrecisionExponent +import org.ksmt.utils.halfPrecisionSignificand +import org.ksmt.utils.significand + +abstract class KFpValue( + ctx: KContext, + val significand: KBitVecValue, + val exponent: KBitVecValue, + val signBit: Boolean +) : KApp>(ctx) { + override val args: List> = emptyList() + + companion object { + const val MAX_EXPONENT_SIZE = 63 + } +} + +/** + * Fp16 value. Note that [value] should has biased Fp32 exponent, + * but a constructed Fp16 will have an unbiased one. + * + * Fp32 to Fp16 transformation: + * sign exponent significand + * 0 00000000 00000000000000000000000 (1 8 23) + * x x___xxxx xxxxxxxxxx_____________ (1 5 10) + */ +class KFp16Value internal constructor(ctx: KContext, val value: Float) : + KFpValue( + ctx, + significand = with(ctx) { value.halfPrecisionSignificand.toBv(KFp16Sort.significandBits - 1u) }, + exponent = with(ctx) { value.getHalfPrecisionExponent(isBiased = false).toBv(KFp16Sort.exponentBits) }, + signBit = value.booleanSignBit + ) { + + init { + // TODO add checks for the bounds + } + + override fun decl(): KDecl = ctx.mkFp16Decl(value) + + override fun sort(): KFp16Sort = ctx.mkFp16Sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFp32Value internal constructor(ctx: KContext, val value: Float) : + KFpValue( + ctx, + significand = with(ctx) { value.significand.toBv(KFp32Sort.significandBits - 1u) }, + exponent = with(ctx) { value.getExponent(isBiased = false).toBv(KFp32Sort.exponentBits) }, + signBit = value.booleanSignBit + ) { + override fun decl(): KDecl = ctx.mkFp32Decl(value) + + override fun sort(): KFp32Sort = ctx.mkFp32Sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFp64Value internal constructor(ctx: KContext, val value: Double) : + KFpValue( + ctx, + significand = with(ctx) { value.significand.toBv(KFp64Sort.significandBits - 1u) }, + exponent = with(ctx) { value.getExponent(isBiased = false).toBv(KFp64Sort.exponentBits) }, + signBit = value.booleanSignBit + ) { + override fun decl(): KDecl = ctx.mkFp64Decl(value) + + override fun sort(): KFp64Sort = ctx.mkFp64Sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +/** + * KFp128 value. + * + * Note: if [exponentValue] contains more than [KFp128Sort.exponentBits] meaningful bits, + * only the last [KFp128Sort.exponentBits] of then will be taken. + */ +class KFp128Value internal constructor( + ctx: KContext, + val significandValue: Long, + val exponentValue: Long, + signBit: Boolean +) : KFpValue( + ctx, + significand = with(ctx) { significandValue.toBv(KFp128Sort.significandBits - 1u) }, + exponent = with(ctx) { exponentValue.toBv(KFp128Sort.exponentBits) }, + signBit +) { + override fun decl(): KDecl = ctx.mkFp128Decl(significandValue, exponentValue, signBit) + + override fun sort(): KFp128Sort = ctx.mkFp128Sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +/** + * KFp value of custom size. + * + * Note: if [exponentValue] contains more than [KFp128Sort.exponentBits] meaningful bits, + * only the last [KFp128Sort.exponentBits] of then will be taken. + * The same is true for the significand. + */ +class KFpCustomSizeValue internal constructor( + ctx: KContext, + val significandSize: UInt, + val exponentSize: UInt, + val significandValue: Long, + val exponentValue: Long, + signBit: Boolean +) : KFpValue( + ctx, + significand = with(ctx) { significandValue.toBv(significandSize - 1u) }, + exponent = with(ctx) { exponentValue.toBv(exponentSize) }, + signBit +) { + init { + require(exponentSize.toInt() <= MAX_EXPONENT_SIZE) { + "Maximum number of exponent bits is $MAX_EXPONENT_SIZE" + } + } + + override fun decl(): KDecl = + ctx.mkFpCustomSizeDecl(significandSize, exponentSize, significandValue, exponentValue, signBit) + + override fun sort(): KFpSort = ctx.mkFpSort(exponentSize, significandSize) + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpAbsExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpAbsDecl(value.sort()) + + override fun sort(): S = value.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +/** + * Inverts the sign bit. + */ +class KFpNegationExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpNegationDecl(value.sort()) + + override fun sort(): S = value.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +// TODO Can they have different sorts? +class KFpAddExpr internal constructor( + ctx: KContext, + val roundingMode: KExpr, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, arg0, arg1) + + override fun decl(): KDecl = with(ctx) { mkFpAddDecl(roundingMode.sort, arg0.sort, arg1.sort) } + + override fun sort(): S = arg0.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpSubExpr internal constructor( + ctx: KContext, + val roundingMode: KExpr, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, arg0, arg1) + + override fun decl(): KDecl = with(ctx) { mkFpSubDecl(roundingMode.sort, arg0.sort, arg1.sort) } + + override fun sort(): S = arg0.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpMulExpr internal constructor( + ctx: KContext, + val roundingMode: KExpr, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, arg0, arg1) + + override fun decl(): KDecl = with(ctx) { mkFpMulDecl(roundingMode.sort, arg0.sort, arg1.sort) } + + override fun sort(): S = arg0.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpDivExpr internal constructor( + ctx: KContext, + val roundingMode: KExpr, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, arg0, arg1) + + override fun decl(): KDecl = with(ctx) { mkFpDivDecl(roundingMode.sort, arg0.sort, arg1.sort) } + + override fun sort(): S = arg0.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpFusedMulAddExpr internal constructor( + ctx: KContext, + val roundingMode: KExpr, + val arg0: KExpr, + val arg1: KExpr, + val arg2: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, arg0, arg1, arg2) + + override fun decl(): KDecl = with(ctx) { + mkFpFusedMulAddDecl( + roundingMode.sort, + arg0.sort, + arg1.sort, + arg2.sort + ) + } + + override fun sort(): S = arg0.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) + +} + +class KFpSqrtExpr internal constructor( + ctx: KContext, + val roundingMode: KExpr, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, value) + + override fun decl(): KDecl = with(ctx) { mkFpSqrtDecl(roundingMode.sort, value.sort) } + + override fun sort(): S = value.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) + +} + +class KFpRemExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(arg0, arg1) + + override fun decl(): KDecl = ctx.mkFpRemDecl(arg0.sort(), arg1.sort()) + + override fun sort(): S = arg0.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpRoundToIntegralExpr internal constructor( + ctx: KContext, + val roundingMode: KExpr, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, value) + + override fun decl(): KDecl = with(ctx) { mkFpRoundToIntegralDecl(roundingMode.sort, value.sort) } + + override fun sort(): S = value.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) + +} + +class KFpMinExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(arg0, arg1) + + override fun decl(): KDecl = ctx.mkFpMinDecl(arg0.sort(), arg1.sort()) + + override fun sort(): S = arg0.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpMaxExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(arg0, arg1) + + override fun decl(): KDecl = ctx.mkFpMaxDecl(arg0.sort(), arg1.sort()) + + override fun sort(): S = arg0.sort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpLessOrEqualExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(arg0, arg1) + + override fun decl(): KDecl = ctx.mkFpLessOrEqualDecl(arg0.sort(), arg1.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpLessExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(arg0, arg1) + + override fun decl(): KDecl = ctx.mkFpLessDecl(arg0.sort(), arg1.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpGreaterOrEqualExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(arg0, arg1) + + override fun decl(): KDecl = ctx.mkFpGreaterOrEqualDecl(arg0.sort(), arg1.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpGreaterExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(arg0, arg1) + + override fun decl(): KDecl = ctx.mkFpGreaterDecl(arg0.sort(), arg1.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpEqualExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(arg0, arg1) + + override fun decl(): KDecl = ctx.mkFpEqualDecl(arg0.sort(), arg1.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpIsNormalExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpIsNormalDecl(value.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpIsSubnormalExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpIsSubnormalDecl(value.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpIsZeroExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpIsZeroDecl(value.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpIsInfiniteExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpIsInfiniteDecl(value.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpIsNaNExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpIsNaNDecl(value.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpIsNegativeExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpIsNegativeDecl(value.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpIsPositiveExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpIsPositiveDecl(value.sort()) + + override fun sort(): KBoolSort = ctx.mkBoolSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +// TODO mkFpToFp ??? + +class KFpToBvExpr internal constructor( + ctx: KContext, + val roundingMode: KExpr, + val value: KExpr, + val bvSize: Int, + val isSigned: Boolean +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, value) + + override fun decl(): KDecl = with(ctx) { mkFpToBvDecl(roundingMode.sort, value.sort, bvSize, isSigned) } + + override fun sort(): KBvSort = decl().sort + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) + +} + +class KFpToRealExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpToRealDecl(value.sort()) + + override fun sort(): KRealSort = ctx.mkRealSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpToIEEEBvExpr internal constructor( + ctx: KContext, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(value) + + override fun decl(): KDecl = ctx.mkFpToIEEEBvDecl(value.sort()) + + override fun sort(): KBvSort = decl().sort + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpFromBvExpr internal constructor( + ctx: KContext, + val sort: S, + val sign: KExpr, + val exponent: KExpr, + val significand: KExpr, +) : KApp>(ctx) { + override val args: List> + get() = listOf(sign, exponent, significand) + + override fun decl(): KDecl = with(ctx) { + mkFpFromBvDecl(sign.sort, exponent.sort, significand.sort) + } + + override fun sort(): S = sort + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KFpToFpExpr internal constructor( + ctx: KContext, + val sort: S, + val roundingMode: KExpr, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, value) + + override fun decl(): KDecl = with(ctx) { + mkFpToFpDecl(sort, roundingMode.sort, value.sort) + } + + override fun sort(): S = sort + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KRealToFpExpr internal constructor( + ctx: KContext, + val sort: S, + val roundingMode: KExpr, + val value: KExpr +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, value) + + override fun decl(): KDecl = with(ctx) { + mkRealToFpDecl(sort, roundingMode.sort, value.sort) + } + + override fun sort(): S = sort + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} + +class KBvToFpExpr internal constructor( + ctx: KContext, + val sort: S, + val roundingMode: KExpr, + val value: KExpr, + val signed: Boolean +) : KApp>(ctx) { + override val args: List> + get() = listOf(roundingMode, value) + + override fun decl(): KDecl = with(ctx) { + mkBvToFpDecl(sort, roundingMode.sort, value.sort, signed) + } + + override fun sort(): S = sort + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/KFpRoundingMode.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/KFpRoundingMode.kt new file mode 100644 index 000000000..c764f6803 --- /dev/null +++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/KFpRoundingMode.kt @@ -0,0 +1,25 @@ +package org.ksmt.expr + +import org.ksmt.KContext +import org.ksmt.decl.KDecl +import org.ksmt.expr.transformer.KTransformer +import org.ksmt.sort.KFpRoundingModeSort + +enum class KFpRoundingMode(val modeName: String) { + RoundNearestTiesToEven("RoundNearestTiesToEven"), + RoundNearestTiesToAway("RoundNearestTiesToAway"), + RoundTowardPositive("RoundTowardPositive"), + RoundTowardNegative("RoundTowardNegative"), + RoundTowardZero("RoundTowardZero") +} + +class KFpRoundingModeExpr(ctx: KContext, val value: KFpRoundingMode): KApp>(ctx) { + override val args: List> + get() = emptyList() + + override fun decl(): KDecl = ctx.mkFpRoundingModeDecl(value) + + override fun sort(): KFpRoundingModeSort = ctx.mkFpRoundingModeSort() + + override fun accept(transformer: KTransformer): KExpr = transformer.transform(this) +} diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt index 164f70f90..1d96693e6 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KTransformer.kt @@ -53,6 +53,7 @@ import org.ksmt.expr.KBvSignedRemExpr import org.ksmt.expr.KBvSubExpr import org.ksmt.expr.KBvSubNoOverflowExpr import org.ksmt.expr.KBvSubNoUnderflowExpr +import org.ksmt.expr.KBvToFpExpr import org.ksmt.expr.KBvUnsignedDivExpr import org.ksmt.expr.KBvUnsignedGreaterExpr import org.ksmt.expr.KBvUnsignedGreaterOrEqualExpr @@ -69,6 +70,42 @@ import org.ksmt.expr.KEqExpr import org.ksmt.expr.KExistentialQuantifier import org.ksmt.expr.KExpr import org.ksmt.expr.KFalse +import org.ksmt.expr.KFp128Value +import org.ksmt.expr.KFp16Value +import org.ksmt.expr.KFp32Value +import org.ksmt.expr.KFp64Value +import org.ksmt.expr.KFpAbsExpr +import org.ksmt.expr.KFpAddExpr +import org.ksmt.expr.KFpCustomSizeValue +import org.ksmt.expr.KFpDivExpr +import org.ksmt.expr.KFpEqualExpr +import org.ksmt.expr.KFpFromBvExpr +import org.ksmt.expr.KFpFusedMulAddExpr +import org.ksmt.expr.KFpGreaterExpr +import org.ksmt.expr.KFpGreaterOrEqualExpr +import org.ksmt.expr.KFpIsInfiniteExpr +import org.ksmt.expr.KFpIsNaNExpr +import org.ksmt.expr.KFpIsNegativeExpr +import org.ksmt.expr.KFpIsNormalExpr +import org.ksmt.expr.KFpIsPositiveExpr +import org.ksmt.expr.KFpIsSubnormalExpr +import org.ksmt.expr.KFpIsZeroExpr +import org.ksmt.expr.KFpLessExpr +import org.ksmt.expr.KFpLessOrEqualExpr +import org.ksmt.expr.KFpMaxExpr +import org.ksmt.expr.KFpMinExpr +import org.ksmt.expr.KFpMulExpr +import org.ksmt.expr.KFpNegationExpr +import org.ksmt.expr.KFpRemExpr +import org.ksmt.expr.KFpRoundToIntegralExpr +import org.ksmt.expr.KFpRoundingModeExpr +import org.ksmt.expr.KFpSqrtExpr +import org.ksmt.expr.KFpSubExpr +import org.ksmt.expr.KFpToBvExpr +import org.ksmt.expr.KFpToFpExpr +import org.ksmt.expr.KFpToIEEEBvExpr +import org.ksmt.expr.KFpToRealExpr +import org.ksmt.expr.KFpValue import org.ksmt.expr.KFunctionApp import org.ksmt.expr.KFunctionAsArray import org.ksmt.expr.KGeArithExpr @@ -88,6 +125,7 @@ import org.ksmt.expr.KNotExpr import org.ksmt.expr.KOrExpr import org.ksmt.expr.KPowerArithExpr import org.ksmt.expr.KRealNumExpr +import org.ksmt.expr.KRealToFpExpr import org.ksmt.expr.KRemIntExpr import org.ksmt.expr.KSubArithExpr import org.ksmt.expr.KToIntRealExpr @@ -96,17 +134,23 @@ import org.ksmt.expr.KTrue import org.ksmt.expr.KUnaryMinusArithExpr import org.ksmt.expr.KUniversalQuantifier import org.ksmt.expr.KXorExpr -import org.ksmt.sort.KArraySort import org.ksmt.sort.KArithSort +import org.ksmt.sort.KArraySort +import org.ksmt.sort.KBoolSort import org.ksmt.sort.KBv16Sort import org.ksmt.sort.KBv1Sort import org.ksmt.sort.KBv32Sort import org.ksmt.sort.KBv64Sort import org.ksmt.sort.KBv8Sort +import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpRoundingModeSort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KIntSort import org.ksmt.sort.KRealSort -import org.ksmt.sort.KBvSort -import org.ksmt.sort.KBoolSort import org.ksmt.sort.KSort @@ -146,53 +190,98 @@ interface KTransformer { fun transform(expr: KBitVecCustomValue): KExpr = transformBitVecValue(expr) // bit-vec expressions transformers - fun transform(expr: KBvNotExpr): KExpr = transformApp(expr) - fun transform(expr: KBvReductionAndExpr): KExpr = transformApp(expr) - fun transform(expr: KBvReductionOrExpr): KExpr = transformApp(expr) - fun transform(expr: KBvAndExpr): KExpr = transformApp(expr) - fun transform(expr: KBvOrExpr): KExpr = transformApp(expr) - fun transform(expr: KBvXorExpr): KExpr = transformApp(expr) - fun transform(expr: KBvNAndExpr): KExpr = transformApp(expr) - fun transform(expr: KBvNorExpr): KExpr = transformApp(expr) - fun transform(expr: KBvXNorExpr): KExpr = transformApp(expr) - fun transform(expr: KBvNegationExpr): KExpr = transformApp(expr) - fun transform(expr: KBvAddExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSubExpr): KExpr = transformApp(expr) - fun transform(expr: KBvMulExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedDivExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedDivExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedRemExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedRemExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedModExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedLessExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedLessExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedLessOrEqualExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedLessOrEqualExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedGreaterOrEqualExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedGreaterOrEqualExpr): KExpr = transformApp(expr) - fun transform(expr: KBvUnsignedGreaterExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSignedGreaterExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNotExpr): KExpr = transformApp(expr) + fun transform(expr: KBvReductionAndExpr): KExpr = transformApp(expr) + fun transform(expr: KBvReductionOrExpr): KExpr = transformApp(expr) + fun transform(expr: KBvAndExpr): KExpr = transformApp(expr) + fun transform(expr: KBvOrExpr): KExpr = transformApp(expr) + fun transform(expr: KBvXorExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNAndExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNorExpr): KExpr = transformApp(expr) + fun transform(expr: KBvXNorExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNegationExpr): KExpr = transformApp(expr) + fun transform(expr: KBvAddExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSubExpr): KExpr = transformApp(expr) + fun transform(expr: KBvMulExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedDivExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedDivExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedRemExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedRemExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedModExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedLessExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedLessExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedLessOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedLessOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedGreaterOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedGreaterOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KBvUnsignedGreaterExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSignedGreaterExpr): KExpr = transformApp(expr) fun transform(expr: KBvConcatExpr): KExpr = transformApp(expr) fun transform(expr: KBvExtractExpr): KExpr = transformApp(expr) fun transform(expr: KBvSignExtensionExpr): KExpr = transformApp(expr) fun transform(expr: KBvZeroExtensionExpr): KExpr = transformApp(expr) fun transform(expr: KBvRepeatExpr): KExpr = transformApp(expr) - fun transform(expr: KBvShiftLeftExpr): KExpr = transformApp(expr) - fun transform(expr: KBvLogicalShiftRightExpr): KExpr = transformApp(expr) - fun transform(expr: KBvArithShiftRightExpr): KExpr = transformApp(expr) - fun transform(expr: KBvRotateLeftExpr): KExpr = transformApp(expr) - fun transform(expr: KBvRotateLeftIndexedExpr): KExpr = transformApp(expr) - fun transform(expr: KBvRotateRightExpr): KExpr = transformApp(expr) - fun transform(expr: KBvRotateRightIndexedExpr): KExpr = transformApp(expr) + fun transform(expr: KBvShiftLeftExpr): KExpr = transformApp(expr) + fun transform(expr: KBvLogicalShiftRightExpr): KExpr = transformApp(expr) + fun transform(expr: KBvArithShiftRightExpr): KExpr = transformApp(expr) + fun transform(expr: KBvRotateLeftExpr): KExpr = transformApp(expr) + fun transform(expr: KBvRotateLeftIndexedExpr): KExpr = transformApp(expr) + fun transform(expr: KBvRotateRightExpr): KExpr = transformApp(expr) + fun transform(expr: KBvRotateRightIndexedExpr): KExpr = transformApp(expr) fun transform(expr: KBv2IntExpr): KExpr = transformApp(expr) - fun transform(expr: KBvAddNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvAddNoUnderflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSubNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvSubNoUnderflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvDivNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvNegNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvMulNoOverflowExpr): KExpr = transformApp(expr) - fun transform(expr: KBvMulNoUnderflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvAddNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvAddNoUnderflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSubNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvSubNoUnderflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvDivNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvNegNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvMulNoOverflowExpr): KExpr = transformApp(expr) + fun transform(expr: KBvMulNoUnderflowExpr): KExpr = transformApp(expr) + + // fp value transformers + fun transformFpValue(expr: KFpValue): KExpr = transformApp(expr) + fun transform(expr: KFp16Value): KExpr = transformFpValue(expr) + fun transform(expr: KFp32Value): KExpr = transformFpValue(expr) + fun transform(expr: KFp64Value): KExpr = transformFpValue(expr) + fun transform(expr: KFp128Value): KExpr = transformFpValue(expr) + fun transform(expr: KFpCustomSizeValue): KExpr = transformFpValue(expr) + + // fp rounding mode + fun transform(expr: KFpRoundingModeExpr): KExpr = transformApp(expr) + + // fp operations tranformation + fun transform(expr: KFpAbsExpr): KExpr = transformApp(expr) + fun transform(expr: KFpNegationExpr): KExpr = transformApp(expr) + fun transform(expr: KFpAddExpr): KExpr = transformApp(expr) + fun transform(expr: KFpSubExpr): KExpr = transformApp(expr) + fun transform(expr: KFpMulExpr): KExpr = transformApp(expr) + fun transform(expr: KFpDivExpr): KExpr = transformApp(expr) + fun transform(expr: KFpFusedMulAddExpr): KExpr = transformApp(expr) + fun transform(expr: KFpSqrtExpr): KExpr = transformApp(expr) + fun transform(expr: KFpRemExpr): KExpr = transformApp(expr) + @Suppress("MaxLineLength") + fun transform(expr: KFpRoundToIntegralExpr): KExpr = transformApp(expr) + fun transform(expr: KFpMinExpr): KExpr = transformApp(expr) + fun transform(expr: KFpMaxExpr): KExpr = transformApp(expr) + fun transform(expr: KFpLessOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KFpLessExpr): KExpr = transformApp(expr) + fun transform(expr: KFpGreaterOrEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KFpGreaterExpr): KExpr = transformApp(expr) + fun transform(expr: KFpEqualExpr): KExpr = transformApp(expr) + fun transform(expr: KFpIsNormalExpr): KExpr = transformApp(expr) + fun transform(expr: KFpIsSubnormalExpr): KExpr = transformApp(expr) + fun transform(expr: KFpIsZeroExpr): KExpr = transformApp(expr) + fun transform(expr: KFpIsInfiniteExpr): KExpr = transformApp(expr) + fun transform(expr: KFpIsNaNExpr): KExpr = transformApp(expr) + fun transform(expr: KFpIsNegativeExpr): KExpr = transformApp(expr) + fun transform(expr: KFpIsPositiveExpr): KExpr = transformApp(expr) + fun transform(expr: KFpToBvExpr): KExpr = transformApp(expr) + fun transform(expr: KFpToRealExpr): KExpr = transformApp(expr) + fun transform(expr: KFpToIEEEBvExpr): KExpr = transformApp(expr) + fun transform(expr: KFpFromBvExpr): KExpr = transformApp(expr) + fun transform(expr: KFpToFpExpr): KExpr = transformApp(expr) + fun transform(expr: KRealToFpExpr): KExpr = transformApp(expr) + fun transform(expr: KBvToFpExpr): KExpr = transformApp(expr) // array transformers fun transform(expr: KArrayStore): KExpr> = transformApp(expr) diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt index b5f0968b6..e9fb60caf 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/model/KModelEvaluator.kt @@ -12,6 +12,7 @@ import org.ksmt.expr.KApp import org.ksmt.expr.KBitVecValue import org.ksmt.expr.KEqExpr import org.ksmt.expr.KFalse +import org.ksmt.expr.KFpRoundingMode import org.ksmt.expr.KIntNumExpr import org.ksmt.expr.KIteExpr import org.ksmt.expr.KNotExpr @@ -21,6 +22,8 @@ import org.ksmt.expr.KTrue import org.ksmt.sort.KArraySort import org.ksmt.sort.KBvSort import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KFpRoundingModeSort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KIntSort import org.ksmt.sort.KRealSort import org.ksmt.sort.KSort @@ -162,8 +165,13 @@ open class KModelEvaluator( override fun visit(sort: KIntSort): KExpr = 0.intExpr as KExpr override fun visit(sort: KRealSort): KExpr = mkRealNum(0) as KExpr override fun visit(sort: S): KExpr = mkBv("0", sort.sizeBits) as KExpr + override fun visit(sort: S): KExpr = mkFp(0f, sort) as KExpr + override fun visit(sort: KFpRoundingModeSort): KExpr = + mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero) as KExpr + override fun visit(sort: KArraySort): KExpr = mkArrayConst(sort, sort.range.sampleValue()) as KExpr + override fun visit(sort: KUninterpretedSort): KExpr = error("Uninterpreted sort has no values") }) diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/util/KExprConverterBase.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/util/KExprConverterBase.kt index f4c12980e..ea3d720f4 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/solver/util/KExprConverterBase.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/util/KExprConverterBase.kt @@ -88,6 +88,19 @@ abstract class KExprConverterBase { op(convertedArgs[0] as KExpr, convertedArgs[1] as KExpr, convertedArgs[2] as KExpr) } + @Suppress("UNCHECKED_CAST", "MagicNumber") + inline fun T.convert( + args: Array, + op: (KExpr, KExpr, KExpr, KExpr) -> KExpr + ) = ensureArgsConvertedAndConvert(this, args, expectedSize = 4) { convertedArgs -> + op( + convertedArgs[0] as KExpr, + convertedArgs[1] as KExpr, + convertedArgs[2] as KExpr, + convertedArgs[3] as KExpr + ) + } + @Suppress("UNCHECKED_CAST") inline fun T.convertList( args: Array, diff --git a/ksmt-core/src/main/kotlin/org/ksmt/solver/util/KExprInternalizerBase.kt b/ksmt-core/src/main/kotlin/org/ksmt/solver/util/KExprInternalizerBase.kt index c5f6787a8..f2885e791 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/solver/util/KExprInternalizerBase.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/solver/util/KExprInternalizerBase.kt @@ -1,6 +1,7 @@ package org.ksmt.solver.util import org.ksmt.expr.KExpr +import org.ksmt.expr.KFpRoundingMode import org.ksmt.expr.transformer.KTransformer import org.ksmt.solver.util.KExprInternalizerBase.ExprInternalizationResult.Companion.argumentsInternalizationRequired import org.ksmt.solver.util.KExprInternalizerBase.ExprInternalizationResult.Companion.notInitializedInternalizationResult @@ -109,6 +110,42 @@ abstract class KExprInternalizerBase : KTransformer { } } + inline fun > S.transform( + arg0: KExpr<*>, + arg1: KExpr<*>, + arg2: KExpr<*>, + arg3: KExpr<*>, + operation: (A0, A1, A2, A3) -> T + ): S = also { + val internalizedArg0 = findInternalizedExpr(arg0) + val internalizedArg1 = findInternalizedExpr(arg1) + val internalizedArg2 = findInternalizedExpr(arg2) + val internalizedArg3 = findInternalizedExpr(arg3) + + val args = listOf(internalizedArg0, internalizedArg1, internalizedArg2, internalizedArg3) + val someArgumentIsNull = args.any { it == null } + + if (someArgumentIsNull) { + exprStack.add(this) + + internalizedArg0 ?: exprStack.add(arg0) + internalizedArg1 ?: exprStack.add(arg1) + internalizedArg2 ?: exprStack.add(arg2) + internalizedArg3 ?: exprStack.add(arg3) + + lastExprInternalizationResult = argumentsInternalizationRequired + } else { + lastExprInternalizationResult = ExprInternalizationResult( + operation( + internalizedArg0 as A0, + internalizedArg1 as A1, + internalizedArg2 as A2, + internalizedArg3 as A3 + ) + ) + } + } + inline fun > S.transformList( args: List>, operation: (Array) -> T diff --git a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt index bb9d63578..90d878c12 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSort.kt @@ -95,3 +95,64 @@ class KUninterpretedSort internal constructor(val name: String, ctx: KContext) : builder.append(name) } } + +sealed class KFpSort(ctx: KContext, val exponentBits: UInt, val significandBits: UInt) : KSort(ctx) { + override fun print(builder: StringBuilder) { + builder.append("FP (eBits: $exponentBits) (sBits: $significandBits)") + } + override fun accept(visitor: KSortVisitor): T = visitor.visit(this) + abstract fun exponentShiftSize(): Int +} + +class KFp16Sort(ctx: KContext) : KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = exponentShiftSize + + companion object { + val exponentBits: UInt = 5.toUInt() + val significandBits: UInt = 11.toUInt() + const val exponentShiftSize: Int = 15 + } +} + +class KFp32Sort(ctx: KContext) : KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = exponentShiftSize + + companion object { + val exponentBits: UInt = 8.toUInt() + val significandBits: UInt = 24.toUInt() + const val exponentShiftSize: Int = 127 + } +} + +class KFp64Sort(ctx: KContext) : KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = exponentShiftSize + + companion object { + val exponentBits: UInt = 11.toUInt() + val significandBits: UInt = 53.toUInt() + const val exponentShiftSize: Int = 1023 + } +} + +class KFp128Sort(ctx: KContext) : KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = exponentShiftSize + + companion object { + val exponentBits: UInt = 15.toUInt() + val significandBits: UInt = 113.toUInt() + const val exponentShiftSize: Int = 16383 + } +} + +class KFpCustomSizeSort(ctx: KContext, exponentBits: UInt, significandBits: UInt) : + KFpSort(ctx, exponentBits, significandBits) { + override fun exponentShiftSize(): Int = (1 shl (exponentBits.toInt() - 1)) - 1 +} + +class KFpRoundingModeSort(ctx: KContext) : KSort(ctx) { + override fun print(builder: StringBuilder) { + builder.append("RoundingModeSort") + } + + override fun accept(visitor: KSortVisitor): T = visitor.visit(this) +} diff --git a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt index 5d71ff6ad..f1cec4587 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/sort/KSortVisitor.kt @@ -6,6 +6,8 @@ interface KSortVisitor { fun visit(sort: KIntSort): T fun visit(sort: KRealSort): T fun visit(sort: S): T + fun visit(sort: S): T fun visit(sort: KArraySort): T + fun visit(sort: KFpRoundingModeSort): T fun visit(sort: KUninterpretedSort): T } diff --git a/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt b/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt index 42725cb73..67b470f83 100644 --- a/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt +++ b/ksmt-core/src/main/kotlin/org/ksmt/utils/Utils.kt @@ -1,5 +1,10 @@ package org.ksmt.utils +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpSort + // We can have here `0` as a pad symbol since `toString` can return a string // containing fewer symbols than `sizeBits` only for non-negative numbers fun Number.toBinary(): String = when (this) { @@ -7,9 +12,178 @@ fun Number.toBinary(): String = when (this) { is Short -> toUShort().toString(radix = 2).padStart(Short.SIZE_BITS, '0') is Int -> toUInt().toString(radix = 2).padStart(Int.SIZE_BITS, '0') is Long -> toULong().toString(radix = 2).padStart(Long.SIZE_BITS, '0') + is Float -> toRawBits().toBinary() + is Double -> toRawBits().toBinary() else -> error("Unsupported type for transformation into a binary string: ${this::class.simpleName}") } +/** + * Significand for Fp16 takes 10 bits from the float value: from 14 to 23 bits + */ +@Suppress("MagicNumber") +val Float.halfPrecisionSignificand: Int + get() = (toRawBits() and 0b0000_0000_0111_1111_1110_0000_0000_0000) shr 13 + +/** + * Take an exponent from the float value. Depending on the [isBiased] is can be either shifted by + * [KFp16Sort.exponentShiftSize] or not. + */ +@Suppress("MagicNumber") +fun Float.getHalfPrecisionExponent(isBiased: Boolean): Int { + // take an unbiased exponent from the given value + val unbiasedFloatExponent = getExponent(isBiased = false) + val unbiasedFp16Exponent = when { + unbiasedFloatExponent <= -KFp16Sort.exponentShiftSize -> -KFp16Sort.exponentShiftSize + unbiasedFloatExponent >= KFp16Sort.exponentShiftSize + 1 -> KFp16Sort.exponentShiftSize + 1 + else -> { + // extract a sign bit from it -- fifth one + val signBit = (unbiasedFloatExponent shr 4) and 1 + // take remaining bits of the exponent + val otherBits = unbiasedFloatExponent and 0b1111 + // create an unbiased fp16 exponent containing five bits + (signBit shl 4) or otherBits + } + } + return if (isBiased) unbiasedFp16Exponent + KFp16Sort.exponentShiftSize else unbiasedFp16Exponent +} + +/** + * Extracts a significand from the float value. + * + * @see [Float.toRawBits] + */ +@Suppress("MagicNumber") +val Float.significand: Int get() = toRawBits() and 0x7fffff + +/** + * Extracts an exponent from the float value. + * Depending on the [isBiased] it can be either biased or not. + * + * @see [Float.toRawBits] + */ +@Suppress("MagicNumber") +fun Float.getExponent(isBiased: Boolean): Int { + // extract exponent using the mask and move it to the right without saving the sign + val exponent = (toRawBits() and 0x7f80_0000) ushr 23 + + return if (isBiased) exponent else exponent - KFp32Sort.exponentShiftSize +} + +@Suppress("MagicNumber") +val Float.signBit: Int get() = (toRawBits() shr 31) and 1 +val Float.booleanSignBit: Boolean get() = signBit == 1 + +/** + * Extracts a significand from the float value. + * + * @see [Double.toRawBits] + */ +@Suppress("MagicNumber") +val Double.significand: Long get() = toRawBits() and 0x000f_ffff_ffff_ffff + +/** + * Extracts an exponent from the float value. + * Depending on the [isBiased] it can be either biased or not. + * + * @see [Double.toRawBits] + */ +@Suppress("MagicNumber") +fun Double.getExponent(isBiased: Boolean): Long { + // extract exponent using the mask and move it to the right without saving the sign + val exponent = (toRawBits() and 0x7ff0_0000_0000_0000) ushr 52 + + return if (isBiased) exponent else exponent - KFp64Sort.exponentShiftSize +} + +@Suppress("MagicNumber") +val Double.signBit: Int get() = (toRawBits() shr 63).toInt() and 1 +val Double.booleanSignBit: Boolean get() = signBit == 1 + +/** + * Extracts a significand of the specific [sort] from a float value. + */ +fun Float.extractSignificand(sort: KFpSort): Int { + val sizeBits = sort.significandBits.toInt() + // If we need more bits in significand than we have in Fp32's significand, take all ones + // Otherwise, take `sizeBits - 1` of them. + val fp32SignificandBits = KFp32Sort.significandBits.toInt() + val significandMask = if (sizeBits >= fp32SignificandBits) -1 else (1 shl sizeBits - 1) - 1 + + // we want to take first `n` bits from the float significand. + // We take at least zero to avoid incorrect shift for sorts with a large significand bits number. + val shiftForSortSpecificSignificandBits = maxOf(0, fp32SignificandBits - sizeBits) + + return (toRawBits() shr shiftForSortSpecificSignificandBits) and significandMask +} + +/** + * Extends the given 32-bits value to a new 64-bits one with zeroes. + * + * We should use this function instead of [Int.toLong] to avoid moving size bit from its place. + * + * It is important in situations when we want to create a bitvector from (-1) -- it is 32 ones in binary representation. + * Then we want to extend it to 64 bits, but [Int.toLong] will move sign one into the first place in a new value, + * 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. + */ +@Suppress("MagicNumber") +fun Int.extendWithLeadingZeros(): Long = toLong().let { + ((((it shr 63) and 1) shl 31) or it) and 0xffff_ffff +} + +/** + * Extracts an exponent of the specific [sort] from the fp32 value. + */ +@Suppress("MagicNumber") +fun Float.extractExponent(sort: KFpSort, isBiased: Boolean): Int { + // extract an exponent from the value in fp32 format + val exponent = getExponent(isBiased = false) + + // find a sign of the exponent + val sign = (exponent shr 7) and 1 + + // take last (exponentBits - 1) bits of the exponent, where exponentBits is specific for the sort + val exponentBits = exponent and ((1 shl (sort.exponentBits.toInt() - 1)) - 1) + + // construct a sort specific exponent + val constructedExponent = (sign shl sort.exponentBits.toInt() - 1) or exponentBits + + return if (isBiased) constructedExponent + sort.exponentShiftSize() else constructedExponent +} + + +/** + * Extracts a significand of the specific [sort] from a double value. + */ +@Suppress("MagicNumber") +fun Double.extractSignificand(sort: KFpSort): Long { + val significandBits = sort.significandBits.toInt() + val fp64Bits = KFp64Sort.significandBits.toInt() + + // If we need more bits in significand than we have in Fp32's significand, take all ones + // Otherwise, take `sizeBits - 1` of them. + val significandMask = if (significandBits >= fp64Bits) -1 else (1L shl significandBits - 1) - 1 + // we want to take first `n` bits from the float significand. + // We take at least zero to avoid incorrect shift for sorts with a large significand bits number. + val shiftForSortSpecificSignificandBits = maxOf(0, 53 - significandBits) + + return (toRawBits() shr shiftForSortSpecificSignificandBits) and significandMask +} + +/** + * Extracts an exponent of the specific [sort] from the fp64 value. + */ +@Suppress("MagicNumber") +fun Double.extractExponent(sort: KFpSort, isBiased: Boolean): Long { + val exponent = getExponent(isBiased = false) + val sign = (exponent shr 10) and 1 + val exponentBits = exponent and (1L shl (sort.exponentBits.toInt() - 1)) - 1 + + val constructedExponent = (sign shl sort.exponentBits.toInt() - 1) or exponentBits + + return if (isBiased) constructedExponent + sort.exponentShiftSize() else constructedExponent +} + inline fun Base.cast(): T where T : Base = this as T @Suppress("UNCHECKED_CAST") diff --git a/ksmt-z3/build.gradle.kts b/ksmt-z3/build.gradle.kts index d73f7fbdb..86229bd30 100644 --- a/ksmt-z3/build.gradle.kts +++ b/ksmt-z3/build.gradle.kts @@ -72,7 +72,21 @@ val smtLibBenchmarks = listOfNotNull( if (!skipBigBenchmarks) "AUFBV" else null, // 1.2G if (!skipBigBenchmarks) "BV" else null, // 847M "QF_ABV", // 253M - if (!skipBigBenchmarks) "QF_BV" else null// 12.3G + if (!skipBigBenchmarks) "QF_BV" else null,// 12.3G + "ABVFP", // 276K + "ABVFPLRA", // 246K + "AUFBVFP", // 14M + "BVFP", // 400K + "BVFPLRA", // 500K + "FP", // 1M + "FPLRA", // 700K + "QF_ABVFP", // 13M + "QF_ABVFPLRA", // 300K + "QF_AUFBVFP", // 200K + "QF_BVFP", // 7M + "QF_BVFPLRA", // 300K + "QF_FPLRA", // 250K + "QF_FP", // 30M ) val smtLibBenchmarkTestData = smtLibBenchmarks.map { mkSmtLibBenchmarkTestData(it) } 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 index f15f5411c..8696eabf2 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprConverter.kt @@ -1,13 +1,20 @@ package org.ksmt.solver.z3 +import com.microsoft.z3.ArithSort import com.microsoft.z3.ArraySort import com.microsoft.z3.BitVecNum import com.microsoft.z3.BitVecSort import com.microsoft.z3.Expr +import com.microsoft.z3.FPExpr +import com.microsoft.z3.FPNum +import com.microsoft.z3.FPRMNum +import com.microsoft.z3.FPRMSort +import com.microsoft.z3.FPSort import com.microsoft.z3.FuncDecl import com.microsoft.z3.IntNum import com.microsoft.z3.Quantifier import com.microsoft.z3.RatNum +import com.microsoft.z3.RealSort import com.microsoft.z3.Sort import com.microsoft.z3.ctx import com.microsoft.z3.enumerations.Z3_ast_kind @@ -21,13 +28,20 @@ import org.ksmt.decl.KDecl import org.ksmt.decl.KFuncDecl import org.ksmt.expr.KBitVecValue import org.ksmt.expr.KExpr +import org.ksmt.expr.KFpRoundingMode +import org.ksmt.expr.KFpRoundingModeExpr import org.ksmt.expr.KIntNumExpr import org.ksmt.expr.KRealNumExpr import org.ksmt.solver.util.KExprConverterBase import org.ksmt.sort.KArithSort import org.ksmt.sort.KArraySort import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KBv1Sort import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpRoundingModeSort +import org.ksmt.sort.KFpSort +import org.ksmt.sort.KRealSort import org.ksmt.sort.KSort open class KZ3ExprConverter( @@ -70,12 +84,16 @@ open class KZ3ExprConverter( mkArraySort(convertSort(it.domain), convertSort(it.range)) } Z3_sort_kind.Z3_BV_SORT -> mkBvSort((sort as BitVecSort).size.toUInt()) + Z3_sort_kind.Z3_FLOATING_POINT_SORT -> { + val fpSort = sort as FPSort + mkFpSort(fpSort.eBits.toUInt(), fpSort.sBits.toUInt()) + } + Z3_sort_kind.Z3_UNINTERPRETED_SORT -> mkUninterpretedSort(sort.name.toString()) + Z3_sort_kind.Z3_ROUNDING_MODE_SORT -> mkFpRoundingModeSort() Z3_sort_kind.Z3_DATATYPE_SORT, Z3_sort_kind.Z3_RELATION_SORT, Z3_sort_kind.Z3_FINITE_DOMAIN_SORT, - Z3_sort_kind.Z3_FLOATING_POINT_SORT, - Z3_sort_kind.Z3_ROUNDING_MODE_SORT, Z3_sort_kind.Z3_SEQ_SORT, Z3_sort_kind.Z3_RE_SORT, Z3_sort_kind.Z3_CHAR_SORT, @@ -105,9 +123,11 @@ open class KZ3ExprConverter( Z3_ast_kind.Z3_SORT_AST, Z3_ast_kind.Z3_FUNC_DECL_AST, Z3_ast_kind.Z3_UNKNOWN_AST -> error("impossible ast kind for expressions") + null -> error("z3 ast kind cannot be null") } + @Suppress( "RemoveExplicitTypeArguments", "USELESS_CAST", @@ -175,8 +195,8 @@ open class KZ3ExprConverter( Z3_decl_kind.Z3_OP_SLT -> expr.convert(::mkBvSignedLessExpr) Z3_decl_kind.Z3_OP_UGT -> expr.convert(::mkBvUnsignedGreaterExpr) Z3_decl_kind.Z3_OP_SGT -> expr.convert(::mkBvSignedGreaterExpr) - Z3_decl_kind.Z3_OP_BAND -> expr.convert(::mkBvAndExpr) - Z3_decl_kind.Z3_OP_BOR -> expr.convert(::mkBvOrExpr) + Z3_decl_kind.Z3_OP_BAND -> expr.convertReduced(::mkBvAndExpr) + Z3_decl_kind.Z3_OP_BOR -> expr.convertReduced(::mkBvOrExpr) Z3_decl_kind.Z3_OP_BNOT -> expr.convert(::mkBvNotExpr) Z3_decl_kind.Z3_OP_BXOR -> expr.convert(::mkBvXorExpr) Z3_decl_kind.Z3_OP_BNAND -> expr.convert(::mkBvNAndExpr) @@ -235,6 +255,7 @@ open class KZ3ExprConverter( Z3_decl_kind.Z3_OP_BUMUL_NO_OVFL -> expr.convert { a0: KExpr, a1: KExpr -> mkBvMulNoOverflowExpr(a0, a1, isSigned = false) } + Z3_decl_kind.Z3_OP_BSMUL_NO_UDFL -> expr.convert(::mkBvMulNoUnderflowExpr) Z3_decl_kind.Z3_OP_AS_ARRAY -> convert { val z3Decl = expr.funcDecl.parameters[0].funcDecl @@ -244,52 +265,135 @@ open class KZ3ExprConverter( ?: error("unexpected as-array decl $z3Decl") mkFunctionAsArray(decl) } + + Z3_decl_kind.Z3_OP_FPA_NEG -> expr.convert(::mkFpNegationExpr) + Z3_decl_kind.Z3_OP_FPA_ADD -> expr.convert(::mkFpAddExpr) + Z3_decl_kind.Z3_OP_FPA_SUB -> expr.convert(::mkFpSubExpr) + Z3_decl_kind.Z3_OP_FPA_MUL -> expr.convert(::mkFpMulExpr) + Z3_decl_kind.Z3_OP_FPA_FMA -> expr.convert(::mkFpFusedMulAddExpr) + Z3_decl_kind.Z3_OP_FPA_DIV -> expr.convert(::mkFpDivExpr) + Z3_decl_kind.Z3_OP_FPA_REM -> expr.convert(::mkFpRemExpr) + Z3_decl_kind.Z3_OP_FPA_ABS -> expr.convert(::mkFpAbsExpr) + Z3_decl_kind.Z3_OP_FPA_MIN -> expr.convert(::mkFpMinExpr) + Z3_decl_kind.Z3_OP_FPA_MAX -> expr.convert(::mkFpMaxExpr) + Z3_decl_kind.Z3_OP_FPA_SQRT -> expr.convert(::mkFpSqrtExpr) + Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL -> expr.convert(::mkFpRoundToIntegralExpr) + Z3_decl_kind.Z3_OP_FPA_EQ -> expr.convert(::mkFpEqualExpr) + Z3_decl_kind.Z3_OP_FPA_LT -> expr.convert(::mkFpLessExpr) + Z3_decl_kind.Z3_OP_FPA_GT -> expr.convert(::mkFpGreaterExpr) + Z3_decl_kind.Z3_OP_FPA_LE -> expr.convert(::mkFpLessOrEqualExpr) + Z3_decl_kind.Z3_OP_FPA_GE -> expr.convert(::mkFpGreaterOrEqualExpr) + Z3_decl_kind.Z3_OP_FPA_IS_NAN -> expr.convert(::mkFpIsNaNExpr) + Z3_decl_kind.Z3_OP_FPA_IS_INF -> expr.convert(::mkFpIsInfiniteExpr) + Z3_decl_kind.Z3_OP_FPA_IS_ZERO -> expr.convert(::mkFpIsZeroExpr) + Z3_decl_kind.Z3_OP_FPA_IS_NORMAL -> expr.convert(::mkFpIsNormalExpr) + Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL -> expr.convert(::mkFpIsSubnormalExpr) + Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE -> expr.convert(::mkFpIsNegativeExpr) + Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE -> expr.convert(::mkFpIsPositiveExpr) + Z3_decl_kind.Z3_OP_FPA_TO_UBV -> expr.convert { rm: KExpr, value: KExpr -> + val size = expr.funcDecl.parameters[0].int + mkFpToBvExpr(rm, value, bvSize = size, isSigned = false) + } + + Z3_decl_kind.Z3_OP_FPA_TO_SBV -> expr.convert { rm: KExpr, value: KExpr -> + val size = expr.funcDecl.parameters[0].int + mkFpToBvExpr(rm, value, bvSize = size, isSigned = true) + } + + Z3_decl_kind.Z3_OP_FPA_FP -> expr.convert(::mkFpFromBvExpr) + Z3_decl_kind.Z3_OP_FPA_TO_REAL -> expr.convert(::mkFpToRealExpr) + Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV -> expr.convert(::mkFpToIEEEBvExpr) + Z3_decl_kind.Z3_OP_FPA_TO_FP -> convertFpaToFp(expr) + Z3_decl_kind.Z3_OP_FPA_PLUS_INF -> convert { + val sort = convertSort(expr.sort) as KFpSort + mkFpInf(signBit = false, sort) + } + + Z3_decl_kind.Z3_OP_FPA_MINUS_INF -> convert { + val sort = convertSort(expr.sort) as KFpSort + mkFpInf(signBit = true, sort) + } + + Z3_decl_kind.Z3_OP_FPA_NAN -> convert { + val sort = convertSort(expr.sort) as KFpSort + mkFpNan(sort) + } + + Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO -> convert { + val sort = convertSort(expr.sort) as KFpSort + mkFpZero(signBit = false, sort) + } + + Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO -> convert { + val sort = convertSort(expr.sort) as KFpSort + mkFpZero(signBit = true, sort) + } + + Z3_decl_kind.Z3_OP_FPA_NUM -> convertNumeral(expr as FPExpr) + Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED -> + expr.convert { rm: KExpr, value: KExpr -> + val fpSort = convertSort(expr.sort) as KFpSort + mkBvToFpExpr(fpSort, rm, value, signed = false) + } + Z3_decl_kind.Z3_OP_FPA_BVWRAP, + Z3_decl_kind.Z3_OP_FPA_BV2RM -> { + TODO("Fp ${expr.funcDecl} (${expr.funcDecl.declKind}) is not supported") + } else -> TODO("${expr.funcDecl} (${expr.funcDecl.declKind}) is not supported") } } - fun Expr<*>.findConvertedExpr(): KExpr<*>? = z3InternCtx.findConvertedExpr(this) + @Suppress("ComplexMethod", "MagicNumber") + private fun KContext.convertFpaToFp(expr: Expr<*>): ExprConversionResult { + val fpSort = convertSort(expr.sort) as KFpSort + val args = expr.args + val sorts = args.map { it.sort } + return when { + args.size == 1 && sorts[0] is BitVecSort -> expr.convert { bv: KExpr -> + val exponentBits = fpSort.exponentBits.toInt() + val size = bv.sort.sizeBits.toInt() - /** - * Ensure all expression arguments are already converted and available in [z3InternCtx]. - * If not so, [argumentsConversionRequired] is returned. - * */ - inline fun ensureArgsAndConvert( - expr: Expr<*>, - args: Array>, - expectedSize: Int, - converter: (List>) -> KExpr<*> - ): ExprConversionResult { - check(args.size == expectedSize) { "arguments size mismatch: expected $expectedSize, actual ${args.size}" } - val convertedArgs = mutableListOf>() - var exprAdded = false - var argsReady = true - for (arg in args) { - val converted = arg.findConvertedExpr() - if (converted != null) { - convertedArgs.add(converted) - continue + @Suppress("UNCHECKED_CAST") + val sign = mkBvExtractExpr(size - 1, size - 1, bv) as KExpr + val exponent = mkBvExtractExpr(size - 2, size - exponentBits - 1, bv) + val significand = mkBvExtractExpr(size - exponentBits - 2, 0, bv) + + mkFpFromBvExpr(sign, exponent, significand) } - argsReady = false - if (!exprAdded) { - exprStack.add(expr) - exprAdded = true + args.size == 2 && sorts[0] is FPRMSort -> when (sorts[1]) { + is FPSort -> expr.convert { rm: KExpr, value: KExpr -> + mkFpToFpExpr(fpSort, rm, value) + } + is RealSort -> expr.convert { rm: KExpr, value: KExpr -> + mkRealToFpExpr(fpSort, rm, value) + } + is BitVecSort -> expr.convert { rm: KExpr, value: KExpr -> + mkBvToFpExpr(fpSort, rm, value, signed = true) + } + else -> TODO("unsupported fpaTofp: $expr") } - exprStack.add(arg) + args.size == 3 && sorts[0] is BitVecSort && sorts[1] is BitVecSort && sorts[2] is BitVecSort -> + expr.convert { sign: KExpr, exp: KExpr, significand: KExpr -> + mkFpFromBvExpr(sign, exp, significand) + } + + args.size == 3 && sorts[0] is FPRMSort && sorts[1] is ArithSort && sorts[2] is ArithSort -> + expr.convert, KArithSort<*>> { + rm: KExpr, arg1: KExpr>, arg2: KExpr> -> + TODO("${rm.sort} + real (${arg1.sort}) + int (${arg2.sort}) -> float") + } + else -> error("unexpected fpaTofp: $expr") } - - if (!argsReady) return argumentsConversionRequired - - val convertedExpr = converter(convertedArgs) - return ExprConversionResult(convertedExpr) } open fun convertNumeral(expr: Expr<*>): ExprConversionResult = when (expr.sort.sortKind) { - Z3_sort_kind.Z3_INT_SORT -> convertNumeral(expr as IntNum) - Z3_sort_kind.Z3_REAL_SORT -> convertNumeral(expr as RatNum) - Z3_sort_kind.Z3_BV_SORT -> convertNumeral(expr as BitVecNum) + Z3_sort_kind.Z3_INT_SORT -> convert { convertNumeral(expr as IntNum) } + Z3_sort_kind.Z3_REAL_SORT -> convert { convertNumeral(expr as RatNum) } + Z3_sort_kind.Z3_BV_SORT -> convert { convertNumeral(expr as BitVecNum) } + Z3_sort_kind.Z3_ROUNDING_MODE_SORT -> convert { convertNumeral(expr as FPRMNum) } + Z3_sort_kind.Z3_FLOATING_POINT_SORT -> convertNumeral(expr as FPExpr) else -> TODO("numerals with ${expr.sort} are not supported") - }.let { ExprConversionResult(it) } + } @Suppress("MemberVisibilityCanBePrivate") fun convertNumeral(expr: IntNum): KIntNumExpr = with(ctx) { @@ -309,6 +413,44 @@ open class KZ3ExprConverter( mkBv(value = expr.toBinaryString().padStart(sizeBits.toInt(), '0'), sizeBits) } + @Suppress("MemberVisibilityCanBePrivate") + fun convertNumeral(expr: FPExpr): ExprConversionResult = when { + expr is FPNum -> convert { + with(ctx) { + val sort = convertSort(expr.sort) as KFpSort + val sBits = sort.significandBits.toInt() + val fp64SizeBits = KFp64Sort.exponentBits.toInt() + KFp64Sort.significandBits.toInt() + + // 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 = expr.significandUInt64 and significandMask + + val exponentMask = (1L shl sort.exponentBits.toInt()) - 1 + val exponent = expr.getExponentInt64(false) and exponentMask + + mkFp(significand, exponent, expr.sign, sort) + } + } + expr.funcDecl.declKind == Z3_decl_kind.Z3_OP_FPA_NUM -> { + TODO("unexpected fpa num") + } + else -> convertApp(expr) + } + + @Suppress("MemberVisibilityCanBePrivate") + fun convertNumeral(expr: FPRMNum): KFpRoundingModeExpr = with(ctx) { + val roundingMode = when (expr.funcDecl.declKind) { + Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN -> KFpRoundingMode.RoundNearestTiesToEven + Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY -> KFpRoundingMode.RoundNearestTiesToAway + Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE -> KFpRoundingMode.RoundTowardPositive + Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE -> KFpRoundingMode.RoundTowardNegative + Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO -> KFpRoundingMode.RoundTowardZero + else -> error("unexpected rounding mode: $expr") + } + mkFpRoundingModeExpr(roundingMode) + } + open fun convertQuantifier(expr: Quantifier): ExprConversionResult = with(ctx) { val z3Bounds = expr.boundVariableSorts .zip(expr.boundVariableNames) @@ -317,7 +459,7 @@ open class KZ3ExprConverter( val preparedBody = expr.body.substituteVars(z3Bounds.toTypedArray()) - val body = preparedBody.findConvertedExpr() + val body = findConvertedNative(preparedBody) if (body == null) { exprStack.add(expr) exprStack.add(preparedBody) @@ -347,6 +489,10 @@ open class KZ3ExprConverter( op: (KExpr, KExpr, KExpr) -> KExpr ) = convert(args, op) + inline fun Expr<*>.convert( + op: (KExpr, KExpr, KExpr, KExpr) -> KExpr + ) = convert(args, op) + inline fun Expr<*>.convertList(op: (List>) -> KExpr) = convertList(args, op) inline fun Expr<*>.convertReduced(op: (KExpr, KExpr) -> KExpr) = convertReduced(args, op) diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt index e9eaadd62..61ac4c2f7 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3ExprInternalizer.kt @@ -4,12 +4,19 @@ import com.microsoft.z3.ArithExpr import com.microsoft.z3.ArithSort import com.microsoft.z3.ArrayExpr import com.microsoft.z3.BitVecExpr +import com.microsoft.z3.BitVecSort import com.microsoft.z3.BoolExpr import com.microsoft.z3.BoolSort import com.microsoft.z3.Context import com.microsoft.z3.Expr +import com.microsoft.z3.FPExpr +import com.microsoft.z3.FPRMExpr +import com.microsoft.z3.FPRMSort +import com.microsoft.z3.FPSort import com.microsoft.z3.FuncDecl import com.microsoft.z3.IntExpr +import com.microsoft.z3.RealExpr +import com.microsoft.z3.RealSort import com.microsoft.z3.Sort import com.microsoft.z3.mkBvNumeral import com.microsoft.z3.mkExistsQuantifier @@ -68,6 +75,7 @@ import org.ksmt.expr.KBvSignedRemExpr import org.ksmt.expr.KBvSubExpr import org.ksmt.expr.KBvSubNoOverflowExpr import org.ksmt.expr.KBvSubNoUnderflowExpr +import org.ksmt.expr.KBvToFpExpr import org.ksmt.expr.KBvUnsignedDivExpr import org.ksmt.expr.KBvUnsignedGreaterExpr import org.ksmt.expr.KBvUnsignedGreaterOrEqualExpr @@ -76,7 +84,6 @@ import org.ksmt.expr.KBvUnsignedLessOrEqualExpr import org.ksmt.expr.KBvUnsignedRemExpr import org.ksmt.expr.KBvXNorExpr import org.ksmt.expr.KBvXorExpr -import org.ksmt.expr.KBvZeroExtensionExpr import org.ksmt.expr.KConst import org.ksmt.expr.KDistinctExpr import org.ksmt.expr.KDivArithExpr @@ -108,11 +115,57 @@ import org.ksmt.expr.KToRealIntExpr import org.ksmt.expr.KTrue import org.ksmt.expr.KUnaryMinusArithExpr import org.ksmt.expr.KUniversalQuantifier +import org.ksmt.expr.KBvZeroExtensionExpr +import org.ksmt.expr.KFp128Value +import org.ksmt.expr.KFp16Value +import org.ksmt.expr.KFp32Value +import org.ksmt.expr.KFp64Value +import org.ksmt.expr.KFpAbsExpr +import org.ksmt.expr.KFpAddExpr +import org.ksmt.expr.KFpCustomSizeValue +import org.ksmt.expr.KFpDivExpr +import org.ksmt.expr.KFpEqualExpr +import org.ksmt.expr.KFpFromBvExpr +import org.ksmt.expr.KFpFusedMulAddExpr +import org.ksmt.expr.KFpGreaterExpr +import org.ksmt.expr.KFpGreaterOrEqualExpr +import org.ksmt.expr.KFpIsInfiniteExpr +import org.ksmt.expr.KFpIsNaNExpr +import org.ksmt.expr.KFpIsNegativeExpr +import org.ksmt.expr.KFpIsNormalExpr +import org.ksmt.expr.KFpIsPositiveExpr +import org.ksmt.expr.KFpIsSubnormalExpr +import org.ksmt.expr.KFpIsZeroExpr +import org.ksmt.expr.KFpLessExpr +import org.ksmt.expr.KFpLessOrEqualExpr +import org.ksmt.expr.KFpMaxExpr +import org.ksmt.expr.KFpMinExpr +import org.ksmt.expr.KFpMulExpr +import org.ksmt.expr.KFpNegationExpr +import org.ksmt.expr.KFpRemExpr +import org.ksmt.expr.KFpRoundToIntegralExpr +import org.ksmt.expr.KFpRoundingMode +import org.ksmt.expr.KFpRoundingModeExpr +import org.ksmt.expr.KFpSqrtExpr +import org.ksmt.expr.KFpSubExpr +import org.ksmt.expr.KFpToBvExpr +import org.ksmt.expr.KFpToFpExpr +import org.ksmt.expr.KFpToIEEEBvExpr +import org.ksmt.expr.KFpToRealExpr +import org.ksmt.expr.KFpValue +import org.ksmt.expr.KRealToFpExpr import org.ksmt.expr.KXorExpr import org.ksmt.solver.util.KExprInternalizerBase import org.ksmt.sort.KArithSort import org.ksmt.sort.KBoolSort import org.ksmt.sort.KBvSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpRoundingModeSort +import org.ksmt.sort.KFpSort +import org.ksmt.sort.KRealSort import org.ksmt.sort.KSort @Suppress("SpreadOperator") @@ -366,6 +419,184 @@ open class KZ3ExprInternalizer( override fun transform(expr: KBvMulNoUnderflowExpr) = with(expr) { transform(arg0, arg1, z3Ctx::mkBVMulNoUnderflow) } + override fun transformFpValue(expr: KFpValue): KExpr = expr.transform { + val sort = with(ctx) { expr.sort.internalizeSort() } as FPSort + with(expr) { + when (this) { + is KFp16Value -> z3Ctx.mkFP(value, sort) + is KFp32Value -> z3Ctx.mkFP(value, sort) + is KFp64Value -> z3Ctx.mkFP(value, sort) + is KFp128Value -> z3Ctx.mkFP(signBit, exponentValue, significandValue, sort) + is KFpCustomSizeValue -> z3Ctx.mkFP(signBit, exponentValue, significandValue, sort) + else -> error("Unexpected KFpValue type: ${this::class.qualifiedName}") + } + } + } + + override fun transform(expr: KFp16Value): KExpr = transformFpValue(expr) + + override fun transform(expr: KFp32Value): KExpr = transformFpValue(expr) + + override fun transform(expr: KFp64Value): KExpr = transformFpValue(expr) + + override fun transform(expr: KFp128Value): KExpr = transformFpValue(expr) + + override fun transform(expr: KFpCustomSizeValue): KExpr = transformFpValue(expr) + + override fun transform(expr: KFpRoundingModeExpr): KExpr = with(expr) { + transform { transformRoundingModeNumeral(value) } + } + + override fun transform(expr: KFpAbsExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPAbs) + } + + override fun transform(expr: KFpNegationExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPNeg) + } + + override fun transform(expr: KFpAddExpr): KExpr = with(expr) { + transform(roundingMode, arg0, arg1, z3Ctx::mkFPAdd) + } + + override fun transform(expr: KFpSubExpr): KExpr = with(expr) { + transform(roundingMode, arg0, arg1, z3Ctx::mkFPSub) + } + + override fun transform(expr: KFpMulExpr): KExpr = with(expr) { + transform(roundingMode, arg0, arg1, z3Ctx::mkFPMul) + } + + override fun transform(expr: KFpDivExpr): KExpr = with(expr) { + transform(roundingMode, arg0, arg1, z3Ctx::mkFPDiv) + } + + override fun transform(expr: KFpFusedMulAddExpr): KExpr = + with(expr) { + transform(roundingMode, arg0, arg1, arg2, z3Ctx::mkFPFMA) + } + + override fun transform(expr: KFpSqrtExpr): KExpr = + with(expr) { + transform(roundingMode, value, z3Ctx::mkFPSqrt) + } + + override fun transform(expr: KFpRemExpr): KExpr = with(expr) { + transform(arg0, arg1, z3Ctx::mkFPRem) + } + + override fun transform(expr: KFpRoundToIntegralExpr): KExpr = + with(expr) { + transform(roundingMode, value, z3Ctx::mkFPRoundToIntegral) + } + + override fun transform(expr: KFpMinExpr): KExpr = with(expr) { + transform(arg0, arg1, z3Ctx::mkFPMin) + } + + override fun transform(expr: KFpMaxExpr): KExpr = with(expr) { + transform(arg0, arg1, z3Ctx::mkFPMax) + } + + override fun transform(expr: KFpLessOrEqualExpr): KExpr = with(expr) { + transform(arg0, arg1, z3Ctx::mkFPLEq) + } + + override fun transform(expr: KFpLessExpr): KExpr = with(expr) { + transform(arg0, arg1, z3Ctx::mkFPLt) + } + + override fun transform(expr: KFpGreaterOrEqualExpr): KExpr = with(expr) { + transform(arg0, arg1, z3Ctx::mkFPGEq) + } + + override fun transform(expr: KFpGreaterExpr): KExpr = with(expr) { + transform(arg0, arg1, z3Ctx::mkFPGt) + } + + override fun transform(expr: KFpEqualExpr): KExpr = with(expr) { + transform(arg0, arg1, z3Ctx::mkFPEq) + } + + override fun transform(expr: KFpIsNormalExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPIsNormal) + } + + override fun transform(expr: KFpIsSubnormalExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPIsSubnormal) + } + + override fun transform(expr: KFpIsZeroExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPIsZero) + } + + override fun transform(expr: KFpIsInfiniteExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPIsInfinite) + } + + override fun transform(expr: KFpIsNaNExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPIsNaN) + } + + override fun transform(expr: KFpIsNegativeExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPIsNegative) + } + + override fun transform(expr: KFpIsPositiveExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPIsPositive) + } + + override fun transform(expr: KFpToBvExpr): KExpr = + with(expr) { + transform(roundingMode, value) { rm: Expr, value: Expr -> + z3Ctx.mkFPToBV(rm, value, bvSize, isSigned) + } + } + + private fun transformRoundingModeNumeral(roundingMode: KFpRoundingMode): FPRMExpr = + with(z3Ctx) { + when (roundingMode) { + KFpRoundingMode.RoundNearestTiesToEven -> mkFPRoundNearestTiesToEven() + KFpRoundingMode.RoundNearestTiesToAway -> mkFPRoundNearestTiesToAway() + KFpRoundingMode.RoundTowardNegative -> mkFPRoundTowardNegative() + KFpRoundingMode.RoundTowardPositive -> mkFPRoundTowardPositive() + KFpRoundingMode.RoundTowardZero -> mkFPRoundTowardZero() + } + } + + override fun transform(expr: KFpToRealExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPToReal) + } + + override fun transform(expr: KFpToIEEEBvExpr): KExpr = with(expr) { + transform(value, z3Ctx::mkFPToIEEEBV) + } + + override fun transform(expr: KFpFromBvExpr): KExpr = with(expr) { + transform(sign, exponent, significand, z3Ctx::mkFP) + } + + override fun transform(expr: KFpToFpExpr): KExpr = with(expr) { + transform(roundingMode, value) { rm: Expr, value: Expr -> + val fpSort = sort.internalizeSort() as FPSort + z3Ctx.mkFPToFP(rm, value as FPExpr, fpSort) + } + } + + override fun transform(expr: KRealToFpExpr): KExpr = with(expr) { + transform(roundingMode, value) { rm: Expr, value: Expr -> + val fpSort = sort.internalizeSort() as FPSort + z3Ctx.mkFPToFP(rm, value as RealExpr, fpSort) + } + } + + override fun transform(expr: KBvToFpExpr): KExpr = with(expr) { + transform(roundingMode, value) { rm: Expr, value: Expr -> + val fpSort = sort.internalizeSort() as FPSort + z3Ctx.mkFPToFP(rm, value as BitVecExpr, fpSort, signed) + } + } + override fun transform(expr: KArrayStore) = with(expr) { transform, Expr, Expr, KArrayStore>( array, index, value, z3Ctx::mkStore diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3InternalizationContext.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3InternalizationContext.kt index 108afd598..e42c25cd8 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3InternalizationContext.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3InternalizationContext.kt @@ -12,19 +12,19 @@ import java.util.WeakHashMap @Suppress("TooManyFunctions") class KZ3InternalizationContext : AutoCloseable { private var closed = false - private val expressions = WeakHashMap, Expr<*>>() - private val z3Expressions = WeakHashMap, WeakReference>>() - private val sorts = WeakHashMap() - private val z3Sorts = WeakHashMap>() - private val decls = WeakHashMap, FuncDecl<*>>() - private val z3Decls = WeakHashMap, WeakReference>>() + private val expressions = HashMap, Expr<*>>() + private val z3Expressions = HashMap, KExpr<*>>() + private val sorts = HashMap() + private val z3Sorts = HashMap() + private val decls = HashMap, FuncDecl<*>>() + private val z3Decls = HashMap, KDecl<*>>() val isActive: Boolean get() = !closed fun findInternalizedExpr(expr: KExpr<*>): Expr<*>? = expressions[expr] - fun findConvertedExpr(expr: Expr<*>): KExpr<*>? = z3Expressions[expr]?.get() + fun findConvertedExpr(expr: Expr<*>): KExpr<*>? = z3Expressions[expr] fun internalizeExpr(expr: KExpr<*>, internalizer: (KExpr<*>) -> Expr<*>): Expr<*> = internalize(expressions, z3Expressions, expr, internalizer) @@ -46,26 +46,26 @@ class KZ3InternalizationContext : AutoCloseable { private inline fun internalize( cache: MutableMap, - reverseCache: MutableMap>, + reverseCache: MutableMap, key: K, internalizer: (K) -> V ): V = cache.getOrPut(key) { - internalizer(key).also { reverseCache[it] = WeakReference(key) } + internalizer(key).also { reverseCache[it] = key } } private inline fun convert( cache: MutableMap, - reverseCache: MutableMap>, + reverseCache: MutableMap, key: V, converter: (V) -> K ): K { - val current = reverseCache[key]?.get() + val current = reverseCache[key] if (current != null) return current val converted = converter(key) cache.getOrPut(converted) { key } - reverseCache[key] = WeakReference(converted) + reverseCache[key] = converted return converted } diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt index 301ac2710..0eb0fc068 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt @@ -121,7 +121,9 @@ open class KZ3Solver(private val ctx: KContext) : KSolver { } override fun model(): KModel = z3Try { - require(lastCheckStatus == KSolverStatus.SAT) { "Model are only available after SAT checks" } + require(lastCheckStatus == KSolverStatus.SAT) { + "Model are only available after SAT checks, current solver status: $lastCheckStatus" + } val model = solver.model KZ3Model(model, ctx, z3InternCtx, exprInternalizer, exprConverter) } diff --git a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt index 8254b10b8..0586a463e 100644 --- a/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt +++ b/ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SortInternalizer.kt @@ -8,6 +8,13 @@ import org.ksmt.sort.KRealSort import org.ksmt.sort.KBvSort import org.ksmt.sort.KArraySort import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KFp128Sort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpCustomSizeSort +import org.ksmt.sort.KFpRoundingModeSort +import org.ksmt.sort.KFpSort import org.ksmt.sort.KSort import org.ksmt.sort.KUninterpretedSort @@ -33,10 +40,25 @@ open class KZ3SortInternalizer( z3Ctx.mkArraySort(sort.domain.internalizeZ3Sort(), sort.range.internalizeZ3Sort()) } + override fun visit(sort: KFpRoundingModeSort): Sort = z3InternCtx.internalizeSort(sort) { + z3Ctx.mkFPRoundingModeSort() + } + override fun visit(sort: T): Sort = z3InternCtx.internalizeSort(sort) { z3Ctx.mkBitVecSort(sort.sizeBits.toInt()) } + override fun visit(sort: S): Sort = z3InternCtx.internalizeSort(sort) { + when (sort) { + is KFp16Sort -> z3Ctx.mkFPSort16() + is KFp32Sort -> z3Ctx.mkFPSort32() + is KFp64Sort -> z3Ctx.mkFPSort64() + is KFp128Sort -> z3Ctx.mkFPSort128() + is KFpCustomSizeSort -> z3Ctx.mkFPSort(sort.exponentBits.toInt(), sort.significandBits.toInt()) + else -> error("Unsupported sort: $sort") + } + } + override fun visit(sort: KUninterpretedSort): Sort = z3InternCtx.internalizeSort(sort) { z3Ctx.mkUninterpretedSort(sort.name) } diff --git a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BenchmarksBasedTest.kt b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BenchmarksBasedTest.kt index 23ea9cfca..11dba8b58 100644 --- a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BenchmarksBasedTest.kt +++ b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BenchmarksBasedTest.kt @@ -14,8 +14,10 @@ import org.junit.jupiter.params.ParameterizedTest import org.junit.jupiter.params.provider.Arguments import org.junit.jupiter.params.provider.MethodSource import org.ksmt.KContext +import org.ksmt.expr.KApp import org.ksmt.expr.KExpr import org.ksmt.expr.KFunctionAsArray +import org.ksmt.expr.transformer.KNonRecursiveTransformer import org.ksmt.expr.transformer.KTransformer import org.ksmt.solver.KModel import org.ksmt.solver.KSolverStatus @@ -52,6 +54,8 @@ class BenchmarksBasedTest { } val ksmtAssertions = parser.convert(ctx, assertions) + ksmtAssertions.forEach { SortChecker(ctx).apply(it) } + parseCtx.performEqualityChecks(ctx) { for ((originalZ3Expr, ksmtExpr) in assertions.zip(ksmtAssertions)) { val internalizedExpr = internalize(ksmtExpr) @@ -284,4 +288,14 @@ class BenchmarksBasedTest { return expr } } + + private class SortChecker(ctx: KContext) : KNonRecursiveTransformer(ctx) { + override fun transformApp(expr: KApp): KExpr = with(ctx) { + // apply internally check arguments sorts + expr.decl.apply(expr.args) + return super.transformApp(expr).also { + check(it.sort == expr.sort) { "sort mismatch" } + } + } + } } diff --git a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BitVecTest.kt b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BitVecTest.kt index 3a04e2f8a..26e36c793 100644 --- a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BitVecTest.kt +++ b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/BitVecTest.kt @@ -3,7 +3,6 @@ package org.ksmt.solver.z3 import kotlin.random.Random import kotlin.random.nextUInt import kotlin.test.assertEquals -import kotlin.test.assertFailsWith import kotlin.test.assertFalse import kotlin.test.assertTrue import org.junit.jupiter.api.AfterEach @@ -178,12 +177,26 @@ class BitVecTest { } @Test - fun testCreateIllegalBv(): Unit = with(context) { + fun testCreateBvNarrowingTransformation(): Unit = with(context) { val sizeBits = 42u - val stringValue = "0".repeat(sizeBits.toInt() - 1) + val bitvector = mkBv(Long.MAX_VALUE, sizeBits) as KBitVecCustomValue - assertFailsWith(IllegalArgumentException::class) { mkBv(stringValue, sizeBits) } - assertFailsWith(IllegalArgumentException::class) { mkBv(Long.MAX_VALUE, sizeBits) } + assertEquals(bitvector.binaryStringValue, Long.MAX_VALUE.toBinary().takeLast(sizeBits.toInt())) + } + + @Test + fun testCreateBvWithGreaterSize(): Unit = with(context) { + val sizeBits = 100u + val positiveBv = mkBv(Long.MAX_VALUE, sizeBits) as KBitVecCustomValue + val negativeBv = mkBv(Long.MIN_VALUE, sizeBits) as KBitVecCustomValue + + val sizeDifference = sizeBits.toInt() - Long.SIZE_BITS + + assertEquals(positiveBv.binaryStringValue.take(sizeDifference), "0".repeat(sizeDifference)) + assertEquals(negativeBv.binaryStringValue.take(sizeDifference), "1".repeat(sizeDifference)) + + assertEquals(positiveBv.binaryStringValue.takeLast(Long.SIZE_BITS), Long.MAX_VALUE.toBinary()) + assertEquals(negativeBv.binaryStringValue.takeLast(Long.SIZE_BITS), Long.MIN_VALUE.toBinary()) } @Test diff --git a/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/FloatingPointTest.kt b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/FloatingPointTest.kt new file mode 100644 index 000000000..cf8e03e9c --- /dev/null +++ b/ksmt-z3/src/test/kotlin/org/ksmt/solver/z3/FloatingPointTest.kt @@ -0,0 +1,607 @@ +package org.ksmt.solver.z3 + +import java.lang.Float.intBitsToFloat +import kotlin.math.abs +import kotlin.math.max +import kotlin.math.min +import kotlin.math.pow +import kotlin.math.sign +import kotlin.math.sqrt +import kotlin.random.Random +import kotlin.random.nextUInt +import kotlin.test.assertEquals +import kotlin.test.assertTrue +import org.junit.jupiter.api.AfterEach +import org.junit.jupiter.api.BeforeEach +import org.junit.jupiter.api.Disabled +import org.junit.jupiter.api.Test +import org.ksmt.KContext +import org.ksmt.expr.KExpr +import org.ksmt.expr.KFp16Value +import org.ksmt.expr.KFp32Value +import org.ksmt.expr.KFp64Value +import org.ksmt.expr.KFpRoundingMode +import org.ksmt.expr.KFpRoundingModeExpr +import org.ksmt.expr.KTrue +import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KFp16Sort +import org.ksmt.sort.KFp32Sort +import org.ksmt.sort.KFp64Sort +import org.ksmt.sort.KFpSort +import org.ksmt.utils.booleanSignBit +import org.ksmt.utils.extractExponent +import org.ksmt.utils.extractSignificand + + +class FloatingPointTest { + private var context = KContext() + private var solver = KZ3Solver(context) + + @BeforeEach + fun createNewEnvironment() { + context = KContext() + solver = KZ3Solver(context) + } + + @AfterEach + fun clearResources() { + solver.close() + } + + private fun KContext.symbolicValuesCheck(symbolicValues: List>, sort: S) { + val symbolicConsts = symbolicValues.indices.map { sort.mkConst("const_${it}") } + val pairs = symbolicValues.zip(symbolicConsts) + + pairs.forEach { (value, const) -> + solver.assert(value eq const) + } + + solver.check() + val model = solver.model() + + pairs.forEach { (value, const) -> + assertTrue( + "Values for $const are different: ${System.lineSeparator()}" + + "expected: $value ${System.lineSeparator()}" + + "found: ${model.eval(const)}" + ) { model.eval(const) === value } + } + } + + private fun KContext.createSymbolicValues( + it: Float, + sort: S, + mkSpecificSort: (Float) -> KExpr + ): List> = listOf( + mkSpecificSort(it), + mkFp(it, sort), + mkFp( + it.extractSignificand(sort), + it.extractExponent(sort, isBiased = false), + signBit = it.booleanSignBit, + sort + ), + mkFp( + it.extractSignificand(sort).toLong(), + it.extractExponent(sort, isBiased = false).toLong(), + signBit = it.booleanSignBit, + sort + ) + ) + + private fun KContext.createSymbolicValues( + it: Double, + sort: S, + mkSpecificSort: (Double) -> KExpr + ): List> = listOf( + mkSpecificSort(it), + mkFp(it, sort), + mkFp( + it.extractSignificand(sort), + it.extractExponent(sort, isBiased = false), + signBit = it.booleanSignBit, + sort + ), + mkFp( + it.extractSignificand(sort), + it.extractExponent(sort, isBiased = false), + signBit = it.booleanSignBit, + sort + ) + ) + + @Test + fun testCreateFp16(): Unit = with(context) { + val values = (0..10000) + .map { + val sign = Random.nextInt(from = 0, until = 2) + val exponent = Random.nextInt(from = 128, until = 142) + val significand = Random.nextInt(from = 0, until = 1024) + intBitsToFloat(((sign shl 31) or (exponent shl 23) or (significand shl 13))) + }.distinct() + + val sort = mkFp16Sort() + + val symbolicValues = values.map { + createSymbolicValues(it, sort, context::mkFp16).distinct().single() + } + + symbolicValuesCheck(symbolicValues, sort) + } + + @Test + fun testCreateFp32(): Unit = with(context) { + val values = (0..10000).map { Random.nextFloat() } + + val sort = mkFp32Sort() + + val symbolicValues = values.map { + createSymbolicValues(it, sort, context::mkFp32).distinct().single() + } + + symbolicValuesCheck(symbolicValues, sort) + } + + @Test + fun testCreateFp64(): Unit = with(context) { + val values = (0..1000).map { + Random.nextFloat().toDouble() + } + + val sort = mkFp64Sort() + + val symbolicValues = values.map { + createSymbolicValues(it, sort, context::mkFp64).distinct().single() + } + + symbolicValuesCheck(symbolicValues, sort) + } + + @Test + fun testCreateFp128(): Unit = with(context) { + val values = (0..1000) + .map { + Random.nextLong() to Random.nextLong( + from = 0b000000000000000.toLong(), + until = 0b011111111111111.toLong() + ) * sign(Random.nextInt().toDouble()).toLong() + } + + val randomDoubles = (0..1000).map { Random.nextDouble() } + val randomFloats = (0..1000).map { Random.nextFloat() } + + val signBit = Random.nextBoolean() + + val sort = mkFp128Sort() + + val symbolicValues = values.map { + listOf( + mkFp128(it.first, it.second, signBit), + mkFp(it.first, it.second, signBit, sort) + ).distinct().single() + }.toMutableList() + + symbolicValues += randomDoubles.map { mkFp(it, sort) } + symbolicValues += randomFloats.map { mkFp(it, sort) } + + symbolicValuesCheck(symbolicValues, sort) + } + + @Test + @Disabled("Not supported yet, doesn't work with particular sorts, for example, FP 32 132") + fun testCreateFpCustomSize(): Unit = + repeat(10) { + createNewEnvironment() + with(context) { + // mkFpSort(3u, 127u) listOf(mkFp(-1054027720, sort)) and 2u don't work + val sort = mkFpSort( + Random.nextInt(from = 2, until = 64).toUInt(), + Random.nextUInt(from = 10u, until = 150u) + ) + // val sort = mkFpSort(4u, 92u) + + println("${it + 1} run, sort: $sort") + + val values = (0..100) + .map { + val (significand, exponent) = Random.nextLong() to Random.nextLong() + val finalSignificand = significand and ((1L shl sort.significandBits.toInt() - 1) - 1) + val finalExponent = exponent and ((1L shl sort.exponentBits.toInt()) - 1) + + finalSignificand to finalExponent + } + // TODO this combination doesn't work + // 7 run, sort: FP (eBits: 6) (sBits: 109) + // val values = listOf((-8634236606667726792L to 33L)) + + // TODO here we should apply masks to avoid exponents that are not in [min..max] range + val randomDoubles = (0..1000).map { Random.nextDouble() } + val randomFloats = (0..1000).map { Random.nextFloat() } + + val signBit = Random.nextBoolean() + + // TODO not supported yet + val symbolicValues = values.mapTo(mutableListOf()) { (significand, exponent) -> + mkFp(significand, exponent, signBit, sort) + } + symbolicValues += randomDoubles.mapTo(mutableListOf()) { value -> mkFp(value, sort) } + symbolicValues += randomFloats.map { value -> mkFp(value, sort) } + + symbolicValuesCheck(symbolicValues, sort) + } + } + + @Test + fun testFpAbsExpr(): Unit = with(context) { + val negativeNumber = Random.nextDouble(from = Long.MIN_VALUE.toDouble(), until = 0.0) + val positiveNumber = Random.nextDouble(from = 0.0, Long.MAX_VALUE.toDouble()) + + val negativeFp = negativeNumber.toFp() as KFp64Value + val positiveFp = positiveNumber.toFp() as KFp64Value + + val negativeVariable = mkFp64Sort().mkConst("negativeValue") + val positiveVariable = mkFp64Sort().mkConst("positiveValue") + + solver.assert(mkFpAbsExpr(negativeFp) eq negativeVariable) + solver.assert(mkFpAbsExpr(positiveFp) eq positiveVariable) + + solver.check() + with(solver.model()) { + assertEquals(abs(negativeNumber), (eval(negativeVariable) as KFp64Value).value, DELTA) + assertEquals(positiveNumber, (eval(positiveVariable) as KFp64Value).value, DELTA) + } + } + + @Test + fun testFpNegation(): Unit = with(context) { + val number = Random.nextDouble() + val numberFp = number.toFp() as KFp64Value + + val variable = mkFp64Sort().mkConst("variable") + + solver.assert(mkFpNegationExpr(numberFp) eq variable) + + solver.check() + with(solver.model()) { + assertEquals(-1 * number, (eval(variable) as KFp64Value).value, DELTA) + } + } + + private fun testBinaryArithOperation( + symbolicOperation: (KFpRoundingModeExpr, KFp64Value, KFp64Value) -> KExpr, + concreteOperation: (Double, Double) -> Double + ): Unit = with(context) { + val fst = Random.nextDouble() + val snd = Random.nextDouble() + + val fstFp = fst.toFp() as KFp64Value + val sndFp = snd.toFp() as KFp64Value + + val fstVariable = mkFp64Sort().mkConst("fstVariable") + val sndVariable = mkFp64Sort().mkConst("sndVariable") + + val roundingMode = KFpRoundingMode.RoundNearestTiesToEven + + solver.assert(symbolicOperation(mkFpRoundingModeExpr(roundingMode), fstFp, sndFp) eq fstVariable) + solver.assert(symbolicOperation(mkFpRoundingModeExpr(roundingMode), sndFp, fstFp) eq sndVariable) + + solver.check() + with(solver.model()) { + assertEquals(concreteOperation(fst, snd), (eval(fstVariable) as KFp64Value).value, DELTA) + assertEquals(concreteOperation(snd, fst), (eval(sndVariable) as KFp64Value).value, DELTA) + } + } + + @Test + fun testFpAddExpr() = testBinaryArithOperation(context::mkFpAddExpr) { a, b -> a + b } + + @Test + fun testFpSubExpr() = testBinaryArithOperation(context::mkFpSubExpr) { a, b -> a - b } + + @Test + fun testFpMulExpr() = testBinaryArithOperation(context::mkFpMulExpr) { a, b -> a * b } + + @Test + fun testFpDivExpr() = testBinaryArithOperation(context::mkFpDivExpr) { a, b -> a / b } + + @Test + fun testFpFusedMulAddExpr(): Unit = with(context) { + val fst = Random.nextDouble() + val snd = Random.nextDouble() + val third = Random.nextDouble() + + val fstFp = fst.toFp() as KFp64Value + val sndFp = snd.toFp() as KFp64Value + val thirdFp = third.toFp() as KFp64Value + + val fstVariable = mkFp64Sort().mkConst("fstVariable") + val sndVariable = mkFp64Sort().mkConst("sndVariable") + val thirdVariable = mkFp64Sort().mkConst("thirdVariable") + + val roundingMode = KFpRoundingMode.RoundNearestTiesToEven + + solver.assert(mkFpFusedMulAddExpr(mkFpRoundingModeExpr(roundingMode), fstFp, sndFp, thirdFp) eq fstVariable) + solver.assert(mkFpFusedMulAddExpr(mkFpRoundingModeExpr(roundingMode), sndFp, thirdFp, fstFp) eq sndVariable) + solver.assert(mkFpFusedMulAddExpr(mkFpRoundingModeExpr(roundingMode), thirdFp, fstFp, sndFp) eq thirdVariable) + + solver.check() + with(solver.model()) { + assertEquals((fst * snd) + third, (eval(fstVariable) as KFp64Value).value, DELTA) + assertEquals((snd * third) + fst, (eval(sndVariable) as KFp64Value).value, DELTA) + assertEquals((third * fst) + snd, (eval(thirdVariable) as KFp64Value).value, DELTA) + } + } + + @Test + fun testFpSqrtExpr(): Unit = with(context) { + val value = Random.nextDouble() + val valueFp = value.toFp() as KFp64Value + val valueVariable = mkFp64Sort().mkConst("fstVariable") + + val roundingMode = KFpRoundingMode.RoundNearestTiesToEven + + solver.assert(mkFpSqrtExpr(mkFpRoundingModeExpr(roundingMode), valueFp) eq valueVariable) + + solver.check() + with(solver.model()) { + assertEquals(sqrt(value), (eval(valueVariable) as KFp64Value).value, DELTA) + } + } + + @Test + fun testFpRoundToIntegral(): Unit = with(context) { + val value = Random.nextDouble() + + val roundingModes = KFpRoundingMode.values() + + val variables = roundingModes.indices.map { mkFp64Sort().mkConst("variable$it") } + + variables.forEachIndexed { index, it -> + val rm = mkFpRoundingModeExpr(roundingModes[index]) + solver.assert(mkFpRoundToIntegralExpr(rm, value.toFp() as KFp64Value) eq it) + } + + solver.check() + with(solver.model()) { + variables.map { (eval(it) as KFp64Value).value } + } + } + + private fun testMinMax( + symbolicOperation: (KFp64Value, KFp64Value) -> KExpr, + concreteOperation: (Double, Double) -> Double + ): Unit = with(context) { + val fst = Random.nextDouble() + val snd = Random.nextDouble() + + val fstFp = fst.toFp() as KFp64Value + val sndFp = snd.toFp() as KFp64Value + + val fstVariable = mkFp64Sort().mkConst("fstVariable") + val sndVariable = mkFp64Sort().mkConst("sndVariable") + + solver.assert(symbolicOperation(fstFp, sndFp) eq fstVariable) + solver.assert(symbolicOperation(sndFp, fstFp) eq sndVariable) + + solver.check() + with(solver.model()) { + assertEquals(concreteOperation(fst, snd), (eval(fstVariable) as KFp64Value).value, DELTA) + assertEquals(concreteOperation(snd, fst), (eval(sndVariable) as KFp64Value).value, DELTA) + } + } + + @Test + fun testMinValue(): Unit = testMinMax(context::mkFpMinExpr) { a: Double, b: Double -> min(a, b) } + + @Test + fun testMaxValue(): Unit = testMinMax(context::mkFpMaxExpr) { a: Double, b: Double -> max(a, b) } + + private inline fun testConstant( + sort: S, + symbolicOperation: () -> KExpr, + concreteOperation: () -> C, + valueGetter: (KExpr) -> C, + assertEquals: (C, C) -> Unit + ): Unit = with(context) { + val constVar by sort + + solver.assert(symbolicOperation() eq constVar) + + solver.check() + with(solver.model()) { + assertEquals(concreteOperation(), valueGetter(eval(constVar))) + } + } + + private fun testDoubleConstant( + symbolicOperation: () -> KExpr, + concreteOperation: () -> Double + ) = testConstant( + context.mkFp64Sort(), + symbolicOperation, + concreteOperation, + { (it as KFp64Value).value }, + { l, r -> assertEquals(l, r, DELTA) } + ) + + private fun testFloatConstant( + symbolicOperation: () -> KExpr, + concreteOperation: () -> Float + ) = testConstant( + context.mkFp32Sort(), + symbolicOperation, + concreteOperation, + { (it as KFp32Value).value }, + { l, r -> assertEquals(l, r, absoluteTolerance = 1e-12f) } + ) + + private fun testHalfConstant( + symbolicOperation: () -> KExpr, + concreteOperation: () -> Float + ) = testConstant( + context.mkFp16Sort(), + symbolicOperation, + concreteOperation, + { (it as KFp16Value).value }, + { l, r -> assertEquals(l, r, absoluteTolerance = 1e-12f) } + ) + + @Test + fun testDoubleNanValue() = testDoubleConstant( + symbolicOperation = { context.mkFpNan(context.mkFp64Sort()) }, + concreteOperation = { Double.NaN } + ) + + @Test + fun testDoublePosInfValue() = testDoubleConstant( + symbolicOperation = { context.mkFpInf(signBit = false, context.mkFp64Sort()) }, + concreteOperation = { Double.POSITIVE_INFINITY } + ) + + @Test + fun testDoubleNegInfValue() = testDoubleConstant( + symbolicOperation = { context.mkFpInf(signBit = true, context.mkFp64Sort()) }, + concreteOperation = { Double.NEGATIVE_INFINITY } + ) + + @Test + fun testDoublePosZeroValue() = testDoubleConstant( + symbolicOperation = { context.mkFpZero(signBit = false, context.mkFp64Sort()) }, + concreteOperation = { +0.0 } + ) + + @Test + fun testDoubleNegZeroValue() = testDoubleConstant( + symbolicOperation = { context.mkFpZero(signBit = true, context.mkFp64Sort()) }, + concreteOperation = { -0.0 } + ) + + @Test + fun testFloatNanValue() = testFloatConstant( + symbolicOperation = { context.mkFpNan(context.mkFp32Sort()) }, + concreteOperation = { Float.NaN } + ) + + @Test + fun testFloatPosInfValue() = testFloatConstant( + symbolicOperation = { context.mkFpInf(signBit = false, context.mkFp32Sort()) }, + concreteOperation = { Float.POSITIVE_INFINITY } + ) + + @Test + fun testFloatNegInfValue() = testFloatConstant( + symbolicOperation = { context.mkFpInf(signBit = true, context.mkFp32Sort()) }, + concreteOperation = { Float.NEGATIVE_INFINITY } + ) + + @Test + fun testFloatPosZeroValue() = testFloatConstant( + symbolicOperation = { context.mkFpZero(signBit = false, context.mkFp32Sort()) }, + concreteOperation = { +0.0f } + ) + + @Test + fun testFloatNegZeroValue() = testFloatConstant( + symbolicOperation = { context.mkFpZero(signBit = true, context.mkFp32Sort()) }, + concreteOperation = { -0.0f } + ) + + @Test + fun testHalfNanValue() = testHalfConstant( + symbolicOperation = { context.mkFpNan(context.mkFp16Sort()) }, + concreteOperation = { Float.NaN } + ) + + @Test + fun testHalfPosInfValue() = testHalfConstant( + symbolicOperation = { context.mkFpInf(signBit = false, context.mkFp16Sort()) }, + concreteOperation = { Float.POSITIVE_INFINITY } + ) + + @Test + fun testHalfNegInfValue() = testHalfConstant( + symbolicOperation = { context.mkFpInf(signBit = true, context.mkFp16Sort()) }, + concreteOperation = { Float.NEGATIVE_INFINITY } + ) + + @Test + fun testHalfPosZeroValue() = testHalfConstant( + symbolicOperation = { context.mkFpZero(signBit = false, context.mkFp16Sort()) }, + concreteOperation = { +0.0f } + ) + + @Test + fun testHalfNegZeroValue() = testHalfConstant( + symbolicOperation = { context.mkFpZero(signBit = true, context.mkFp16Sort()) }, + concreteOperation = { -0.0f } + ) + + private fun testCompare( + symbolicOperation: (KExpr, KExpr) -> KExpr, + concreteOperation: (Double, Double) -> Boolean + ): Unit = with(context) { + val fst = Random.nextDouble() + val snd = Random.nextDouble() + + val fstFp = fst.toFp() as KFp64Value + val sndFp = snd.toFp() as KFp64Value + + val fstVariable = mkBoolSort().mkConst("fstVariable") + val sndVariable = mkBoolSort().mkConst("sndVariable") + + solver.assert(symbolicOperation(fstFp, sndFp) eq fstVariable) + solver.assert(symbolicOperation(sndFp, fstFp) eq sndVariable) + + solver.check() + with(solver.model()) { + assertEquals(concreteOperation(fst, snd), eval(fstVariable) is KTrue) + assertEquals(concreteOperation(snd, fst), eval(sndVariable) is KTrue) + } + } + + private fun testPredicate( + symbolicPredicate: (KExpr) -> KExpr, + concreteOperation: (Double) -> Boolean + ): Unit = with(context) { + val values = listOf(Double.NaN, +0.0, -0.0, Double.POSITIVE_INFINITY, Double.NEGATIVE_INFINITY, 1.0.pow(-126)) + val fpValues = values.map { it.toFp() as KFp64Value } + val variables = values.indices.map { mkBoolSort().mkConst("variable$it") } + + val valuesWithVariables = fpValues.zip(variables) + valuesWithVariables.forEach { (value, variable) -> + solver.assert(symbolicPredicate(value) eq variable) + } + + solver.check() + with(solver.model()) { + valuesWithVariables.forEach { (fp, variable) -> + assertEquals(concreteOperation(fp.value), eval(variable) is KTrue) + } + } + } + + @Test + fun testLessOrEqualExpr() = testCompare(context::mkFpLessOrEqualExpr) { a: Double, b: Double -> a <= b } + + @Test + fun testLessExpr() = testCompare(context::mkFpLessExpr) { a: Double, b: Double -> a < b } + + @Test + fun testGreaterExpr() = testCompare(context::mkFpGreaterExpr) { a: Double, b: Double -> a > b } + + @Test + fun testGreaterOrEqualExpr() = testCompare(context::mkFpGreaterOrEqualExpr) { a: Double, b: Double -> a >= b } + + @Test + fun testEqualExpr() = testCompare(context::mkFpEqualExpr) { a: Double, b: Double -> abs(a - b) <= DELTA } + + @Test + fun testIsZero() = testPredicate(context::mkFpIsZeroExpr) { value: Double -> value == +0.0 || value == -0.0 } + + @Test + fun testIsInfinite() = testPredicate(context::mkFpIsInfiniteExpr) { value: Double -> value.isInfinite() } + + companion object { + const val DELTA = 1e-15 + } +}