JNA to JNI migration (#69)

UnitTestBot · Saloed · Feb 17, 2023 · Jan 25, 2023 · Jan 27, 2023 · Jan 17, 2023
commit e723c109bdfb1b2904ff6360dca0449457ef7004
diff --git a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
@@ -29,7 +29,7 @@ tasks.withType<KotlinCompile> {
 }
 
 tasks.getByName<KotlinCompile>("compileKotlin") {
-    kotlinOptions.allWarningsAsErrors = true
+    kotlinOptions.allWarningsAsErrors = false
 }
 
 tasks.withType<Test> {

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
@@ -4,6 +4,7 @@ import com.sun.jna.Pointer
 import org.ksmt.decl.KDecl
 import org.ksmt.expr.KExpr
 import org.ksmt.solver.KSolverException
+import org.ksmt.solver.bitwuzla.bindings.BitwuzlaException
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
 import org.ksmt.solver.bitwuzla.bindings.Native
@@ -119,7 +120,7 @@ open class KBitwuzlaContext : AutoCloseable {
     /**
      * Keep strong reference to bitwuzla timeout callback to avoid sigsegv.
      * */
-    private var timeoutTerminator: BitwuzlaTimeout? = null
+    //private var timeoutTerminator: BitwuzlaTimeout? = null
 
     @OptIn(ExperimentalTime::class)
     fun <T> withTimeout(timeout: Duration, body: () -> T): T {
@@ -130,21 +131,21 @@ open class KBitwuzlaContext : AutoCloseable {
 
         val currentTime = TimeSource.Monotonic.markNow()
         val finishTime = currentTime + timeout
-        timeoutTerminator = BitwuzlaTimeout(finishTime)
+        //timeoutTerminator = BitwuzlaTimeout(finishTime)
 
         try {
-            Native.bitwuzlaSetTerminationCallback(bitwuzla, timeoutTerminator, state = null)
+            //Native.bitwuzlaSetTerminationCallback(bitwuzla, timeoutTerminator, state = null)
             return body()
         } finally {
-            timeoutTerminator = null
-            Native.bitwuzlaResetTerminationCallback(bitwuzla)
+            //timeoutTerminator = null
+            //Native.bitwuzlaResetTerminationCallback(bitwuzla)
         }
     }
 
     inline fun <reified T> bitwuzlaTry(body: () -> T): T = try {
         ensureActive()
         body()
-    } catch (ex: Native.BitwuzlaException) {
+    } catch (ex: BitwuzlaException) {
         throw KSolverException(ex)
     }
 
@@ -221,8 +222,8 @@ open class KBitwuzlaContext : AutoCloseable {
             constants[decl to sort] ?: parent.mkConstant(decl, sort)
     }
 
-    @OptIn(ExperimentalTime::class)
+/*    @OptIn(ExperimentalTime::class)
     class BitwuzlaTimeout(private val finishTime: TimeMark) : Native.BitwuzlaTerminationCallback {
         override fun terminate(state: Pointer?): Int = if (finishTime.hasNotPassedNow()) 0 else 1
-    }
+    }*/
 }
diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt
@@ -103,7 +103,7 @@ open class KBitwuzlaExprConverter(
 
     @Suppress("LongMethod", "ComplexMethod")
     override fun convertNativeExpr(expr: BitwuzlaTerm): ExprConversionResult = with(ctx) {
-        when (val kind = Native.bitwuzlaTermGetKind(expr)) {
+        when (val kind = BitwuzlaKind.fromValue(Native.bitwuzlaTermGetKind(expr))) {
             // constants, functions, values
             BitwuzlaKind.BITWUZLA_KIND_CONST -> convertConst(expr)
             BitwuzlaKind.BITWUZLA_KIND_APPLY -> convertFunctionApp(expr)
@@ -927,34 +927,34 @@ open class KBitwuzlaExprConverter(
         op: (KExpr<A0>) -> KExpr<T>
     ): ExprConversionResult {
         val args = Native.bitwuzlaTermGetChildren(this)
-        return convert(args, op)
+        return convert(Array(args.size) { args[it] }, op)
     }
 
     inline fun <T : KSort, A0 : KSort, A1 : KSort> BitwuzlaTerm.convert(
         op: (KExpr<A0>, KExpr<A1>) -> KExpr<T>
     ): ExprConversionResult {
         val args = Native.bitwuzlaTermGetChildren(this)
-        return convert(args, op)
+        return convert(Array(args.size) { args[it] }, op)
     }
 
     inline fun <T : KSort, A0 : KSort, A1 : KSort, A2 : KSort> BitwuzlaTerm.convert(
         op: (KExpr<A0>, KExpr<A1>, KExpr<A2>) -> KExpr<T>
     ): ExprConversionResult {
         val args = Native.bitwuzlaTermGetChildren(this)
-        return convert(args, op)
+        return convert(Array(args.size) { args[it] }, op)
     }
 
     inline fun <T : KSort, A0 : KSort, A1 : KSort, A2 : KSort, A3 : KSort> BitwuzlaTerm.convert(
         op: (KExpr<A0>, KExpr<A1>, KExpr<A2>, KExpr<A3>) -> KExpr<T>
     ): ExprConversionResult {
         val args = Native.bitwuzlaTermGetChildren(this)
-        return convert(args, op)
+        return convert(Array(args.size) { args[it] }, op)
     }
 
     inline fun <T : KSort, A : KSort> BitwuzlaTerm.convertList(
         op: (List<KExpr<A>>) -> KExpr<T>
     ): ExprConversionResult {
         val args = Native.bitwuzlaTermGetChildren(this)
-        return convertList(args, op)
+        return convertList(Array(args.size) { args[it] }, op)
     }
 }
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
@@ -209,7 +209,7 @@ open class KBitwuzlaExprInternalizer(
         // Save only constants
         if (expr !is KInterpretedValue<*>) return
 
-        val kind = Native.bitwuzlaTermGetKind(term)
+        val kind = BitwuzlaKind.fromValue(Native.bitwuzlaTermGetKind(term))
 
         /*
          * Save internalized values for [KBitwuzlaExprConverter] needs
@@ -229,7 +229,7 @@ open class KBitwuzlaExprInternalizer(
             val const = bitwuzlaCtx.mkConstant(decl, decl.bitwuzlaFunctionSort())
             val termArgs = (listOf(const) + args).toTypedArray()
 
-            Native.bitwuzlaMkTerm(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_APPLY, termArgs)
+            Native.bitwuzlaMkTerm(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_APPLY.value, termArgs.toLongArray())
         }
     }
 
@@ -243,7 +243,7 @@ open class KBitwuzlaExprInternalizer(
                 0 -> bitwuzlaCtx.trueTerm
                 1 -> args[0]
                 else -> Native.bitwuzlaMkTerm(
-                    bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_AND, args
+                    bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_AND.value, args.toLongArray()
                 )
             }
         }
@@ -255,7 +255,7 @@ open class KBitwuzlaExprInternalizer(
                 0 -> bitwuzlaCtx.falseTerm
                 1 -> args[0]
                 else -> Native.bitwuzlaMkTerm(
-                    bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_OR, args
+                    bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_OR.value, args.toLongArray()
                 )
             }
         }
@@ -284,7 +284,7 @@ open class KBitwuzlaExprInternalizer(
     override fun <T : KSort> transform(expr: KDistinctExpr<T>) = with(expr) {
         transformList(args) { args: Array<BitwuzlaTerm> ->
             Native.bitwuzlaMkTerm(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_DISTINCT, args
+                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_DISTINCT.value, args.toLongArray()
             )
         }
     }
@@ -332,7 +332,7 @@ open class KBitwuzlaExprInternalizer(
             )
             Native.bitwuzlaMkTerm2(
                 bitwuzlaCtx.bitwuzla,
-                BitwuzlaKind.BITWUZLA_KIND_BV_CONCAT,
+                BitwuzlaKind.BITWUZLA_KIND_BV_CONCAT.value,
                 higherBitsTerm,
                 lowerBitsTerm
             ).also { bitwuzlaCtx.saveInternalizedValue(expr, it) }
@@ -345,7 +345,7 @@ open class KBitwuzlaExprInternalizer(
                 bitwuzlaCtx.bitwuzla,
                 sort.internalizeSort(),
                 stringValue,
-                BitwuzlaBVBase.BITWUZLA_BV_BASE_BIN
+                BitwuzlaBVBase.BITWUZLA_BV_BASE_BIN.value
             ).also { bitwuzlaCtx.saveInternalizedValue(expr, it) }
         }
     }
@@ -461,7 +461,7 @@ open class KBitwuzlaExprInternalizer(
     override fun transform(expr: KBvExtractExpr) = with(expr) {
         transform(value) { arg: BitwuzlaTerm ->
             Native.bitwuzlaMkTerm1Indexed2(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_EXTRACT,
+                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_EXTRACT.value,
                 arg,
                 high, low
             )
@@ -471,7 +471,7 @@ open class KBitwuzlaExprInternalizer(
     override fun transform(expr: KBvSignExtensionExpr) = with(expr) {
         transform(value) { arg: BitwuzlaTerm ->
             Native.bitwuzlaMkTerm1Indexed1(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_SIGN_EXTEND,
+                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_SIGN_EXTEND.value,
                 arg,
                 extensionSize
             )
@@ -481,7 +481,7 @@ open class KBitwuzlaExprInternalizer(
     override fun transform(expr: KBvZeroExtensionExpr) = with(expr) {
         transform(value) { arg: BitwuzlaTerm ->
             Native.bitwuzlaMkTerm1Indexed1(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_ZERO_EXTEND,
+                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_ZERO_EXTEND.value,
                 arg,
                 extensionSize
             )
@@ -491,7 +491,7 @@ open class KBitwuzlaExprInternalizer(
     override fun transform(expr: KBvRepeatExpr) = with(expr) {
         transform(value) { arg: BitwuzlaTerm ->
             Native.bitwuzlaMkTerm1Indexed1(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_REPEAT,
+                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_REPEAT.value,
                 arg,
                 repeatNumber
             )
@@ -521,7 +521,7 @@ open class KBitwuzlaExprInternalizer(
     override fun <T : KBvSort> transform(expr: KBvRotateLeftIndexedExpr<T>) = with(expr) {
         transform(value) { arg: BitwuzlaTerm ->
             Native.bitwuzlaMkTerm1Indexed1(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_ROLI,
+                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_ROLI.value,
                 arg,
                 rotationNumber
             )
@@ -531,7 +531,7 @@ open class KBitwuzlaExprInternalizer(
     override fun <T : KBvSort> transform(expr: KBvRotateRightIndexedExpr<T>) = with(expr) {
         transform(value) { arg: BitwuzlaTerm ->
             Native.bitwuzlaMkTerm1Indexed1(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_RORI,
+                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_BV_RORI.value,
                 arg,
                 rotationNumber
             )
@@ -600,7 +600,7 @@ open class KBitwuzlaExprInternalizer(
                 val body = with(bodyInternalizer) {
                     body.internalize()
                 }
-                val bodyKind = Native.bitwuzlaTermGetKind(body)
+                val bodyKind = BitwuzlaKind.fromValue(Native.bitwuzlaTermGetKind(body))
 
                 if (bodyKind == BitwuzlaKind.BITWUZLA_KIND_ARRAY_SELECT) {
                     val selectArgs = Native.bitwuzlaTermGetChildren(body)
@@ -623,13 +623,13 @@ open class KBitwuzlaExprInternalizer(
     override fun transform(
         expr: KExistentialQuantifier
     ): KExpr<KBoolSort> = expr.internalizeQuantifier { args ->
-        Native.bitwuzlaMkTerm(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_EXISTS, args)
+        Native.bitwuzlaMkTerm(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_EXISTS.value, args.toLongArray())
     }
 
     override fun transform(
         expr: KUniversalQuantifier
     ): KExpr<KBoolSort> = expr.internalizeQuantifier { args ->
-        Native.bitwuzlaMkTerm(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_FORALL, args)
+        Native.bitwuzlaMkTerm(bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_FORALL.value, args.toLongArray())
     }
 
     override fun transform(expr: KBv2IntExpr): KExpr<KIntSort> {
@@ -740,11 +740,11 @@ open class KBitwuzlaExprInternalizer(
     override fun transform(expr: KFpRoundingModeExpr): KExpr<KFpRoundingModeSort> = with(expr) {
         transform {
             val rmMode = when (value) {
-                KFpRoundingMode.RoundNearestTiesToEven -> BitwuzlaRoundingMode.BITWUZLA_RM_RNE
-                KFpRoundingMode.RoundNearestTiesToAway -> BitwuzlaRoundingMode.BITWUZLA_RM_RNA
-                KFpRoundingMode.RoundTowardPositive -> BitwuzlaRoundingMode.BITWUZLA_RM_RTP
-                KFpRoundingMode.RoundTowardNegative -> BitwuzlaRoundingMode.BITWUZLA_RM_RTN
-                KFpRoundingMode.RoundTowardZero -> BitwuzlaRoundingMode.BITWUZLA_RM_RTZ
+                KFpRoundingMode.RoundNearestTiesToEven -> BitwuzlaRoundingMode.BITWUZLA_RM_RNE.value
+                KFpRoundingMode.RoundNearestTiesToAway -> BitwuzlaRoundingMode.BITWUZLA_RM_RNA.value
+                KFpRoundingMode.RoundTowardPositive -> BitwuzlaRoundingMode.BITWUZLA_RM_RTP.value
+                KFpRoundingMode.RoundTowardNegative -> BitwuzlaRoundingMode.BITWUZLA_RM_RTN.value
+                KFpRoundingMode.RoundTowardZero -> BitwuzlaRoundingMode.BITWUZLA_RM_RTZ.value
             }
             Native.bitwuzlaMkRmValue(bitwuzlaCtx.bitwuzla, rmMode)
         }
@@ -849,7 +849,7 @@ open class KBitwuzlaExprInternalizer(
     override fun <T : KFpSort> transform(expr: KFpToBvExpr<T>): KExpr<KBvSort> = with(expr) {
         transform(roundingMode, value) { rm: BitwuzlaTerm, value: BitwuzlaTerm ->
             val operation = if (isSigned) BitwuzlaKind.BITWUZLA_KIND_FP_TO_SBV else BitwuzlaKind.BITWUZLA_KIND_FP_TO_UBV
-            Native.bitwuzlaMkTerm2Indexed1(bitwuzlaCtx.bitwuzla, operation, rm, value, bvSize)
+            Native.bitwuzlaMkTerm2Indexed1(bitwuzlaCtx.bitwuzla, operation.value, rm, value, bvSize)
         }
     }
 
@@ -861,7 +861,7 @@ open class KBitwuzlaExprInternalizer(
         transform(roundingMode, value) { rm: BitwuzlaTerm, value: BitwuzlaTerm ->
             Native.bitwuzlaMkTerm2Indexed2(
                 bitwuzlaCtx.bitwuzla,
-                BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_FP,
+                BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_FP.value,
                 rm,
                 value,
                 sort.exponentBits.toInt(),
@@ -877,7 +877,7 @@ open class KBitwuzlaExprInternalizer(
             significand
         ) { sign: BitwuzlaTerm, exp: BitwuzlaTerm, significand: BitwuzlaTerm ->
             Native.bitwuzlaMkTerm3(
-                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_FP_FP, sign, exp, significand
+                bitwuzlaCtx.bitwuzla, BitwuzlaKind.BITWUZLA_KIND_FP_FP.value, sign, exp, significand
             )
         }
     }
@@ -890,7 +890,7 @@ open class KBitwuzlaExprInternalizer(
                 BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_UBV
             }
             Native.bitwuzlaMkTerm2Indexed2(
-                bitwuzlaCtx.bitwuzla, operation, rm, value, sort.exponentBits.toInt(), sort.significandBits.toInt()
+                bitwuzlaCtx.bitwuzla, operation.value, rm, value, sort.exponentBits.toInt(), sort.significandBits.toInt()
             )
         }
     }
@@ -992,22 +992,22 @@ open class KBitwuzlaExprInternalizer(
 
             if (domain.isEmpty()) return@internalizeDeclSort range
 
-            Native.bitwuzlaMkFunSort(bitwuzlaCtx.bitwuzla, domain.size, domain, range)
+            Native.bitwuzlaMkFunSort(bitwuzlaCtx.bitwuzla, domain.size, domain.toLongArray(), range)
         }
     }
 
     fun <S : KExpr<*>> S.transform(
         arg: KExpr<*>,
         kind: BitwuzlaKind
-    ): S = transform(arg) { a0: BitwuzlaTerm -> Native.bitwuzlaMkTerm1(bitwuzlaCtx.bitwuzla, kind, a0) }
+    ): S = transform(arg) { a0: BitwuzlaTerm -> Native.bitwuzlaMkTerm1(bitwuzlaCtx.bitwuzla, kind.value, a0) }
 
 
     fun <S : KExpr<*>> S.transform(
         arg0: KExpr<*>,
         arg1: KExpr<*>,
         kind: BitwuzlaKind
     ): S = transform(arg0, arg1) { a0: BitwuzlaTerm, a1: BitwuzlaTerm ->
-        Native.bitwuzlaMkTerm2(bitwuzlaCtx.bitwuzla, kind, a0, a1)
+        Native.bitwuzlaMkTerm2(bitwuzlaCtx.bitwuzla, kind.value, a0, a1)
     }
 
     fun <S : KExpr<*>> S.transform(
@@ -1016,7 +1016,7 @@ open class KBitwuzlaExprInternalizer(
         arg2: KExpr<*>,
         kind: BitwuzlaKind
     ): S = transform(arg0, arg1, arg2) { a0: BitwuzlaTerm, a1: BitwuzlaTerm, a2: BitwuzlaTerm ->
-        Native.bitwuzlaMkTerm3(bitwuzlaCtx.bitwuzla, kind, a0, a1, a2)
+        Native.bitwuzlaMkTerm3(bitwuzlaCtx.bitwuzla, kind.value, a0, a1, a2)
     }
 
     fun <S : KExpr<*>> S.transform(
@@ -1027,6 +1027,6 @@ open class KBitwuzlaExprInternalizer(
         kind: BitwuzlaKind
     ): S = transform(arg0, arg1, arg2, arg3) { a0: BitwuzlaTerm, a1: BitwuzlaTerm, a2: BitwuzlaTerm, a3: BitwuzlaTerm ->
         val args = arrayOf(a0, a1, a2, a3)
-        Native.bitwuzlaMkTerm(bitwuzlaCtx.bitwuzla, kind, args)
+        Native.bitwuzlaMkTerm(bitwuzlaCtx.bitwuzla, kind.value, args.toLongArray())
     }
 }
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
@@ -101,8 +101,8 @@ open class KBitwuzlaModel(
         val vars = decl.argSorts.map { it.mkFreshConstDecl("x") }
         for (i in 0 until interp.size) {
             // Don't substitute vars since arguments in Bitwuzla model are always constants
-            val args = interp.args[i].zip(decl.argSorts) { arg, sort -> arg.convertExpr(sort) }
-            val value = interp.values[i].convertExpr(decl.sort)
+            val args = interp.args!![i].zip(decl.argSorts) { arg, sort -> arg.convertExpr(sort) }
+            val value = interp.values!![i].convertExpr(decl.sort)
             entries += KModel.KFuncInterpEntry(args, value)
         }
 
@@ -123,8 +123,8 @@ open class KBitwuzlaModel(
         val interp = Native.bitwuzlaGetArrayValue(bitwuzlaCtx.bitwuzla, term)
 
         for (i in 0 until interp.size) {
-            val index = interp.indices[i].convertExpr(sort.domain)
-            val value = interp.values[i].convertExpr(sort.range)
+            val index = interp.indices!![i].convertExpr(sort.domain)
+            val value = interp.values!![i].convertExpr(sort.range)
             entries += KModel.KFuncInterpEntry(listOf(index), value)
         }