Solver configuration fixes

README.md

@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.6)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.6.7)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.6.6")
+implementation("io.ksmt:ksmt-core:0.6.7")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.6.6")
+implementation("io.ksmt:ksmt-z3:0.6.7")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 

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

@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.6.6"
+version = "0.6.7"
 
 repositories {
     mavenCentral()

docs/getting-started.md

@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.6.6")    
+    implementation("io.ksmt:ksmt-core:0.6.7")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.6.6")
+    implementation("io.ksmt:ksmt-z3:0.6.7")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.6.6")
+    implementation("io.ksmt:ksmt-bitwuzla:0.6.7")
 }
 ```
 

examples/build.gradle.kts

@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.6.6")
+    implementation("io.ksmt:ksmt-core:0.6.7")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.6.6")
+    implementation("io.ksmt:ksmt-z3:0.6.7")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.6.6")
+    implementation("io.ksmt:ksmt-runner:0.6.7")
 }
 
 java {

ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt

@@ -37,6 +37,9 @@ class KCvc5Context(
 ) : AutoCloseable {
     private var isClosed = false
 
+    /** Chosen with the logic, see [KCvc5SolverLazyConfiguration.optimizeForTheories]. */
+    var uninterpretedValueDescriptor: KCvc5UninterpretedValueDescriptor = KCvc5UninterpretedValueDescriptor.INT
+
     private val uninterpretedSortCollector = KUninterpretedSortCollector(this)
     private var exprCurrentLevelCacheRestorer = KCurrentScopeExprCacheRestorer(uninterpretedSortCollector, ctx)
 

ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt

@@ -1152,18 +1152,29 @@ class KCvc5ExprInternalizer(
      * assertion forces that all values of T are also distinct.
      * */
     override fun transform(expr: KUninterpretedSortValue): KExpr<KUninterpretedSort> = with(expr) {
-        transform(ctx.mkIntNum(expr.valueIdx)) { intValueExpr: Term ->
+        transform(mkUniqueValueDescriptor(expr.valueIdx)) { descriptorExpr: Term ->
             val exprSort = sort.internalizeSort()
             cvc5Ctx.saveUninterpretedSortValue(tm.builder { mkConst(exprSort) }, expr).also {
-                cvc5Ctx.registerUninterpretedSortValue(expr, intValueExpr, it) {
-                    val descriptorSort = ctx.intSort.internalizeSort()
+                cvc5Ctx.registerUninterpretedSortValue(expr, descriptorExpr, it) {
+                    val descriptorSort = uniqueValueDescriptorSort().internalizeSort()
                     solver.declareFun("${sort.name}!interpreter", arrayOf(exprSort), descriptorSort)
                         .also { f -> tm.registerPointer(f) }
                 }
             }
         }
     }
 
+    private fun uniqueValueDescriptorSort(): KSort = when (cvc5Ctx.uninterpretedValueDescriptor) {
+        KCvc5UninterpretedValueDescriptor.INT -> cvc5Ctx.ctx.intSort
+        KCvc5UninterpretedValueDescriptor.BV -> cvc5Ctx.ctx.bv32Sort
+    }
+
+    private fun mkUniqueValueDescriptor(valueIdx: Int): KExpr<*> =
+        when (cvc5Ctx.uninterpretedValueDescriptor) {
+            KCvc5UninterpretedValueDescriptor.INT -> cvc5Ctx.ctx.mkIntNum(valueIdx)
+            KCvc5UninterpretedValueDescriptor.BV -> cvc5Ctx.ctx.mkBv(valueIdx)
+        }
+
     private fun <E : KExpr<*>> E.transformQuantifiedExpression(
         bounds: List<KDecl<*>>,
         body: KExpr<*>,

ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt

@@ -9,6 +9,7 @@ import io.ksmt.solver.KModel
 import io.ksmt.solver.KSolver
 import io.ksmt.solver.KSolverException
 import io.ksmt.solver.KSolverStatus
+import io.ksmt.solver.KTheory
 import io.ksmt.solver.model.KNativeSolverModel
 import io.ksmt.sort.KBoolSort
 import io.ksmt.utils.library.NativeLibraryLoaderUtils
@@ -43,17 +44,29 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver<KCvc5SolverConfigura
         val solver = termManager.builder { Solver(this) }
 
         solverInitialized = true
-        solverLazyConfiguration?.configure(solver)
+        val configuration = solverLazyConfiguration
+        configuration?.configure(solver)
         solverLazyConfiguration = null
 
+        configuration?.let { cvc5Ctx.uninterpretedValueDescriptor = it.valueDescriptor }
+
         solver.setOption("produce-models", "true")
         solver.setOption("produce-unsat-cores", "true")
 
+        val theories = configuration?.declaredTheories
+
         /**
          * Allow floating-point sorts of all sizes, rather than
          * only Float32 (8/24) or Float64 (11/53) (experimental in cvc5 1.0.2)
          */
-        solver.setOption("fp-exp", "true")
+        if (theories == null || KTheory.FP in theories) {
+            solver.setOption("fp-exp", "true")
+        }
+
+        // Allow const arrays, which mkArrayConst is internalized to (experimental in cvc5 1.3.4)
+        if (theories == null || KTheory.Array in theories) {
+            solver.setOption("arrays-exp", "true")
+        }
 
         return solver
     }

ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5SolverConfiguration.kt

@@ -38,10 +38,26 @@ interface KCvc5SolverConfiguration : KSolverConfiguration {
     }
 }
 
+/**
+ * Sort of the descriptor values ksmt uses to keep uninterpreted sort values distinct
+ * (see `KCvc5ExprInternalizer.transform(KUninterpretedSortValue)`).
+ * */
+enum class KCvc5UninterpretedValueDescriptor { INT, BV }
+
 class KCvc5SolverLazyConfiguration : KCvc5SolverConfiguration {
     private var logicConfiguration: String? = null
     private val options = mutableMapOf<String, String>()
 
+    /**
+     * Theories the caller declared, or `null` when they did not, in which case
+     * nothing is known about the query and every theory has to be assumed.
+     * */
+    var declaredTheories: Set<KTheory>? = null
+        private set
+
+    var valueDescriptor: KCvc5UninterpretedValueDescriptor = KCvc5UninterpretedValueDescriptor.INT
+        private set
+
     override fun setCvc5Option(option: String, value: String) {
         options[option] = value
     }
@@ -50,8 +66,29 @@ class KCvc5SolverLazyConfiguration : KCvc5SolverConfiguration {
         logicConfiguration = value
     }
 
+    /**
+     * ksmt keeps uninterpreted sort values distinct through values of a descriptor sort, so every
+     * query constrains that sort whether or not the caller declared its theory. A logic that
+     * forbids it makes cvc5 reject the check, so the two are chosen together.
+     * */
     override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
-        logicConfiguration = theories.smtLib2String(quantifiersAllowed)
+        declaredTheories = theories
+
+        if (theories.isNullOrEmpty()) {
+            logicConfiguration = theories.smtLib2String(quantifiersAllowed)
+            return
+        }
+
+        val hasIntegerArithmetic = KTheory.LIA in theories || KTheory.NIA in theories
+
+        if (KTheory.BV in theories && !hasIntegerArithmetic) {
+            valueDescriptor = KCvc5UninterpretedValueDescriptor.BV
+            logicConfiguration = theories.smtLib2String(quantifiersAllowed)
+            return
+        }
+
+        val theoriesWithDescriptor = if (hasIntegerArithmetic) theories else theories + KTheory.LIA
+        logicConfiguration = theoriesWithDescriptor.smtLib2String(quantifiersAllowed)
     }
 
     fun configure(solver: Solver) {

ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/ConstArrayTest.kt

@@ -0,0 +1,80 @@
+package io.ksmt.solver.cvc5
+
+import io.ksmt.KContext
+import io.ksmt.expr.KExpr
+import io.ksmt.solver.KSolverStatus
+import io.ksmt.solver.KTheory
+import io.ksmt.sort.KArraySort
+import io.ksmt.sort.KBv64Sort
+import io.ksmt.sort.KBv8Sort
+import io.ksmt.utils.mkConst
+import kotlin.test.Test
+import kotlin.test.assertEquals
+
+private typealias ByteArraySort = KArraySort<KBv64Sort, KBv8Sort>
+
+/**
+ * Guards the `arrays-exp` option [KCvc5Solver] sets. [KContext.mkArrayConst] is internalized as
+ * cvc5's `STORE_ALL`, which cvc5 refuses without that option:
+ * *"Cannot handle assertion with term of kind STORE_ALL in this configuration. Try --arrays-exp."*
+ *
+ * Only a store over a const array read at a symbolic index reaches the refusal -- with no store, or
+ * at a concrete index, cvc5's rewriter eliminates the const array first, and over an uninterpreted
+ * base there is no `STORE_ALL` at all. The other tests pin that, so a regression narrows to either
+ * the option or the rewriter.
+ *
+ * There is no test for the unset option: on the Linux natives ksmt ships, each library statically
+ * links its own libstdc++, so the refusal cannot unwind out of libcvc5 and the process dies at exit
+ * code 134 with no diagnostic, taking the JUnit worker with it.
+ */
+class ConstArrayTest {
+
+    @Test
+    fun constArrayStoreSelectAtSymbolicIndexIsSat() =
+        assertEquals(KSolverStatus.SAT, solve(Shape.CONST_ARRAY_STORE_SYMBOLIC_INDEX))
+
+    /** `arrays-exp` is only set when the caller declares [KTheory.Array], or declares nothing. */
+    @Test
+    fun constArrayIsSupportedWhenOptimizedForArrayTheory() =
+        assertEquals(
+            KSolverStatus.SAT,
+            solve(Shape.CONST_ARRAY_STORE_SYMBOLIC_INDEX, setOf(KTheory.Array, KTheory.BV))
+        )
+
+    @Test
+    fun uninterpretedArrayBaseIsUnaffected() =
+        assertEquals(KSolverStatus.SAT, solve(Shape.UNINTERPRETED_BASE))
+
+    @Test
+    fun constArrayWithoutStoreIsUnaffected() =
+        assertEquals(KSolverStatus.UNSAT, solve(Shape.NO_STORE))
+
+    @Test
+    fun constArrayReadAtConcreteIndexIsUnaffected() =
+        assertEquals(KSolverStatus.UNSAT, solve(Shape.CONCRETE_INDEX))
+
+    private enum class Shape { CONST_ARRAY_STORE_SYMBOLIC_INDEX, UNINTERPRETED_BASE, NO_STORE, CONCRETE_INDEX }
+
+    private companion object {
+        private const val STORED_BYTE = 0xaa.toByte()
+
+        private fun solve(shape: Shape, theories: Set<KTheory>? = null): KSolverStatus =
+            KContext().use { ctx ->
+                KCvc5Solver(ctx).use { solver ->
+                    theories?.let { solver.configure { optimizeForTheories(it, quantifiersAllowed = false) } }
+                    solver.assert(ctx.query(shape))
+                    solver.check()
+                }
+            }
+
+        private fun KContext.query(shape: Shape) = mkArraySort(bv64Sort, bv8Sort).let { sort ->
+            val base: KExpr<ByteArraySort> = when (shape) {
+                Shape.UNINTERPRETED_BASE -> sort.mkConst("memory")
+                else -> mkArrayConst(sort, mkBv(0.toByte()))
+            }
+            val array = if (shape == Shape.NO_STORE) base else mkArrayStore(base, mkBv(0L), mkBv(STORED_BYTE))
+            val index = if (shape == Shape.CONCRETE_INDEX) mkBv(1L) else bv64Sort.mkConst("index")
+            mkArraySelect(array, index) eq mkBv(STORED_BYTE)
+        }
+    }
+}