Retyping arrays and lambdas with Address domain sorts

buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts

@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.6.7"
+version = project.findProperty("ksmtVersion")?.toString()?.takeIf { it.isNotBlank() } ?: "0.6.7"
 
 repositories {
     mavenCentral()

jitpack.yml

@@ -0,0 +1,4 @@
+jdk:
+  - openjdk17
+install:
+  - ./gradlew :ksmt-core:publishToMavenLocal :ksmt-bitwuzla:ksmt-bitwuzla-core:publishToMavenLocal ":ksmt-bitwuzla:ksmt-bitwuzla-native:publishMaven-linux-x64PublicationToMavenLocal" -PksmtVersion=$VERSION -x test -x dokkaJavadoc -Dorg.gradle.jvmargs=-Xmx1g

ksmt-bitwuzla/dist/build.md

@@ -8,6 +8,22 @@ To make our distribution portable we statically link Bitwuzla against `libgmp`.
 
 Jni bindings `bitwuzla_jni` are built without any tricks.
 
+### Linux x64 library from the Bitwuzla fork
+
+`libbitwuzla.so` in `bitwuzla-linux64-1.0.zip` is the release `1.0-ksmt.1` of the fork https://github.com/metametamoon/bitwuzla, built from its branch `c-api-1.0`.
+That branch starts at Bitwuzla commit `1230d80a5275ddf525da9c218c2bcd29c3130e49`, the commit of the original binary, and adds fixes for lambdas reached through array updates in beta reduction and model generation, with tests.
+The fork's `contrib/ksmt/build-linux64.sh` builds the library in Docker, with GMP, libstdc++ and libgcc linked statically, and its release workflow attaches the library to the tag's GitHub release.
+
+`fetch-linux64.sh` downloads the library of a release, checks its sha256 and that it defines every `bzla_*` and `bitwuzla_*` symbol the unchanged `libbitwuzla_jni.so` imports, and repacks the zip.
+
+```shell
+./fetch-linux64.sh 1.0-ksmt.1
+```
+
+`libbitwuzla_jni.so` in the zip is still the original binary.
+The library of `1.0-ksmt.1` has sha256 `51d57475e5e19286496f48da6f62acb59d164c26c373c6b30707461532fdce49`.
+It also lists `ld-linux-x86-64.so.2` as a dependency and needs glibc 2.33 or newer, because the build image is Ubuntu 22.04; the 2023 binary needed glibc 2.14.
+
 ### Building on windows
 To produce Windows builds we use MSYS2 environment prepared as described [here](https://github.com/aytey/bitwuzla/blob/refreshed_windows_instructions/docs/building_on_windows.rst).
 Also, it is important to link statically with `libwinpthread`.

ksmt-bitwuzla/dist/fetch-linux64.sh

@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+tag=${1:?usage: fetch-linux64.sh <release tag of metametamoon/bitwuzla>}
+here=$(cd "$(dirname "$(readlink -f "$0")")" && pwd)
+url="https://github.com/metametamoon/bitwuzla/releases/download/$tag"
+work=$(mktemp -d)
+trap 'rm -rf "$work"' EXIT
+
+curl -fsSL -o "$work/libbitwuzla.so" "$url/libbitwuzla.so"
+curl -fsSL -o "$work/libbitwuzla.so.sha256" "$url/libbitwuzla.so.sha256"
+(cd "$work" && sha256sum -c --quiet libbitwuzla.so.sha256)
+
+python3 - "$here/bitwuzla-linux64-1.0.zip" "$work" <<'PY'
+import sys, zipfile
+with zipfile.ZipFile(sys.argv[1]) as z:
+    z.extract("libbitwuzla_jni.so", sys.argv[2])
+PY
+
+nm -D --undefined-only "$work/libbitwuzla_jni.so" | awk '{ print $NF }' | grep -E '^(bzla|bitwuzla)_' | sort -u > "$work/needed"
+nm -D --defined-only "$work/libbitwuzla.so" | awk '{ print $NF }' | sort -u > "$work/defined"
+missing=$(comm -23 "$work/needed" "$work/defined")
+if [ -n "$missing" ]; then
+  echo "libbitwuzla.so lacks symbols that libbitwuzla_jni.so imports:" >&2
+  echo "$missing" >&2
+  exit 1
+fi
+
+python3 - "$work" "$here/bitwuzla-linux64-1.0.zip" <<'PY'
+import os, sys, zipfile
+work, target = sys.argv[1], sys.argv[2]
+with zipfile.ZipFile(target + ".new", "w", zipfile.ZIP_DEFLATED) as z:
+    for name in ("libbitwuzla.so", "libbitwuzla_jni.so"):
+        info = zipfile.ZipInfo(name, date_time=(1980, 1, 1, 0, 0, 0))
+        info.external_attr = 0o755 << 16
+        info.compress_type = zipfile.ZIP_DEFLATED
+        with open(os.path.join(work, name), "rb") as f:
+            z.writestr(info, f.read())
+os.replace(target + ".new", target)
+PY
+
+cut -d' ' -f1 "$work/libbitwuzla.so.sha256"

ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt

@@ -15,6 +15,17 @@ import io.ksmt.expr.KConst
 import io.ksmt.expr.KEqExpr
 import io.ksmt.expr.KExpr
 import io.ksmt.expr.KFpRoundingMode
+import io.ksmt.expr.KApp
+import io.ksmt.expr.KArray2Lambda
+import io.ksmt.expr.KArray2Store
+import io.ksmt.expr.KArray3Lambda
+import io.ksmt.expr.KArray3Store
+import io.ksmt.expr.KArrayLambda
+import io.ksmt.expr.KArrayLambdaBase
+import io.ksmt.expr.KArrayNLambda
+import io.ksmt.expr.KArrayNStore
+import io.ksmt.expr.KArrayStore
+import io.ksmt.expr.KArrayStoreBase
 import io.ksmt.expr.KInterpretedValue
 import io.ksmt.expr.KIteExpr
 import io.ksmt.expr.printer.ExpressionPrinter
@@ -1186,6 +1197,11 @@ open class KBitwuzlaExprConverter(
                 return@with expr.arg.uncheckedCast()
             }
 
+            val retypedArray = ArrayDomainRetyper(fromSort, toSort).retype(expr.arg)
+            if (retypedArray != null) {
+                return@with AdapterTermRewriter(ctx).apply(retypedArray).uncheckedCast()
+            }
+
             val indices = toSort.domainSorts.map {
                 mkFreshConst("i", it)
             }
@@ -1216,6 +1232,135 @@ open class KBitwuzlaExprConverter(
         }
     }
 
+    private inner class ArrayDomainRetyper(
+        private val fromSort: KArraySortBase<*>,
+        private val toSort: KArraySortBase<*>
+    ) : KNonRecursiveTransformer(ctx) {
+        private val retypedIndices = hashMapOf<KDecl<*>, KDecl<*>>()
+        private var failed = false
+
+        fun retype(array: KExpr<*>): KExpr<*>? {
+            val result = apply(array)
+            return if (failed || result.sort != toSort) null else result
+        }
+
+        override fun <T : KSort> exprTransformationRequired(expr: KExpr<T>): Boolean =
+            expr !is KInterpretedValue<T> && !expr.isAdapterTerm()
+
+        private fun KExpr<*>.isAdapterTerm(): Boolean =
+            this is BoolToBv1AdapterExpr ||
+                this is Bv1ToBoolAdapterExpr ||
+                this is Bv32ToUninterpretedSortAdapterExpr ||
+                this is ArrayAdapterExpr<*, *>
+
+        override fun <T : KSort, A : KSort> transformApp(expr: KApp<T, A>): KExpr<T> {
+            if (expr.sort == fromSort || expr.args.any { it.isRetypedIndex() }) failed = true
+            return expr
+        }
+
+        override fun <T : KSort> transform(expr: KEqExpr<T>): KExpr<KBoolSort> =
+            transformExprAfterTransformed(expr, expr.lhs, expr.rhs) { lhs, rhs ->
+                retypedEquality(lhs, rhs) ?: retypedEquality(rhs, lhs) ?: run {
+                    if (lhs.isRetypedIndex() || rhs.isRetypedIndex()) failed = true
+                    ctx.mkEq(lhs, rhs)
+                }
+            }
+
+        override fun <A : KArraySortBase<R>, R : KSort> transform(expr: KArrayConst<A, R>): KExpr<A> =
+            if (expr.sort != fromSort) super.transform(expr) else retypedConstArray(expr)
+
+        override fun <D : KSort, R : KSort> transform(expr: KArrayStore<D, R>): KExpr<KArraySort<D, R>> =
+            if (expr.sort != fromSort) super.transform(expr) else retypedStore(expr)
+
+        override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+            expr: KArray2Store<D0, D1, R>
+        ): KExpr<KArray2Sort<D0, D1, R>> =
+            if (expr.sort != fromSort) super.transform(expr) else retypedStore(expr)
+
+        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+            expr: KArray3Store<D0, D1, D2, R>
+        ): KExpr<KArray3Sort<D0, D1, D2, R>> =
+            if (expr.sort != fromSort) super.transform(expr) else retypedStore(expr)
+
+        override fun <R : KSort> transform(expr: KArrayNStore<R>): KExpr<KArrayNSort<R>> =
+            if (expr.sort != fromSort) super.transform(expr) else retypedStore(expr)
+
+        override fun <D : KSort, R : KSort> transform(expr: KArrayLambda<D, R>): KExpr<KArraySort<D, R>> =
+            if (expr.sort != fromSort) super.transform(expr) else retypedLambda(expr)
+
+        override fun <D0 : KSort, D1 : KSort, R : KSort> transform(
+            expr: KArray2Lambda<D0, D1, R>
+        ): KExpr<KArray2Sort<D0, D1, R>> =
+            if (expr.sort != fromSort) super.transform(expr) else retypedLambda(expr)
+
+        override fun <D0 : KSort, D1 : KSort, D2 : KSort, R : KSort> transform(
+            expr: KArray3Lambda<D0, D1, D2, R>
+        ): KExpr<KArray3Sort<D0, D1, D2, R>> =
+            if (expr.sort != fromSort) super.transform(expr) else retypedLambda(expr)
+
+        override fun <R : KSort> transform(expr: KArrayNLambda<R>): KExpr<KArrayNSort<R>> =
+            if (expr.sort != fromSort) super.transform(expr) else retypedLambda(expr)
+
+        private fun <T : KSort> retypedConstArray(expr: KArrayConst<*, *>): KExpr<T> {
+            val array: KExpr<KSort> = expr.uncheckedCast()
+            return transformExprAfterTransformed(array, expr.value) { value ->
+                val wellSortedValue: KExpr<KSort> = value.convertToExpectedIfNeeded(toSort.range)
+                val arraySort: KArraySortBase<KSort> = toSort.uncheckedCast()
+                ctx.mkArrayConst(arraySort, wellSortedValue).uncheckedCast()
+            }.uncheckedCast()
+        }
+
+        private fun <T : KSort> retypedStore(expr: KArrayStoreBase<*, *>): KExpr<T> {
+            val store: KExpr<KSort> = expr.uncheckedCast()
+            return transformExprAfterTransformed(store, expr.args) { args ->
+                val indices = args.subList(1, args.lastIndex)
+                if (indices.any { it !is KInterpretedValue<*> }) failed = true
+                val array: KExpr<KArraySortBase<KSort>> = args.first().uncheckedCast()
+                with(ctx) { mkAnyArrayStore(array, indices, args.last()) }.uncheckedCast()
+            }.uncheckedCast()
+        }
+
+        private fun <T : KSort> retypedLambda(expr: KArrayLambdaBase<*, *>): KExpr<T> {
+            val oldDecls = expr.indexVarDeclarations
+            if (oldDecls.size != toSort.domainSorts.size) failed = true
+            val newDecls = oldDecls.zip(toSort.domainSorts) { old, sort -> retypedIndexDecl(old, sort) }
+
+            val lambda: KExpr<KSort> = expr.uncheckedCast()
+            val body: KExpr<KSort> = expr.body.uncheckedCast()
+            return transformExprAfterTransformed(lambda, body) { transformedBody ->
+                val wellSortedBody: KExpr<KSort> = transformedBody.convertToExpectedIfNeeded(toSort.range)
+                with(ctx) { mkAnyArrayLambda(newDecls, wellSortedBody) }.uncheckedCast()
+            }.uncheckedCast()
+        }
+
+        private fun retypedIndexDecl(old: KDecl<*>, sort: KSort): KDecl<*> = when {
+            old.sort == sort -> old
+            old.sort == ctx.bv32Sort && sort is KUninterpretedSort ->
+                retypedIndices.getOrPut(old) { ctx.mkFreshConstDecl(old.name, sort) }
+            else -> {
+                failed = true
+                old
+            }
+        }
+
+        private fun <T : KSort> retypedEquality(index: KExpr<T>, other: KExpr<T>): KExpr<KBoolSort>? {
+            val newIndex = retypedConst(index) ?: return null
+            val newOther: KExpr<KUninterpretedSort> = when {
+                other is KBitVec32Value -> Bv32ToUninterpretedSortAdapterExpr(other, newIndex.sort)
+                else -> retypedConst(other) ?: return null
+            }
+            return ctx.mkEq(newIndex, newOther)
+        }
+
+        private fun KExpr<*>.isRetypedIndex(): Boolean = this is KConst<*> && decl in retypedIndices
+
+        private fun retypedConst(expr: KExpr<*>): KExpr<KUninterpretedSort>? {
+            if (expr !is KConst<*>) return null
+            val newDecl = retypedIndices[expr.decl] ?: return null
+            return ctx.mkConstApp(newDecl).uncheckedCast()
+        }
+    }
+
     inline fun <T : KSort> BitwuzlaTerm.convertBv(
         op: (KExpr<KBvSort>, KExpr<KBvSort>) -> KExpr<T>
     ) = convert { a0: KExpr<KSort>, a1: KExpr<KSort> ->

ksmt-bitwuzla/ksmt-bitwuzla-core/src/test/kotlin/io/ksmt/solver/bitwuzla/UninterpretedSortArrayModelTest.kt

@@ -0,0 +1,56 @@
+package io.ksmt.solver.bitwuzla
+
+import io.ksmt.KContext
+import io.ksmt.solver.KSolverStatus
+import kotlin.test.Test
+import kotlin.test.assertEquals
+
+class UninterpretedSortArrayModelTest {
+    private val ctx = KContext()
+    private val solver = KBitwuzlaSolver(ctx)
+
+    @Test
+    fun detachModelOfSelectedTwoIndexArrayOverUninterpretedSort(): Unit = with(ctx) {
+        val address = mkUninterpretedSort("Address")
+        val array = mkConst("input", mkArraySort(address, bv32Sort, bv8Sort))
+        val a = mkConst("a", address)
+        val i = mkConst("i", bv32Sort)
+        val selected = array.select(a, i)
+
+        solver.assert(selected eq mkBv(5.toByte()))
+        assertEquals(KSolverStatus.SAT, solver.check())
+
+        val model = solver.model().detach()
+        assertEquals(mkBv(5.toByte()), model.eval(selected))
+    }
+
+    @Test
+    fun detachModelOfEqualTwoIndexArraysOverUninterpretedSort(): Unit = with(ctx) {
+        val address = mkUninterpretedSort("Address")
+        val sort = mkArraySort(address, bv32Sort, bv8Sort)
+        val array = mkConst("input", sort)
+        val other = mkConst("other", sort)
+
+        solver.assert(array eq other)
+        assertEquals(KSolverStatus.SAT, solver.check())
+
+        val model = solver.model().detach()
+        assertEquals(model.eval(array), model.eval(other))
+    }
+
+    @Test
+    fun detachModelOfStoredTwoIndexArrayOverUninterpretedSort(): Unit = with(ctx) {
+        val address = mkUninterpretedSort("Address")
+        val sort = mkArraySort(address, bv32Sort, bv8Sort)
+        val array = mkConst("input", sort)
+        val other = mkConst("other", sort)
+        val a = mkConst("a", address)
+        val i = mkConst("i", bv32Sort)
+
+        solver.assert(array eq other.store(a, i, mkBv(7.toByte())))
+        assertEquals(KSolverStatus.SAT, solver.check())
+
+        val model = solver.model().detach()
+        assertEquals(mkBv(7.toByte()), model.eval(array.select(a, i)))
+    }
+}