Fixes

UnitTestBot · Feb 17, 2023 · 4e021a3 · 4e021a3
1 parent 8a0540d
commit 4e021a3
Show file tree

Hide file tree

Showing 6 changed files with 41 additions and 13 deletions.
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/BitUtils.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/BitUtils.kt
@@ -6,7 +6,7 @@ private const val BYTE_MASK = 0xff
 
 /**
  * Construct BigInteger value from bits array of the form:
- * array[0] = array[0] = bits[31:0], array[1] = bits[64:32], ...
+ * array[0] = bits[31:0], array[1] = bits[64:32], ...
  * */
 fun bvBitsToBigInteger(bvBits: IntArray): BigInteger {
     val valueByteArray = ByteArray(bvBits.size * Int.SIZE_BYTES) {

diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaContext.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaContext.kt
@@ -126,8 +126,8 @@ open class KBitwuzlaContext : AutoCloseable {
 
     /**
      * Internalize constant.
-     *  Since [Native.bitwuzlaMkConst] creates fresh constant on each invocation caches are used
-     *  to guarantee that if two constants are equal in ksmt they are also equal in Bitwuzla.
+     * Since [Native.bitwuzlaMkConst] creates fresh constant on each invocation caches are used
+     * to guarantee that if two constants are equal in ksmt they are also equal in Bitwuzla.
      * */
     fun mkConstant(decl: KDecl<*>, sort: BitwuzlaSort): BitwuzlaTerm = constants.getOrPut(decl) {
         Native.bitwuzlaMkConst(bitwuzla, sort, decl.name).also {

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
@@ -1104,7 +1104,14 @@ open class KBitwuzlaExprInternalizer(
         Native.bitwuzlaMkTerm(bitwuzlaCtx.bitwuzla, kind, args.toLongArray())
     }
 
+    /**
+     * Abort current internalization because we found an unsupported expression,
+     * that can be rewritten using axioms.
+     *
+     * See [internalizeAssertion].
+     * */
     class TryRewriteExpressionUsingAxioms(override val message: String) : Exception(message) {
+        // Not a real exception -> we can avoid stacktrace collection
         override fun fillInStackTrace(): Throwable = this
     }
 

diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaInternalizationAxioms.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaInternalizationAxioms.kt
@@ -33,9 +33,15 @@ class KBitwuzlaInternalizationAxioms(ctx: KContext) : KNonRecursiveTransformer(c
 
                 val size = stub.sort.sizeBits.toInt()
                 val exponentBits = value.sort.exponentBits.toInt()
-                val sign = mkBvExtractExpr(size - 1, size - 1, stub)
-                val exponent = mkBvExtractExpr(size - 2, size - exponentBits - 1, stub)
-                val significand = mkBvExtractExpr(size - exponentBits - 2, 0, stub)
+
+                val signBitIdx = size - 1
+                val exponentFirstBitIdx = signBitIdx - 1
+                val exponentLastBitIdx = size - exponentBits - 1
+                val significandFirstBitIdx = exponentLastBitIdx - 1
+
+                val sign = mkBvExtractExpr(high = signBitIdx, low = signBitIdx, value = stub)
+                val exponent = mkBvExtractExpr(high = exponentFirstBitIdx, low = exponentLastBitIdx, value = stub)
+                val significand = mkBvExtractExpr(high = significandFirstBitIdx, low = 0, value = stub)
 
                 val inverseOperation = mkFpFromBvExpr<T>(sign.uncheckedCast(), exponent, significand)
                 axioms += value eq inverseOperation

diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaModel.kt
@@ -197,10 +197,27 @@ open class KBitwuzlaModel(
     private inline fun <T> handleModelIsUnsupportedWithQuantifiers(body: () -> T): T = try {
         body()
     } catch (ex: BitwuzlaNativeException) {
-        val modelUnsupportedMessage = "'get-value' is currently not supported with quantifiers"
-        if (modelUnsupportedMessage in (ex.message ?: "")) {
-            throw KSolverUnsupportedFeatureException(modelUnsupportedMessage)
+        if (isModelUnsupportedWithQuantifiers(ex)) {
+            throw KSolverUnsupportedFeatureException("Model are not supported for formulas with quantifiers")
         }
         throw ex
     }
+
+    companion object {
+        private const val MODEL_UNSUPPORTED_WITH_QUANTIFIERS =
+            "'get-value' is currently not supported with quantifiers\n"
+
+        private fun isModelUnsupportedWithQuantifiers(ex: BitwuzlaNativeException): Boolean {
+            val message = ex.message ?: return false
+            /**
+             * Bitwuzla exception message has the following format:
+             * `[bitwuzla] <api method name> 'get-value' is currently ....`.
+             *
+             * Since we don't know the actual api method name
+             * (we have multiple ways to trigger get-value),
+             * we use `endsWith`.
+             * */
+            return message.endsWith(MODEL_UNSUPPORTED_WITH_QUANTIFIERS)
+        }
+    }
 }
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/bindings/FpValue.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/bindings/FpValue.kt
@@ -2,10 +2,8 @@ package org.ksmt.solver.bitwuzla.bindings
 
 /**
  * @param sign Binary string representation of the sign bit.
- * @param exponent Binary string representation of the exponent bit-vector
- * value.
- * @param significand Binary string representation of the significand
- * bit-vector value.
+ * @param exponent Binary string representation of the exponent bit-vector value.
+ * @param significand Binary string representation of the significand bit-vector value.
  * */
 
 class FpValue {