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 { 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 10d3b4f01..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 @@ -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() + /** + * 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 + + 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?, 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/ConstArrayTest.kt b/ksmt-cvc5/ksmt-cvc5-core/src/test/kotlin/io/ksmt/solver/cvc5/ConstArrayTest.kt new file mode 100644 index 000000000..c46ca5043 --- /dev/null +++ b/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 + +/** + * 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? = 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 = 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) + } + } +} 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 }}" + } + } + } + } +} 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 }}" + } + } + } + } +}