From 250b14eb44cf9245ecf697aba71d60f2fe343ec4 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Fri, 10 Mar 2023 15:05:49 +0300 Subject: [PATCH] Test refactoring and documentation update (#82) * Move benchmarks tests * Move benchmarks tests * Update release workflow * Update docs --- .github/workflows/release.yml | 3 ++- .github/workflows/run-long-tests.yml | 2 +- README.md | 15 ++++++++------- Requirements.md | 2 +- ksmt-test/build.gradle.kts | 7 ++++--- .../test/{ => benchmarks}/BenchmarksBasedTest.kt | 6 +++++- .../BitwuzlaBenchmarksBasedTest.kt | 2 +- .../ContextMemoryUsageBenchmarksBasedTest.kt | 2 +- .../{ => benchmarks}/Cvc5BenchmarksBasedTest.kt | 2 +- .../PortfolioBenchmarksBasedTest.kt | 2 +- .../SerializerBenchmarksBasedTest.kt | 2 +- .../SimplifierBenchmarksBasedTest.kt | 2 +- .../{ => benchmarks}/YicesBenchmarksBasedTest.kt | 2 +- .../{ => benchmarks}/Z3BenchmarksBasedTest.kt | 2 +- .../test/{ => benchmarks}/Z3ConverterBenchmark.kt | 2 +- 15 files changed, 30 insertions(+), 23 deletions(-) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/BenchmarksBasedTest.kt (99%) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/BitwuzlaBenchmarksBasedTest.kt (98%) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/ContextMemoryUsageBenchmarksBasedTest.kt (98%) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/Cvc5BenchmarksBasedTest.kt (99%) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/PortfolioBenchmarksBasedTest.kt (98%) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/SerializerBenchmarksBasedTest.kt (98%) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/SimplifierBenchmarksBasedTest.kt (97%) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/YicesBenchmarksBasedTest.kt (98%) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/Z3BenchmarksBasedTest.kt (97%) rename ksmt-test/src/test/kotlin/org/ksmt/test/{ => benchmarks}/Z3ConverterBenchmark.kt (99%) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index bef5b9477..5267b580d 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -31,5 +31,6 @@ jobs: ksmt-core/build/release/**/ksmt-core-*.jar ksmt-z3/build/release/**/ksmt-z3-*.jar ksmt-bitwuzla/build/release/**/ksmt-bitwuzla-*.jar + ksmt-yices/build/release/**/ksmt-yices-*.jar + ksmt-cvc5/build/release/**/ksmt-cvc5-*.jar ksmt-runner/build/release/**/ksmt-runner-*.jar - diff --git a/.github/workflows/run-long-tests.yml b/.github/workflows/run-long-tests.yml index e5649dca2..b93f9357e 100644 --- a/.github/workflows/run-long-tests.yml +++ b/.github/workflows/run-long-tests.yml @@ -157,7 +157,7 @@ jobs: uses: gradle/gradle-build-action@v2 with: arguments: | - :ksmt-test:test --tests ${{ format('"org.ksmt.test.{0}"', matrix.test) }} + :ksmt-test:test --tests ${{ format('"org.ksmt.test.benchmarks.{0}"', matrix.test) }} --no-daemon --continue -PrunBenchmarksBasedTests=true diff --git a/README.md b/README.md index c2166b9fe..857ad7b66 100644 --- a/README.md +++ b/README.md @@ -31,16 +31,17 @@ Currently, KSMT supports the following SMT solvers: | [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | [Bitwuzla](https://github.com/bitwuzla/bitwuzla) | :heavy_check_mark: | :heavy_check_mark: | | | [Yices2](https://github.com/SRI-CSL/yices2) | :heavy_check_mark: | :heavy_check_mark: | | +| [cvc5](https://github.com/cvc5/cvc5) | :heavy_check_mark: | :heavy_check_mark: | | KSMT can express formulas in the following theories: -| Theory | Z3 | Bitwuzla | Yices2 | -|-------------------------|:------------------:|:------------------:|--------------------| -| Bitvectors | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | -| Arrays | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | -| IEEE Floats | :heavy_check_mark: | :heavy_check_mark: | | -| Uninterpreted Functions | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | -| Arithmetic | :heavy_check_mark: | | :heavy_check_mark: | +| Theory | Z3 | Bitwuzla | Yices2 | cvc5 | +|-------------------------|:------------------:|:------------------:|--------------------|--------------------| +| Bitvectors | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | +| Arrays | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | +| IEEE Floats | :heavy_check_mark: | :heavy_check_mark: | | :heavy_check_mark: | +| Uninterpreted Functions | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | +| Arithmetic | :heavy_check_mark: | | :heavy_check_mark: | :heavy_check_mark: | Check out our [roadmap](Requirements.md) for detailed description of features and future plans. diff --git a/Requirements.md b/Requirements.md index 272a2982f..cb3a6aba3 100644 --- a/Requirements.md +++ b/Requirements.md @@ -10,7 +10,7 @@ | [Z3 solver support](#z3-solver-support) | Done | | [Bitwuzla solver support](#bitwuzla-solver-support) | Done | | [Yices2 solver support](#yices2-solver-support) | Done | -| [CVC5 solver support](#cvc5-solver-support) | In progress | +| [CVC5 solver support](#cvc5-solver-support) | Done | | [External process runner](#external-process-runner) | Done | | [Portfolio solver](#portfolio-solver) | Done | | [Solver configuration API](#solver-configuration-api) | Done | diff --git a/ksmt-test/build.gradle.kts b/ksmt-test/build.gradle.kts index 4db9d5f91..7d83dcbfc 100644 --- a/ksmt-test/build.gradle.kts +++ b/ksmt-test/build.gradle.kts @@ -106,12 +106,13 @@ val downloadPreparedBenchmarksTestData = downloadPreparedSmtLibBenchmarkTestData ) tasks.withType { - enabled = runBenchmarksBasedTests if (runBenchmarksBasedTests) { dependsOn.add(prepareTestData) + environment("benchmarkChunkMaxSize", benchmarkChunkMaxSize) + environment("benchmarkChunk", benchmarkChunk) + } else { + exclude("org/ksmt/test/benchmarks/**") } - environment("benchmarkChunkMaxSize", benchmarkChunkMaxSize) - environment("benchmarkChunk", benchmarkChunk) } /** diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/BenchmarksBasedTest.kt similarity index 99% rename from ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/BenchmarksBasedTest.kt index b920c1a31..63ea4f7e8 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/BenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/BenchmarksBasedTest.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import com.jetbrains.rd.util.reactive.RdFault import kotlinx.coroutines.TimeoutCancellationException @@ -44,6 +44,10 @@ import org.ksmt.sort.KFpSort import org.ksmt.sort.KIntSort import org.ksmt.sort.KRealSort import org.ksmt.sort.KSort +import org.ksmt.test.SmtLibParseError +import org.ksmt.test.TestRunner +import org.ksmt.test.TestWorker +import org.ksmt.test.TestWorkerProcess import org.ksmt.utils.FpUtils.isZero import java.nio.file.Path import java.nio.file.Paths diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/BitwuzlaBenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/BitwuzlaBenchmarksBasedTest.kt similarity index 98% rename from ksmt-test/src/test/kotlin/org/ksmt/test/BitwuzlaBenchmarksBasedTest.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/BitwuzlaBenchmarksBasedTest.kt index 2b9a57ef4..90d4d49f3 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/BitwuzlaBenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/BitwuzlaBenchmarksBasedTest.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import org.junit.jupiter.api.parallel.Execution import org.junit.jupiter.api.parallel.ExecutionMode diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/ContextMemoryUsageBenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/ContextMemoryUsageBenchmarksBasedTest.kt similarity index 98% rename from ksmt-test/src/test/kotlin/org/ksmt/test/ContextMemoryUsageBenchmarksBasedTest.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/ContextMemoryUsageBenchmarksBasedTest.kt index 190b9938a..dffb50dea 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/ContextMemoryUsageBenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/ContextMemoryUsageBenchmarksBasedTest.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import org.junit.jupiter.api.AfterAll import org.junit.jupiter.api.BeforeAll diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/Cvc5BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/Cvc5BenchmarksBasedTest.kt similarity index 99% rename from ksmt-test/src/test/kotlin/org/ksmt/test/Cvc5BenchmarksBasedTest.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/Cvc5BenchmarksBasedTest.kt index 87cc4ea56..fdf76ab72 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/Cvc5BenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/Cvc5BenchmarksBasedTest.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import org.junit.jupiter.api.parallel.Execution import org.junit.jupiter.api.parallel.ExecutionMode diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/PortfolioBenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/PortfolioBenchmarksBasedTest.kt similarity index 98% rename from ksmt-test/src/test/kotlin/org/ksmt/test/PortfolioBenchmarksBasedTest.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/PortfolioBenchmarksBasedTest.kt index 70509b0a8..60c41db78 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/PortfolioBenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/PortfolioBenchmarksBasedTest.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import org.junit.jupiter.api.AfterAll import org.junit.jupiter.api.BeforeAll diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/SerializerBenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/SerializerBenchmarksBasedTest.kt similarity index 98% rename from ksmt-test/src/test/kotlin/org/ksmt/test/SerializerBenchmarksBasedTest.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/SerializerBenchmarksBasedTest.kt index ab2d6fe1d..f75b17938 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/SerializerBenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/SerializerBenchmarksBasedTest.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import com.jetbrains.rd.framework.IMarshaller import com.jetbrains.rd.framework.SerializationCtx diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/SimplifierBenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/SimplifierBenchmarksBasedTest.kt similarity index 97% rename from ksmt-test/src/test/kotlin/org/ksmt/test/SimplifierBenchmarksBasedTest.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/SimplifierBenchmarksBasedTest.kt index ed7d89344..6d772b86f 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/SimplifierBenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/SimplifierBenchmarksBasedTest.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import org.junit.jupiter.api.parallel.Execution import org.junit.jupiter.api.parallel.ExecutionMode diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/YicesBenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/YicesBenchmarksBasedTest.kt similarity index 98% rename from ksmt-test/src/test/kotlin/org/ksmt/test/YicesBenchmarksBasedTest.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/YicesBenchmarksBasedTest.kt index f6b051bc9..7dc77087f 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/YicesBenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/YicesBenchmarksBasedTest.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import org.junit.jupiter.api.parallel.Execution import org.junit.jupiter.api.parallel.ExecutionMode diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/Z3BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/Z3BenchmarksBasedTest.kt similarity index 97% rename from ksmt-test/src/test/kotlin/org/ksmt/test/Z3BenchmarksBasedTest.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/Z3BenchmarksBasedTest.kt index 3539d5b31..17c2cd99f 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/Z3BenchmarksBasedTest.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/Z3BenchmarksBasedTest.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import org.junit.jupiter.api.parallel.Execution import org.junit.jupiter.api.parallel.ExecutionMode diff --git a/ksmt-test/src/test/kotlin/org/ksmt/test/Z3ConverterBenchmark.kt b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/Z3ConverterBenchmark.kt similarity index 99% rename from ksmt-test/src/test/kotlin/org/ksmt/test/Z3ConverterBenchmark.kt rename to ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/Z3ConverterBenchmark.kt index 1ffddec02..e7a166065 100644 --- a/ksmt-test/src/test/kotlin/org/ksmt/test/Z3ConverterBenchmark.kt +++ b/ksmt-test/src/test/kotlin/org/ksmt/test/benchmarks/Z3ConverterBenchmark.kt @@ -1,4 +1,4 @@ -package org.ksmt.test +package org.ksmt.test.benchmarks import com.microsoft.z3.Context import kotlinx.coroutines.async