Solver configuration api (#34)

* KModel toString/equals/hashCode

* Solver configuration api

* Fix example and documentation

* Solver configuration docs

* Update version

* Fix Fp custom sized decl

* Skip bad test case

* Handle failed worker initialization

* Fix test data cache

* Cache downloaded testData

* Cache on all os

* Handle hard timeout in check-sat as Unknown

Author: Saloed

.github/workflows/release.yml

@@ -31,4 +31,5 @@ jobs:
             ksmt-core/build/release/**/ksmt-core-*.jar
             ksmt-z3/build/release/**/ksmt-z3-*.jar
             ksmt-bitwuzla/build/release/**/ksmt-bitwuzla-*.jar
+            ksmt-runner/build/release/**/ksmt-runner-*.jar
             

.github/workflows/run-long-tests.yml

@@ -20,6 +20,9 @@ on:
         type: number
         default: 170000
 
+env:
+  TEST_DATA_REVISION: 0.2.1
+
 jobs:
   setup:
     runs-on: ubuntu-latest
@@ -58,53 +61,95 @@ jobs:
           TEST_ARRAY+="]"
           echo "tests=$TEST_ARRAY" >> $GITHUB_OUTPUT
 
-  run_tests:
-    needs: setup
-    continue-on-error: true
+  prepare_test_data:
     strategy:
       matrix:
         os: [ ubuntu-latest, windows-latest ]
-        test: ${{ fromJSON(needs.setup.outputs.matrix-tests) }}
-        chunk: ${{ fromJSON(needs.setup.outputs.matrix-chunks) }}
-
-    name: Run ${{ matrix.test }}[${{ matrix.chunk }}] on ${{ matrix.os }}
 
     runs-on: ${{ matrix.os }}
 
     steps:
       - uses: actions/checkout@v3
 
+      - name: Prepare test data (cache)
+        id: test-data-cache
+        uses: actions/cache@v3
+        env:
+          cache-name: cache-test-data
+        with:
+          key: test-data-${{ env.TEST_DATA_REVISION }}-${{ matrix.os }}
+          path: ksmt-test/testData/testData.zip
+
       - name: Set up JDK 1.8
+        if: steps.test-data-cache.outputs.cache-hit != 'true'
         uses: actions/setup-java@v3
         with:
           java-version: 8
           distribution: 'zulu'
           cache: gradle
 
-      - name: Build project
+      - name: Prepare test data (download)
+        if: steps.test-data-cache.outputs.cache-hit != 'true'
         uses: gradle/gradle-build-action@v2
         with:
           arguments: |
-            build
+            :ksmt-test:downloadPreparedSmtLibBenchmarkTestData
             --no-daemon
+            -PtestDataRevision=${{ env.TEST_DATA_REVISION }}
+
+  run_tests:
+    needs: [setup, prepare_test_data]
+    continue-on-error: true
+    strategy:
+      matrix:
+        os: [ ubuntu-latest, windows-latest ]
+        test: ${{ fromJSON(needs.setup.outputs.matrix-tests) }}
+        chunk: ${{ fromJSON(needs.setup.outputs.matrix-chunks) }}
+
+    name: Run ${{ matrix.test }}[${{ matrix.chunk }}] on ${{ matrix.os }}
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - uses: actions/checkout@v3
 
       - name: Prepare test data (cache)
         id: test-data-cache
         uses: actions/cache@v3
         env:
           cache-name: cache-test-data
         with:
-          key: test-data-0.2.1-${{ matrix.os }}
-          path: ksmt-test/testData
+          key: test-data-${{ env.TEST_DATA_REVISION }}-${{ matrix.os }}
+          path: ksmt-test/testData/testData.zip
 
-      - name: Prepare test data (download)
+      - name: Check test data downloaded
         if: steps.test-data-cache.outputs.cache-hit != 'true'
+        run: |
+          echo "Test data is not available"
+          exit 1
+
+      - name: Set up JDK 1.8
+        uses: actions/setup-java@v3
+        with:
+          java-version: 8
+          distribution: 'zulu'
+          cache: gradle
+
+      # 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: |
             :ksmt-test:downloadPreparedSmtLibBenchmarkTestData
             --no-daemon
-            -PtestDataRevision=0.2.1
+            -PtestDataRevision=${{ env.TEST_DATA_REVISION }}
+
+      - name: Build project
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: |
+            build
+            --no-daemon
 
       - name: Run ${{ matrix.test }}
         uses: gradle/gradle-build-action@v2

README.md

@@ -14,9 +14,9 @@ repositories {
 }
 
 // core 
-implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.2.1")
+implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.0")
 // z3 solver
-implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.2.1")
+implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.0")
 ```
 
 ## Usage
@@ -52,8 +52,8 @@ val array by mkArraySort(intSort, intSort)
 val index by intSort
 val value by intSort
 
-val expr = (array.select(index - 1.intExpr) lt value) and
-        (array.select(index + 1.intExpr) gt value)
+val expr = (array.select(index - 1.expr) lt value) and
+        (array.select(index + 1.expr) gt value)
 ```
 Check out our [example project](examples) for more complicated examples.
 

Requirements.md

@@ -13,7 +13,7 @@
 | [CVC5 solver support](#cvc5-solver-support)                                       | TODO            |
 | [External process runner](#external-process-runner)                               | Done            |
 | [Portfolio solver](#portfolio-solver)                                             | TODO            |
-| [Solver configuration API](#solver-configuration-api)                             | In progress     |
+| [Solver configuration API](#solver-configuration-api)                             | Done            |
 | [Deployment](#deployment)                                                         | Done partially  |
 | [Expression simplification / evaluation](#expression-simplification--evaluation)  | Done partially  |
 | [Performance tests](#performance-tests)                                           | TODO            |

buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt

@@ -54,19 +54,16 @@ fun Project.usePreparedSmtLibBenchmarkTestData(path: File) = tasks.register("smt
     }
 }
 
-fun Project.downloadPreparedSmtLibBenchmarkTestData(path: File, version: String) =
+fun Project.downloadPreparedSmtLibBenchmarkTestData(downloadPath: File, testDataPath: File, version: String) =
     tasks.register("downloadPreparedSmtLibBenchmarkTestData") {
         doLast {
-            path.mkdir()
-
             val benchmarksUrl = "https://github.com/UnitTestBot/ksmt/releases/download/$version/benchmarks.zip"
-            val downloadPath = buildDir.resolve("benchmarks.zip")
 
             download(benchmarksUrl, downloadPath)
 
             copy {
                 from(zipTree(downloadPath))
-                into(path)
+                into(testDataPath)
                 duplicatesStrategy = DuplicatesStrategy.EXCLUDE
             }
         }

buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts

@@ -9,7 +9,7 @@ plugins {
 }
 
 group = "org.ksmt"
-version = "0.2.1"
+version = "0.3.0"
 
 repositories {
     mavenCentral()

docs/getting-started.md

@@ -18,17 +18,17 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.2.1")    
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.0")    
 }
 ```
 
 #### 3. Add one or more SMT solver dependencies:
 ```kotlin
 dependencies {
     // z3 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.2.1")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.0")
     // bitwuzla
-    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.2.1")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.3.0")
 }
 ```
 SMT solver specific packages are provided with solver native binaries. 
@@ -51,19 +51,24 @@ In this example, we want to create an expression
 over Boolean variable `a` and integer variables `b` and `c`.
 
 ```kotlin
+import org.ksmt.utils.getValue
+
 with(ctx) {
     // create symbolic variables
     val a by boolSort
     val b by intSort
     val c by intSort
 
     // create expression
-    val constraint = a and (b ge c + 3.intExpr)
+    val constraint = a and (b ge c + 3.expr)
 }
 ```
 All KSMT expressions are typed and incorrect terms (e.g. `and` with integer arguments) 
 result in a compile-time error.
 
+Note the use of `import getValue`, which is required for the `by` syntax.
+Alternatively, `mkConst(name, sort)` can be used. 
+
 ### Working with SMT solvers
 
 To check SMT formula satisfiability we need to instantiate an SMT solver. 
@@ -112,10 +117,10 @@ with(ctx) {
     // create symbolic variables
     val cond1 by boolSort
     val cond2 by boolSort
-    val a by mkBv32Sort()
-    val b by mkBv32Sort()
-    val c by mkBv32Sort()
-    val goal by mkBv32Sort()
+    val a by bv32Sort
+    val b by bv32Sort
+    val c by bv32Sort
+    val goal by bv32Sort
 
     KZ3Solver(this).use { solver ->
         // a == 0
@@ -212,10 +217,10 @@ with(ctx) {
     // create symbolic variables
     val cond1 by boolSort
     val cond2 by boolSort
-    val a by mkBv32Sort()
-    val b by mkBv32Sort()
-    val c by mkBv32Sort()
-    val goal by mkBv32Sort()
+    val a by bv32Sort
+    val b by bv32Sort
+    val c by bv32Sort
+    val goal by bv32Sort
 
     KZ3Solver(this).use { solver ->
         // a == 0
@@ -357,3 +362,21 @@ with(ctx) {
     val assertions = KZ3SMTLibParser().parse(formula)
 }
 ```
+
+### Solver configuration
+
+KSMT provides an API for modifying solver-specific parameters. 
+Since the parameters and their correct values are solver-specific 
+KSMT does not perform any checks. 
+See the corresponding solver documentation for a list of available options. 
+
+```kotlin
+with(ctx) {
+    KZ3Solver(this).use { solver ->
+        solver.configure {
+            // set Z3 solver parameter random_seed to 42 
+            setZ3Option("random_seed", 42)
+        }
+    }
+}
+```

examples/build.gradle.kts

@@ -1,6 +1,6 @@
 plugins {
     kotlin("jvm") version "1.7.20"
-    `java-library`
+    java
 }
 
 repositories {
@@ -10,9 +10,9 @@ repositories {
 
 dependencies {
     // core
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.2.1")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.0")
     // z3 solver
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.2.1")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.0")
 }
 
 java {

examples/src/main/java/Sudoku.java

@@ -53,7 +53,7 @@ public static void main(String[] args) {
             final List<KExpr<KBoolSort>> symbolAssignments = assignSymbols(ctx, symbols, initialGrid);
 
             // Create Z3 SMT solver instance.
-            try (final KSolver solver = new KZ3Solver(ctx)) {
+            try (final KSolver<?> solver = new KZ3Solver(ctx)) {
                 // Assert all constraints.
                 rules.forEach(solver::assertExpr);
                 symbolAssignments.forEach(solver::assertExpr);
@@ -79,7 +79,7 @@ private static List<List<KExpr<KIntSort>>> createSymbolicGrid(final KContext ctx
         for (int row = 0; row < SIZE; row++) {
             final List<KExpr<KIntSort>> gridRow = new ArrayList<>();
             for (int col = 0; col < SIZE; col++) {
-                gridRow.add(ctx.mkConst(ctx.getIntSort(), "x_" + row + "_" + col));
+                gridRow.add(ctx.mkConst("x_" + row + "_" + col, ctx.getIntSort()));
             }
             grid.add(gridRow);
         }
@@ -93,8 +93,8 @@ private static List<KExpr<KBoolSort>> sudokuRules(final KContext ctx,
         final Stream<KExpr<KBoolSort>> symbolConstraints = symbols
                 .stream().flatMap(Collection::stream)
                 .map(cell -> ctx.and(
-                        ctx.ge(cell, ctx.getIntExpr(1)),
-                        ctx.le(cell, ctx.getIntExpr(9))));
+                        ctx.ge(cell, ctx.getExpr(1)),
+                        ctx.le(cell, ctx.getExpr(9))));
 
         // Each row contains distinct numbers.
         final Stream<KExpr<KBoolSort>> rowDistinctConstraints = symbols.stream()
@@ -138,7 +138,7 @@ private static List<KExpr<KBoolSort>> assignSymbols(final KContext ctx,
             for (int col = 0; col < SIZE; col++) {
                 int cell = grid.get(row).get(col);
                 if (cell != EMPTY_CELL_VALUE) {
-                    assignments.add(ctx.eq(symbols.get(row).get(col), ctx.getIntExpr(cell)));
+                    assignments.add(ctx.eq(symbols.get(row).get(col), ctx.getExpr(cell)));
                 }
             }
         }

examples/src/main/kotlin/GettingStartedExample.kt

@@ -1,5 +1,6 @@
 import org.ksmt.KContext
 import org.ksmt.solver.z3.KZ3Solver
+import org.ksmt.utils.getValue
 import kotlin.time.Duration.Companion.seconds
 
 fun main() {
@@ -22,7 +23,7 @@ private fun basicSolverUsageExample(ctx: KContext) =
         val c by intSort
 
         // create expression
-        val constraint = a and (b ge c + 3.intExpr)
+        val constraint = a and (b ge c + 3.expr)
 
         KZ3Solver(this).use { solver -> // create s Z3 Smt solver instance
             // assert expression
@@ -46,10 +47,10 @@ private fun pushPopIncrementalExample(ctx: KContext) =
         // create symbolic variables
         val cond1 by boolSort
         val cond2 by boolSort
-        val a by mkBv32Sort()
-        val b by mkBv32Sort()
-        val c by mkBv32Sort()
-        val goal by mkBv32Sort()
+        val a by bv32Sort
+        val b by bv32Sort
+        val c by bv32Sort
+        val goal by bv32Sort
 
         KZ3Solver(this).use { solver ->
             // a == 0
@@ -138,10 +139,10 @@ private fun assumptionsIncrementalExample(ctx: KContext) =
         // create symbolic variables
         val cond1 by boolSort
         val cond2 by boolSort
-        val a by mkBv32Sort()
-        val b by mkBv32Sort()
-        val c by mkBv32Sort()
-        val goal by mkBv32Sort()
+        val a by bv32Sort
+        val b by bv32Sort
+        val c by bv32Sort
+        val goal by bv32Sort
 
         KZ3Solver(this).use { solver ->
             // a == 0