Test refactoring and documentation update (#82)

* Move benchmarks tests * Move benchmarks tests * Update release workflow * Update docs
UnitTestBot · Mar 10, 2023 · 250b14e · 250b14e
1 parent 6921c86
commit 250b14e
Show file tree

Hide file tree

Showing 15 changed files with 30 additions and 23 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -106,12 +106,13 @@ val downloadPreparedBenchmarksTestData = downloadPreparedSmtLibBenchmarkTestData
 )
 
 tasks.withType<Test> {
-    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/...tlin/org/ksmt/test/BenchmarksBasedTest.kt → ...mt/test/benchmarks/BenchmarksBasedTest.kt b/...tlin/org/ksmt/test/BenchmarksBasedTest.kt → ...mt/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/BitwuzlaBenchmarksBasedTest.kt → ...benchmarks/BitwuzlaBenchmarksBasedTest.kt b/.../ksmt/test/BitwuzlaBenchmarksBasedTest.kt → ...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/.../ContextMemoryUsageBenchmarksBasedTest.kt → .../ContextMemoryUsageBenchmarksBasedTest.kt b/.../ContextMemoryUsageBenchmarksBasedTest.kt → .../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/.../org/ksmt/test/Cvc5BenchmarksBasedTest.kt → ...est/benchmarks/Cvc5BenchmarksBasedTest.kt b/.../org/ksmt/test/Cvc5BenchmarksBasedTest.kt → ...est/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/PortfolioBenchmarksBasedTest.kt → ...enchmarks/PortfolioBenchmarksBasedTest.kt b/...ksmt/test/PortfolioBenchmarksBasedTest.kt → ...enchmarks/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/...smt/test/SerializerBenchmarksBasedTest.kt → ...nchmarks/SerializerBenchmarksBasedTest.kt b/...smt/test/SerializerBenchmarksBasedTest.kt → ...nchmarks/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/...smt/test/SimplifierBenchmarksBasedTest.kt → ...nchmarks/SimplifierBenchmarksBasedTest.kt b/...smt/test/SimplifierBenchmarksBasedTest.kt → ...nchmarks/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/...org/ksmt/test/YicesBenchmarksBasedTest.kt → ...st/benchmarks/YicesBenchmarksBasedTest.kt b/...org/ksmt/test/YicesBenchmarksBasedTest.kt → ...st/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/...in/org/ksmt/test/Z3BenchmarksBasedTest.kt → .../test/benchmarks/Z3BenchmarksBasedTest.kt b/...in/org/ksmt/test/Z3BenchmarksBasedTest.kt → .../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/...lin/org/ksmt/test/Z3ConverterBenchmark.kt → ...t/test/benchmarks/Z3ConverterBenchmark.kt b/...lin/org/ksmt/test/Z3ConverterBenchmark.kt → ...t/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