From c5fee2cdea45f3e2305a167909a9a02340d0c0af Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Fri, 21 Jul 2023 17:59:03 +0300 Subject: [PATCH] Expression visitor (#122) * Expression visitor * Visit expressions in more intuitive order * Better cache reuse in visitor/transformer * Upgrade version to 0.5.5 --- README.md | 6 +- .../main/kotlin/io.ksmt.ksmt-base.gradle.kts | 2 +- docs/getting-started.md | 6 +- examples/build.gradle.kts | 6 +- .../KNonRecursiveTransformerBase.kt | 11 +- .../expr/transformer/KNonRecursiveVisitor.kt | 807 ++++++++++++++++++ .../transformer/KNonRecursiveVisitorBase.kt | 371 ++++++++ .../io/ksmt/expr/transformer/KVisitor.kt | 635 ++++++++++++++ .../kotlin/io/ksmt/ExpressionVisitorTest.kt | 100 +++ 9 files changed, 1929 insertions(+), 15 deletions(-) create mode 100644 ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitor.kt create mode 100644 ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt create mode 100644 ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KVisitor.kt create mode 100644 ksmt-core/src/test/kotlin/io/ksmt/ExpressionVisitorTest.kt diff --git a/README.md b/README.md index 765b480ff..6002ef7b7 100644 --- 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.4) +[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.5) [![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.4") +implementation("io.ksmt:ksmt-core:0.5.5") // z3 solver -implementation("io.ksmt:ksmt-z3:0.5.4") +implementation("io.ksmt:ksmt-z3:0.5.5") ``` 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 index 2d8323a84..03d589fdc 100644 --- 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.4" +version = "0.5.5" repositories { mavenCentral() diff --git a/docs/getting-started.md b/docs/getting-started.md index cc67839d7..fdf6d8c35 100644 --- 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.4") + implementation("io.ksmt:ksmt-core:0.5.5") } ``` @@ -43,9 +43,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("io.ksmt:ksmt-z3:0.5.4") + implementation("io.ksmt:ksmt-z3:0.5.5") // bitwuzla - implementation("io.ksmt:ksmt-bitwuzla:0.5.4") + implementation("io.ksmt:ksmt-bitwuzla:0.5.5") } ``` diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index b61c0a6dc..7446db668 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -9,11 +9,11 @@ repositories { dependencies { // core - implementation("io.ksmt:ksmt-core:0.5.4") + implementation("io.ksmt:ksmt-core:0.5.5") // z3 solver - implementation("io.ksmt:ksmt-z3:0.5.4") + implementation("io.ksmt:ksmt-z3:0.5.5") // Runner and portfolio solver - implementation("io.ksmt:ksmt-runner:0.5.4") + implementation("io.ksmt:ksmt-runner:0.5.5") } java { 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 index 0e2277a0c..288280cee 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformerBase.kt @@ -35,16 +35,17 @@ abstract class KNonRecursiveTransformerBase: KTransformer { * Transform [expr] and all it sub-expressions non-recursively. * */ override fun apply(expr: KExpr): KExpr { - val cachedExpr = transformedExpr(expr) - if (cachedExpr != null) { - return cachedExpr - } - val initialStackSize = exprStack.size try { exprStack.add(expr) while (exprStack.size > initialStackSize) { val e = exprStack.removeLast() + + val cachedExpr = transformedExpr(expr) + if (cachedExpr != null) { + continue + } + exprWasTransformed = true val transformedExpr = e.accept(this) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitor.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitor.kt new file mode 100644 index 000000000..35bd4d57b --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitor.kt @@ -0,0 +1,807 @@ +package io.ksmt.expr.transformer + +import io.ksmt.KContext +import io.ksmt.expr.KAddArithExpr +import io.ksmt.expr.KAndBinaryExpr +import io.ksmt.expr.KAndExpr +import io.ksmt.expr.KApp +import io.ksmt.expr.KArray2Lambda +import io.ksmt.expr.KArray2Select +import io.ksmt.expr.KArray2Store +import io.ksmt.expr.KArray3Lambda +import io.ksmt.expr.KArray3Select +import io.ksmt.expr.KArray3Store +import io.ksmt.expr.KArrayConst +import io.ksmt.expr.KArrayLambda +import io.ksmt.expr.KArrayNLambda +import io.ksmt.expr.KArrayNSelect +import io.ksmt.expr.KArrayNStore +import io.ksmt.expr.KArraySelect +import io.ksmt.expr.KArrayStore +import io.ksmt.expr.KBv2IntExpr +import io.ksmt.expr.KBvAddExpr +import io.ksmt.expr.KBvAddNoOverflowExpr +import io.ksmt.expr.KBvAddNoUnderflowExpr +import io.ksmt.expr.KBvAndExpr +import io.ksmt.expr.KBvArithShiftRightExpr +import io.ksmt.expr.KBvConcatExpr +import io.ksmt.expr.KBvDivNoOverflowExpr +import io.ksmt.expr.KBvExtractExpr +import io.ksmt.expr.KBvLogicalShiftRightExpr +import io.ksmt.expr.KBvMulExpr +import io.ksmt.expr.KBvMulNoOverflowExpr +import io.ksmt.expr.KBvMulNoUnderflowExpr +import io.ksmt.expr.KBvNAndExpr +import io.ksmt.expr.KBvNegNoOverflowExpr +import io.ksmt.expr.KBvNegationExpr +import io.ksmt.expr.KBvNorExpr +import io.ksmt.expr.KBvNotExpr +import io.ksmt.expr.KBvOrExpr +import io.ksmt.expr.KBvReductionAndExpr +import io.ksmt.expr.KBvReductionOrExpr +import io.ksmt.expr.KBvRepeatExpr +import io.ksmt.expr.KBvRotateLeftExpr +import io.ksmt.expr.KBvRotateLeftIndexedExpr +import io.ksmt.expr.KBvRotateRightExpr +import io.ksmt.expr.KBvRotateRightIndexedExpr +import io.ksmt.expr.KBvShiftLeftExpr +import io.ksmt.expr.KBvSignExtensionExpr +import io.ksmt.expr.KBvSignedDivExpr +import io.ksmt.expr.KBvSignedGreaterExpr +import io.ksmt.expr.KBvSignedGreaterOrEqualExpr +import io.ksmt.expr.KBvSignedLessExpr +import io.ksmt.expr.KBvSignedLessOrEqualExpr +import io.ksmt.expr.KBvSignedModExpr +import io.ksmt.expr.KBvSignedRemExpr +import io.ksmt.expr.KBvSubExpr +import io.ksmt.expr.KBvSubNoOverflowExpr +import io.ksmt.expr.KBvSubNoUnderflowExpr +import io.ksmt.expr.KBvToFpExpr +import io.ksmt.expr.KBvUnsignedDivExpr +import io.ksmt.expr.KBvUnsignedGreaterExpr +import io.ksmt.expr.KBvUnsignedGreaterOrEqualExpr +import io.ksmt.expr.KBvUnsignedLessExpr +import io.ksmt.expr.KBvUnsignedLessOrEqualExpr +import io.ksmt.expr.KBvUnsignedRemExpr +import io.ksmt.expr.KBvXNorExpr +import io.ksmt.expr.KBvXorExpr +import io.ksmt.expr.KBvZeroExtensionExpr +import io.ksmt.expr.KConst +import io.ksmt.expr.KDistinctExpr +import io.ksmt.expr.KDivArithExpr +import io.ksmt.expr.KEqExpr +import io.ksmt.expr.KExistentialQuantifier +import io.ksmt.expr.KExpr +import io.ksmt.expr.KFpAbsExpr +import io.ksmt.expr.KFpAddExpr +import io.ksmt.expr.KFpDivExpr +import io.ksmt.expr.KFpEqualExpr +import io.ksmt.expr.KFpFromBvExpr +import io.ksmt.expr.KFpFusedMulAddExpr +import io.ksmt.expr.KFpGreaterExpr +import io.ksmt.expr.KFpGreaterOrEqualExpr +import io.ksmt.expr.KFpIsInfiniteExpr +import io.ksmt.expr.KFpIsNaNExpr +import io.ksmt.expr.KFpIsNegativeExpr +import io.ksmt.expr.KFpIsNormalExpr +import io.ksmt.expr.KFpIsPositiveExpr +import io.ksmt.expr.KFpIsSubnormalExpr +import io.ksmt.expr.KFpIsZeroExpr +import io.ksmt.expr.KFpLessExpr +import io.ksmt.expr.KFpLessOrEqualExpr +import io.ksmt.expr.KFpMaxExpr +import io.ksmt.expr.KFpMinExpr +import io.ksmt.expr.KFpMulExpr +import io.ksmt.expr.KFpNegationExpr +import io.ksmt.expr.KFpRemExpr +import io.ksmt.expr.KFpRoundToIntegralExpr +import io.ksmt.expr.KFpSqrtExpr +import io.ksmt.expr.KFpSubExpr +import io.ksmt.expr.KFpToBvExpr +import io.ksmt.expr.KFpToFpExpr +import io.ksmt.expr.KFpToIEEEBvExpr +import io.ksmt.expr.KFpToRealExpr +import io.ksmt.expr.KFunctionApp +import io.ksmt.expr.KGeArithExpr +import io.ksmt.expr.KGtArithExpr +import io.ksmt.expr.KImpliesExpr +import io.ksmt.expr.KInterpretedValue +import io.ksmt.expr.KIsIntRealExpr +import io.ksmt.expr.KIteExpr +import io.ksmt.expr.KLeArithExpr +import io.ksmt.expr.KLtArithExpr +import io.ksmt.expr.KModIntExpr +import io.ksmt.expr.KMulArithExpr +import io.ksmt.expr.KNotExpr +import io.ksmt.expr.KOrBinaryExpr +import io.ksmt.expr.KOrExpr +import io.ksmt.expr.KPowerArithExpr +import io.ksmt.expr.KRealToFpExpr +import io.ksmt.expr.KRemIntExpr +import io.ksmt.expr.KSubArithExpr +import io.ksmt.expr.KToIntRealExpr +import io.ksmt.expr.KToRealIntExpr +import io.ksmt.expr.KUnaryMinusArithExpr +import io.ksmt.expr.KUniversalQuantifier +import io.ksmt.expr.KXorExpr +import io.ksmt.sort.KArithSort +import io.ksmt.sort.KArraySortBase +import io.ksmt.sort.KBvSort +import io.ksmt.sort.KFpSort +import io.ksmt.sort.KSort + +/** + * Apply specialized non-recursive visit for all KSMT expressions. + * See [KNonRecursiveVisitorBase] for details. + * */ +abstract class KNonRecursiveVisitor( + override val ctx: KContext +) : KNonRecursiveVisitorBase() { + + /** + * Provides a default value for leaf expressions + * that don't have a special visit and are not accepted by the generic visitor [visitExpr]. + * + * @see [visitExprAfterVisitedDefault] + * */ + abstract fun defaultValue(expr: KExpr): V + + /** + * Merge subexpressions visit results. + * + * @see [visitExprAfterVisitedDefault] + * */ + abstract fun mergeResults(left: V, right: V): V + + override fun visitExpr(expr: KExpr): KExprVisitResult = KExprVisitResult.EMPTY + + override fun visitApp(expr: KApp): KExprVisitResult = visitExpr(expr) + + // function visitors + override fun visit(expr: KFunctionApp): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.args, ::visitApp) + + override fun visit(expr: KConst): KExprVisitResult = + visitExprAfterVisitedDefault(expr, ::visitApp) + + override fun visitValue(expr: KInterpretedValue): KExprVisitResult = + visitExprAfterVisitedDefault(expr, ::visitApp) + + // bool visitors + override fun visit(expr: KAndExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.args, ::visitApp + ) + + override fun visit(expr: KAndBinaryExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.lhs, expr.rhs, ::visitApp + ) + + override fun visit(expr: KOrExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.args, ::visitApp + ) + + override fun visit(expr: KOrBinaryExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.lhs, expr.rhs, ::visitApp + ) + + override fun visit(expr: KNotExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KImpliesExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.p, expr.q, ::visitApp) + + override fun visit(expr: KXorExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.a, expr.b, ::visitApp) + + override fun visit(expr: KEqExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.lhs, expr.rhs, ::visitApp + ) + + override fun visit(expr: KDistinctExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.args, ::visitApp + ) + + override fun visit(expr: KIteExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, + expr.condition, + expr.trueBranch, + expr.falseBranch, + ::visitApp + ) + + // bit-vec expressions visitors + override fun visit(expr: KBvNotExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvReductionAndExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvReductionOrExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvAndExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvOrExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvXorExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvNAndExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvNorExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvXNorExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvNegationExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvAddExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvSubExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvMulExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvUnsignedDivExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvSignedDivExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvUnsignedRemExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvSignedRemExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvSignedModExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvUnsignedLessExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvSignedLessExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvUnsignedLessOrEqualExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KBvSignedLessOrEqualExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KBvUnsignedGreaterOrEqualExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KBvSignedGreaterOrEqualExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KBvUnsignedGreaterExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KBvSignedGreaterExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KBvConcatExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvExtractExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvSignExtensionExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvZeroExtensionExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvRepeatExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvShiftLeftExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, expr.shift, ::visitApp) + + override fun visit(expr: KBvLogicalShiftRightExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg, expr.shift, ::visitApp + ) + + override fun visit(expr: KBvArithShiftRightExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg, expr.shift, ::visitApp + ) + + override fun visit(expr: KBvRotateLeftExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg, expr.rotation, ::visitApp + ) + + override fun visit(expr: KBvRotateLeftIndexedExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvRotateRightExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg, expr.rotation, ::visitApp + ) + + override fun visit(expr: KBvRotateRightIndexedExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBv2IntExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvAddNoOverflowExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvAddNoUnderflowExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KBvSubNoOverflowExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KBvSubNoUnderflowExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvDivNoOverflowExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KBvNegNoOverflowExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KBvMulNoOverflowExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KBvMulNoUnderflowExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + // fp operations tranformation + override fun visit(expr: KFpAbsExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpNegationExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpAddExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KFpSubExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KFpMulExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KFpDivExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KFpFusedMulAddExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.arg0, expr.arg1, expr.arg2, ::visitApp + ) + + override fun visit(expr: KFpSqrtExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.value, ::visitApp + ) + + override fun visit(expr: KFpRemExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KFpRoundToIntegralExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.value, ::visitApp + ) + + override fun visit(expr: KFpMinExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KFpMaxExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KFpLessOrEqualExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KFpLessExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KFpGreaterOrEqualExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.arg0, expr.arg1, ::visitApp + ) + + override fun visit(expr: KFpGreaterExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KFpEqualExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KFpIsNormalExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpIsSubnormalExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpIsZeroExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpIsInfiniteExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpIsNaNExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpIsNegativeExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpIsPositiveExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpToBvExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.roundingMode, expr.value, ::visitApp) + + override fun visit(expr: KFpToRealExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpToIEEEBvExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + override fun visit(expr: KFpFromBvExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.sign, expr.biasedExponent, expr.significand, ::visitApp + ) + + override fun visit(expr: KFpToFpExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.value, ::visitApp + ) + + override fun visit(expr: KRealToFpExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.value, ::visitApp + ) + + override fun visit(expr: KBvToFpExpr): KExprVisitResult = + visitExprAfterVisitedDefault( + expr, expr.roundingMode, expr.value, ::visitApp + ) + + // array visitors + override fun visit( + expr: KArrayStore + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.array, expr.index, expr.value, ::visitArrayStore + ) + + override fun visit( + expr: KArray2Store + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.array, expr.index0, expr.index1, expr.value, ::visitArrayStore + ) + + override fun visit( + expr: KArray3Store + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.array, expr.index0, expr.index1, expr.index2, expr.value, + ::visitArrayStore + ) + + override fun visit( + expr: KArrayNStore + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.args, ::visitArrayStore + ) + + override fun visit( + expr: KArraySelect + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.array, expr.index, ::visitArraySelect + ) + + override fun visit( + expr: KArray2Select + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.array, expr.index0, expr.index1, ::visitArraySelect + ) + + override fun visit( + expr: KArray3Select + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.array, expr.index0, expr.index1, expr.index2, ::visitArraySelect + ) + + override fun visit( + expr: KArrayNSelect + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.args, ::visitArraySelect + ) + + override fun visit( + expr: KArrayLambda + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.body, ::visitArrayLambda + ) + + override fun visit( + expr: KArray2Lambda + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.body, ::visitArrayLambda + ) + + override fun visit( + expr: KArray3Lambda + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.body, ::visitArrayLambda + ) + + override fun visit( + expr: KArrayNLambda + ): KExprVisitResult = visitExprAfterVisitedDefault( + expr, expr.body, ::visitArrayLambda + ) + + override fun , R : KSort> visit(expr: KArrayConst): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.value, ::visitApp) + + // arith visitors + override fun visit(expr: KAddArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.args, ::visitApp) + + override fun visit(expr: KMulArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.args, ::visitApp) + + override fun visit(expr: KSubArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.args, ::visitApp) + + override fun visit(expr: KUnaryMinusArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KDivArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.lhs, expr.rhs, ::visitApp) + + override fun visit(expr: KPowerArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.lhs, expr.rhs, ::visitApp) + + override fun visit(expr: KLtArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.lhs, expr.rhs, ::visitApp) + + override fun visit(expr: KLeArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.lhs, expr.rhs, ::visitApp) + + override fun visit(expr: KGtArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.lhs, expr.rhs, ::visitApp) + + override fun visit(expr: KGeArithExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.lhs, expr.rhs, ::visitApp) + + // integer visitors + override fun visit(expr: KModIntExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.lhs, expr.rhs, ::visitApp) + + override fun visit(expr: KRemIntExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.lhs, expr.rhs, ::visitApp) + + override fun visit(expr: KToRealIntExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + // real visitors + override fun visit(expr: KToIntRealExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KIsIntRealExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + // quantified expressions + override fun visit(expr: KExistentialQuantifier): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.body, ::visitExpr) + + override fun visit(expr: KUniversalQuantifier): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.body, ::visitExpr) + + /** + * 1. Visit [dependencies] and merge their results. + * 2. Visit [expr] with generic visitor [visitDefault]. + * Merge result with dependencies visit results. + * 3. If merged result is empty return [defaultValue]. + * */ + inline fun > visitExprAfterVisitedDefault( + expr: E, + dependencies: List>, + visitDefault: (E) -> KExprVisitResult + ): KExprVisitResult = visitExprAfterVisited(expr, dependencies) { visitedDependencies -> + val defaultRes = visitDefault(expr) + if (defaultRes.dependencyVisitRequired) { + return defaultRes + } + + val dependenciesResults = visitedDependencies.reduceOrNull(::mergeResults) + if (dependenciesResults == null) { + if (defaultRes.hasResult) { + defaultRes.result + } else { + defaultValue(expr) + } + } else { + if (defaultRes.hasResult) { + mergeResults(dependenciesResults, defaultRes.result) + } else { + dependenciesResults + } + } + } + + /** + * Specialized version of [visitExprAfterVisitedDefault] for expression with zero arguments. + * */ + inline fun > visitExprAfterVisitedDefault( + expr: E, + visitDefault: (E) -> KExprVisitResult + ): KExprVisitResult { + val defaultRes = visitDefault(expr) + if (defaultRes.isNotEmpty) { + return defaultRes + } + + return saveVisitResult(expr, defaultValue(expr)) + } + + /** + * Specialized version of [visitExprAfterVisitedDefault] for expression with single argument. + * */ + inline fun > visitExprAfterVisitedDefault( + expr: E, + dependency: KExpr<*>, + visitDefault: (E) -> KExprVisitResult + ): KExprVisitResult = visitExprAfterVisited(expr, dependency) { dr -> + val defaultRes = visitDefault(expr) + if (defaultRes.dependencyVisitRequired) { + return defaultRes + } + if (defaultRes.hasResult) { + mergeResults(dr, defaultRes.result) + } else { + dr + } + } + + /** + * Specialized version of [visitExprAfterVisitedDefault] for expression with two arguments. + * */ + inline fun > visitExprAfterVisitedDefault( + expr: E, + dependency0: KExpr<*>, + dependency1: KExpr<*>, + visitDefault: (E) -> KExprVisitResult + ): KExprVisitResult = visitExprAfterVisited(expr, dependency0, dependency1) { dr0, dr1 -> + val defaultRes = visitDefault(expr) + if (defaultRes.dependencyVisitRequired) { + return defaultRes + } + + val dependencyResults = mergeResults(dr0, dr1) + if (defaultRes.hasResult) { + mergeResults(dependencyResults, defaultRes.result) + } else { + dependencyResults + } + } + + /** + * Specialized version of [visitExprAfterVisitedDefault] for expression with three arguments. + * */ + @Suppress("LongParameterList") + inline fun > visitExprAfterVisitedDefault( + expr: E, + dependency0: KExpr<*>, + dependency1: KExpr<*>, + dependency2: KExpr<*>, + visitDefault: (E) -> KExprVisitResult + ): KExprVisitResult = visitExprAfterVisited(expr, dependency0, dependency1, dependency2) { dr0, dr1, dr2 -> + val defaultRes = visitDefault(expr) + if (defaultRes.dependencyVisitRequired) { + return defaultRes + } + + val dependencyResults = mergeResults(mergeResults(dr0, dr1), dr2) + if (defaultRes.hasResult) { + mergeResults(dependencyResults, defaultRes.result) + } else { + dependencyResults + } + } + + /** + * Specialized version of [visitExprAfterVisitedDefault] for expression with four arguments. + * */ + @Suppress("LongParameterList", "ComplexCondition") + inline fun > visitExprAfterVisitedDefault( + expr: E, + dependency0: KExpr<*>, + dependency1: KExpr<*>, + dependency2: KExpr<*>, + dependency3: KExpr<*>, + visitDefault: (E) -> KExprVisitResult + ): KExprVisitResult = + visitExprAfterVisited(expr, dependency0, dependency1, dependency2, dependency3) { dr0, dr1, dr2, dr3 -> + val defaultRes = visitDefault(expr) + if (defaultRes.dependencyVisitRequired) { + return defaultRes + } + + val dependencyResults = mergeResults(mergeResults(dr0, dr1), mergeResults(dr2, dr3)) + if (defaultRes.hasResult) { + mergeResults(dependencyResults, defaultRes.result) + } else { + dependencyResults + } + } + + /** + * Specialized version of [visitExprAfterVisitedDefault] for expression with five arguments. + * */ + @Suppress("LongParameterList", "ComplexCondition") + inline fun > visitExprAfterVisitedDefault( + expr: E, + d0: KExpr<*>, + d1: KExpr<*>, + d2: KExpr<*>, + d3: KExpr<*>, + d4: KExpr<*>, + visitDefault: (E) -> KExprVisitResult + ): KExprVisitResult = visitExprAfterVisited( + expr, d0, d1, d2, d3, d4 + ) { dr0, dr1, dr2, dr3, dr4 -> + val defaultRes = visitDefault(expr) + if (defaultRes.dependencyVisitRequired) { + return defaultRes + } + + val dependencyResults = mergeResults( + mergeResults(mergeResults(dr0, dr1), mergeResults(dr2, dr3)), + dr4 + ) + if (defaultRes.hasResult) { + mergeResults(dependencyResults, defaultRes.result) + } else { + dependencyResults + } + } +} 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 new file mode 100644 index 000000000..4e453bfc3 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitorBase.kt @@ -0,0 +1,371 @@ +package io.ksmt.expr.transformer + +import io.ksmt.expr.KApp +import io.ksmt.expr.KArray2Lambda +import io.ksmt.expr.KArray3Lambda +import io.ksmt.expr.KArrayLambda +import io.ksmt.expr.KArrayNLambda +import io.ksmt.expr.KExistentialQuantifier +import io.ksmt.expr.KExpr +import io.ksmt.expr.KUniversalQuantifier +import io.ksmt.sort.KSort +import java.util.IdentityHashMap + +/** + * Non-recursive expression visitor. + * + * Standard use-case: perform bottom-up expression visit. + * In this scenario, we need to visit expression arguments first, + * and then perform visit of the expression using + * the arguments visit result. + * For this scenario, non-recursive visitor provides + * a [visitExprAfterVisited] method. + * */ +abstract class KNonRecursiveVisitorBase : KVisitor> { + private val visitResults = IdentityHashMap, V>() + private val exprStack = ArrayList>() + + private var lastVisitedExpr: KExpr<*>? = null + private var lastVisitResult: KExprVisitResult = KExprVisitResult.EMPTY + + /** + * Visit [expr] and all it sub-expressions non-recursively. + * */ + fun applyVisitor(expr: KExpr): V { + apply(expr) + return result(expr) + } + + override fun > exprVisitResult(expr: E, result: KExprVisitResult) { + lastVisitedExpr = expr + lastVisitResult = result + } + + fun resetLastVisitResult() { + lastVisitedExpr = null + lastVisitResult = KExprVisitResult.EMPTY + } + + fun lastVisitResult(expr: KExpr<*>): KExprVisitResult { + check(lastVisitResult.isNotEmpty && expr === lastVisitedExpr) { + "Expression $expr was not properly visited" + } + return lastVisitResult + } + + fun > saveVisitResult(expr: E, result: V): KExprVisitResult { + val wrappedResult = KExprVisitResult(result) + exprVisitResult(expr, wrappedResult) + return wrappedResult + } + + /** + * Get [expr] visit result. + * Returns null if expression was not visited. + * */ + fun visitResult(expr: KExpr): V? = + visitResults[expr] + + fun result(expr: KExpr): V = + visitResult(expr) ?: error("Expr $expr was not properly visited") + + override fun apply(expr: KExpr): KExpr { + val initialStackSize = exprStack.size + try { + exprStack.add(expr) + while (exprStack.size > initialStackSize) { + val e = exprStack.removeLast() + + val cached = visitResult(e) + if (cached != null) { + continue + } + + resetLastVisitResult() + e.accept(this) + val result = lastVisitResult(e) + + if (result.hasResult) { + visitResults[e] = result.result + } + } + } finally { + resetLastVisitResult() + // cleanup stack after exceptions + while (exprStack.size > initialStackSize) { + exprStack.removeLast() + } + } + + return expr + } + + /** + * Disable [KVisitor] visitApp implementation since it is incorrect + * for non-recursive usage. + * */ + abstract override fun visitApp(expr: KApp): KExprVisitResult + + /** + * Disable [KVisitor] visit KArrayLambda implementation since it is incorrect + * for non-recursive usage. + * */ + abstract override fun visit(expr: KArrayLambda): KExprVisitResult + + /** + * Disable [KVisitor] visit KArray2Lambda implementation since it is incorrect + * for non-recursive usage. + * */ + abstract override fun visit( + expr: KArray2Lambda + ): KExprVisitResult + + /** + * Disable [KVisitor] visit KArray3Lambda implementation since it is incorrect + * for non-recursive usage. + * */ + abstract override fun visit( + expr: KArray3Lambda + ): KExprVisitResult + + /** + * Disable [KVisitor] visit KArrayNLambda implementation since it is incorrect + * for non-recursive usage. + * */ + abstract override fun visit(expr: KArrayNLambda): KExprVisitResult + + /** + * Disable [KVisitor] visit KExistentialQuantifier implementation since it is incorrect + * for non-recursive usage. + * */ + abstract override fun visit(expr: KExistentialQuantifier): KExprVisitResult + + /** + * Disable [KVisitor] visit KUniversalQuantifier implementation since it is incorrect + * for non-recursive usage. + * */ + abstract override fun visit(expr: KUniversalQuantifier): KExprVisitResult + + /** + * Visit [this] expression after [dependencies] expressions + * */ + fun KExpr<*>.visitAfter(dependencies: List>) { + exprStack += this + exprStack += dependencies + } + + fun KExpr<*>.visitAfter(dependency: KExpr<*>) { + exprStack += this + exprStack += dependency + } + + fun retryExprVisit(expr: KExpr<*>) { + exprStack += expr + } + + fun visitExprDependencyIfNeeded(dependency: KExpr<*>, dependencyResult: V?) { + if (dependencyResult == null) { + exprStack += dependency + } + } + + /** + * Visit [expr] only if all it sub-expressions + * [dependencies] were already visited. + * Otherwise, register [expr] for visit after [dependencies]. + * */ + inline fun > visitExprAfterVisited( + expr: E, + dependencies: List>, + visitor: (List) -> V + ): KExprVisitResult { + val dependenciesResults = ArrayList(dependencies.size) + var hasNonVisitedDependencies = false + + for (dependency in dependencies) { + val dependencyResult = visitResult(dependency) + + if (dependencyResult != null) { + dependenciesResults += dependencyResult + continue + } + + if (!hasNonVisitedDependencies) { + hasNonVisitedDependencies = true + retryExprVisit(expr) + } + visitExprDependencyIfNeeded(dependency, dependencyResult) + } + + if (hasNonVisitedDependencies) { + return KExprVisitResult.VISIT_DEPENDENCY + } + + val result = visitor(dependenciesResults) + return saveVisitResult(expr, result) + } + + /** + * Specialized version of [visitExprAfterVisited] for expression with single argument. + * */ + inline fun > visitExprAfterVisited( + expr: E, + dependency: KExpr<*>, + visitor: (V) -> V + ): KExprVisitResult { + val dependencyResult = visitResult(dependency) + + if (dependencyResult == null) { + expr.visitAfter(dependency) + + return KExprVisitResult.VISIT_DEPENDENCY + } + + val result = visitor(dependencyResult) + return saveVisitResult(expr, result) + } + + /** + * Specialized version of [visitExprAfterVisited] for expression with two arguments. + * */ + inline fun > visitExprAfterVisited( + expr: E, + dependency0: KExpr<*>, + dependency1: KExpr<*>, + visitor: (V, V) -> V + ): KExprVisitResult { + val dependency0Result = visitResult(dependency0) + val dependency1Result = visitResult(dependency1) + + if (dependency0Result == null || dependency1Result == null) { + retryExprVisit(expr) + + visitExprDependencyIfNeeded(dependency0, dependency0Result) + visitExprDependencyIfNeeded(dependency1, dependency1Result) + + return KExprVisitResult.VISIT_DEPENDENCY + } + + val result = visitor(dependency0Result, dependency1Result) + return saveVisitResult(expr, result) + } + + /** + * Specialized version of [visitExprAfterVisited] for expression with three arguments. + * */ + inline fun > visitExprAfterVisited( + expr: E, + dependency0: KExpr<*>, + dependency1: KExpr<*>, + dependency2: KExpr<*>, + visitor: (V, V, V) -> V + ): KExprVisitResult { + val dependency0Result = visitResult(dependency0) + val dependency1Result = visitResult(dependency1) + val dependency2Result = visitResult(dependency2) + + if (dependency0Result == null || dependency1Result == null || dependency2Result == null) { + retryExprVisit(expr) + + visitExprDependencyIfNeeded(dependency0, dependency0Result) + visitExprDependencyIfNeeded(dependency1, dependency1Result) + visitExprDependencyIfNeeded(dependency2, dependency2Result) + + return KExprVisitResult.VISIT_DEPENDENCY + } + + val result = visitor(dependency0Result, dependency1Result, dependency2Result) + return saveVisitResult(expr, result) + } + + /** + * Specialized version of [visitExprAfterVisited] for expression with four arguments. + * */ + @Suppress("LongParameterList", "ComplexCondition") + inline fun > visitExprAfterVisited( + expr: E, + dependency0: KExpr<*>, + dependency1: KExpr<*>, + dependency2: KExpr<*>, + dependency3: KExpr<*>, + visitor: (V, V, V, V) -> V + ): KExprVisitResult { + val d0r = visitResult(dependency0) + val d1r = visitResult(dependency1) + val d2r = visitResult(dependency2) + val d3r = visitResult(dependency3) + + if (d0r == null || d1r == null || d2r == null || d3r == null) { + retryExprVisit(expr) + + visitExprDependencyIfNeeded(dependency0, d0r) + visitExprDependencyIfNeeded(dependency1, d1r) + visitExprDependencyIfNeeded(dependency2, d2r) + visitExprDependencyIfNeeded(dependency3, d3r) + + return KExprVisitResult.VISIT_DEPENDENCY + } + + val result = visitor(d0r, d1r, d2r, d3r) + return saveVisitResult(expr, result) + } + + /** + * Specialized version of [visitExprAfterVisited] for expression with five arguments. + * */ + @Suppress("LongParameterList", "ComplexCondition") + inline fun > visitExprAfterVisited( + expr: E, + dependency0: KExpr<*>, + dependency1: KExpr<*>, + dependency2: KExpr<*>, + dependency3: KExpr<*>, + dependency4: KExpr<*>, + visitor: (V, V, V, V, V) -> V + ): KExprVisitResult { + val d0r = visitResult(dependency0) + val d1r = visitResult(dependency1) + val d2r = visitResult(dependency2) + val d3r = visitResult(dependency3) + val d4r = visitResult(dependency4) + + if (d0r == null || d1r == null || d2r == null || d3r == null || d4r == null) { + retryExprVisit(expr) + + visitExprDependencyIfNeeded(dependency0, d0r) + visitExprDependencyIfNeeded(dependency1, d1r) + visitExprDependencyIfNeeded(dependency2, d2r) + visitExprDependencyIfNeeded(dependency3, d3r) + visitExprDependencyIfNeeded(dependency4, d4r) + + return KExprVisitResult.VISIT_DEPENDENCY + } + + val result = visitor(d0r, d1r, d2r, d3r, d4r) + return saveVisitResult(expr, result) + } +} + +@JvmInline +value class KExprVisitResult internal constructor(private val value: Any?) { + val isNotEmpty: Boolean + get() = value !== empty + + val dependencyVisitRequired: Boolean + get() = value === visitDependency + + val hasResult: Boolean + get() = value !== empty && value !== visitDependency + + @Suppress("UNCHECKED_CAST") + val result: V + get() = value as? V ?: error("expr is not visited") + + companion object { + private val empty = Any() + private val visitDependency = Any() + + val EMPTY = KExprVisitResult(empty) + val VISIT_DEPENDENCY = KExprVisitResult(visitDependency) + } +} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KVisitor.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KVisitor.kt new file mode 100644 index 000000000..3f114a9e1 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KVisitor.kt @@ -0,0 +1,635 @@ +package io.ksmt.expr.transformer + +import io.ksmt.expr.KAddArithExpr +import io.ksmt.expr.KAndBinaryExpr +import io.ksmt.expr.KAndExpr +import io.ksmt.expr.KApp +import io.ksmt.expr.KArray2Lambda +import io.ksmt.expr.KArray2Select +import io.ksmt.expr.KArray2Store +import io.ksmt.expr.KArray3Lambda +import io.ksmt.expr.KArray3Select +import io.ksmt.expr.KArray3Store +import io.ksmt.expr.KArrayConst +import io.ksmt.expr.KArrayLambda +import io.ksmt.expr.KArrayLambdaBase +import io.ksmt.expr.KArrayNLambda +import io.ksmt.expr.KArrayNSelect +import io.ksmt.expr.KArrayNStore +import io.ksmt.expr.KArraySelect +import io.ksmt.expr.KArraySelectBase +import io.ksmt.expr.KArrayStore +import io.ksmt.expr.KArrayStoreBase +import io.ksmt.expr.KBitVec16Value +import io.ksmt.expr.KBitVec1Value +import io.ksmt.expr.KBitVec32Value +import io.ksmt.expr.KBitVec64Value +import io.ksmt.expr.KBitVec8Value +import io.ksmt.expr.KBitVecCustomValue +import io.ksmt.expr.KBitVecValue +import io.ksmt.expr.KBv2IntExpr +import io.ksmt.expr.KBvAddExpr +import io.ksmt.expr.KBvAddNoOverflowExpr +import io.ksmt.expr.KBvAddNoUnderflowExpr +import io.ksmt.expr.KBvAndExpr +import io.ksmt.expr.KBvArithShiftRightExpr +import io.ksmt.expr.KBvConcatExpr +import io.ksmt.expr.KBvDivNoOverflowExpr +import io.ksmt.expr.KBvExtractExpr +import io.ksmt.expr.KBvLogicalShiftRightExpr +import io.ksmt.expr.KBvMulExpr +import io.ksmt.expr.KBvMulNoOverflowExpr +import io.ksmt.expr.KBvMulNoUnderflowExpr +import io.ksmt.expr.KBvNAndExpr +import io.ksmt.expr.KBvNegNoOverflowExpr +import io.ksmt.expr.KBvNegationExpr +import io.ksmt.expr.KBvNorExpr +import io.ksmt.expr.KBvNotExpr +import io.ksmt.expr.KBvOrExpr +import io.ksmt.expr.KBvReductionAndExpr +import io.ksmt.expr.KBvReductionOrExpr +import io.ksmt.expr.KBvRepeatExpr +import io.ksmt.expr.KBvRotateLeftExpr +import io.ksmt.expr.KBvRotateLeftIndexedExpr +import io.ksmt.expr.KBvRotateRightExpr +import io.ksmt.expr.KBvRotateRightIndexedExpr +import io.ksmt.expr.KBvShiftLeftExpr +import io.ksmt.expr.KBvSignExtensionExpr +import io.ksmt.expr.KBvSignedDivExpr +import io.ksmt.expr.KBvSignedGreaterExpr +import io.ksmt.expr.KBvSignedGreaterOrEqualExpr +import io.ksmt.expr.KBvSignedLessExpr +import io.ksmt.expr.KBvSignedLessOrEqualExpr +import io.ksmt.expr.KBvSignedModExpr +import io.ksmt.expr.KBvSignedRemExpr +import io.ksmt.expr.KBvSubExpr +import io.ksmt.expr.KBvSubNoOverflowExpr +import io.ksmt.expr.KBvSubNoUnderflowExpr +import io.ksmt.expr.KBvToFpExpr +import io.ksmt.expr.KBvUnsignedDivExpr +import io.ksmt.expr.KBvUnsignedGreaterExpr +import io.ksmt.expr.KBvUnsignedGreaterOrEqualExpr +import io.ksmt.expr.KBvUnsignedLessExpr +import io.ksmt.expr.KBvUnsignedLessOrEqualExpr +import io.ksmt.expr.KBvUnsignedRemExpr +import io.ksmt.expr.KBvXNorExpr +import io.ksmt.expr.KBvXorExpr +import io.ksmt.expr.KBvZeroExtensionExpr +import io.ksmt.expr.KConst +import io.ksmt.expr.KDistinctExpr +import io.ksmt.expr.KDivArithExpr +import io.ksmt.expr.KEqExpr +import io.ksmt.expr.KExistentialQuantifier +import io.ksmt.expr.KExpr +import io.ksmt.expr.KFalse +import io.ksmt.expr.KFp128Value +import io.ksmt.expr.KFp16Value +import io.ksmt.expr.KFp32Value +import io.ksmt.expr.KFp64Value +import io.ksmt.expr.KFpAbsExpr +import io.ksmt.expr.KFpAddExpr +import io.ksmt.expr.KFpCustomSizeValue +import io.ksmt.expr.KFpDivExpr +import io.ksmt.expr.KFpEqualExpr +import io.ksmt.expr.KFpFromBvExpr +import io.ksmt.expr.KFpFusedMulAddExpr +import io.ksmt.expr.KFpGreaterExpr +import io.ksmt.expr.KFpGreaterOrEqualExpr +import io.ksmt.expr.KFpIsInfiniteExpr +import io.ksmt.expr.KFpIsNaNExpr +import io.ksmt.expr.KFpIsNegativeExpr +import io.ksmt.expr.KFpIsNormalExpr +import io.ksmt.expr.KFpIsPositiveExpr +import io.ksmt.expr.KFpIsSubnormalExpr +import io.ksmt.expr.KFpIsZeroExpr +import io.ksmt.expr.KFpLessExpr +import io.ksmt.expr.KFpLessOrEqualExpr +import io.ksmt.expr.KFpMaxExpr +import io.ksmt.expr.KFpMinExpr +import io.ksmt.expr.KFpMulExpr +import io.ksmt.expr.KFpNegationExpr +import io.ksmt.expr.KFpRemExpr +import io.ksmt.expr.KFpRoundToIntegralExpr +import io.ksmt.expr.KFpRoundingModeExpr +import io.ksmt.expr.KFpSqrtExpr +import io.ksmt.expr.KFpSubExpr +import io.ksmt.expr.KFpToBvExpr +import io.ksmt.expr.KFpToFpExpr +import io.ksmt.expr.KFpToIEEEBvExpr +import io.ksmt.expr.KFpToRealExpr +import io.ksmt.expr.KFpValue +import io.ksmt.expr.KFunctionApp +import io.ksmt.expr.KFunctionAsArray +import io.ksmt.expr.KGeArithExpr +import io.ksmt.expr.KGtArithExpr +import io.ksmt.expr.KImpliesExpr +import io.ksmt.expr.KInt32NumExpr +import io.ksmt.expr.KInt64NumExpr +import io.ksmt.expr.KIntBigNumExpr +import io.ksmt.expr.KIntNumExpr +import io.ksmt.expr.KInterpretedValue +import io.ksmt.expr.KIsIntRealExpr +import io.ksmt.expr.KIteExpr +import io.ksmt.expr.KLeArithExpr +import io.ksmt.expr.KLtArithExpr +import io.ksmt.expr.KModIntExpr +import io.ksmt.expr.KMulArithExpr +import io.ksmt.expr.KNotExpr +import io.ksmt.expr.KOrBinaryExpr +import io.ksmt.expr.KOrExpr +import io.ksmt.expr.KPowerArithExpr +import io.ksmt.expr.KRealNumExpr +import io.ksmt.expr.KRealToFpExpr +import io.ksmt.expr.KRemIntExpr +import io.ksmt.expr.KSubArithExpr +import io.ksmt.expr.KToIntRealExpr +import io.ksmt.expr.KToRealIntExpr +import io.ksmt.expr.KTrue +import io.ksmt.expr.KUnaryMinusArithExpr +import io.ksmt.expr.KUninterpretedSortValue +import io.ksmt.expr.KUniversalQuantifier +import io.ksmt.expr.KXorExpr +import io.ksmt.sort.KArithSort +import io.ksmt.sort.KArray2Sort +import io.ksmt.sort.KArray3Sort +import io.ksmt.sort.KArrayNSort +import io.ksmt.sort.KArraySort +import io.ksmt.sort.KArraySortBase +import io.ksmt.sort.KBoolSort +import io.ksmt.sort.KBv16Sort +import io.ksmt.sort.KBv1Sort +import io.ksmt.sort.KBv32Sort +import io.ksmt.sort.KBv64Sort +import io.ksmt.sort.KBv8Sort +import io.ksmt.sort.KBvSort +import io.ksmt.sort.KFp128Sort +import io.ksmt.sort.KFp16Sort +import io.ksmt.sort.KFp32Sort +import io.ksmt.sort.KFp64Sort +import io.ksmt.sort.KFpRoundingModeSort +import io.ksmt.sort.KFpSort +import io.ksmt.sort.KIntSort +import io.ksmt.sort.KRealSort +import io.ksmt.sort.KSort +import io.ksmt.sort.KUninterpretedSort + + +interface KVisitor : KTransformer { + fun > exprVisitResult(expr: E, result: V): Unit {} + + fun visitExpr(expr: KExpr): V + + override fun transformExpr(expr: KExpr): KExpr = visitExpr(expr, ::visitExpr) + + // function visitors + fun visitApp(expr: KApp): V = visitExpr(expr) + fun visit(expr: KFunctionApp): V = visitApp(expr) + fun visit(expr: KConst): V = visit(expr as KFunctionApp) + fun visitValue(expr: KInterpretedValue): V = visitApp(expr) + + override fun transformApp(expr: KApp): KExpr = visitExpr(expr, ::visitApp) + override fun transform(expr: KFunctionApp): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KConst): KExpr = visitExpr(expr, ::visit) + override fun transformValue(expr: KInterpretedValue): KExpr = visitExpr(expr, ::visitValue) + + // bool visitors + fun visit(expr: KAndExpr): V = visitApp(expr) + fun visit(expr: KAndBinaryExpr): V = visit(expr as KAndExpr) + fun visit(expr: KOrExpr): V = visitApp(expr) + fun visit(expr: KOrBinaryExpr): V = visit(expr as KOrExpr) + fun visit(expr: KNotExpr): V = visitApp(expr) + fun visit(expr: KImpliesExpr): V = visitApp(expr) + fun visit(expr: KXorExpr): V = visitApp(expr) + fun visit(expr: KTrue): V = visitValue(expr) + fun visit(expr: KFalse): V = visitValue(expr) + fun visit(expr: KEqExpr): V = visitApp(expr) + fun visit(expr: KDistinctExpr): V = visitApp(expr) + fun visit(expr: KIteExpr): V = visitApp(expr) + + override fun transform(expr: KAndExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KAndBinaryExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KOrExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KOrBinaryExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KNotExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KImpliesExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KXorExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KTrue): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFalse): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KEqExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KDistinctExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KIteExpr): KExpr = visitExpr(expr, ::visit) + + // bit-vec visitors + fun visitBitVecValue(expr: KBitVecValue): V = visitValue(expr) + fun visit(expr: KBitVec1Value): V = visitBitVecValue(expr) + fun visit(expr: KBitVec8Value): V = visitBitVecValue(expr) + fun visit(expr: KBitVec16Value): V = visitBitVecValue(expr) + fun visit(expr: KBitVec32Value): V = visitBitVecValue(expr) + fun visit(expr: KBitVec64Value): V = visitBitVecValue(expr) + fun visit(expr: KBitVecCustomValue): V = visitBitVecValue(expr) + + override fun transformBitVecValue(expr: KBitVecValue): KExpr = + visitExpr(expr, ::visitBitVecValue) + + override fun transform(expr: KBitVec1Value): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBitVec8Value): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBitVec16Value): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBitVec32Value): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBitVec64Value): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBitVecCustomValue): KExpr = visitExpr(expr, ::visit) + + // bit-vec expressions visitors + fun visit(expr: KBvNotExpr): V = visitApp(expr) + fun visit(expr: KBvReductionAndExpr): V = visitApp(expr) + fun visit(expr: KBvReductionOrExpr): V = visitApp(expr) + fun visit(expr: KBvAndExpr): V = visitApp(expr) + fun visit(expr: KBvOrExpr): V = visitApp(expr) + fun visit(expr: KBvXorExpr): V = visitApp(expr) + fun visit(expr: KBvNAndExpr): V = visitApp(expr) + fun visit(expr: KBvNorExpr): V = visitApp(expr) + fun visit(expr: KBvXNorExpr): V = visitApp(expr) + fun visit(expr: KBvNegationExpr): V = visitApp(expr) + fun visit(expr: KBvAddExpr): V = visitApp(expr) + fun visit(expr: KBvSubExpr): V = visitApp(expr) + fun visit(expr: KBvMulExpr): V = visitApp(expr) + fun visit(expr: KBvUnsignedDivExpr): V = visitApp(expr) + fun visit(expr: KBvSignedDivExpr): V = visitApp(expr) + fun visit(expr: KBvUnsignedRemExpr): V = visitApp(expr) + fun visit(expr: KBvSignedRemExpr): V = visitApp(expr) + fun visit(expr: KBvSignedModExpr): V = visitApp(expr) + fun visit(expr: KBvUnsignedLessExpr): V = visitApp(expr) + fun visit(expr: KBvSignedLessExpr): V = visitApp(expr) + fun visit(expr: KBvUnsignedLessOrEqualExpr): V = visitApp(expr) + fun visit(expr: KBvSignedLessOrEqualExpr): V = visitApp(expr) + fun visit(expr: KBvUnsignedGreaterOrEqualExpr): V = visitApp(expr) + fun visit(expr: KBvSignedGreaterOrEqualExpr): V = visitApp(expr) + fun visit(expr: KBvUnsignedGreaterExpr): V = visitApp(expr) + fun visit(expr: KBvSignedGreaterExpr): V = visitApp(expr) + fun visit(expr: KBvConcatExpr): V = visitApp(expr) + fun visit(expr: KBvExtractExpr): V = visitApp(expr) + fun visit(expr: KBvSignExtensionExpr): V = visitApp(expr) + fun visit(expr: KBvZeroExtensionExpr): V = visitApp(expr) + fun visit(expr: KBvRepeatExpr): V = visitApp(expr) + fun visit(expr: KBvShiftLeftExpr): V = visitApp(expr) + fun visit(expr: KBvLogicalShiftRightExpr): V = visitApp(expr) + fun visit(expr: KBvArithShiftRightExpr): V = visitApp(expr) + fun visit(expr: KBvRotateLeftExpr): V = visitApp(expr) + fun visit(expr: KBvRotateLeftIndexedExpr): V = visitApp(expr) + fun visit(expr: KBvRotateRightExpr): V = visitApp(expr) + fun visit(expr: KBvRotateRightIndexedExpr): V = visitApp(expr) + fun visit(expr: KBv2IntExpr): V = visitApp(expr) + fun visit(expr: KBvAddNoOverflowExpr): V = visitApp(expr) + fun visit(expr: KBvAddNoUnderflowExpr): V = visitApp(expr) + fun visit(expr: KBvSubNoOverflowExpr): V = visitApp(expr) + fun visit(expr: KBvSubNoUnderflowExpr): V = visitApp(expr) + fun visit(expr: KBvDivNoOverflowExpr): V = visitApp(expr) + fun visit(expr: KBvNegNoOverflowExpr): V = visitApp(expr) + fun visit(expr: KBvMulNoOverflowExpr): V = visitApp(expr) + fun visit(expr: KBvMulNoUnderflowExpr): V = visitApp(expr) + + override fun transform(expr: KBvNotExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvReductionAndExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvReductionOrExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvAndExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvOrExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvXorExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvNAndExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvNorExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvXNorExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvNegationExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvAddExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvSubExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvMulExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvUnsignedDivExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvSignedDivExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvUnsignedRemExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvSignedRemExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvSignedModExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvUnsignedLessExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvSignedLessExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvUnsignedLessOrEqualExpr): KExpr = visitExpr( + expr, + ::visit + ) + + override fun transform(expr: KBvSignedLessOrEqualExpr): KExpr = visitExpr( + expr, + ::visit + ) + + override fun transform(expr: KBvUnsignedGreaterOrEqualExpr): KExpr = + visitExpr(expr, ::visit) + + override fun transform(expr: KBvSignedGreaterOrEqualExpr): KExpr = visitExpr( + expr, + ::visit + ) + + override fun transform(expr: KBvUnsignedGreaterExpr): KExpr = visitExpr( + expr, + ::visit + ) + + override fun transform(expr: KBvSignedGreaterExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvConcatExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvExtractExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvSignExtensionExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvZeroExtensionExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvRepeatExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvShiftLeftExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvLogicalShiftRightExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvArithShiftRightExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvRotateLeftExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvRotateLeftIndexedExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvRotateRightExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvRotateRightIndexedExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBv2IntExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvAddNoOverflowExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvAddNoUnderflowExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvSubNoOverflowExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvSubNoUnderflowExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvDivNoOverflowExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvNegNoOverflowExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvMulNoOverflowExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvMulNoUnderflowExpr): KExpr = visitExpr(expr, ::visit) + + // fp value visitors + fun visitFpValue(expr: KFpValue): V = visitValue(expr) + fun visit(expr: KFp16Value): V = visitFpValue(expr) + fun visit(expr: KFp32Value): V = visitFpValue(expr) + fun visit(expr: KFp64Value): V = visitFpValue(expr) + fun visit(expr: KFp128Value): V = visitFpValue(expr) + fun visit(expr: KFpCustomSizeValue): V = visitFpValue(expr) + + override fun transformFpValue(expr: KFpValue): KExpr = + visitExpr(expr, ::visitFpValue) + + override fun transform(expr: KFp16Value): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFp32Value): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFp64Value): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFp128Value): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpCustomSizeValue): KExpr = visitExpr(expr, ::visit) + + // fp rounding mode + fun visit(expr: KFpRoundingModeExpr): V = visitValue(expr) + + override fun transform(expr: KFpRoundingModeExpr): KExpr = + visitExpr(expr, ::visit) + + // fp operations visit + fun visit(expr: KFpAbsExpr): V = visitApp(expr) + fun visit(expr: KFpNegationExpr): V = visitApp(expr) + fun visit(expr: KFpAddExpr): V = visitApp(expr) + fun visit(expr: KFpSubExpr): V = visitApp(expr) + fun visit(expr: KFpMulExpr): V = visitApp(expr) + fun visit(expr: KFpDivExpr): V = visitApp(expr) + fun visit(expr: KFpFusedMulAddExpr): V = visitApp(expr) + fun visit(expr: KFpSqrtExpr): V = visitApp(expr) + fun visit(expr: KFpRemExpr): V = visitApp(expr) + + fun visit(expr: KFpRoundToIntegralExpr): V = visitApp(expr) + fun visit(expr: KFpMinExpr): V = visitApp(expr) + fun visit(expr: KFpMaxExpr): V = visitApp(expr) + fun visit(expr: KFpLessOrEqualExpr): V = visitApp(expr) + fun visit(expr: KFpLessExpr): V = visitApp(expr) + fun visit(expr: KFpGreaterOrEqualExpr): V = visitApp(expr) + fun visit(expr: KFpGreaterExpr): V = visitApp(expr) + fun visit(expr: KFpEqualExpr): V = visitApp(expr) + fun visit(expr: KFpIsNormalExpr): V = visitApp(expr) + fun visit(expr: KFpIsSubnormalExpr): V = visitApp(expr) + fun visit(expr: KFpIsZeroExpr): V = visitApp(expr) + fun visit(expr: KFpIsInfiniteExpr): V = visitApp(expr) + fun visit(expr: KFpIsNaNExpr): V = visitApp(expr) + fun visit(expr: KFpIsNegativeExpr): V = visitApp(expr) + fun visit(expr: KFpIsPositiveExpr): V = visitApp(expr) + fun visit(expr: KFpToBvExpr): V = visitApp(expr) + fun visit(expr: KFpToRealExpr): V = visitApp(expr) + fun visit(expr: KFpToIEEEBvExpr): V = visitApp(expr) + fun visit(expr: KFpFromBvExpr): V = visitApp(expr) + fun visit(expr: KFpToFpExpr): V = visitApp(expr) + fun visit(expr: KRealToFpExpr): V = visitApp(expr) + fun visit(expr: KBvToFpExpr): V = visitApp(expr) + + override fun transform(expr: KFpAbsExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpNegationExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpAddExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpSubExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpMulExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpDivExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpFusedMulAddExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpSqrtExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpRemExpr): KExpr = visitExpr(expr, ::visit) + + override fun transform(expr: KFpRoundToIntegralExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpMinExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpMaxExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpLessOrEqualExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpLessExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpGreaterOrEqualExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpGreaterExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpEqualExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpIsNormalExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpIsSubnormalExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpIsZeroExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpIsInfiniteExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpIsNaNExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpIsNegativeExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpIsPositiveExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpToBvExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpToRealExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpToIEEEBvExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpFromBvExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KFpToFpExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRealToFpExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KBvToFpExpr): KExpr = visitExpr(expr, ::visit) + + // array visitors + fun , R : KSort> visitArrayStore(expr: KArrayStoreBase): V = + visitApp(expr) + + fun visit(expr: KArrayStore): V = + visitArrayStore(expr) + + fun visit(expr: KArray2Store): V = + visitArrayStore(expr) + + fun visit(expr: KArray3Store): V = + visitArrayStore(expr) + + fun visit(expr: KArrayNStore): V = + visitArrayStore(expr) + + fun , R : KSort> visitArraySelect(expr: KArraySelectBase): V = + visitApp(expr) + + fun visit(expr: KArraySelect): V = + visitArraySelect(expr) + + fun visit(expr: KArray2Select): V = + visitArraySelect(expr) + + fun visit(expr: KArray3Select): V = + visitArraySelect(expr) + + fun visit(expr: KArrayNSelect): V = + visitArraySelect(expr) + + fun , R : KSort> visit(expr: KArrayConst): V = + visitApp(expr) + + fun , R : KSort> visit(expr: KFunctionAsArray): V = + visitExpr(expr) + + fun , R : KSort> visitArrayLambda(expr: KArrayLambdaBase): V = + visitExpr(expr) + + fun visit(expr: KArrayLambda): V = + visitArrayLambda(expr) + + fun visit(expr: KArray2Lambda): V = + visitArrayLambda(expr) + + fun visit(expr: KArray3Lambda): V = + visitArrayLambda(expr) + + fun visit(expr: KArrayNLambda): V = + visitArrayLambda(expr) + + override fun , R : KSort> transformArrayStore( + expr: KArrayStoreBase + ): KExpr = visitExpr(expr, ::visitArrayStore) + + override fun transform( + expr: KArrayStore + ): KExpr> = visitExpr(expr, ::visit) + + override fun transform( + expr: KArray2Store + ): KExpr> = visitExpr(expr, ::visit) + + override fun transform( + expr: KArray3Store + ): KExpr> = visitExpr(expr, ::visit) + + override fun transform( + expr: KArrayNStore + ): KExpr> = visitExpr(expr, ::visit) + + override fun , R : KSort> transformArraySelect( + expr: KArraySelectBase + ): KExpr = visitExpr(expr, ::visitArraySelect) + + override fun transform( + expr: KArraySelect + ): KExpr = visitExpr(expr, ::visit) + + override fun transform( + expr: KArray2Select + ): KExpr = visitExpr(expr, ::visit) + + override fun transform( + expr: KArray3Select + ): KExpr = visitExpr(expr, ::visit) + + override fun transform( + expr: KArrayNSelect + ): KExpr = visitExpr(expr, ::visit) + + override fun , R : KSort> transform( + expr: KArrayConst + ): KExpr = visitExpr(expr, ::visit) + + override fun , R : KSort> transform( + expr: KFunctionAsArray + ): KExpr = visitExpr(expr, ::visit) + + override fun , R : KSort> transformArrayLambda( + expr: KArrayLambdaBase + ): KExpr = visitExpr(expr, ::visitArrayLambda) + + override fun transform( + expr: KArrayLambda + ): KExpr> = visitExpr(expr, ::visit) + + override fun transform( + expr: KArray2Lambda + ): KExpr> = visitExpr(expr, ::visit) + + override fun transform( + expr: KArray3Lambda + ): KExpr> = visitExpr(expr, ::visit) + + override fun transform( + expr: KArrayNLambda + ): KExpr> = visitExpr(expr, ::visit) + + // arith visitors + fun visit(expr: KAddArithExpr): V = visitApp(expr) + fun visit(expr: KMulArithExpr): V = visitApp(expr) + fun visit(expr: KSubArithExpr): V = visitApp(expr) + fun visit(expr: KUnaryMinusArithExpr): V = visitApp(expr) + fun visit(expr: KDivArithExpr): V = visitApp(expr) + fun visit(expr: KPowerArithExpr): V = visitApp(expr) + fun visit(expr: KLtArithExpr): V = visitApp(expr) + fun visit(expr: KLeArithExpr): V = visitApp(expr) + fun visit(expr: KGtArithExpr): V = visitApp(expr) + fun visit(expr: KGeArithExpr): V = visitApp(expr) + + override fun transform(expr: KAddArithExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KMulArithExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KSubArithExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KUnaryMinusArithExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KDivArithExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KPowerArithExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KLtArithExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KLeArithExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KGtArithExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KGeArithExpr): KExpr = visitExpr(expr, ::visit) + + // integer visitors + fun visit(expr: KModIntExpr): V = visitApp(expr) + fun visit(expr: KRemIntExpr): V = visitApp(expr) + fun visit(expr: KToRealIntExpr): V = visitApp(expr) + + override fun transform(expr: KModIntExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRemIntExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KToRealIntExpr): KExpr = visitExpr(expr, ::visit) + + fun visitIntNum(expr: KIntNumExpr): V = visitValue(expr) + fun visit(expr: KInt32NumExpr): V = visitIntNum(expr) + fun visit(expr: KInt64NumExpr): V = visitIntNum(expr) + fun visit(expr: KIntBigNumExpr): V = visitIntNum(expr) + + override fun transformIntNum(expr: KIntNumExpr): KExpr = visitExpr(expr, ::visitIntNum) + override fun transform(expr: KInt32NumExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KInt64NumExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KIntBigNumExpr): KExpr = visitExpr(expr, ::visit) + + // real visitors + fun visit(expr: KToIntRealExpr): V = visitApp(expr) + fun visit(expr: KIsIntRealExpr): V = visitApp(expr) + fun visit(expr: KRealNumExpr): V = visitValue(expr) + + override fun transform(expr: KToIntRealExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KIsIntRealExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRealNumExpr): KExpr = visitExpr(expr, ::visit) + + // quantifier visitors + fun visit(expr: KExistentialQuantifier): V = visitExpr(expr) + fun visit(expr: KUniversalQuantifier): V = visitExpr(expr) + + override fun transform(expr: KExistentialQuantifier): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KUniversalQuantifier): KExpr = visitExpr(expr, ::visit) + + // uninterpreted sort value + fun visit(expr: KUninterpretedSortValue): V = visitValue(expr) + + override fun transform(expr: KUninterpretedSortValue): KExpr = visitExpr(expr, ::visit) + +} + +inline fun > KVisitor.visitExpr(expr: E, visitor: (E) -> V): E { + val result = visitor(expr) + exprVisitResult(expr, result) + return expr +} diff --git a/ksmt-core/src/test/kotlin/io/ksmt/ExpressionVisitorTest.kt b/ksmt-core/src/test/kotlin/io/ksmt/ExpressionVisitorTest.kt new file mode 100644 index 000000000..9fc479c53 --- /dev/null +++ b/ksmt-core/src/test/kotlin/io/ksmt/ExpressionVisitorTest.kt @@ -0,0 +1,100 @@ +package io.ksmt + +import io.ksmt.KContext.SimplificationMode.NO_SIMPLIFY +import io.ksmt.expr.KAndExpr +import io.ksmt.expr.KApp +import io.ksmt.expr.KEqExpr +import io.ksmt.expr.KExpr +import io.ksmt.expr.transformer.KExprVisitResult +import io.ksmt.expr.transformer.KNonRecursiveVisitor +import io.ksmt.sort.KSort +import kotlin.test.Test +import kotlin.test.assertEquals + +class ExpressionVisitorTest { + + @Test + fun testExpressionVisitTrace(): Unit = with(KContext(simplificationMode = NO_SIMPLIFY)) { + val x = mkConst("x", boolSort) + val y = mkConst("y", boolSort) + val e0 = mkAnd(y, y) + val e1 = mkEq(x, x) + val e2 = mkImplies(x, x) + val expr = mkOr(e0, e1, e2) + + val trace = mutableListOf() + val visitor = TracingVisitor(this, trace) + + val leafs = visitor.applyVisitor(expr) + assertEquals(setOf(x, y), leafs.toSet()) + + val expectedTrace = listOf( + VisitEvent(VisitTraceKind.APP, x), + VisitEvent(VisitTraceKind.EXPR, x), + VisitEvent(VisitTraceKind.DEFAULT, x), + + VisitEvent(VisitTraceKind.APP, e2), + VisitEvent(VisitTraceKind.EXPR, e2), + + VisitEvent(VisitTraceKind.EQ_ENTER, e1), + VisitEvent(VisitTraceKind.EQ_VISIT, e1), + + VisitEvent(VisitTraceKind.APP, y), + VisitEvent(VisitTraceKind.EXPR, y), + VisitEvent(VisitTraceKind.DEFAULT, y), + + VisitEvent(VisitTraceKind.APP, e0), + + VisitEvent(VisitTraceKind.APP, expr), + VisitEvent(VisitTraceKind.EXPR, expr), + ) + + assertEquals(expectedTrace, trace) + } + + private class TracingVisitor( + ctx: KContext, + val trace: MutableList + ) : KNonRecursiveVisitor>>(ctx) { + + override fun defaultValue(expr: KExpr): List> { + trace += VisitEvent(VisitTraceKind.DEFAULT, expr) + return listOf(expr) + } + + override fun mergeResults(left: List>, right: List>): List> = + left + right + + override fun visitExpr(expr: KExpr): KExprVisitResult>> { + trace += VisitEvent(VisitTraceKind.EXPR, expr) + return super.visitExpr(expr) + } + + override fun visitApp(expr: KApp): KExprVisitResult>> { + trace += VisitEvent(VisitTraceKind.APP, expr) + return if (expr is KAndExpr) { + val argsRecursive = expr.args.map { + applyVisitor(it) + } + val result = argsRecursive.reduce { res, arg -> res + arg } + saveVisitResult(expr, result) + } else { + super.visitApp(expr) + } + } + + override fun visit(expr: KEqExpr): KExprVisitResult>> { + trace += VisitEvent(VisitTraceKind.EQ_ENTER, expr) + return visitExprAfterVisited(expr, expr.lhs, expr.rhs) { l, r -> + trace += VisitEvent(VisitTraceKind.EQ_VISIT, expr) + l + r + } + } + } + + enum class VisitTraceKind { + EXPR, APP, DEFAULT, EQ_ENTER, EQ_VISIT + } + + data class VisitEvent(val kind: VisitTraceKind, val expr: KExpr<*>) +}