Nested transformers (#98)

* Nested transformers * Remove deprecated methods * Update examples * Upgrade version to 0.5.0
UnitTestBot · Apr 14, 2023 · 551cdcf · 551cdcf
1 parent fbe2aa1
commit 551cdcf
Show file tree

Hide file tree

Showing 8 changed files with 80 additions and 52 deletions.
diff --git a/README.md b/README.md
@@ -14,9 +14,9 @@ repositories {
 }
 
 // core 
-implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.6")
+implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")
 // z3 solver
-implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.6")
+implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.0")
 ```
 
 ## Usage

diff --git a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts
@@ -9,7 +9,7 @@ plugins {
 }
 
 group = "org.ksmt"
-version = "0.4.6"
+version = "0.5.0"
 
 repositories {
     mavenCentral()

diff --git a/docs/getting-started.md b/docs/getting-started.md
@@ -18,17 +18,17 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.6")    
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")    
 }
 ```
 
 #### 3. Add one or more SMT solver dependencies:
 ```kotlin
 dependencies {
     // z3 
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.6")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.0")
     // bitwuzla
-    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.6")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.5.0")
 }
 ```
 SMT solver specific packages are provided with solver native binaries. 

diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
@@ -10,9 +10,9 @@ repositories {
 
 dependencies {
     // core
-    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.6")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0")
     // z3 solver
-    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.6")
+    implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.0")
 }
 
 java {

diff --git a/examples/src/main/kotlin/CustomExpressions.kt b/examples/src/main/kotlin/CustomExpressions.kt
@@ -4,6 +4,7 @@ import org.ksmt.cache.structurallyEqual
 import org.ksmt.decl.KConstDecl
 import org.ksmt.decl.KDecl
 import org.ksmt.expr.KExpr
+import org.ksmt.expr.KUninterpretedSortValue
 import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.expr.transformer.KNonRecursiveTransformer
 import org.ksmt.expr.transformer.KTransformer
@@ -221,7 +222,7 @@ class CustomModel(
     override fun <T : KSort> interpretation(decl: KDecl<T>): KModel.KFuncInterp<T>? =
         model.interpretation(decl)
 
-    override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KExpr<KUninterpretedSort>>? =
+    override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set<KUninterpretedSortValue>? =
         model.uninterpretedSortUniverse(sort)
 
     override fun detach(): KModel = CustomModel(model.detach(), transformer)

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
@@ -689,14 +689,6 @@ open class KContext(
         createNoSimplify = ::mkAndNoSimplify
     )
 
-    @Deprecated(
-        "NoFlat builders are deprecated",
-        replaceWith = ReplaceWith("mkAnd(args, flat = false)"),
-        level = DeprecationLevel.ERROR
-    )
-    open fun mkAndNoFlat(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkAnd(args, flat = false)
-
     /**
      * Create boolean binary AND expression.
      *
@@ -715,14 +707,6 @@ open class KContext(
         createNoSimplify = ::mkAndNoSimplify
     )
 
-    @Deprecated(
-        "NoFlat builders are deprecated",
-        replaceWith = ReplaceWith("mkAnd(lhs, rhs, flat = false)"),
-        level = DeprecationLevel.ERROR
-    )
-    open fun mkAndNoFlat(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkAnd(lhs, rhs, flat = false)
-
     open fun mkAndNoSimplify(args: List<KExpr<KBoolSort>>): KAndExpr =
         if (args.size == 2) {
             mkAndNoSimplify(args.first(), args.last())
@@ -759,14 +743,6 @@ open class KContext(
         createNoSimplify = ::mkOrNoSimplify
     )
 
-    @Deprecated(
-        "NoFlat builders are deprecated",
-        replaceWith = ReplaceWith("mkOr(args, flat = false)"),
-        level = DeprecationLevel.ERROR
-    )
-    open fun mkOrNoFlat(args: List<KExpr<KBoolSort>>): KExpr<KBoolSort> =
-        mkOr(args, flat = false)
-
     /**
      * Create boolean binary OR expression.
      *
@@ -785,14 +761,6 @@ open class KContext(
         createNoSimplify = ::mkOrNoSimplify
     )
 
-    @Deprecated(
-        "NoFlat builders are deprecated",
-        replaceWith = ReplaceWith("mkOr(lhs, rhs, flat = false)"),
-        level = DeprecationLevel.ERROR
-    )
-    open fun mkOrNoFlat(lhs: KExpr<KBoolSort>, rhs: KExpr<KBoolSort>): KExpr<KBoolSort> =
-        mkOr(lhs, rhs, flat = false)
-
     open fun mkOrNoSimplify(args: List<KExpr<KBoolSort>>): KOrExpr =
         if (args.size == 2) {
             mkOrNoSimplify(args.first(), args.last())

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt b/ksmt-core/src/main/kotlin/org/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt
@@ -40,17 +40,22 @@ abstract class KNonRecursiveTransformerBase: KTransformer {
             return cachedExpr
         }
 
-        // In case of exceptional execution we may have some expressions on the stack
-        exprStack.clear()
-
-        exprStack.add(expr)
-        while (exprStack.isNotEmpty()) {
-            val e = exprStack.removeLast()
-            exprWasTransformed = true
-            val transformedExpr = e.accept(this)
-
-            if (exprWasTransformed) {
-                transformed[e] = transformedExpr
+        val initialStackSize = exprStack.size
+        try {
+            exprStack.add(expr)
+            while (exprStack.size > initialStackSize) {
+                val e = exprStack.removeLast()
+                exprWasTransformed = true
+                val transformedExpr = e.accept(this)
+
+                if (exprWasTransformed) {
+                    transformed[e] = transformedExpr
+                }
+            }
+        } finally {
+            // cleanup stack after exceptions
+            while (exprStack.size > initialStackSize) {
+                exprStack.removeLast()
             }
         }
 

diff --git a/ksmt-core/src/test/kotlin/org/ksmt/NestedTransformationTest.kt b/ksmt-core/src/test/kotlin/org/ksmt/NestedTransformationTest.kt
@@ -0,0 +1,54 @@
+package org.ksmt
+
+import org.ksmt.expr.KExpr
+import org.ksmt.expr.printer.ExpressionPrinter
+import org.ksmt.expr.transformer.KNonRecursiveTransformer
+import org.ksmt.expr.transformer.KTransformerBase
+import org.ksmt.sort.KSort
+import org.ksmt.utils.getValue
+import kotlin.test.Test
+import kotlin.test.assertEquals
+
+class NestedTransformationTest {
+
+    @Test
+    fun nestedTransformationTest(): Unit = with(KContext()) {
+        val a by intSort
+        val b by intSort
+
+        val transformer = TestAuxTransformer(this)
+
+        val e0 = TestAuxExpr(this, TestAuxExpr(this, a) + TestAuxExpr(this, b))
+        val e1 = TestAuxExpr(this, e0 * TestAuxExpr(this, a))
+        val expr = TestAuxExpr(this, e1 / TestAuxExpr(this, b))
+        val actual = transformer.apply(expr)
+
+        val expected = transformer.apply(((a + b) * a) / b)
+
+        assertEquals(expected, actual)
+    }
+
+    class TestAuxTransformer(ctx: KContext) : KNonRecursiveTransformer(ctx) {
+        fun <T : KSort> transformAux(expr: TestAuxExpr<T>): KExpr<T> {
+            // nested transformation
+            return apply(expr.nested)
+        }
+    }
+
+    class TestAuxExpr<T : KSort>(ctx: KContext, val nested: KExpr<T>) : KExpr<T>(ctx) {
+        override val sort: T
+            get() = nested.sort
+
+        override fun accept(transformer: KTransformerBase): KExpr<T> {
+            transformer as TestAuxTransformer
+            return transformer.transformAux(this)
+        }
+
+        override fun print(printer: ExpressionPrinter) {
+            printer.append(nested)
+        }
+
+        override fun internEquals(other: Any): Boolean = error("Interning is not used")
+        override fun internHashCode(): Int = error("Interning is not used")
+    }
+}