diff --git a/README.md b/README.md index d854ae7af..d74fb022c 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.5.24) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.25) [![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.5.24") +implementation("io.ksmt:ksmt-core:0.5.25") // z3 solver -implementation("io.ksmt:ksmt-z3:0.5.24") +implementation("io.ksmt:ksmt-z3:0.5.25") ``` 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 9d4c32cab..2a5b6b211 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.5.24" +version = "0.5.25" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 7c21999c8..81d46341f 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.5.24") + implementation("io.ksmt:ksmt-core:0.5.25") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.5.24") + implementation("io.ksmt:ksmt-z3:0.5.25") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.5.24") + implementation("io.ksmt:ksmt-bitwuzla:0.5.25") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index d66d85954..625c84973 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -9,11 +9,11 @@ repositories { dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.24") + implementation("io.ksmt:ksmt-core:0.5.25") // z3 solver - implementation("io.ksmt:ksmt-z3:0.5.24") + implementation("io.ksmt:ksmt-z3:0.5.25") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.5.24") + implementation("io.ksmt:ksmt-runner:0.5.25") } java { diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvSimplificationRules.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvSimplificationRules.kt index b93d20078..7b9c4bc97 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvSimplificationRules.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/BvSimplificationRules.kt @@ -12,6 +12,7 @@ import io.ksmt.expr.KBvNotExpr import io.ksmt.expr.KBvOrExpr import io.ksmt.expr.KBvShiftLeftExpr import io.ksmt.expr.KBvXorExpr +import io.ksmt.expr.KBvZeroExtensionExpr import io.ksmt.expr.KExpr import io.ksmt.expr.KIteExpr import io.ksmt.sort.KBoolSort @@ -826,6 +827,8 @@ inline fun KContext.simplifyBvLogicalShiftRightExprLight( shift: KExpr, cont: (KExpr, KExpr) -> KExpr ): KExpr { + val sizeBits = shift.sort.sizeBits + if (shift is KBitVecValue) { // (x >>> 0) ==> x if (shift.isBvZero()) { @@ -833,8 +836,13 @@ inline fun KContext.simplifyBvLogicalShiftRightExprLight( } // (x >>> shift), shift >= size ==> 0 - if (shift.signedGreaterOrEqual(shift.sort.sizeBits.toInt())) { - return bvZero(shift.sort.sizeBits) + if (shift.signedGreaterOrEqual(sizeBits.toInt())) { + return bvZero(sizeBits) + } + + // ((zero-ext x E) >>> shift), shift >= sizeOf(x) ==> 0 + if (lhs is KBvZeroExtensionExpr && shift.signedGreaterOrEqual(lhs.value.sort.sizeBits.toInt())) { + return bvZero(sizeBits) } if (lhs is KBitVecValue) { @@ -844,7 +852,7 @@ inline fun KContext.simplifyBvLogicalShiftRightExprLight( // (x >>> x) ==> 0 if (lhs == shift) { - return bvZero(shift.sort.sizeBits) + return bvZero(sizeBits) } return cont(lhs, shift) diff --git a/ksmt-core/src/test/kotlin/io/ksmt/BvSimplifyTest.kt b/ksmt-core/src/test/kotlin/io/ksmt/BvSimplifyTest.kt index 076f240b6..1460f2973 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/BvSimplifyTest.kt +++ b/ksmt-core/src/test/kotlin/io/ksmt/BvSimplifyTest.kt @@ -121,6 +121,7 @@ class BvSimplifyTest: ExpressionSimplifyTest() { bvValue(it.sizeBits, 3), bvValue(it.sizeBits, BV_SIZE.toInt() + 5), bvZero(it.sizeBits), + mkBvZeroExtensionExpr((it.sizeBits.toInt() - 3).coerceAtLeast(0), mkConst("b", mkBvSort(3u))), mkConst("a", it) // same as lhs ) } 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 a1be461da..39dae685d 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 @@ -1215,11 +1215,17 @@ class KCvc5ExprInternalizer( private fun Term.mkFunctionApp(args: List): Term = tm.mkTerm(Kind.APPLY_UF, arrayOf(this) + args) - private fun mkAndTerm(args: List): Term = - if (args.size == 1) args.single() else tm.mkTerm(Kind.AND, args.toTypedArray()) + private fun mkAndTerm(args: List): Term = when (args.size) { + 0 -> tm.builder { mkTrue() } + 1 -> args.single() + else -> tm.mkTerm(Kind.AND, args.toTypedArray()) + } - private fun mkOrTerm(args: List): Term = - if (args.size == 1) args.single() else tm.mkTerm(Kind.OR, args.toTypedArray()) + private fun mkOrTerm(args: List): Term = when (args.size) { + 0 -> tm.builder { mkFalse() } + 1 -> args.single() + else -> tm.mkTerm(Kind.OR, args.toTypedArray()) + } private fun mkArraySelectTerm(array: Term, indices: List): Term = if (tm.termSort(array).isArray) { diff --git a/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt b/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt index 2c92bf563..12781bcd2 100644 --- a/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt +++ b/ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt @@ -91,8 +91,14 @@ class TestWorkerProcess : ChildProcessBase() { } private fun convertAssertions(nativeAssertions: List): List> { - val converter = KZ3ExprConverter(ctx, KZ3Context(ctx, z3Ctx)) - return with(converter) { nativeAssertions.map { it.convertExpr() } } + val context = KZ3Context(ctx, z3Ctx) + return try { + val converter = KZ3ExprConverter(ctx, context) + with(converter) { nativeAssertions.map { it.convertExpr() } } + } finally { + // Don't close native context, only release native refs + context.releaseNativeMemory() + } } private fun internalizeAndConvertBitwuzla(assertions: List>): List> = diff --git a/ksmt-z3/dist/z3-native-linux-x86-64-4.13.0.zip b/ksmt-z3/dist/z3-native-linux-x86-64-4.13.0.zip new file mode 100644 index 000000000..f0f4c87b4 Binary files /dev/null and b/ksmt-z3/dist/z3-native-linux-x86-64-4.13.0.zip differ diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/ExpressionUninterpretedValuesTracker.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/ExpressionUninterpretedValuesTracker.kt index 8c8a74e2f..470d8ebba 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/ExpressionUninterpretedValuesTracker.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/ExpressionUninterpretedValuesTracker.kt @@ -214,6 +214,13 @@ class ExpressionUninterpretedValuesTracker(val ctx: KContext, val z3Ctx: KZ3Cont } } + fun containsExpressionOnCurrentLevel(expr: KExpr<*>): Boolean { + // Was not initialized --> has no expressions + if (!initialized) return false + + return expr in currentLevelExpressions + } + fun addRegisteredValueToCurrentLevel(value: KUninterpretedSortValue) { val descriptor = tracker.registeredUninterpretedSortValues[value] ?: error("Value $value was not registered") @@ -250,7 +257,7 @@ class ExpressionUninterpretedValuesTracker(val ctx: KContext, val z3Ctx: KZ3Cont if (frameLevel < level) { val levelFrame = getFrame(frameLevel) // If expr is valid on its level we don't need to move it - return expr !in levelFrame.currentLevelExpressions + return !levelFrame.containsExpressionOnCurrentLevel(expr) } return super.exprTransformationRequired(expr) } 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 834c28b7c..d8f2a614a 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 @@ -264,6 +264,12 @@ class KZ3Context( if (isClosed) return isClosed = true + releaseNativeMemory() + + ctx.close() + } + + fun releaseNativeMemory() { uninterpretedSortValueInterpreter.clear() uninterpretedSortValueDecls.keys.decRefAll() @@ -289,8 +295,6 @@ class KZ3Context( z3Sorts.keys.decRefAll() sorts.clear() z3Sorts.clear() - - ctx.close() } private fun LongSet.decRefAll() = diff --git a/ksmt-z3/ksmt-z3-native/build.gradle.kts b/ksmt-z3/ksmt-z3-native/build.gradle.kts index 6843c21ab..587c5253c 100644 --- a/ksmt-z3/ksmt-z3-native/build.gradle.kts +++ b/ksmt-z3/ksmt-z3-native/build.gradle.kts @@ -27,7 +27,7 @@ val macDylibPath = listOf("**/libz3.dylib", "**/libz3java.dylib") val z3Binaries = listOf( Triple(`windows-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-win", winDllPath), null), - Triple(`linux-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-glibc-2.31", linuxSoPath), null), + Triple(`linux-x64`, null, z3NativeLinuxX64), Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-11.7.10", macDylibPath), null), Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-11.0", macDylibPath), null), Triple(`linux-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-glibc-2.35", linuxSoPath), null),