From 551cdcfa197767ea20302601ccc3a668ff5cf9fb Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Fri, 14 Apr 2023 16:40:29 +0300 Subject: [PATCH] Nested transformers (#98) * Nested transformers * Remove deprecated methods * Update examples * Upgrade version to 0.5.0 --- README.md | 4 +- .../main/kotlin/org.ksmt.ksmt-base.gradle.kts | 2 +- docs/getting-started.md | 6 +-- examples/build.gradle.kts | 4 +- examples/src/main/kotlin/CustomExpressions.kt | 3 +- .../src/main/kotlin/org/ksmt/KContext.kt | 32 ----------- .../KNonRecursiveTransformerBase.kt | 27 ++++++---- .../org/ksmt/NestedTransformationTest.kt | 54 +++++++++++++++++++ 8 files changed, 80 insertions(+), 52 deletions(-) create mode 100644 ksmt-core/src/test/kotlin/org/ksmt/NestedTransformationTest.kt diff --git a/README.md b/README.md index c24a8b223..c245d52f8 100644 --- 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 index 8b9ec051d..ef65d7a5f 100644 --- 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 index 488f0b2f4..55a66e543 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -18,7 +18,7 @@ repositories { ```kotlin dependencies { // core - implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.6") + implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.0") } ``` @@ -26,9 +26,9 @@ 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 index d06bc3b1c..b82ed11eb 100644 --- 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 index e16212cde..1bac4f248 100644 --- 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 interpretation(decl: KDecl): KModel.KFuncInterp? = model.interpretation(decl) - override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set>? = + override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set? = 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 index 6570c8f93..6a49f0070 100644 --- 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 = - 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, rhs: KExpr): KExpr = - mkAnd(lhs, rhs, flat = false) - open fun mkAndNoSimplify(args: List>): 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 = - 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, rhs: KExpr): KExpr = - mkOr(lhs, rhs, flat = false) - open fun mkOrNoSimplify(args: List>): 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 index 0e7810b69..dd9bbc56e 100644 --- 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 new file mode 100644 index 000000000..371be47f6 --- /dev/null +++ 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 transformAux(expr: TestAuxExpr): KExpr { + // nested transformation + return apply(expr.nested) + } + } + + class TestAuxExpr(ctx: KContext, val nested: KExpr) : KExpr(ctx) { + override val sort: T + get() = nested.sort + + override fun accept(transformer: KTransformerBase): KExpr { + 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") + } +}