Upgrade KSMT and add solver theory specialization for jvm (#218)

UnitTestBot · Oct 21, 2024 · 158ad96 · 158ad96
1 parent 0acf657
commit 158ad96
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 5 deletions.
diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt
@@ -13,7 +13,7 @@ object Versions {
     const val kotlinx_collections = "0.3.5"
     const val kotlinx_coroutines = "1.6.4"
     const val kotlinx_serialization = "1.4.1"
-    const val ksmt = "0.5.21"
+    const val ksmt = "0.5.26"
     const val logback = "1.4.8"
     const val mockk = "1.13.4"
     const val rd = "2023.2.0"

diff --git a/usvm-jvm/src/main/kotlin/org/usvm/machine/JcSolverFactory.kt b/usvm-jvm/src/main/kotlin/org/usvm/machine/JcSolverFactory.kt
@@ -3,6 +3,7 @@ package org.usvm.machine
 import io.ksmt.KContext
 import io.ksmt.solver.KSolver
 import io.ksmt.solver.KSolverConfiguration
+import io.ksmt.solver.KTheory
 import io.ksmt.solver.runner.KSolverRunnerManager
 import io.ksmt.solver.yices.KYicesSolver
 import io.ksmt.solver.yices.KYicesSolverConfiguration
@@ -30,8 +31,18 @@ private object SameProcessSolverFactory : SolverFactory {
         solverType: SolverType
     ): KSolver<out KSolverConfiguration> = when (solverType) {
         // Yices with Fp support via SymFpu
-        SolverType.YICES -> KSymFpuSolver(KYicesSolver(ctx), ctx)
-        SolverType.Z3 -> KZ3Solver(ctx)
+        SolverType.YICES -> KSymFpuSolver(KYicesSolver(ctx), ctx).apply {
+            configure {
+                // Fp theory is handled by the SymFpu
+                optimizeForTheories(setOf(KTheory.Array, KTheory.BV, KTheory.UF))
+            }
+        }
+
+        SolverType.Z3 -> KZ3Solver(ctx).apply {
+            configure {
+                optimizeForTheories(setOf(KTheory.Array, KTheory.BV, KTheory.UF, KTheory.FP))
+            }
+        }
     }
 
     override fun close() {
@@ -52,8 +63,18 @@ private class AnotherProcessSolverFactory : SolverFactory {
         solverType: SolverType
     ): KSolver<out KSolverConfiguration> = when (solverType) {
         // Yices with Fp support via SymFpu
-        SolverType.YICES -> solverManager.createSolver(ctx, YicesWithSymFpu::class)
-        SolverType.Z3 -> solverManager.createSolver(ctx, KZ3Solver::class)
+        SolverType.YICES -> solverManager.createSolver(ctx, YicesWithSymFpu::class).apply {
+            configure {
+                // Fp theory is handled by the SymFpu
+                optimizeForTheories(setOf(KTheory.Array, KTheory.BV, KTheory.UF))
+            }
+        }
+
+        SolverType.Z3 -> solverManager.createSolver(ctx, KZ3Solver::class).apply {
+            configure {
+                optimizeForTheories(setOf(KTheory.Array, KTheory.BV, KTheory.UF, KTheory.FP))
+            }
+        }
     }
 
     override fun close() {