Bulk assert solver API (UnitTestBot#134)

* Solver bulk assert API * Fix transformer cache * Transformer cache reset API
dee-tree · Oct 24, 2023 · edae365 · edae365
1 parent 3efd7a0
commit edae365
Show file tree

Hide file tree

Showing 17 changed files with 322 additions and 52 deletions.
diff --git a/README.md b/README.md
@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.9)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.10)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.9")
+implementation("io.ksmt:ksmt-core:0.5.10")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.9")
+implementation("io.ksmt:ksmt-z3:0.5.10")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 

diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.9"
+version = "0.5.10"
 
 repositories {
     mavenCentral()

diff --git a/docs/getting-started.md b/docs/getting-started.md
@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.9")    
+    implementation("io.ksmt:ksmt-core:0.5.10")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.9")
+    implementation("io.ksmt:ksmt-z3:0.5.10")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.9")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.10")
 }
 ```
 

diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.9")
+    implementation("io.ksmt:ksmt-core:0.5.10")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.9")
+    implementation("io.ksmt:ksmt-z3:0.5.10")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.9")
+    implementation("io.ksmt:ksmt-runner:0.5.10")
 }
 
 java {

diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/KBoolExprSimplifier.kt
@@ -78,6 +78,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
 
         // Simplify argument and retry expr simplification
         if (simplifiedArgument == null) {
+            markExpressionAsNotTransformed()
             expr.transformAfter(argument)
             return expr
         }
@@ -92,6 +93,7 @@ interface KBoolExprSimplifier : KExprSimplifierBase {
         expr.processNextArgument()
 
         // Repeat simplification with next argument
+        markExpressionAsNotTransformed()
         retryExprTransformation(expr)
 
         return expr

diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt
@@ -27,7 +27,7 @@ import java.util.IdentityHashMap
  * a [transformExprAfterTransformed] method.
  * */
 abstract class KNonRecursiveTransformerBase: KTransformer {
-    private val transformed = IdentityHashMap<KExpr<*>, KExpr<*>>()
+    private var transformed = IdentityHashMap<KExpr<*>, KExpr<*>>()
     private val exprStack = ArrayList<KExpr<*>>()
     private var exprWasTransformed = false
 
@@ -41,7 +41,7 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
             while (exprStack.size > initialStackSize) {
                 val e = exprStack.removeLast()
 
-                val cachedExpr = transformedExpr(expr)
+                val cachedExpr = transformedExpr(e)
                 if (cachedExpr != null) {
                     continue
                 }
@@ -63,6 +63,14 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
         return transformedExpr(expr) ?: error("expr was not properly transformed: $expr")
     }
 
+    /**
+     * Reset transformer expression cache.
+     * */
+    fun resetCache() {
+        check(exprStack.isEmpty()) { "Can not reset cache during expression transformation" }
+        transformed = IdentityHashMap()
+    }
+
     /**
      * Disable [KTransformer] transformApp implementation since it is incorrect
      * for non-recursive usage.

diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt
@@ -22,7 +22,7 @@ import java.util.IdentityHashMap
  * a [visitExprAfterVisited] method.
  * */
 abstract class KNonRecursiveVisitorBase<V : Any> : KVisitor<KExprVisitResult<V>> {
-    private val visitResults = IdentityHashMap<KExpr<*>, V>()
+    private var visitResults = IdentityHashMap<KExpr<*>, V>()
     private val exprStack = ArrayList<KExpr<*>>()
 
     private var lastVisitedExpr: KExpr<*>? = null
@@ -100,6 +100,14 @@ abstract class KNonRecursiveVisitorBase<V : Any> : KVisitor<KExprVisitResult<V>>
         return expr
     }
 
+    /**
+     * Reset visitor expression cache.
+     * */
+    fun resetCache() {
+        check(exprStack.isEmpty()) { "Can not reset cache during expression visit" }
+        visitResults = IdentityHashMap()
+    }
+
     /**
      * Disable [KVisitor] visitApp implementation since it is incorrect
      * for non-recursive usage.

diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt
@@ -20,6 +20,15 @@ interface KSolver<Config: KSolverConfiguration> : AutoCloseable {
     @JvmName("assertExpr")
     fun assert(expr: KExpr<KBoolSort>)
 
+
+    /**
+     * Assert multiple expressions into solver.
+     *
+     * @see check
+     * */
+    @JvmName("assertExprs")
+    fun assert(exprs: List<KExpr<KBoolSort>>) = exprs.forEach { assert(it) }
+
     /**
      * Assert an expression into solver and track it in unsat cores.
      *
@@ -28,6 +37,14 @@ interface KSolver<Config: KSolverConfiguration> : AutoCloseable {
      * */
     fun assertAndTrack(expr: KExpr<KBoolSort>)
 
+    /**
+     * Assert multiple expressions into solver and track them in unsat cores.
+     *
+     * @see checkWithAssumptions
+     * @see unsatCore
+     * */
+    fun assertAndTrack(exprs: List<KExpr<KBoolSort>>) = exprs.forEach { assertAndTrack(it) }
+
     /**
      * Create a backtracking point for assertion stack.
      *