From 425dd732e84b09ca2ab03a1ecdd8babdcc12a292 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol <8640896+Saloed@users.noreply.github.com> Date: Tue, 11 Aug 2026 21:34:44 +0000 Subject: [PATCH 1/5] Enable cvc5 const arrays KContext.mkArrayConst is internalized as cvc5's STORE_ALL, which cvc5 refuses unless the arrays-exp option is set: Cannot handle assertion with term of kind STORE_ALL in this configuration. Try --arrays-exp. So ksmt emitted terms its own solver rejects. It went unnoticed because cvc5's rewriter eliminates the const array in most shapes: only a store over a const array, read back at a symbolic index, survives to the check. Set the option alongside fp-exp, which is the same kind of opt-in. On the Linux natives ksmt ships, the rejection did not even surface as a CVC5ApiException: libcvc5, libcvc5parser and libcvc5jni each statically link their own libstdc++, so the exception could not be unwound across the library boundary and the unwinder called abort(). The JVM does not trap SIGABRT, so the process died at exit code 134 with no diagnostic. That packaging issue is not addressed here and is why ConstArrayTest has no negative test - a JUnit worker does not survive the unset case. Co-Authored-By: Claude Opus 5 (1M context) --- .../kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt | 3 + .../io/ksmt/solver/cvc5/ConstArrayTest.kt | 70 +++++++++++++++++++ 2 files changed, 73 insertions(+) create mode 100644 ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/ConstArrayTest.kt diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt index 10d3b4f01..fdc0eed77 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt @@ -55,6 +55,9 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver + +/** + * 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)) + + @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): KSolverStatus = + KContext().use { ctx -> + KCvc5Solver(ctx).use { solver -> + solver.assert(ctx.query(shape)) + solver.check() + } + } + + private fun KContext.query(shape: Shape) = mkArraySort(bv64Sort, bv8Sort).let { sort -> + val base: KExpr = 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) + } + } +} From 8e39062232e6be8707413bd18568b9c83afa90cc Mon Sep 17 00:00:00 2001 From: Valentyn Sobol <8640896+Saloed@users.noreply.github.com> Date: Tue, 11 Aug 2026 21:35:31 +0000 Subject: [PATCH 2/5] Set cvc5 experimental options only for the declared theories fp-exp and arrays-exp were set on every solver, whether or not the query could contain a floating-point sort or a const array. Both are cvc5 experimental extensions, so enabling them unconditionally opts every query into behaviour it does not need. Gate them on the theory set passed to optimizeForTheories. A caller that does not call it declares nothing about the query, so both options are still set - that stays the default. Co-Authored-By: Claude Opus 5 (1M context) --- .../main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt | 14 +++++++++++--- .../ksmt/solver/cvc5/KCvc5SolverConfiguration.kt | 8 ++++++++ .../kotlin/io/ksmt/solver/cvc5/ConstArrayTest.kt | 12 +++++++++++- 3 files changed, 30 insertions(+), 4 deletions(-) diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt index fdc0eed77..d064f4342 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt +++ b/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,20 +44,27 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver() + /** + * 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? = null + private set + override fun setCvc5Option(option: String, value: String) { options[option] = value } @@ -52,6 +59,7 @@ class KCvc5SolverLazyConfiguration : KCvc5SolverConfiguration { override fun optimizeForTheories(theories: Set?, quantifiersAllowed: Boolean) { logicConfiguration = theories.smtLib2String(quantifiersAllowed) + declaredTheories = theories } fun configure(solver: Solver) { diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/ConstArrayTest.kt b/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/ConstArrayTest.kt index 3ec5e8534..c46ca5043 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/ConstArrayTest.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/ConstArrayTest.kt @@ -3,6 +3,7 @@ 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 @@ -32,6 +33,14 @@ class ConstArrayTest { 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)) @@ -49,9 +58,10 @@ class ConstArrayTest { private companion object { private const val STORED_BYTE = 0xaa.toByte() - private fun solve(shape: Shape): KSolverStatus = + private fun solve(shape: Shape, theories: Set? = null): KSolverStatus = KContext().use { ctx -> KCvc5Solver(ctx).use { solver -> + theories?.let { solver.configure { optimizeForTheories(it, quantifiersAllowed = false) } } solver.assert(ctx.query(shape)) solver.check() } From 70f17d21a271eecc55c47afc602e97c70e0618a7 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol <8640896+Saloed@users.noreply.github.com> Date: Tue, 11 Aug 2026 21:35:42 +0000 Subject: [PATCH 3/5] Fix optimizeForTheories for uninterpreted sort values KZ3ExprInternalizer keeps uninterpreted sort values distinct by mapping each to a distinct value of a descriptor sort, so every query carries constraints over that sort whichever theories the caller declared. optimizeForTheories derived the logic from the caller's theory set alone, so the declared logic and the actual benchmark disagreed, and Z3 failed in one of two ways, neither naming the logic: - UNKNOWN, "Benchmark constrains arithmetic, but specified logic does not support it" - QF_UF, QF_LRA and QF_NRA; - or SAT with the descriptor sort treated as uninterpreted, which put it in Z3_model_get_sort and made KZ3Model.uninterpretedSorts throw ClassCastException: KIntSort cannot be cast to KUninterpretedSort - every logic containing bitvectors. 7 of the 26 emittable combinations were affected. {UF, Array, BV} is a complete declaration of such a caller's own theories and still failed, because the caller cannot declare a theory ksmt adds on its own behalf. resolveLogic now picks the logic and the descriptor sort together: a bitvector descriptor when the theory set has BV and no integer arithmetic, otherwise an integer one, adding LIA only when neither LIA nor NIA is present. Combinations with no specialized Z3 solver fall back to the general solver, which accepts either descriptor. 21 of 26 keep a specialized logic. QF_AX, QF_LRA and QF_UF widen to QF_ALIA, QF_LIRA and QF_UFLIA; QF_FP, QF_FPLRA, QF_UFLRA and QF_UFNRA fall back, since whether a logic tolerates a sort it does not declare is per-logic Z3 behaviour that cannot be derived from the theory set. assert internalizes before it touches solver, so exprInternalizer now forces solver creation to resolve the configuration first. Co-Authored-By: Claude Opus 5 (1M context) --- .../kotlin/io/ksmt/solver/z3/KZ3Context.kt | 3 + .../io/ksmt/solver/z3/KZ3ExprInternalizer.kt | 17 ++- .../kotlin/io/ksmt/solver/z3/KZ3Solver.kt | 8 +- .../ksmt/solver/z3/KZ3SolverConfiguration.kt | 49 ++++++- .../ksmt/solver/z3/OptimizeForTheoriesTest.kt | 130 ++++++++++++++++++ 5 files changed, 198 insertions(+), 9 deletions(-) create mode 100644 ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/OptimizeForTheoriesTest.kt diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt index d8f2a614a..eea447d5d 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Context.kt @@ -148,6 +148,9 @@ class KZ3Context( return ast } + /** Chosen with the logic, see [KZ3SolverLazyConfiguration.resolveLogic]. */ + var uninterpretedValueDescriptor: KZ3UninterpretedValueDescriptor = KZ3UninterpretedValueDescriptor.INT + private val uninterpretedSortValueInterpreter = hashMapOf() private val uninterpretedSortValueDecls = Long2ObjectOpenHashMap() diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt index 75cdfc558..2749671a7 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt @@ -863,7 +863,7 @@ open class KZ3ExprInternalizer( * assertion forces that all values of T are also distinct. * */ override fun transform(expr: KUninterpretedSortValue): KExpr = with(expr) { - transform(ctx.mkIntNum(expr.valueIdx)) { intValueExpr -> + transform(mkUniqueValueDescriptor(expr.valueIdx)) { descriptorExpr -> val nativeSort = sort.internalizeSort() val valueDecl = z3InternCtx.saveUninterpretedSortValueDecl( Native.mkFreshFuncDecl(nCtx, "value", 0, null, nativeSort), @@ -874,8 +874,8 @@ open class KZ3ExprInternalizer( // Force expression save to perform `incRef` and prevent possible reference counting issues saveInternalizedExpr(expr, it) - z3InternCtx.registerUninterpretedSortValue(expr, intValueExpr, it) { - val descriptorSort = ctx.intSort.internalizeSort() + z3InternCtx.registerUninterpretedSortValue(expr, descriptorExpr, it) { + val descriptorSort = uniqueValueDescriptorSort().internalizeSort() z3InternCtx.saveUninterpretedSortValueInterpreter( Native.mkFreshFuncDecl(nCtx, "interpreter", 1, longArrayOf(nativeSort), descriptorSort) ) @@ -884,6 +884,17 @@ open class KZ3ExprInternalizer( } } + private fun uniqueValueDescriptorSort(): KSort = when (z3InternCtx.uninterpretedValueDescriptor) { + KZ3UninterpretedValueDescriptor.INT -> ctx.intSort + KZ3UninterpretedValueDescriptor.BV -> ctx.bv32Sort + } + + private fun mkUniqueValueDescriptor(valueIdx: Int): KExpr<*> = + when (z3InternCtx.uninterpretedValueDescriptor) { + KZ3UninterpretedValueDescriptor.INT -> ctx.mkIntNum(valueIdx) + KZ3UninterpretedValueDescriptor.BV -> ctx.mkBv(valueIdx) + } + inline fun > S.transform( arg: KExpr<*>, operation: (Long, Long) -> Long diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt index 9faecab6e..2d2cacbef 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt @@ -42,6 +42,8 @@ open class KZ3Solver(private val ctx: KContext) : KSolver? = null + private var quantifiersAllowed: Boolean = false + override fun optimizeForTheories(theories: Set?, quantifiersAllowed: Boolean) { - if (theories.isNullOrEmpty() || !supportedLogicCombination(theories, quantifiersAllowed)) { - logicConfiguration = null - return + this.theories = theories + this.quantifiersAllowed = quantifiersAllowed + } + + /** + * 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 Z3 answer UNKNOWN or expose the sort in the model, so the two are chosen + * together. Combinations with no specialized solver fall back to the general one. + * */ + fun resolveLogic(): KZ3ResolvedLogic { + val requestedTheories = theories + if (requestedTheories.isNullOrEmpty()) return GENERAL_SOLVER + + val hasIntegerArithmetic = LIA in requestedTheories || NIA in requestedTheories + + if (BV in requestedTheories && !hasIntegerArithmetic) { + return resolve(requestedTheories, KZ3UninterpretedValueDescriptor.BV) } - logicConfiguration = theories.smtLib2String(quantifiersAllowed) + val theoriesWithDescriptor = if (hasIntegerArithmetic) requestedTheories else requestedTheories + LIA + return resolve(theoriesWithDescriptor, KZ3UninterpretedValueDescriptor.INT) } + private fun resolve(theories: Set, descriptor: KZ3UninterpretedValueDescriptor) = + if (supportedLogicCombination(theories, quantifiersAllowed)) { + KZ3ResolvedLogic(theories.smtLib2String(quantifiersAllowed), descriptor) + } else { + GENERAL_SOLVER + } + /** * Z3 provide special solver only for the following theory combinations * */ @@ -78,6 +115,8 @@ class KZ3SolverLazyConfiguration(params: Params) : KZ3SolverConfigurationImpl(pa } companion object { + private val GENERAL_SOLVER = KZ3ResolvedLogic(logic = null, KZ3UninterpretedValueDescriptor.INT) + private fun l(vararg theories: KTheory) = theories.toSet() private val supportedTheoriesWithQuantifiers = setOf( diff --git a/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/OptimizeForTheoriesTest.kt b/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/OptimizeForTheoriesTest.kt new file mode 100644 index 000000000..a9a529eb2 --- /dev/null +++ b/ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/OptimizeForTheoriesTest.kt @@ -0,0 +1,130 @@ +package io.ksmt.solver.z3 + +import io.ksmt.KContext +import io.ksmt.solver.KSolverException +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.KTheory +import io.ksmt.solver.KTheory.Array +import io.ksmt.solver.KTheory.BV +import io.ksmt.solver.KTheory.FP +import io.ksmt.solver.KTheory.LIA +import io.ksmt.solver.KTheory.LRA +import io.ksmt.solver.KTheory.NIA +import io.ksmt.solver.KTheory.NRA +import io.ksmt.solver.KTheory.UF +import io.ksmt.utils.mkConst +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertTrue + +/** + * ksmt keeps uninterpreted sort values distinct through values of a descriptor sort, so every query + * constrains that sort whichever theories the caller declared. When the logic from + * [io.ksmt.solver.KSolverConfiguration.optimizeForTheories] forbade it, Z3 either answered UNKNOWN + * (`QF_UF`, `QF_LRA`, `QF_NRA`) or treated the descriptor sort as uninterpreted, which put it in + * the model and made [KZ3Model.uninterpretedSorts] throw `ClassCastException` (every BV logic). + * + * 7 of the 26 emittable combinations were affected. {[UF], [Array], [BV]} is a complete declaration + * of such a caller's own theories and still failed, since a caller cannot declare a theory ksmt adds + * on its own behalf. + */ +class OptimizeForTheoriesTest { + + @Test + fun checkAndModelWorkForEveryTheoryCombination() { + val broken = ALL_THEORY_COMBINATIONS.mapNotNull { theories -> + val outcome = runCatching { solveAndReadModel(theories) } + .fold({ it }, { "threw ${it::class.simpleName}: ${it.message?.take(80)}" }) + outcome.takeIf { it != EXPECTED_OUTCOME }?.let { "${theories.describe()} -> $it" } + } + + assertTrue( + broken.isEmpty(), + "Expected '$EXPECTED_OUTCOME' for every theory combination, but:\n" + broken.joinToString("\n") + ) + } + + /** + * The logic is fixed when the solver is created, and the first assertion already depends on it, + * so it cannot be changed afterwards. + */ + @Test + fun optimizeForTheoriesIsRejectedAfterFirstAssert() { + KContext().use { ctx -> + KZ3Solver(ctx).use { solver -> + solver.assert(ctx.boolSort.mkConst("a")) + + assertFailsWith { + solver.configure { optimizeForTheories(setOf(BV), quantifiersAllowed = false) } + } + } + } + } + + /** Uninterpreted sort values must stay distinct whichever descriptor sort encodes them. */ + @Test + fun uninterpretedSortValuesStayDistinctUnderBvDescriptor() { + KContext().use { ctx -> + KZ3Solver(ctx).use { solver -> + solver.configure { optimizeForTheories(setOf(BV), quantifiersAllowed = false) } + with(ctx) { + val ref = mkUninterpretedSort(UNINTERPRETED_SORT_NAME) + // two different values of the same sort cannot be equal + solver.assert(mkUninterpretedSortValue(ref, 0) eq mkUninterpretedSortValue(ref, 1)) + } + assertEquals(KSolverStatus.UNSAT, solver.check()) + } + } + } + + private companion object { + private const val UNINTERPRETED_SORT_NAME = "Ref" + private const val VALUE_COUNT = 3 + private const val EXPECTED_OUTCOME = "SAT, model sorts=[$UNINTERPRETED_SORT_NAME]" + + private fun t(vararg theories: KTheory) = theories.toSet() + + /** Every combination [KZ3SolverLazyConfiguration] has a specialized Z3 solver for, plus none. */ + private val ALL_THEORY_COMBINATIONS: List?> = listOf( + null, emptySet(), + t(Array), t(Array, BV), t(Array, LIA), t(Array, NIA), t(Array, UF, BV), t(Array, UF, LIA), + t(Array, UF, LIA, LRA), t(Array, UF, NIA), t(Array, UF, NIA, NRA), t(BV), t(BV, FP), t(FP), + t(FP, LRA), t(LIA), t(LIA, LRA), t(LRA), t(NIA), t(NIA, NRA), t(NRA), t(UF), t(UF, BV), + t(UF, LIA), t(UF, LRA), t(UF, NIA), t(UF, NIA, NRA), t(UF, NRA), + ) + + private fun Set?.describe() = + this?.map { it.name }?.sorted()?.joinToString(",")?.ifEmpty { "" } ?: "" + + /** + * The query is what a symbolic execution engine emits for a handful of concrete heap + * references: distinct [io.ksmt.expr.KUninterpretedSortValue]s, each pinned to a constant. + * The bitvector assertion makes [BV] an honest part of the declared theory sets. + */ + private fun solveAndReadModel(theories: Set?): String = + KContext().use { ctx -> + KZ3Solver(ctx).use { solver -> + theories?.let { solver.configure { optimizeForTheories(it, quantifiersAllowed = false) } } + + with(ctx) { + val ref = mkUninterpretedSort(UNINTERPRETED_SORT_NAME) + val consts = List(VALUE_COUNT) { i -> + ref.mkConst("c$i").also { solver.assert(it eq mkUninterpretedSortValue(ref, i)) } + } + for (i in consts.indices) { + for (j in i + 1 until consts.size) solver.assert(consts[i] neq consts[j]) + } + solver.assert(bv32Sort.mkConst("x") eq mkBv(42)) + } + + val status = solver.check() + if (status != KSolverStatus.SAT) { + "$status" + } else { + "SAT, model sorts=${solver.model().uninterpretedSorts.map { it.name }}" + } + } + } + } +} From b96b20f2a5f4b578668a6240ad028f5d7ff5d94e Mon Sep 17 00:00:00 2001 From: Valentyn Sobol <8640896+Saloed@users.noreply.github.com> Date: Tue, 11 Aug 2026 21:50:05 +0000 Subject: [PATCH 4/5] Fix cvc5 optimizeForTheories for uninterpreted sort values Same defect as the Z3 one, in KCvc5ExprInternalizer: uninterpreted sort values are kept distinct by mapping each to a distinct value of a descriptor sort, so every query carries constraints over that sort whichever theories the caller declared. optimizeForTheories derived the logic from the caller's theory set alone, and cvc5 then rejected the check under QF_UF, QF_UFBV, QF_AUFBV, QF_AX and QF_ABV among others. Worse than on Z3: cvc5 has no supported-combination filter, so any generated logic reaches setLogic, and the rejection cannot unwind out of the shipped Linux natives, so it killed the process at exit code 134 with no diagnostic instead of raising CVC5ApiException. optimizeForTheories now picks the logic and the descriptor sort together, with the same rule as Z3: a bitvector descriptor when the theory set has BV and no integer arithmetic, otherwise an integer one, adding LIA only when neither LIA nor NIA is present. An empty theory set keeps QF_SAT, since it declares no theory that could carry an uninterpreted sort. All 17 combinations under which an uninterpreted sort is legal now check and produce a readable model; previously 13 of 29 aborted. Sets that declare neither UF nor Array still fail, but there the query is outside the declared logic and cvc5 is right to reject it. Co-Authored-By: Claude Opus 5 (1M context) --- .../io/ksmt/solver/cvc5/KCvc5Context.kt | 3 + .../ksmt/solver/cvc5/KCvc5ExprInternalizer.kt | 17 ++- .../kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt | 2 + .../solver/cvc5/KCvc5SolverConfiguration.kt | 31 ++++- .../solver/cvc5/OptimizeForTheoriesTest.kt | 116 ++++++++++++++++++ 5 files changed, 165 insertions(+), 4 deletions(-) create mode 100644 ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/OptimizeForTheoriesTest.kt diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt index 124227a45..696ffbb8b 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt +++ b/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) diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt index 7deb73ae1..361f4e417 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt @@ -1152,11 +1152,11 @@ class KCvc5ExprInternalizer( * assertion forces that all values of T are also distinct. * */ override fun transform(expr: KUninterpretedSortValue): KExpr = 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) } } @@ -1164,6 +1164,17 @@ class KCvc5ExprInternalizer( } } + 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.transformQuantifiedExpression( bounds: List>, body: KExpr<*>, diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt index d064f4342..9307012a9 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Solver.kt @@ -48,6 +48,8 @@ open class KCvc5Solver(private val ctx: KContext) : KSolver() @@ -49,6 +55,9 @@ class KCvc5SolverLazyConfiguration : KCvc5SolverConfiguration { var declaredTheories: Set? = null private set + var valueDescriptor: KCvc5UninterpretedValueDescriptor = KCvc5UninterpretedValueDescriptor.INT + private set + override fun setCvc5Option(option: String, value: String) { options[option] = value } @@ -57,9 +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?, 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) { diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/OptimizeForTheoriesTest.kt b/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/OptimizeForTheoriesTest.kt new file mode 100644 index 000000000..0b3deab6b --- /dev/null +++ b/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/OptimizeForTheoriesTest.kt @@ -0,0 +1,116 @@ +package io.ksmt.solver.cvc5 + +import io.ksmt.KContext +import io.ksmt.solver.KSolverException +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.KTheory +import io.ksmt.solver.KTheory.Array +import io.ksmt.solver.KTheory.BV +import io.ksmt.solver.KTheory.LIA +import io.ksmt.solver.KTheory.LRA +import io.ksmt.solver.KTheory.NIA +import io.ksmt.solver.KTheory.NRA +import io.ksmt.solver.KTheory.UF +import io.ksmt.utils.mkConst +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertTrue + +/** + * ksmt keeps uninterpreted sort values distinct through values of a descriptor sort, so every query + * constrains that sort whichever theories the caller declared. When the logic from + * [io.ksmt.solver.KSolverConfiguration.optimizeForTheories] forbade it, cvc5 rejected the check -- + * `QF_UF`, `QF_UFBV`, `QF_AUFBV`, `QF_AX` and `QF_ABV` among them. + * + * Only theory sets containing [UF] or [Array] appear below, since those are the ones under which an + * uninterpreted sort is legal at all. A regression here does not fail the test, it kills the JUnit + * worker: on the Linux natives ksmt ships, cvc5's rejection cannot unwind out of libcvc5 and the + * process dies at exit code 134 with no diagnostic. + */ +class OptimizeForTheoriesTest { + + @Test + fun checkAndModelWorkForEveryTheoryCombination() { + val broken = THEORY_COMBINATIONS_WITH_UNINTERPRETED_SORTS.mapNotNull { theories -> + val outcome = runCatching { solveAndReadModel(theories) } + .fold({ it }, { "threw ${it::class.simpleName}: ${it.message?.take(80)}" }) + outcome.takeIf { it != EXPECTED_OUTCOME }?.let { "${theories.describe()} -> $it" } + } + + assertTrue( + broken.isEmpty(), + "Expected '$EXPECTED_OUTCOME' for every theory combination, but:\n" + broken.joinToString("\n") + ) + } + + @Test + fun optimizeForTheoriesIsRejectedAfterFirstAssert() { + KContext().use { ctx -> + KCvc5Solver(ctx).use { solver -> + solver.assert(ctx.boolSort.mkConst("a")) + + assertFailsWith { + solver.configure { optimizeForTheories(setOf(UF, BV), quantifiersAllowed = false) } + } + } + } + } + + /** Uninterpreted sort values must stay distinct whichever descriptor sort encodes them. */ + @Test + fun uninterpretedSortValuesStayDistinctUnderBvDescriptor() { + KContext().use { ctx -> + KCvc5Solver(ctx).use { solver -> + solver.configure { optimizeForTheories(setOf(UF, BV), quantifiersAllowed = false) } + with(ctx) { + val ref = mkUninterpretedSort(UNINTERPRETED_SORT_NAME) + solver.assert(mkUninterpretedSortValue(ref, 0) eq mkUninterpretedSortValue(ref, 1)) + } + assertEquals(KSolverStatus.UNSAT, solver.check()) + } + } + } + + private companion object { + private const val UNINTERPRETED_SORT_NAME = "Ref" + private const val VALUE_COUNT = 3 + private const val EXPECTED_OUTCOME = "SAT, model sorts=[$UNINTERPRETED_SORT_NAME]" + + private fun t(vararg theories: KTheory) = theories.toSet() + + private val THEORY_COMBINATIONS_WITH_UNINTERPRETED_SORTS: List?> = listOf( + null, + t(Array), t(Array, BV), t(Array, LIA), t(Array, NIA), t(Array, UF), t(Array, UF, BV), + t(Array, UF, LIA), t(Array, UF, LIA, LRA), t(Array, UF, NIA), t(Array, UF, NIA, NRA), + t(UF), t(UF, BV), t(UF, LIA), t(UF, LRA), t(UF, NIA), t(UF, NIA, NRA), t(UF, NRA), + ) + + private fun Set?.describe() = + this?.map { it.name }?.sorted()?.joinToString(",") ?: "" + + private fun solveAndReadModel(theories: Set?): String = + KContext().use { ctx -> + KCvc5Solver(ctx).use { solver -> + theories?.let { solver.configure { optimizeForTheories(it, quantifiersAllowed = false) } } + + with(ctx) { + val ref = mkUninterpretedSort(UNINTERPRETED_SORT_NAME) + val consts = List(VALUE_COUNT) { i -> + ref.mkConst("c$i").also { solver.assert(it eq mkUninterpretedSortValue(ref, i)) } + } + for (i in consts.indices) { + for (j in i + 1 until consts.size) solver.assert(consts[i] neq consts[j]) + } + } + + val status = solver.check() + if (status != KSolverStatus.SAT) { + "$status" + } else { + "SAT, model sorts=${solver.model().uninterpretedSorts.map { it.name }}" + } + } + } + } +} From 2af5e8f63b5ee3be9fdd70800816bf340a6bf152 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol <8640896+Saloed@users.noreply.github.com> Date: Tue, 11 Aug 2026 21:35:42 +0000 Subject: [PATCH 5/5] Upgrade version to 0.6.7 Co-Authored-By: Claude Opus 5 (1M context) --- README.md | 6 +++--- buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts | 2 +- docs/getting-started.md | 6 +++--- examples/build.gradle.kts | 6 +++--- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index 5d01a7b81..55af96a2b 100644 --- a/README.md +++ b/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 diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts index fa3143a65..cfb3207ef 100644 --- a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts +++ b/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() diff --git a/docs/getting-started.md b/docs/getting-started.md index 3722a1fd7..c8bc466ac 100644 --- a/docs/getting-started.md +++ b/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") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index c57a7f000..c805f32af 100644 --- a/examples/build.gradle.kts +++ b/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 {