Yices: native bulk asserts (#150)

UnitTestBot · Jan 29, 2024 · c1335bb · c1335bb
1 parent 8296717
commit c1335bb
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuSolver.kt b/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/KSymFpuSolver.kt
@@ -20,6 +20,9 @@ open class KSymFpuSolver<Config : KSolverConfiguration>(
 
     override fun assert(expr: KExpr<KBoolSort>) = solver.assert(transformer.applyAndGetExpr(expr))
 
+    override fun assert(exprs: List<KExpr<KBoolSort>>) =
+        solver.assert(exprs.map { transformer.applyAndGetExpr(it) })
+
     override fun assertAndTrack(expr: KExpr<KBoolSort>) {
         val transformedExpr = transformer.applyAndGetExpr(expr).also { mapTransformedToOriginalAssertions[it] = expr }
         solver.assertAndTrack(transformedExpr)

diff --git a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolver.kt b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolver.kt
@@ -58,6 +58,15 @@ class KYicesSolver(private val ctx: KContext) : KSolver<KYicesSolverConfiguratio
         nativeContext.assertFormula(yicesExpr)
     }
 
+    override fun assert(exprs: List<KExpr<KBoolSort>>) = yicesTry {
+        ctx.ensureContextMatch(exprs)
+
+        val yicesExprs = with(exprInternalizer) {
+            IntArray(exprs.size) { idx -> exprs[idx].internalize() }
+        }
+        nativeContext.assertFormulas(yicesExprs)
+    }
+
     override fun assertAndTrack(expr: KExpr<KBoolSort>) = yicesTry {
         ctx.ensureContextMatch(expr)