diff --git a/.github/workflows/build-and-run-tests.yml b/.github/workflows/build-and-run-tests.yml index c08903899..b187e1d10 100644 --- a/.github/workflows/build-and-run-tests.yml +++ b/.github/workflows/build-and-run-tests.yml @@ -20,37 +20,28 @@ jobs: runs-on: ${{ matrix.os }} steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up JDK 1.8 - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: java-version: 8 distribution: 'zulu' cache: gradle + - name: Setup gradle + uses: gradle/actions/setup-gradle@v3 + - name: Build and run z3 tests on macOS - uses: gradle/gradle-build-action@v2 if: runner.os == 'macOS' - with: - arguments: | - :ksmt-z3:build - --no-daemon - --continue - -PrunBenchmarksBasedTests=false + run: ./gradlew :ksmt-z3:build --no-daemon --continue -PrunBenchmarksBasedTests=false - name: Build and run simple tests on Linux or Windows - uses: gradle/gradle-build-action@v2 if: runner.os != 'macOS' - with: - arguments: | - build - --no-daemon - --continue - -PrunBenchmarksBasedTests=false + run: ./gradlew build --no-daemon --continue -PrunBenchmarksBasedTests=false - name: Upload ksmt test reports - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 if: always() with: name: ksmt-tests-report-${{ matrix.os }} diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 2129da139..182719583 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -10,19 +10,21 @@ jobs: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Set up JDK 1.8 - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: java-version: 8 distribution: 'zulu' cache: gradle + - name: Setup gradle + uses: gradle/actions/setup-gradle@v3 + - name: Build artifacts - uses: gradle/gradle-build-action@v2 - with: - arguments: | + run: > + ./gradlew publishAllPublicationsToCentralRepository publishAllPublicationsToReleaseDirRepository --no-daemon diff --git a/.github/workflows/run-long-tests.yml b/.github/workflows/run-long-tests.yml index 8cee5f37b..5d4932928 100644 --- a/.github/workflows/run-long-tests.yml +++ b/.github/workflows/run-long-tests.yml @@ -69,11 +69,11 @@ jobs: runs-on: ${{ matrix.os }} steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Prepare test data (cache) id: test-data-cache - uses: actions/cache@v3 + uses: actions/cache@v4 env: cache-name: cache-test-data with: @@ -82,20 +82,23 @@ jobs: - name: Set up JDK 1.8 if: steps.test-data-cache.outputs.cache-hit != 'true' - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: java-version: 8 distribution: 'zulu' cache: gradle + - name: Setup gradle + if: steps.test-data-cache.outputs.cache-hit != 'true' + uses: gradle/actions/setup-gradle@v3 + - name: Prepare test data (download) if: steps.test-data-cache.outputs.cache-hit != 'true' - uses: gradle/gradle-build-action@v2 - with: - arguments: | + run: > + ./gradlew :ksmt-test:downloadPreparedSmtLibBenchmarkTestData --no-daemon - -PtestDataRevision=${{ env.TEST_DATA_REVISION }} + '-PtestDataRevision=${{ env.TEST_DATA_REVISION }}' run_tests: needs: [setup, prepare_test_data] @@ -111,11 +114,11 @@ jobs: runs-on: ${{ matrix.os }} steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - name: Prepare test data (cache) id: test-data-cache - uses: actions/cache@v3 + uses: actions/cache@v4 env: cache-name: cache-test-data with: @@ -129,34 +132,31 @@ jobs: exit 1 - name: Set up JDK 1.8 - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: java-version: 8 distribution: 'zulu' cache: gradle + - name: Setup gradle + uses: gradle/actions/setup-gradle@v3 + # Since ksmt-test/testData/testData.zip exists task will not download it again - name: Prepare test data (unpack) - uses: gradle/gradle-build-action@v2 - with: - arguments: | + run: > + ./gradlew :ksmt-test:downloadPreparedSmtLibBenchmarkTestData --no-daemon - -PtestDataRevision=${{ env.TEST_DATA_REVISION }} + '-PtestDataRevision=${{ env.TEST_DATA_REVISION }}' # We don't want to run basic KSMT tests on each chunk - name: Build project - uses: gradle/gradle-build-action@v2 if: ${{ matrix.chunk == '0' }} - with: - arguments: | - build - --no-daemon + run: ./gradlew build --no-daemon - name: Run ${{ matrix.test }} - uses: gradle/gradle-build-action@v2 - with: - arguments: | + run: > + ./gradlew :ksmt-test:test --tests ${{ format('"io.ksmt.test.benchmarks.{0}"', matrix.test) }} --no-daemon --continue @@ -165,7 +165,7 @@ jobs: -PbenchmarkChunk=${{ matrix.chunk }} - name: Upload ksmt test reports - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 if: always() with: name: ${{ format('ksmt-test-report-{0}-{1}-{2}', matrix.os, matrix.test, matrix.chunk) }} @@ -179,36 +179,37 @@ jobs: if: ${{ always() }} steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - - uses: actions/download-artifact@v3 + - uses: actions/download-artifact@v4 with: path: reports - name: Set up JDK 1.8 - uses: actions/setup-java@v3 + uses: actions/setup-java@v4 with: java-version: 8 distribution: 'zulu' + - name: Setup gradle + uses: gradle/actions/setup-gradle@v3 + - name: Merge test report [ubuntu-latest] - uses: gradle/gradle-build-action@v2 - with: - arguments: | + run: > + ./gradlew :ksmt-test:mergeTestReports --no-daemon -PtestReportMergePrefix=ksmt-test-report-ubuntu-latest - name: Merge test report [windows-latest] - uses: gradle/gradle-build-action@v2 - with: - arguments: | + run: > + ./gradlew :ksmt-test:mergeTestReports --no-daemon -PtestReportMergePrefix=ksmt-test-report-windows-latest - name: Upload merged test reports - uses: actions/upload-artifact@v3 + uses: actions/upload-artifact@v4 with: name: ksmt-test-report path: ksmt-test-report-* diff --git a/README.md b/README.md index b61dcbd3e..a6dc6dcec 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.16) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.17) [![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.16") +implementation("io.ksmt:ksmt-core:0.5.17") // z3 solver -implementation("io.ksmt:ksmt-z3:0.5.16") +implementation("io.ksmt:ksmt-z3:0.5.17") ``` 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 211aded43..a9a255882 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.16" +version = "0.5.17" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index 319fd5871..9900b3c75 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.16") + implementation("io.ksmt:ksmt-core:0.5.17") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.5.16") + implementation("io.ksmt:ksmt-z3:0.5.17") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.5.16") + implementation("io.ksmt:ksmt-bitwuzla:0.5.17") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index f6d3cae66..602fe3391 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.16") + implementation("io.ksmt:ksmt-core:0.5.17") // z3 solver - implementation("io.ksmt:ksmt-z3:0.5.16") + implementation("io.ksmt:ksmt-z3:0.5.17") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.5.16") + implementation("io.ksmt:ksmt-runner:0.5.17") } java { diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/FpUtils.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/FpUtils.kt index 2581e971b..e820e45ab 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/utils/FpUtils.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/utils/FpUtils.kt @@ -1155,10 +1155,6 @@ object FpUtils { ): KFpValue<*> { val (normalizedValue, normalizationStickyBit) = fpFmaRoundNormalizeSignificand(value, exponentSize) - if (normalizedValue.unbiasedExponent > fpMaxExponentValue(exponentSize)) { - return mkFpInf(value.sign, mkFpSort(exponentSize, significandSize)) - } - val valueWithoutExtraBits = fpFmaRoundRemoveExtraBits(normalizedValue, normalizationStickyBit, significandSize) if (valueWithoutExtraBits.significand.isZero()) { @@ -1210,18 +1206,28 @@ object FpUtils { stickyBit: Boolean, significandSize: UInt ): UnpackedFp { - var (significand, resultStickyBit) = if (significandSize >= 4u) { - val (quot, rem) = value.significand.divAndRem2k(significandSize - 4u + 3u) - quot to (stickyBit || !rem.isZero()) + val exponent: BigInteger + var significand: BigInteger + var sticky: Boolean = stickyBit + + if (significandSize >= 4u) { + val (sig, rem) = value.significand.divAndRem2k(significandSize + 3u - 4u) + exponent = value.unbiasedExponent + significand = sig + sticky = sticky || !rem.isZero() } else { - value.significand.mul2k(4u - significandSize + 3u) to false + val exponentDelta = 4u - significandSize + 3u + significand = value.significand.mul2k(exponentDelta) + exponent = value.unbiasedExponent - exponentDelta.toInt().toBigInteger() } - if (resultStickyBit && significand.isEven()) { + if (sticky && significand.isEven()) { significand++ } - return value.copy(significand = significand) + return normalizeUpperBound(exponent, significand, significandSize + 4u) { exp, sig -> + value.copy(unbiasedExponent = exp, significand = sig) + } } private fun UnpackedFp.addSignificandExtraBits(bits: UInt) = copy( @@ -1275,40 +1281,58 @@ object FpUtils { private fun KContext.fpRoundToIntegralUnpacked(rm: KFpRoundingMode, value: UnpackedFp): KFpValue<*> { val shift = (value.significandSize - 1u).toInt().toBigInteger() - value.unbiasedExponent - var resultSignificand = fpRoundSignificandToIntegral(value, shift, rm) - var resultExponent = value.unbiasedExponent + val resultSignificand = fpRoundSignificandToIntegral(value, shift, rm) + val resultExponent = value.unbiasedExponent // re-normalize - val powerToNormalize = resultSignificand.log2() - value.significandSize.toInt() + 1 - if (powerToNormalize > 0) { - resultExponent += powerToNormalize.toBigInteger() - resultSignificand = resultSignificand.div2k(powerToNormalize.toUInt()) + return normalizeUpperBound(resultExponent, resultSignificand, value.significandSize) { exp, sig -> + mkRoundedValue( + rm, exp, sig, value.sign, value.exponentSize, value.significandSize + ) } - - return mkRoundedValue( - rm, resultExponent, resultSignificand, value.sign, value.exponentSize, value.significandSize - ) } private fun fpNormalize(value: UnpackedFp): UnpackedFp { if (value.significand.isZero()) return value + return normalizeUpperBound(value.unbiasedExponent, value.significand, value.significandSize) { e, s -> + normalizeLowerBound(e, s, value.significandSize) { exp, sig -> + UnpackedFp(value.exponentSize, value.significandSize, value.sign, exp, sig) + } + } + } - var sig = value.significand - var exp = value.unbiasedExponent - - val normalizeUpperBound = sig.log2() - value.significandSize.toInt() + 1 - if (normalizeUpperBound > 0) { - sig = sig.div2k(normalizeUpperBound.toUInt()) - exp += normalizeUpperBound.toBigInteger() + private inline fun normalizeUpperBound( + exponent: BigInteger, + significand: BigInteger, + significandSize: UInt, + body: (exponent: BigInteger, significand: BigInteger) -> T + ): T { + val exponentDelta = significand.log2() - significandSize.toInt() + 1 + if (exponentDelta <= 0) { + return body(exponent, significand) } - val normalizeLowerBound = value.significandSize.toInt() - 1 - sig.log2() - if (normalizeLowerBound > 0){ - sig = sig.mul2k(normalizeLowerBound.toUInt()) - exp -= normalizeLowerBound.toBigInteger() + return body( + exponent.plus(exponentDelta.toBigInteger()), + significand.div2k(exponentDelta.toUInt()) + ) + } + + private inline fun normalizeLowerBound( + exponent: BigInteger, + significand: BigInteger, + significandSize: UInt, + body: (exponent: BigInteger, significand: BigInteger) -> T + ): T { + val exponentDelta = significandSize.toInt() - 1 - significand.log2() + if (exponentDelta <= 0) { + return body(exponent, significand) } - return UnpackedFp(value.exponentSize, value.significandSize, value.sign, exp, sig) + return body( + exponent.minus(exponentDelta.toBigInteger()), + significand.mul2k(exponentDelta.toUInt()) + ) } private fun fpRoundSignificandToIntegral( diff --git a/ksmt-core/src/test/kotlin/io/ksmt/ExpressionEvalTest.kt b/ksmt-core/src/test/kotlin/io/ksmt/ExpressionEvalTest.kt index 1f2f9e3e3..fdcb04a4d 100644 --- a/ksmt-core/src/test/kotlin/io/ksmt/ExpressionEvalTest.kt +++ b/ksmt-core/src/test/kotlin/io/ksmt/ExpressionEvalTest.kt @@ -11,6 +11,7 @@ import io.ksmt.expr.KInt32NumExpr import io.ksmt.expr.KInterpretedValue import io.ksmt.expr.KRealNumExpr import io.ksmt.expr.rewrite.simplify.KExprSimplifier +import io.ksmt.solver.KSolver import io.ksmt.solver.KSolverStatus import io.ksmt.solver.z3.KZ3Solver import io.ksmt.sort.KBvSort @@ -164,7 +165,7 @@ open class ExpressionEvalTest { testCases.clear() } - private fun computeSolverValues(solver: KZ3Solver) = with(ctx) { + private fun computeSolverValues(solver: KSolver<*>) = with(ctx) { val testCaseVars = testCases.map { val valueVar = mkFreshConst("v", it.unsimplifiedExpr.sort) solver.assert(valueVar eq it.unsimplifiedExpr.uncheckedCast()) diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/BenchmarksBasedTest.kt index 49551cd87..d08ecd5c5 100644 --- a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/BenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/BenchmarksBasedTest.kt @@ -144,11 +144,6 @@ abstract class BenchmarksBasedTest { * */ val assertionsToCheck = evaluatedAssertions.filterNot { hasUnderspecifiedOperations(it) } - // Samples are false UNSAT in Z3 because of incorrect FMA eval - if (name in KnownZ3Issues.z3FpFmaFalseUnsatSamples) { - ignoreTest { "Example is known to be false UNSAT in Z3 test oracle" } - } - worker.performEqualityChecks { cardinalityConstraints.forEach { assume(it) } assertionsToCheck.forEach { isTrue(it) } @@ -181,15 +176,7 @@ abstract class BenchmarksBasedTest { worker.assert(solver, it) } - var expectedStatus = worker.check(solver) - - // Fix known Z3 satisfiability issues - if (expectedStatus == KSolverStatus.UNSAT && name in KnownZ3Issues.z3FpFmaFalseUnsatSamples) { - expectedStatus = KSolverStatus.SAT - } - if (expectedStatus == KSolverStatus.SAT && name in KnownZ3Issues.z3FpFmaFalseSatSamples) { - expectedStatus = KSolverStatus.UNSAT - } + val expectedStatus = worker.check(solver) if (expectedStatus == KSolverStatus.UNKNOWN) { ignoreTest { "Expected status is unknown" } @@ -543,178 +530,4 @@ abstract class BenchmarksBasedTest { Assumptions.assumeTrue(false) } } - - object KnownZ3Issues { - /** - * These samples are known to be SAT according to the annotation - * in the source and according to the previous versions of Z3 (e.g. 4.8.15). - * Currently used z3 4.11.2 treat these samples as UNSAT. - * - * Todo: remove when this issue will be fixed in Z3. - * */ - val z3FpFmaFalseUnsatSamples = setOf( - "QF_FP_fma-has-solution-10232.smt2", - "QF_FP_fma-has-solution-10256.smt2", - "QF_FP_fma-has-solution-10601.smt2", - "QF_FP_fma-has-solution-10792.smt2", - "QF_FP_fma-has-solution-10834.smt2", - "QF_FP_fma-has-solution-10856.smt2", - "QF_FP_fma-has-solution-10867.smt2", - "QF_FP_fma-has-solution-10998.smt2", - "QF_FP_fma-has-solution-11152.smt2", - "QF_FP_fma-has-solution-11193.smt2", - "QF_FP_fma-has-solution-11245.smt2", - "QF_FP_fma-has-solution-11482.smt2", - "QF_FP_fma-has-solution-11503.smt2", - "QF_FP_fma-has-solution-12238.smt2", - "QF_FP_fma-has-solution-12329.smt2", - "QF_FP_fma-has-solution-1247.smt2", - "QF_FP_fma-has-solution-12600.smt2", - "QF_FP_fma-has-solution-12639.smt2", - "QF_FP_fma-has-solution-12682.smt2", - "QF_FP_fma-has-solution-12789.smt2", - "QF_FP_fma-has-solution-12840.smt2", - "QF_FP_fma-has-solution-12969.smt2", - "QF_FP_fma-has-solution-1325.smt2", - "QF_FP_fma-has-solution-13421.smt2", - "QF_FP_fma-has-solution-13786.smt2", - "QF_FP_fma-has-solution-14111.smt2", - "QF_FP_fma-has-solution-14346.smt2", - "QF_FP_fma-has-solution-14535.smt2", - "QF_FP_fma-has-solution-14613.smt2", - "QF_FP_fma-has-solution-14742.smt2", - "QF_FP_fma-has-solution-14799.smt2", - "QF_FP_fma-has-solution-14835.smt2", - "QF_FP_fma-has-solution-154.smt2", - "QF_FP_fma-has-solution-15774.smt2", - "QF_FP_fma-has-solution-15798.smt2", - "QF_FP_fma-has-solution-15963.smt2", - "QF_FP_fma-has-solution-15995.smt2", - "QF_FP_fma-has-solution-17127.smt2", - "QF_FP_fma-has-solution-17650.smt2", - "QF_FP_fma-has-solution-17915.smt2", - "QF_FP_fma-has-solution-17959.smt2", - "QF_FP_fma-has-solution-1809.smt2", - "QF_FP_fma-has-solution-18220.smt2", - "QF_FP_fma-has-solution-18700.smt2", - "QF_FP_fma-has-solution-19191.smt2", - "QF_FP_fma-has-solution-19593.smt2", - "QF_FP_fma-has-solution-2988.smt2", - "QF_FP_fma-has-solution-3042.smt2", - "QF_FP_fma-has-solution-3742.smt2", - "QF_FP_fma-has-solution-4281.smt2", - "QF_FP_fma-has-solution-457.smt2", - "QF_FP_fma-has-solution-4615.smt2", - "QF_FP_fma-has-solution-4981.smt2", - "QF_FP_fma-has-solution-4983.smt2", - "QF_FP_fma-has-solution-5056.smt2", - "QF_FP_fma-has-solution-5127.smt2", - "QF_FP_fma-has-solution-5213.smt2", - "QF_FP_fma-has-solution-5986.smt2", - "QF_FP_fma-has-solution-6211.smt2", - "QF_FP_fma-has-solution-6468.smt2", - "QF_FP_fma-has-solution-6573.smt2", - "QF_FP_fma-has-solution-6673.smt2", - "QF_FP_fma-has-solution-6822.smt2", - "QF_FP_fma-has-solution-7580.smt2", - "QF_FP_fma-has-solution-7736.smt2", - "QF_FP_fma-has-solution-7832.smt2", - "QF_FP_fma-has-solution-7920.smt2", - "QF_FP_fma-has-solution-80.smt2", - "QF_FP_fma-has-solution-8278.smt2", - "QF_FP_fma-has-solution-8475.smt2", - "QF_FP_fma-has-solution-8483.smt2", - "QF_FP_fma-has-solution-9132.smt2", - "QF_FP_fma-has-solution-9188.smt2", - "QF_FP_fma-has-solution-9455.smt2", - "QF_FP_fma-has-solution-9467.smt2", - "QF_FP_fma-has-solution-9517.smt2", - ) - - /** - * These samples are known to be UNSAT according to the annotation - * in the source and according to the previous versions of Z3 (e.g. 4.8.15). - * Currently used z3 4.11.2 treat these samples as SAT. - * - * Todo: remove when this issue will be fixed in Z3. - * */ - val z3FpFmaFalseSatSamples = setOf( - "QF_FP_fma-has-no-other-solution-10232.smt2", - "QF_FP_fma-has-no-other-solution-10256.smt2", - "QF_FP_fma-has-no-other-solution-10601.smt2", - "QF_FP_fma-has-no-other-solution-10856.smt2", - "QF_FP_fma-has-no-other-solution-10834.smt2", - "QF_FP_fma-has-no-other-solution-10792.smt2", - "QF_FP_fma-has-no-other-solution-10867.smt2", - "QF_FP_fma-has-no-other-solution-10998.smt2", - "QF_FP_fma-has-no-other-solution-11152.smt2", - "QF_FP_fma-has-no-other-solution-11193.smt2", - "QF_FP_fma-has-no-other-solution-11245.smt2", - "QF_FP_fma-has-no-other-solution-11482.smt2", - "QF_FP_fma-has-no-other-solution-11503.smt2", - "QF_FP_fma-has-no-other-solution-12238.smt2", - "QF_FP_fma-has-no-other-solution-12329.smt2", - "QF_FP_fma-has-no-other-solution-1247.smt2", - "QF_FP_fma-has-no-other-solution-12639.smt2", - "QF_FP_fma-has-no-other-solution-12600.smt2", - "QF_FP_fma-has-no-other-solution-12682.smt2", - "QF_FP_fma-has-no-other-solution-12789.smt2", - "QF_FP_fma-has-no-other-solution-12840.smt2", - "QF_FP_fma-has-no-other-solution-12969.smt2", - "QF_FP_fma-has-no-other-solution-1325.smt2", - "QF_FP_fma-has-no-other-solution-13421.smt2", - "QF_FP_fma-has-no-other-solution-13786.smt2", - "QF_FP_fma-has-no-other-solution-14111.smt2", - "QF_FP_fma-has-no-other-solution-14346.smt2", - "QF_FP_fma-has-no-other-solution-14613.smt2", - "QF_FP_fma-has-no-other-solution-14535.smt2", - "QF_FP_fma-has-no-other-solution-14742.smt2", - "QF_FP_fma-has-no-other-solution-14835.smt2", - "QF_FP_fma-has-no-other-solution-14799.smt2", - "QF_FP_fma-has-no-other-solution-154.smt2", - "QF_FP_fma-has-no-other-solution-15774.smt2", - "QF_FP_fma-has-no-other-solution-15798.smt2", - "QF_FP_fma-has-no-other-solution-15963.smt2", - "QF_FP_fma-has-no-other-solution-15995.smt2", - "QF_FP_fma-has-no-other-solution-17127.smt2", - "QF_FP_fma-has-no-other-solution-17650.smt2", - "QF_FP_fma-has-no-other-solution-17915.smt2", - "QF_FP_fma-has-no-other-solution-17959.smt2", - "QF_FP_fma-has-no-other-solution-1809.smt2", - "QF_FP_fma-has-no-other-solution-18220.smt2", - "QF_FP_fma-has-no-other-solution-18700.smt2", - "QF_FP_fma-has-no-other-solution-19191.smt2", - "QF_FP_fma-has-no-other-solution-19593.smt2", - "QF_FP_fma-has-no-other-solution-2988.smt2", - "QF_FP_fma-has-no-other-solution-3042.smt2", - "QF_FP_fma-has-no-other-solution-3742.smt2", - "QF_FP_fma-has-no-other-solution-4281.smt2", - "QF_FP_fma-has-no-other-solution-457.smt2", - "QF_FP_fma-has-no-other-solution-4615.smt2", - "QF_FP_fma-has-no-other-solution-4981.smt2", - "QF_FP_fma-has-no-other-solution-5056.smt2", - "QF_FP_fma-has-no-other-solution-4983.smt2", - "QF_FP_fma-has-no-other-solution-5213.smt2", - "QF_FP_fma-has-no-other-solution-5127.smt2", - "QF_FP_fma-has-no-other-solution-5986.smt2", - "QF_FP_fma-has-no-other-solution-6211.smt2", - "QF_FP_fma-has-no-other-solution-6468.smt2", - "QF_FP_fma-has-no-other-solution-6573.smt2", - "QF_FP_fma-has-no-other-solution-6673.smt2", - "QF_FP_fma-has-no-other-solution-6822.smt2", - "QF_FP_fma-has-no-other-solution-7580.smt2", - "QF_FP_fma-has-no-other-solution-7736.smt2", - "QF_FP_fma-has-no-other-solution-7832.smt2", - "QF_FP_fma-has-no-other-solution-7920.smt2", - "QF_FP_fma-has-no-other-solution-80.smt2", - "QF_FP_fma-has-no-other-solution-8278.smt2", - "QF_FP_fma-has-no-other-solution-8475.smt2", - "QF_FP_fma-has-no-other-solution-8483.smt2", - "QF_FP_fma-has-no-other-solution-9132.smt2", - "QF_FP_fma-has-no-other-solution-9188.smt2", - "QF_FP_fma-has-no-other-solution-9517.smt2", - "QF_FP_fma-has-no-other-solution-9455.smt2", - "QF_FP_fma-has-no-other-solution-9467.smt2", - ) - } } diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Z3BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Z3BenchmarksBasedTest.kt index b9692c14f..fd176a591 100644 --- a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Z3BenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Z3BenchmarksBasedTest.kt @@ -25,7 +25,7 @@ class Z3BenchmarksBasedTest : BenchmarksBasedTest() { @Execution(ExecutionMode.CONCURRENT) @ParameterizedTest(name = "{0}") - @MethodSource("z3SolverTestData") + @MethodSource("z3TestData") fun testSolver(name: String, samplePath: Path) = testSolver(name, samplePath, KZ3Solver::class) @@ -33,11 +33,5 @@ class Z3BenchmarksBasedTest : BenchmarksBasedTest() { companion object { @JvmStatic fun z3TestData() = testData() - - @JvmStatic - fun z3SolverTestData() = z3TestData() - .filter { it.name !in KnownZ3Issues.z3FpFmaFalseSatSamples } - .filter { it.name !in KnownZ3Issues.z3FpFmaFalseUnsatSamples } - .ensureNotEmpty() } } diff --git a/ksmt-z3/dist/z3-native-linux-x86-64-4.12.2.zip b/ksmt-z3/dist/z3-native-linux-x86-64-4.12.5.zip similarity index 59% rename from ksmt-z3/dist/z3-native-linux-x86-64-4.12.2.zip rename to ksmt-z3/dist/z3-native-linux-x86-64-4.12.5.zip index 06a2ee74b..44862044b 100644 Binary files a/ksmt-z3/dist/z3-native-linux-x86-64-4.12.2.zip and b/ksmt-z3/dist/z3-native-linux-x86-64-4.12.5.zip differ diff --git a/ksmt-z3/ksmt-z3-core/build.gradle.kts b/ksmt-z3/ksmt-z3-core/build.gradle.kts index 48646a4da..32dd538a2 100644 --- a/ksmt-z3/ksmt-z3-core/build.gradle.kts +++ b/ksmt-z3/ksmt-z3-core/build.gradle.kts @@ -9,7 +9,7 @@ repositories { mavenCentral() } -val z3Version = "4.12.2" +val z3Version = "4.12.5" val z3JavaJar by lazy { mkZ3ReleaseDownloadTask(z3Version, "x64-win", "*.jar") } diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt index 9ade756ae..1bd9097e7 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt @@ -131,6 +131,7 @@ open class KZ3ExprConverter( Z3_sort_kind.Z3_SEQ_SORT, Z3_sort_kind.Z3_RE_SORT, Z3_sort_kind.Z3_CHAR_SORT, + Z3_sort_kind.Z3_TYPE_VAR, Z3_sort_kind.Z3_UNKNOWN_SORT -> TODO("$sort is not supported yet") null -> error("z3 sort kind cannot be null") } diff --git a/ksmt-z3/ksmt-z3-native/build.gradle.kts b/ksmt-z3/ksmt-z3-native/build.gradle.kts index eb1895559..e49fab2e9 100644 --- a/ksmt-z3/ksmt-z3-native/build.gradle.kts +++ b/ksmt-z3/ksmt-z3-native/build.gradle.kts @@ -17,12 +17,12 @@ val `linux-x64` by sourceSets.creating val `mac-x64` by sourceSets.creating val `mac-arm` by sourceSets.creating -val z3Version = "4.12.2" +val z3Version = "4.12.5" val z3Binaries = listOf( Triple(`windows-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-win", "*.dll"), null), Triple(`linux-x64`, null, z3NativeLinuxX64), - Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-10.16", "*.dylib"), null), + Triple(`mac-x64`, mkZ3ReleaseDownloadTask(z3Version, "x64-osx-11.7.10", "*.dylib"), null), Triple(`mac-arm`, mkZ3ReleaseDownloadTask(z3Version, "arm64-osx-11.0", "*.dylib"), null), )