diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt index 5fb618e35..91cd8148f 100644 --- a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt +++ b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt @@ -18,6 +18,7 @@ import io.ksmt.expr.KFunctionAsArray import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.transformer.KNonRecursiveTransformer import io.ksmt.solver.KSolverException +import io.ksmt.solver.KSolverUnsupportedFeatureException import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm @@ -34,6 +35,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -362,6 +365,12 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable { override fun visit(sort: KRealSort) { } + override fun visit(sort: KStringSort) { + } + + override fun visit(sort: KRegexSort) { + } + override fun visit(sort: S) { } diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt index 322d90569..2e8465893 100644 --- a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt +++ b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt @@ -151,6 +151,48 @@ import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoUnderflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoUnderflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvNegNoOverflowExpr @@ -183,6 +225,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -1405,6 +1449,174 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL ) } + override fun transform(expr: KStringConcatExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringLenExpr): KExpr { + throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringToRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringInRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringSuffixOfExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringPrefixOfExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringLtExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringLeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringGtExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringGeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringContainsExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringSingletonSubExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringSubExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringIndexOfExpr): KExpr { + throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringIndexOfRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringReplaceExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringReplaceAllExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringReplaceWithRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringReplaceAllWithRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringToLowerExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringToUpperExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringReverseExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringIsDigitExpr): KExpr { + throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringToCodeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringFromCodeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringToIntExpr): KExpr { + throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringFromIntExpr): KExpr { + throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla") + } + + override fun transform(expr: KStringLiteralExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexConcatExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexUnionExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexIntersectionExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexStarExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexCrossExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexDifferenceExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexComplementExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexOptionExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexRangeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexPowerExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexLoopExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexEpsilon): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexAll): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + + override fun transform(expr: KRegexAllChar): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla") + } + private inline fun T.internalizeQuantifier( crossinline mkQuantifierTerm: (LongArray) -> BitwuzlaTerm ): T { @@ -1554,7 +1766,7 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL } /** - * Bitwuzla doesn't support integers and reals. + * Bitwuzla doesn't support strings, regular expressions, integers and reals. * */ override fun visit(sort: KIntSort) = throw KSolverUnsupportedFeatureException("Unsupported sort $sort") @@ -1562,6 +1774,12 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL override fun visit(sort: KRealSort) = throw KSolverUnsupportedFeatureException("Unsupported sort $sort") + override fun visit(sort: KStringSort) = + throw KSolverUnsupportedFeatureException("Unsupported sort $sort") + + override fun visit(sort: KRegexSort) = + throw KSolverUnsupportedFeatureException("Unsupported sort $sort") + /** * Replace Uninterpreted sorts with (BitVec 32). * The sort universe size is limited by 2^32 values which should be enough. @@ -1704,6 +1922,8 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL override fun visit(sort: KBoolSort): Boolean = false override fun visit(sort: KIntSort): Boolean = false override fun visit(sort: KRealSort): Boolean = false + override fun visit(sort: KStringSort): Boolean = false + override fun visit(sort: KRegexSort): Boolean = false override fun visit(sort: S): Boolean = false override fun visit(sort: S): Boolean = false override fun visit(sort: KFpRoundingModeSort): Boolean = false diff --git a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt index 3b6edfc6e..64f4fe2fb 100644 --- a/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt +++ b/ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt @@ -9,6 +9,7 @@ import io.ksmt.solver.KTheory.LIA import io.ksmt.solver.KTheory.LRA import io.ksmt.solver.KTheory.NIA import io.ksmt.solver.KTheory.NRA +import io.ksmt.solver.KTheory.S import org.ksmt.solver.bitwuzla.bindings.Bitwuzla import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption import org.ksmt.solver.bitwuzla.bindings.Native @@ -52,7 +53,7 @@ class KBitwuzlaSolverConfigurationImpl(private val bitwuzla: Bitwuzla) : KBitwuz override fun optimizeForTheories(theories: Set?, quantifiersAllowed: Boolean) { if (theories.isNullOrEmpty()) return - if (setOf(LIA, LRA, NIA, NRA).intersect(theories).isNotEmpty()) { + if (setOf(LIA, LRA, NIA, NRA, S).intersect(theories).isNotEmpty()) { throw KSolverUnsupportedFeatureException("Unsupported theories $theories") } } diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index 4e49399f9..d91da1743 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt @@ -129,6 +129,48 @@ import io.ksmt.decl.KIntModDecl import io.ksmt.decl.KIntNumDecl import io.ksmt.decl.KIntRemDecl import io.ksmt.decl.KIntToRealDecl +import io.ksmt.decl.KStringLiteralDecl +import io.ksmt.decl.KStringConcatDecl +import io.ksmt.decl.KStringLenDecl +import io.ksmt.decl.KStringToRegexDecl +import io.ksmt.decl.KStringInRegexDecl +import io.ksmt.decl.KStringSuffixOfDecl +import io.ksmt.decl.KStringPrefixOfDecl +import io.ksmt.decl.KStringLtDecl +import io.ksmt.decl.KStringLeDecl +import io.ksmt.decl.KStringGtDecl +import io.ksmt.decl.KStringGeDecl +import io.ksmt.decl.KStringContainsDecl +import io.ksmt.decl.KStringSingletonSubDecl +import io.ksmt.decl.KStringSubDecl +import io.ksmt.decl.KStringIndexOfDecl +import io.ksmt.decl.KStringIndexOfRegexDecl +import io.ksmt.decl.KStringReplaceDecl +import io.ksmt.decl.KStringReplaceAllDecl +import io.ksmt.decl.KStringReplaceWithRegexDecl +import io.ksmt.decl.KStringReplaceAllWithRegexDecl +import io.ksmt.decl.KStringToLowerDecl +import io.ksmt.decl.KStringToUpperDecl +import io.ksmt.decl.KStringReverseDecl +import io.ksmt.decl.KStringIsDigitDecl +import io.ksmt.decl.KStringToCodeDecl +import io.ksmt.decl.KStringFromCodeDecl +import io.ksmt.decl.KStringToIntDecl +import io.ksmt.decl.KStringFromIntDecl +import io.ksmt.decl.KRegexEpsilonDecl +import io.ksmt.decl.KRegexAllDecl +import io.ksmt.decl.KRegexAllCharDecl +import io.ksmt.decl.KRegexConcatDecl +import io.ksmt.decl.KRegexUnionDecl +import io.ksmt.decl.KRegexIntersectionDecl +import io.ksmt.decl.KRegexStarDecl +import io.ksmt.decl.KRegexCrossDecl +import io.ksmt.decl.KRegexDifferenceDecl +import io.ksmt.decl.KRegexComplementDecl +import io.ksmt.decl.KRegexOptionDecl +import io.ksmt.decl.KRegexRangeDecl +import io.ksmt.decl.KRegexPowerDecl +import io.ksmt.decl.KRegexLoopDecl import io.ksmt.decl.KIteDecl import io.ksmt.decl.KNotDecl import io.ksmt.decl.KOrDecl @@ -272,6 +314,48 @@ import io.ksmt.expr.KInt64NumExpr import io.ksmt.expr.KIntBigNumExpr import io.ksmt.expr.KIntNumExpr import io.ksmt.expr.KIsIntRealExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr import io.ksmt.expr.KIteExpr import io.ksmt.expr.KLeArithExpr import io.ksmt.expr.KLtArithExpr @@ -399,6 +483,44 @@ import io.ksmt.expr.rewrite.simplify.simplifyRealIsInt import io.ksmt.expr.rewrite.simplify.simplifyRealToFpExpr import io.ksmt.expr.rewrite.simplify.simplifyRealToInt import io.ksmt.expr.rewrite.simplify.simplifyXor +import io.ksmt.expr.rewrite.simplify.simplifyStringConcat +import io.ksmt.expr.rewrite.simplify.simplifyStringLen +import io.ksmt.expr.rewrite.simplify.simplifyStringToRegex +import io.ksmt.expr.rewrite.simplify.simplifyStringInRegex +import io.ksmt.expr.rewrite.simplify.simplifyStringSuffixOf +import io.ksmt.expr.rewrite.simplify.simplifyStringPrefixOf +import io.ksmt.expr.rewrite.simplify.simplifyStringLt +import io.ksmt.expr.rewrite.simplify.simplifyStringLe +import io.ksmt.expr.rewrite.simplify.simplifyStringGt +import io.ksmt.expr.rewrite.simplify.simplifyStringGe +import io.ksmt.expr.rewrite.simplify.simplifyStringContains +import io.ksmt.expr.rewrite.simplify.simplifyStringSingletonSub +import io.ksmt.expr.rewrite.simplify.simplifyStringSub +import io.ksmt.expr.rewrite.simplify.simplifyStringIndexOf +import io.ksmt.expr.rewrite.simplify.simplifyStringIndexOfRegex +import io.ksmt.expr.rewrite.simplify.simplifyStringReplace +import io.ksmt.expr.rewrite.simplify.simplifyStringReplaceAll +import io.ksmt.expr.rewrite.simplify.simplifyStringReplaceWithRegex +import io.ksmt.expr.rewrite.simplify.simplifyStringReplaceAllWithRegex +import io.ksmt.expr.rewrite.simplify.simplifyStringToLower +import io.ksmt.expr.rewrite.simplify.simplifyStringToUpper +import io.ksmt.expr.rewrite.simplify.simplifyStringReverse +import io.ksmt.expr.rewrite.simplify.simplifyStringIsDigit +import io.ksmt.expr.rewrite.simplify.simplifyStringToCode +import io.ksmt.expr.rewrite.simplify.simplifyStringFromCode +import io.ksmt.expr.rewrite.simplify.simplifyStringToInt +import io.ksmt.expr.rewrite.simplify.simplifyStringFromInt +import io.ksmt.expr.rewrite.simplify.simplifyRegexConcat +import io.ksmt.expr.rewrite.simplify.simplifyRegexUnion +import io.ksmt.expr.rewrite.simplify.simplifyRegexIntersection +import io.ksmt.expr.rewrite.simplify.simplifyRegexStar +import io.ksmt.expr.rewrite.simplify.simplifyRegexCross +import io.ksmt.expr.rewrite.simplify.simplifyRegexDifference +import io.ksmt.expr.rewrite.simplify.simplifyRegexComplement +import io.ksmt.expr.rewrite.simplify.simplifyRegexOption +import io.ksmt.expr.rewrite.simplify.simplifyRegexRange +import io.ksmt.expr.rewrite.simplify.simplifyRegexPower +import io.ksmt.expr.rewrite.simplify.simplifyRegexLoop import io.ksmt.sort.KArithSort import io.ksmt.sort.KArray2Sort import io.ksmt.sort.KArray3Sort @@ -422,6 +544,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -591,6 +715,24 @@ open class KContext( * */ fun mkRealSort(): KRealSort = realSortCache + private val stringSortCache by lazy { + ensureContextActive { KStringSort(this) } + } + + /** + * Create a String sort. + * */ + fun mkStringSort(): KStringSort = stringSortCache + + private val regexSortCache by lazy { + ensureContextActive { KRegexSort(this) } + } + + /** + * Create a Regex sort. + * */ + fun mkRegexSort(): KRegexSort = regexSortCache + // bit-vec private val bv1SortCache: KBv1Sort by lazy { KBv1Sort(this) } private val bv8SortCache: KBv8Sort by lazy { KBv8Sort(this) } @@ -709,6 +851,12 @@ open class KContext( val realSort: KRealSort get() = mkRealSort() + val stringSort: KStringSort + get() = mkStringSort() + + val regexSort: KRegexSort + get() = mkRegexSort() + val bv1Sort: KBv1Sort get() = mkBv1Sort() @@ -1864,6 +2012,773 @@ open class KContext( fun KExpr.toIntExpr() = mkRealToInt(this) fun KExpr.isIntExpr() = mkRealIsInt(this) + // strings + private val stringLiteralCache = mkAstInterner() + + /** + * Create a String value. + * */ + fun mkStringLiteral(value: String): KStringLiteralExpr = stringLiteralCache.createIfContextActive { + KStringLiteralExpr(this, value) + } + + /** + * Create a String value. + * */ + val String.expr + get() = mkStringLiteral(this) + + private val stringConcatExprCache = mkAstInterner() + + /** + * Create String concatenation (`concat`) expression. + * */ + open fun mkStringConcat(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyStringConcat, ::mkStringConcatNoSimplify) // Add simplified version + + /** + * Create String concatenation (`concat`) expression. + * */ + open fun mkStringConcatNoSimplify(arg0: KExpr, arg1: KExpr): KStringConcatExpr = + stringConcatExprCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KStringConcatExpr(this, arg0, arg1) + } + + /** + * Create String concatenation (`concat`) expression. + * */ + @JvmName("stringConcat") + operator fun KExpr.plus(other: KExpr) = mkStringConcat(this, other) + + private val stringLenExprCache = mkAstInterner() + + /** + * Create string's length expression. + * */ + open fun mkStringLen(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringLen, ::mkStringLenNoSimplify) // Add simplified version + + /** + * Create string's length expression. + * */ + open fun mkStringLenNoSimplify(arg: KExpr): KStringLenExpr = stringLenExprCache.createIfContextActive { + ensureContextMatch(arg) + KStringLenExpr(this, arg) + } + + val KExpr.len + get() = mkStringLen(this) + + val String.len + get() = mkStringLen(this.expr) + + private val stringSuffixOfExprCache = mkAstInterner() + + /** + * Check if first string is a suffix of second. + * */ + open fun mkStringSuffixOf(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyStringSuffixOf, ::mkStringSuffixOfNoSimplify) // Add simplified version + + /** + * Check if first string is a suffix of second. + * */ + open fun mkStringSuffixOfNoSimplify(arg0: KExpr, arg1: KExpr): KStringSuffixOfExpr = + stringSuffixOfExprCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KStringSuffixOfExpr(this, arg0, arg1) + } + + infix fun KExpr.isSuffixOf(other: KExpr) = mkStringSuffixOf(this, other) + + private val stringPrefixOfExprCache = mkAstInterner() + + /** + * Check if first string is a prefix of second. + * */ + open fun mkStringPrefixOf(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyStringPrefixOf, ::mkStringPrefixOfNoSimplify) // Add simplified version + + /** + * Check if first string is a prefix of second. + * */ + open fun mkStringPrefixOfNoSimplify(arg0: KExpr, arg1: KExpr): KStringPrefixOfExpr = + stringPrefixOfExprCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KStringPrefixOfExpr(this, arg0, arg1) + } + + infix fun KExpr.isPrefixOf(other: KExpr) = mkStringPrefixOf(this, other) + + private val stringLtCache = mkAstInterner() + + /** + * Create a lexicographic ordering (`<` (less)) expression. + * */ + open fun mkStringLt(lhs: KExpr, rhs: KExpr): KExpr = + mkSimplified(lhs, rhs, KContext::simplifyStringLt, ::mkStringLtNoSimplify) // Add simplified version + + /** + * Create a lexicographic ordering (`<` (less)) expression. + * */ + open fun mkStringLtNoSimplify(lhs: KExpr, rhs: KExpr): KStringLtExpr = + stringLtCache.createIfContextActive { + ensureContextMatch(lhs, rhs) + KStringLtExpr(this, lhs, rhs) + } + + @JvmName("stringLt") + infix fun KExpr.lt(other: KExpr) = mkStringLt(this, other) + + private val stringLeCache = mkAstInterner() + + /** + * Create a lexicographic ordering reflexive closure (`<=` (less or equal)) expression. + * */ + open fun mkStringLe(lhs: KExpr, rhs: KExpr): KExpr = + mkSimplified(lhs, rhs, KContext::simplifyStringLe, ::mkStringLeNoSimplify) // Add simplified version + + /** + * Create a lexicographic ordering reflexive closure (`<=` (less or equal)) expression. + * */ + open fun mkStringLeNoSimplify(lhs: KExpr, rhs: KExpr): KStringLeExpr = + stringLeCache.createIfContextActive { + ensureContextMatch(lhs, rhs) + KStringLeExpr(this, lhs, rhs) + } + + @JvmName("stringLe") + infix fun KExpr.le(other: KExpr) = mkStringLe(this, other) + + private val stringGtCache = mkAstInterner() + + /** + * Create a lexicographic ordering (`>` (greater)) expression. + * */ + open fun mkStringGt(lhs: KExpr, rhs: KExpr): KExpr = + mkSimplified(lhs, rhs, KContext::simplifyStringGt, ::mkStringGtNoSimplify) // Add simplified version + + /** + * Create a lexicographic ordering (`>` (greater)) expression. + * */ + open fun mkStringGtNoSimplify(lhs: KExpr, rhs: KExpr): KStringGtExpr = + stringGtCache.createIfContextActive { + ensureContextMatch(lhs, rhs) + KStringGtExpr(this, lhs, rhs) + } + + @JvmName("stringGt") + infix fun KExpr.gt(other: KExpr) = mkStringGt(this, other) + + private val stringGeCache = mkAstInterner() + + /** + * Create a lexicographic ordering reflexive closure (`>=` (greater or equal)) expression. + * */ + open fun mkStringGe(lhs: KExpr, rhs: KExpr): KExpr = + mkSimplified(lhs, rhs, KContext::simplifyStringGe, ::mkStringGeNoSimplify) // Add simplified version + + /** + * Create a lexicographic ordering reflexive closure (`>=` (greater or equal)) expression. + * */ + open fun mkStringGeNoSimplify(lhs: KExpr, rhs: KExpr): KStringGeExpr = + stringGeCache.createIfContextActive { + ensureContextMatch(lhs, rhs) + KStringGeExpr(this, lhs, rhs) + } + + @JvmName("stringGe") + infix fun KExpr.ge(other: KExpr) = mkStringGe(this, other) + + private val stringContainsCache = mkAstInterner() + + /** + * Check if first string contains second one. + * */ + open fun mkStringContains(lhs: KExpr, rhs: KExpr): KExpr = + mkSimplified(lhs, rhs, KContext::simplifyStringContains, ::mkStringContainsNoSimplify) // Add simplified version + + /** + * Check if first string contains second one. + * */ + open fun mkStringContainsNoSimplify(lhs: KExpr, rhs: KExpr): KStringContainsExpr = + stringContainsCache.createIfContextActive { + ensureContextMatch(lhs, rhs) + KStringContainsExpr(this, lhs, rhs) + } + + @JvmName("strContains") + infix fun KExpr.contains(other: KExpr) = mkStringContains(this, other) + + private val stringSingletonSubCache = mkAstInterner() + + /** + * Returns singleton string containing a character at given position. + * If position is out of range (less than 0, or grater than (string length - 1)), then returns empty string. + * */ + open fun mkStringSingletonSub(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyStringSingletonSub, ::mkStringSingletonSubNoSimplify) // Add simplified version + + /** + * Returns singleton string containing a character at given position. + * If position is out of range (less than 0, or grater than (string length - 1)), then returns empty string. + * */ + open fun mkStringSingletonSubNoSimplify(arg0: KExpr, arg1: KExpr): KStringSingletonSubExpr = + stringSingletonSubCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KStringSingletonSubExpr(this, arg0, arg1) + } + + private val stringSubCache = mkAstInterner() + + /** + * Evaluates the longest substring from the input string, starting at the specified position + * and extending up to the given length. Returns an empty string if the given length is negative + * or the given position is out of bounds. + */ + open fun mkStringSub(arg0: KExpr, arg1: KExpr, arg2: KExpr): KExpr = + mkSimplified(arg0, arg1, arg2, KContext::simplifyStringSub, ::mkStringSubNoSimplify) // Add simplified version + + /** + * Evaluates the longest substring from the input string, starting at the specified position + * and extending up to the given length. Returns an empty string if the given length is negative + * or the given position is out of bounds. + */ + open fun mkStringSubNoSimplify(arg0: KExpr, arg1: KExpr, arg2: KExpr): KStringSubExpr = + stringSubCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KStringSubExpr(this, arg0, arg1, arg2) + } + + private val stringIndexOfCache = mkAstInterner() + + /** + * Find the index of the first occurrence of the second string in the first string, + * starting at the specified position. Returns -1 if not found + * or if the position is out of bounds. + * Returns the position if the second string is empty. + */ + open fun mkStringIndexOf(arg0: KExpr, arg1: KExpr, arg2: KExpr): KExpr = + mkSimplified(arg0, arg1, arg2, KContext::simplifyStringIndexOf, ::mkStringIndexOfNoSimplify) // Add simplified version + + /** + * Find the index of the first occurrence of the second string in the first string, + * starting at the specified position. Returns -1 if not found + * or if the position is out of bounds. + * Returns the position if the second string is empty. + */ + open fun mkStringIndexOfNoSimplify(arg0: KExpr, arg1: KExpr, arg2: KExpr): KStringIndexOfExpr = + stringIndexOfCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KStringIndexOfExpr(this, arg0, arg1, arg2) + } + + private val stringIndexOfRegexCache = mkAstInterner() + + /** + * Find the index of the first match of a regular expression in the string, + * starting at the specified position. Returns -1 if not found + * or if the position is out of bounds. + */ + open fun mkStringIndexOfRegex(arg0: KExpr, arg1: KExpr, arg2: KExpr): KExpr = + mkSimplified(arg0, arg1, arg2, KContext::simplifyStringIndexOfRegex, ::mkStringIndexOfRegexNoSimplify) // Add simplified version + + /** + * Find the index of the first match of a regular expression in the string, + * starting at the specified position. Returns -1 if not found + * or if the position is out of bounds. + */ + open fun mkStringIndexOfRegexNoSimplify(arg0: KExpr, arg1: KExpr, arg2: KExpr): KStringIndexOfRegexExpr = + stringIndexOfRegexCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KStringIndexOfRegexExpr(this, arg0, arg1, arg2) + } + + private val stringReplaceCache = mkAstInterner() + + /** + * Replace the first occurrence of the second string in the first string with the third, + * if there are such occurrences, otherwise return the first string. + * If the second line is empty, then the third is inserted at the beginning of the first. + * */ + open fun mkStringReplace(arg0: KExpr, arg1: KExpr, arg2: KExpr): KExpr = + mkSimplified(arg0, arg1, arg2, KContext::simplifyStringReplace, ::mkStringReplaceNoSimplify) // Add simplified version + + /** + * Replace the first occurrence of the second string in the first string with the third, + * if there are such occurrences, otherwise return the first string. + * If the second line is empty, then the third is inserted at the beginning of the first. + * */ + open fun mkStringReplaceNoSimplify(arg0: KExpr, arg1: KExpr, arg2: KExpr): KStringReplaceExpr = + stringReplaceCache.createIfContextActive { + ensureContextMatch(arg0, arg1, arg2) + KStringReplaceExpr(this, arg0, arg1, arg2) + } + + private val stringReplaceAllCache = mkAstInterner() + + /** + * Replace the all occurrences of the second string in the first string with the third, + * if there are such occurrences, otherwise return the first string. + * */ + open fun mkStringReplaceAll(arg0: KExpr, arg1: KExpr, arg2: KExpr): KExpr = + mkSimplified(arg0, arg1, arg2, KContext::simplifyStringReplaceAll, ::mkStringReplaceAllNoSimplify) // Add simplified version + + /** + * Replace the all occurrences of the second string in the first string with the third, + * if there are such occurrences, otherwise return the first string. + * */ + open fun mkStringReplaceAllNoSimplify(arg0: KExpr, arg1: KExpr, arg2: KExpr): KStringReplaceAllExpr = + stringReplaceAllCache.createIfContextActive { + ensureContextMatch(arg0, arg1, arg2) + KStringReplaceAllExpr(this, arg0, arg1, arg2) + } + + private val stringReplaceWithRegexCache = mkAstInterner() + + /** + * Replace the shortest leftmost match of regex in first string, if any, by second string. + * If the language of r contains the empty string, the result is to prepend second string to first one. + * */ + open fun mkStringReplaceWithRegex(arg0: KExpr, arg1: KExpr, arg2: KExpr): KExpr = + mkSimplified(arg0, arg1, arg2, KContext::simplifyStringReplaceWithRegex, ::mkStringReplaceWithRegexNoSimplify) // Add simplified version + + /** + * Replace the shortest leftmost match of regex in first string, if any, by second string. + * If the language of r contains the empty string, the result is to prepend second string to first one. + * */ + open fun mkStringReplaceWithRegexNoSimplify(arg0: KExpr, arg1: KExpr, arg2: KExpr): KStringReplaceWithRegexExpr = + stringReplaceWithRegexCache.createIfContextActive { + ensureContextMatch(arg0, arg1, arg2) + KStringReplaceWithRegexExpr(this, arg0, arg1, arg2) + } + + private val stringReplaceAllWithRegexCache = mkAstInterner() + + /** + * Replace left-to right, each shortest non-empty match of regex in first string by seconds. + * */ + open fun mkStringReplaceAllWithRegex(arg0: KExpr, arg1: KExpr, arg2: KExpr): KExpr = + mkSimplified(arg0, arg1, arg2, KContext::simplifyStringReplaceAllWithRegex, ::mkStringReplaceAllWithRegexNoSimplify) // Add simplified version + + /** + * Replace left-to right, each shortest non-empty match of regex in first string by seconds. + * */ + open fun mkStringReplaceAllWithRegexNoSimplify(arg0: KExpr, arg1: KExpr, arg2: KExpr): KStringReplaceAllWithRegexExpr = + stringReplaceAllWithRegexCache.createIfContextActive { + ensureContextMatch(arg0, arg1, arg2) + KStringReplaceAllWithRegexExpr(this, arg0, arg1, arg2) + } + + private val stringToLowerExprCache = mkAstInterner() + + /** + * Convert string to lower case. + * */ + open fun mkStringToLower(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringToLower, ::mkStringToLowerNoSimplify) // Add simplified version + + /** + * Convert string to lower case. + * */ + open fun mkStringToLowerNoSimplify(arg: KExpr): KStringToLowerExpr = + stringToLowerExprCache.createIfContextActive { + ensureContextMatch(arg) + KStringToLowerExpr(this, arg) + } + + private val stringToUpperExprCache = mkAstInterner() + + /** + * Convert string to upper case. + * */ + open fun mkStringToUpper(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringToUpper, ::mkStringToUpperNoSimplify) // Add simplified version + + /** + * Convert string to upper case. + * */ + open fun mkStringToUpperNoSimplify(arg: KExpr): KStringToUpperExpr = + stringToUpperExprCache.createIfContextActive { + ensureContextMatch(arg) + KStringToUpperExpr(this, arg) + } + + private val stringReverseExprCache = mkAstInterner() + + /** + * Reverse string. + * */ + open fun mkStringReverse(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringReverse, ::mkStringReverseNoSimplify) // Add simplified version + + /** + * Reverse string. + * */ + open fun mkStringReverseNoSimplify(arg: KExpr): KStringReverseExpr = + stringReverseExprCache.createIfContextActive { + ensureContextMatch(arg) + KStringReverseExpr(this, arg) + } + + private val stringIsDigitCache = mkAstInterner() + + /** + * Check that the string contains only decimal digit characters. + * */ + open fun mkStringIsDigit(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringIsDigit, ::mkStringIsDigitNoSimplify) // Add simplified version + + /** + * Check that the string contains only decimal digit characters. + * */ + open fun mkStringIsDigitNoSimplify(arg: KExpr): KStringIsDigitExpr = + stringIsDigitCache.createIfContextActive { + ensureContextMatch(arg) + KStringIsDigitExpr(this, arg) + } + + private val stringToCodeCache = mkAstInterner() + + /** + * Returns the code point of the only character in the string if the string is a singleton. + * Otherwise, returns -1. + * */ + open fun mkStringToCode(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringToCode, ::mkStringToCodeNoSimplify) // Add simplified version + + /** + * Returns the code point of the only character in the string if the string is a singleton. + * Otherwise, returns -1. + * */ + open fun mkStringToCodeNoSimplify(arg: KExpr): KStringToCodeExpr = + stringToCodeCache.createIfContextActive { + ensureContextMatch(arg) + KStringToCodeExpr(this, arg) + } + + private val stringFromCodeCache = mkAstInterner() + + /** + * Returns a singleton string consisting of a character, with the given code point. + * If codepoint not in range [0, 196607], returns empty string. + * */ + open fun mkStringFromCode(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringFromCode, ::mkStringFromCodeNoSimplify) // Add simplified version + + /** + * Returns a singleton string consisting of a character, with the given code point. + * If codepoint not in range [0, 196607], returns empty string. + * */ + open fun mkStringFromCodeNoSimplify(arg: KExpr): KStringFromCodeExpr = + stringFromCodeCache.createIfContextActive { + ensureContextMatch(arg) + KStringFromCodeExpr(this, arg) + } + + private val stringToIntCache = mkAstInterner() + + /** + * Converts a string containing only decimal digits to a positive integer. + * Otherwise, if the string contains a character that is not a decimal number, then returns -1. + * */ + open fun mkStringToInt(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringToInt, ::mkStringToIntNoSimplify) // Add simplified version + + /** + * Converts a string containing only decimal digits to a positive integer. + * Otherwise, if the string contains a character that is not a decimal number, then returns -1. + * */ + open fun mkStringToIntNoSimplify(arg: KExpr): KStringToIntExpr = + stringToIntCache.createIfContextActive { + ensureContextMatch(arg) + KStringToIntExpr(this, arg) + } + + private val stringFromIntCache = mkAstInterner() + + /** + * Converts a positive integer to a string consisting of the decimal digits of that number, with no leading zeros. + * If the number is negative, it returns an empty string. + * */ + open fun mkStringFromInt(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringFromInt, ::mkStringFromIntNoSimplify) // Add simplified version + + /** + * Converts a positive integer to a string consisting of the decimal digits of that number, with no leading zeros. + * If the number is negative, it returns an empty string. + * */ + open fun mkStringFromIntNoSimplify(arg: KExpr): KStringFromIntExpr = + stringFromIntCache.createIfContextActive { + ensureContextMatch(arg) + KStringFromIntExpr(this, arg) + } + + private val stringToRegexExprCache = mkAstInterner() + + /** + * Create a regular expression based on a string expression. + * */ + open fun mkStringToRegex(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyStringToRegex, ::mkStringToRegexNoSimplify) // Add simplified version + + /** + * Create a regular expression based on a string expression. + * */ + open fun mkStringToRegexNoSimplify(arg: KExpr): KStringToRegexExpr = stringToRegexExprCache.createIfContextActive { + ensureContextMatch(arg) + KStringToRegexExpr(this, arg) + } + + fun KExpr.toRegex() = mkStringToRegex(this) + + fun String.toRegex() = mkStringToRegex(this.expr) + + private val stringInRegexExprCache = mkAstInterner() + + /** + * Check if a string belongs to the language defined by the regular expression. + * */ + open fun mkStringInRegex(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyStringInRegex, ::mkStringInRegexNoSimplify) // Add simplified version + + /** + * Check if a string belongs to the language defined by the regular expression. + * */ + open fun mkStringInRegexNoSimplify(arg0: KExpr, arg1: KExpr): KStringInRegexExpr = + stringInRegexExprCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KStringInRegexExpr(this, arg0, arg1) + } + + infix fun KExpr.inRegex(other: KExpr) = mkStringInRegex(this, other) + + infix fun String.inRegex(other: KExpr) = mkStringInRegex(this.expr, other) + + @JvmName("regexContains") + infix fun KExpr.contains(other: KExpr) = mkStringInRegex(other, this) + + private val regexConcatExprCache = mkAstInterner() + + /** + * Create Regex concatenation (`concat`) expression. + * */ + open fun mkRegexConcat(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyRegexConcat, ::mkRegexConcatNoSimplify) // Add simplified version + + /** + * Create Regex concatenation (`concat`) expression. + * */ + open fun mkRegexConcatNoSimplify(arg0: KExpr, arg1: KExpr): KRegexConcatExpr = + regexConcatExprCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KRegexConcatExpr(this, arg0, arg1) + } + + @JvmName("regexConcat") + operator fun KExpr.plus(other: KExpr) = mkRegexConcat(this, other) + + private val regexUnionExprCache = mkAstInterner() + + /** + * Create Regex union (`union`) expression. + * */ + open fun mkRegexUnion(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyRegexUnion, ::mkRegexUnionNoSimplify) // Add simplified version + + /** + * Create Regex union (`union`) expression. + * */ + open fun mkRegexUnionNoSimplify(arg0: KExpr, arg1: KExpr): KRegexUnionExpr = + regexUnionExprCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KRegexUnionExpr(this, arg0, arg1) + } + + private val regexIntersectionExprCache = mkAstInterner() + + /** + * Create Regex intersection (`intersect`) expression. + * */ + open fun mkRegexIntersection(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyRegexIntersection, ::mkRegexIntersectionNoSimplify) // Add simplified version + + /** + * Create Regex intersection (`intersect`) expression. + * */ + open fun mkRegexIntersectionNoSimplify(arg0: KExpr, arg1: KExpr): KRegexIntersectionExpr = + regexIntersectionExprCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KRegexIntersectionExpr(this, arg0, arg1) + } + + private val regexStarExprCache = mkAstInterner() + + /** + * Create regular expression's Kleene closure. + * */ + open fun mkRegexStar(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyRegexStar, ::mkRegexStarNoSimplify) // Add simplified version + + /** + * Create regular expression's Kleene closure. + * */ + open fun mkRegexStarNoSimplify(arg: KExpr): KRegexStarExpr = + regexStarExprCache.createIfContextActive { + ensureContextMatch(arg) + KRegexStarExpr(this, arg) + } + + private val regexCrossExprCache = mkAstInterner() + + /** + * Create regular expression's Kleene cross. + * */ + open fun mkRegexCross(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyRegexCross, ::mkRegexCrossNoSimplify) // Add simplified version + + /** + * Create regular expression's Kleene cross. + * */ + open fun mkRegexCrossNoSimplify(arg: KExpr): KRegexCrossExpr = + regexCrossExprCache.createIfContextActive { + ensureContextMatch(arg) + KRegexCrossExpr(this, arg) + } + + private val regexDifferenceExprCache = mkAstInterner() + + /** + * Create Regex difference (`diff`) expression. + * */ + open fun mkRegexDifference(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyRegexDifference, ::mkRegexDifferenceNoSimplify) // Add simplified version + + /** + * Create Regex difference (`diff`) expression. + * */ + open fun mkRegexDifferenceNoSimplify(arg0: KExpr, arg1: KExpr): KRegexDifferenceExpr = + regexDifferenceExprCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KRegexDifferenceExpr(this, arg0, arg1) + } + + private val regexComplementExprCache = mkAstInterner() + + /** + * Create regular expression's complement. + * */ + open fun mkRegexComplement(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyRegexComplement, ::mkRegexComplementNoSimplify) // Add simplified version + + /** + * Create regular expression's complement. + * */ + open fun mkRegexComplementNoSimplify(arg: KExpr): KRegexComplementExpr = regexComplementExprCache.createIfContextActive { + ensureContextMatch(arg) + KRegexComplementExpr(this, arg) + } + + private val regexOptionExprCache = mkAstInterner() + + /** + * Make regular expression optional. + * Equivalent to concatenating a regular expression with the empty string. + * */ + open fun mkRegexOption(arg: KExpr): KExpr = + mkSimplified(arg, KContext::simplifyRegexOption, ::mkRegexOptionNoSimplify) // Add simplified version + + /** + * Make regular expression optional. + * Equivalent to concatenating a regular expression with the empty string. + * */ + open fun mkRegexOptionNoSimplify(arg: KExpr): KRegexOptionExpr = regexOptionExprCache.createIfContextActive { + ensureContextMatch(arg) + KRegexOptionExpr(this, arg) + } + + private val regexRangeExprCache = mkAstInterner() + + /** + * Return the set of all singleton strings in the range + * between the first and second string that are also singletons. + * Otherwise the empty set. + * */ + open fun mkRegexRange(arg0: KExpr, arg1: KExpr): KExpr = + mkSimplified(arg0, arg1, KContext::simplifyRegexRange, ::mkRegexRangeNoSimplify) // Add simplified version + + /** + * Return the set of all singleton strings in the range + * between the first and second string that are also singletons. + * Otherwise the empty set. + * */ + open fun mkRegexRangeNoSimplify(arg0: KExpr, arg1: KExpr): KRegexRangeExpr = + regexRangeExprCache.createIfContextActive { + ensureContextMatch(arg0, arg1) + KRegexRangeExpr(this, arg0, arg1) + } + + private val regexPowerExprCache = mkAstInterner() + + /** + * Constructs a regex expression that represents the concatenation + * of the given `arg` regex repeated `power` times. + * */ + open fun mkRegexPower(power: Int, arg: KExpr): KExpr = + mkSimplified(power, arg, KContext::simplifyRegexPower, ::mkRegexPowerNoSimplify) // Add simplified version + + /** + * Constructs a regex expression that represents the concatenation + * of the given `arg` regex repeated `power` times. + * */ + open fun mkRegexPowerNoSimplify(power: Int, arg: KExpr): KRegexPowerExpr = + regexPowerExprCache.createIfContextActive { + ensureContextMatch(arg) + KRegexPowerExpr(this, power, arg) + } + + private val regexLoopExprCache = mkAstInterner() + + /** + * Constructs a regex expression that represents the union of regexes + * formed by repeating the given `arg` regex from `from` to `to` times inclusively. + * */ + open fun mkRegexLoop(from: Int, to: Int, arg: KExpr): KExpr = + mkSimplified(from, to, arg, KContext::simplifyRegexLoop, ::mkRegexLoopNoSimplify) // Add simplified version + + /** + * Constructs a regex expression that represents the union of regexes + * formed by repeating the given `arg` regex from `from` to `to` times inclusively. + * */ + open fun mkRegexLoopNoSimplify(from: Int, to: Int, arg: KExpr): KRegexLoopExpr = + regexLoopExprCache.createIfContextActive { + ensureContextMatch(arg) + KRegexLoopExpr(this, from, to, arg) + } + + val regexEpsilonExpr: KRegexEpsilon = KRegexEpsilon(this) + + /** + * Create regex Epsilon constant. + * Epsilon regular expression denoting the empty set of strings. + * */ + fun mkRegexEpsilon(): KRegexEpsilon = regexEpsilonExpr + + val regexAllExpr: KRegexAll = KRegexAll(this) + + /** + * Create regex constant denoting the set of all strings. + * */ + fun mkRegexAll(): KRegexAll = regexAllExpr + + val regexAllCharExpr: KRegexAllChar = KRegexAllChar(this) + + /** + * Create regex constant denoting the set of all strings of length 1. + * */ + fun mkRegexAllChar(): KRegexAllChar = regexAllCharExpr + // bitvectors private val bv1Cache = mkAstInterner() private val bv8Cache = mkAstInterner() @@ -4301,6 +5216,10 @@ open class KContext( open fun realSortDefaultValue(): KExpr = mkRealNum(0) + open fun stringSortDefaultValue(): KExpr = mkStringLiteral("") + + open fun regexSortDefaultValue(): KExpr = mkRegexEpsilon() + open fun bvSortDefaultValue(sort: S): KExpr = mkBv(0, sort) open fun fpSortDefaultValue(sort: S): KExpr = mkFpZero(signBit = false, sort) @@ -4463,6 +5382,93 @@ open class KContext( fun mkRealNumDecl(value: String): KRealNumDecl = KRealNumDecl(this, value) + // string + fun mkStringLiteralDecl(value: String): KStringLiteralDecl = KStringLiteralDecl(this, value) + + fun mkStringConcatDecl(): KStringConcatDecl = KStringConcatDecl(this) + + fun mkStringLenDecl(): KStringLenDecl = KStringLenDecl(this) + + fun mkStringToRegexDecl(): KStringToRegexDecl = KStringToRegexDecl(this) + + fun mkStringInRegexDecl(): KStringInRegexDecl = KStringInRegexDecl(this) + + fun mkStringSuffixOfDecl(): KStringSuffixOfDecl = KStringSuffixOfDecl(this) + + fun mkStringPrefixOfDecl(): KStringPrefixOfDecl = KStringPrefixOfDecl(this) + + fun mkStringLtDecl(): KStringLtDecl = KStringLtDecl(this) + + fun mkStringLeDecl(): KStringLeDecl = KStringLeDecl(this) + + fun mkStringGtDecl(): KStringGtDecl = KStringGtDecl(this) + + fun mkStringGeDecl(): KStringGeDecl = KStringGeDecl(this) + + fun mkStringContainsDecl(): KStringContainsDecl = KStringContainsDecl(this) + + fun mkStringSingletonSubDecl(): KStringSingletonSubDecl = KStringSingletonSubDecl(this) + + fun mkStringSubDecl(): KStringSubDecl = KStringSubDecl(this) + + fun mkStringIndexOfDecl(): KStringIndexOfDecl = KStringIndexOfDecl(this) + + fun mkStringIndexOfRegexDecl(): KStringIndexOfRegexDecl = KStringIndexOfRegexDecl(this) + + fun mkStringReplaceDecl(): KStringReplaceDecl = KStringReplaceDecl(this) + + fun mkStringReplaceAllDecl(): KStringReplaceAllDecl = KStringReplaceAllDecl(this) + + fun mkStringReplaceWithRegexDecl(): KStringReplaceWithRegexDecl = KStringReplaceWithRegexDecl(this) + + fun mkStringReplaceAllWithRegexDecl(): KStringReplaceAllWithRegexDecl = KStringReplaceAllWithRegexDecl(this) + + fun mkStringToLowerDecl(): KStringToLowerDecl = KStringToLowerDecl(this) + + fun mkStringToUpperDecl(): KStringToUpperDecl = KStringToUpperDecl(this) + + fun mkStringReverseDecl(): KStringReverseDecl = KStringReverseDecl(this) + + fun mkStringIsDigitDecl(): KStringIsDigitDecl = KStringIsDigitDecl(this) + + fun mkStringToCodeDecl(): KStringToCodeDecl = KStringToCodeDecl(this) + + fun mkStringFromCodeDecl(): KStringFromCodeDecl = KStringFromCodeDecl(this) + + fun mkStringToIntDecl(): KStringToIntDecl = KStringToIntDecl(this) + + fun mkStringFromIntDecl(): KStringFromIntDecl = KStringFromIntDecl(this) + + // regex + fun mkRegexConcatDecl(): KRegexConcatDecl = KRegexConcatDecl(this) + + fun mkRegexUnionDecl(): KRegexUnionDecl = KRegexUnionDecl(this) + + fun mkRegexIntersectionDecl(): KRegexIntersectionDecl = KRegexIntersectionDecl(this) + + fun mkRegexStarDecl(): KRegexStarDecl = KRegexStarDecl(this) + + fun mkRegexCrossDecl(): KRegexCrossDecl = KRegexCrossDecl(this) + + fun mkRegexDifferenceDecl(): KRegexDifferenceDecl = KRegexDifferenceDecl(this) + + fun mkRegexComplementDecl(): KRegexComplementDecl = KRegexComplementDecl(this) + + fun mkRegexOptionDecl(): KRegexOptionDecl = KRegexOptionDecl(this) + + fun mkRegexRangeDecl(): KRegexRangeDecl = KRegexRangeDecl(this) + + fun mkRegexPowerDecl(power: Int): KRegexPowerDecl = KRegexPowerDecl(this, power) + + fun mkRegexLoopDecl(from: Int, to: Int): KRegexLoopDecl = KRegexLoopDecl(this, from, to) + + fun mkRegexEpsilonDecl(): KRegexEpsilonDecl = KRegexEpsilonDecl(this) + + fun mkRegexAllDecl(): KRegexAllDecl = KRegexAllDecl(this) + + fun mkRegexAllCharDecl(): KRegexAllCharDecl = KRegexAllCharDecl(this) + + // Bit vectors fun mkBvDecl(value: Boolean): KDecl = KBitVec1ValueDecl(this, value) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/decl/KDecl.kt b/ksmt-core/src/main/kotlin/io/ksmt/decl/KDecl.kt index f309d187a..147162fb7 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/decl/KDecl.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/decl/KDecl.kt @@ -18,7 +18,12 @@ abstract class KDecl( override fun print(builder: StringBuilder): Unit = with(builder) { append('(') - append(name) + + if (this@KDecl is KStringLiteralDecl) { + append("\"$name\"") + } else { + append(name) + } if (this@KDecl is KParameterizedFuncDecl) { append(parameters.joinToString(separator = " ", prefix = " [", postfix = "]")) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/decl/KDeclVisitor.kt b/ksmt-core/src/main/kotlin/io/ksmt/decl/KDeclVisitor.kt index 2f162efdd..a439866dd 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/decl/KDeclVisitor.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/decl/KDeclVisitor.kt @@ -15,6 +15,8 @@ import io.ksmt.sort.KBv8Sort import io.ksmt.sort.KBvSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort interface KDeclVisitor { @@ -131,4 +133,48 @@ interface KDeclVisitor { fun visit(decl: KBvNegNoOverflowDecl): T = visit(decl as KFuncDecl) fun visit(decl: KBvMulNoOverflowDecl): T = visit(decl as KFuncDecl) fun visit(decl: KBvMulNoUnderflowDecl): T = visit(decl as KFuncDecl) + + fun visit(decl: KStringConcatDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringLenDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringToRegexDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringInRegexDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringSuffixOfDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringPrefixOfDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringLtDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringLeDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringGtDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringGeDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringContainsDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringSingletonSubDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringSubDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringIndexOfDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringIndexOfRegexDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringReplaceDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringReplaceAllDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringReplaceWithRegexDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringReplaceAllWithRegexDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringToLowerDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringToUpperDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringReverseDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringIsDigitDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringToCodeDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringFromCodeDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringToIntDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringFromIntDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KStringLiteralDecl): T = visit(decl as KConstDecl) + + fun visit(decl: KRegexConcatDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexUnionDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexIntersectionDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexStarDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexCrossDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexDifferenceDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexComplementDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexOptionDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexRangeDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexPowerDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexLoopDecl): T = visit(decl as KFuncDecl) + fun visit(decl: KRegexEpsilonDecl): T = visit(decl as KConstDecl) + fun visit(decl: KRegexAllDecl): T = visit(decl as KConstDecl) + fun visit(decl: KRegexAllCharDecl): T = visit(decl as KConstDecl) } diff --git a/ksmt-core/src/main/kotlin/io/ksmt/decl/Regex.kt b/ksmt-core/src/main/kotlin/io/ksmt/decl/Regex.kt new file mode 100644 index 000000000..21def6469 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/decl/Regex.kt @@ -0,0 +1,227 @@ +package io.ksmt.decl + +import io.ksmt.KContext +import io.ksmt.expr.KApp +import io.ksmt.expr.KExpr +import io.ksmt.sort.KRegexSort +import io.ksmt.sort.KStringSort + +class KRegexConcatDecl internal constructor( + ctx: KContext, +) : KFuncDecl2( + ctx, + "regex_concat", + ctx.mkRegexSort(), + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkRegexConcatNoSimplify(arg0, arg1) +} + +class KRegexUnionDecl internal constructor( + ctx: KContext, +) : KFuncDecl2( + ctx, + "regex_union", + ctx.mkRegexSort(), + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkRegexUnionNoSimplify(arg0, arg1) +} + +class KRegexIntersectionDecl internal constructor( + ctx: KContext, +) : KFuncDecl2( + ctx, + "regex_intersect", + ctx.mkRegexSort(), + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkRegexIntersectionNoSimplify(arg0, arg1) +} + +class KRegexStarDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "regex_star", + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkRegexStarNoSimplify(arg) +} + +class KRegexCrossDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "regex_cross", + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkRegexCrossNoSimplify(arg) +} + +class KRegexDifferenceDecl internal constructor( + ctx: KContext, +) : KFuncDecl2( + ctx, + "regex_diff", + ctx.mkRegexSort(), + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkRegexDifferenceNoSimplify(arg0, arg1) +} + +class KRegexComplementDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "regex_comp", + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkRegexComplementNoSimplify(arg) +} + +class KRegexOptionDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "regex_opt", + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkRegexOptionNoSimplify(arg) +} + +class KRegexRangeDecl internal constructor( + ctx: KContext, +) : KFuncDecl2( + ctx, + "regex_range", + ctx.mkRegexSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkRegexRangeNoSimplify(arg0, arg1) +} + +class KRegexPowerDecl internal constructor( + ctx: KContext, + val power: Int +) : KFuncDecl1( + ctx, + "(regex_power $power)", + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkRegexPowerNoSimplify(power, arg) +} + +class KRegexLoopDecl internal constructor( + ctx: KContext, + val from: Int, + val to: Int +) : KFuncDecl1( + ctx, + "(regex_loop $from $to)", + ctx.mkRegexSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkRegexLoopNoSimplify(from, to, arg) +} + +class KRegexEpsilonDecl internal constructor( + ctx: KContext +) : KConstDecl( + ctx, + "regex_eps", + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun apply( + args: List> + ): KApp = ctx.mkRegexEpsilon() +} + +class KRegexAllDecl internal constructor( + ctx: KContext +) : KConstDecl( + ctx, + "regex_all", + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun apply( + args: List> + ): KApp = ctx.mkRegexAll() +} + +class KRegexAllCharDecl internal constructor( + ctx: KContext +) : KConstDecl( + ctx, + "regex_all_char", + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun apply( + args: List> + ): KApp = ctx.mkRegexAllChar() +} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/decl/String.kt b/ksmt-core/src/main/kotlin/io/ksmt/decl/String.kt new file mode 100644 index 000000000..8304d96af --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/decl/String.kt @@ -0,0 +1,472 @@ +package io.ksmt.decl + +import io.ksmt.KContext +import io.ksmt.expr.KApp +import io.ksmt.expr.KExpr +import io.ksmt.sort.KBoolSort +import io.ksmt.sort.KIntSort +import io.ksmt.sort.KRegexSort +import io.ksmt.sort.KStringSort + +class KStringConcatDecl internal constructor( + ctx: KContext, +) : KFuncDecl2( + ctx, + "str_concat", + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringConcatNoSimplify(arg0, arg1) +} + +class KStringLenDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_len", + ctx.mkIntSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkStringLenNoSimplify(arg) +} + +class KStringToRegexDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_to_regex", + ctx.mkRegexSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkStringToRegexNoSimplify(arg) +} + +class KStringInRegexDecl internal constructor( + ctx: KContext, +) : KFuncDecl2( + ctx, + "str_in_regex", + ctx.mkBoolSort(), + ctx.mkStringSort(), + ctx.mkRegexSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringInRegexNoSimplify(arg0, arg1) +} + +class KStringSuffixOfDecl internal constructor( + ctx: KContext, +) : KFuncDecl2( + ctx, + "str_suffix_of", + ctx.mkBoolSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringSuffixOfNoSimplify(arg0, arg1) +} + +class KStringPrefixOfDecl internal constructor( + ctx: KContext, +) : KFuncDecl2( + ctx, + "str_prefix_of", + ctx.mkBoolSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringPrefixOfNoSimplify(arg0, arg1) +} + +class KStringLtDecl internal constructor( + ctx: KContext +) : KFuncDecl2( + ctx, + "str_lt", + ctx.mkBoolSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringLtNoSimplify(arg0, arg1) +} + +class KStringLeDecl internal constructor( + ctx: KContext +) : KFuncDecl2( + ctx, + "str_le", + ctx.mkBoolSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringLeNoSimplify(arg0, arg1) +} + +class KStringGtDecl internal constructor( + ctx: KContext +) : KFuncDecl2( + ctx, + "str_gt", + ctx.mkBoolSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringGtNoSimplify(arg0, arg1) +} + +class KStringGeDecl internal constructor( + ctx: KContext +) : KFuncDecl2( + ctx, + "str_ge", + ctx.mkBoolSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringGeNoSimplify(arg0, arg1) +} + +class KStringContainsDecl internal constructor( + ctx: KContext +) : KFuncDecl2( + ctx, + "str_contains", + ctx.mkBoolSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringContainsNoSimplify(arg0, arg1) +} + +class KStringSingletonSubDecl internal constructor( + ctx: KContext +) : KFuncDecl2( + ctx, + "str_singleton_sub", + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkIntSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr + ): KApp = mkStringSingletonSubNoSimplify(arg0, arg1) +} + +class KStringSubDecl internal constructor( + ctx: KContext, +) : KFuncDecl3( + ctx, + "str_sub", + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkIntSort(), + ctx.mkIntSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr + ): KApp = mkStringSubNoSimplify(arg0, arg1, arg2) +} + +class KStringIndexOfDecl internal constructor( + ctx: KContext, +) : KFuncDecl3( + ctx, + "str_index_of", + ctx.mkIntSort(), + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkIntSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr + ): KApp = mkStringIndexOfNoSimplify(arg0, arg1, arg2) +} + +class KStringIndexOfRegexDecl internal constructor( + ctx: KContext, +) : KFuncDecl3( + ctx, + "str_index_of_regex", + ctx.mkIntSort(), + ctx.mkStringSort(), + ctx.mkRegexSort(), + ctx.mkIntSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr + ): KApp = mkStringIndexOfRegexNoSimplify(arg0, arg1, arg2) +} + +class KStringReplaceDecl internal constructor( + ctx: KContext, +) : KFuncDecl3( + ctx, + "str_replace", + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr + ): KApp = mkStringReplaceNoSimplify(arg0, arg1, arg2) +} + +class KStringReplaceAllDecl internal constructor( + ctx: KContext, +) : KFuncDecl3( + ctx, + "str_replace_all", + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr + ): KApp = mkStringReplaceAllNoSimplify(arg0, arg1, arg2) +} + +class KStringReplaceWithRegexDecl internal constructor( + ctx: KContext, +) : KFuncDecl3( + ctx, + "str_replace_with_regex", + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkRegexSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr + ): KApp = mkStringReplaceWithRegexNoSimplify(arg0, arg1, arg2) +} + +class KStringReplaceAllWithRegexDecl internal constructor( + ctx: KContext, +) : KFuncDecl3( + ctx, + "str_replace_all_with_regex", + ctx.mkStringSort(), + ctx.mkStringSort(), + ctx.mkRegexSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr + ): KApp = mkStringReplaceAllWithRegexNoSimplify(arg0, arg1, arg2) +} + +class KStringToLowerDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_to_lower", + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkStringToLowerNoSimplify(arg) +} + +class KStringToUpperDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_to_upper", + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkStringToUpperNoSimplify(arg) +} + +class KStringReverseDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_rev", + ctx.mkStringSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply( + arg: KExpr + ): KApp = mkStringReverseNoSimplify(arg) +} + +/* + Maps to and from integers. + */ + +class KStringIsDigitDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_is_digit", + ctx.mkBoolSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp = mkStringIsDigitNoSimplify(arg) +} + +class KStringToCodeDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_to_code", + ctx.mkIntSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp = mkStringToCodeNoSimplify(arg) +} + +class KStringFromCodeDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_from_code", + ctx.mkStringSort(), + ctx.mkIntSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp = mkStringFromCodeNoSimplify(arg) +} + +class KStringToIntDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_to_int", + ctx.mkIntSort(), + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp = mkStringToIntNoSimplify(arg) +} + +class KStringFromIntDecl internal constructor( + ctx: KContext +) : KFuncDecl1( + ctx, + "str_from_int", + ctx.mkStringSort(), + ctx.mkIntSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun KContext.apply(arg: KExpr): KApp = mkStringFromIntNoSimplify(arg) +} + +/* + Literals + */ + +class KStringLiteralDecl internal constructor( + ctx: KContext, + val value: String +) : KConstDecl( + ctx, + value, + ctx.mkStringSort() +) { + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) + + override fun apply(args: List>): KApp = ctx.mkStringLiteral(value) +} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/Regex.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/Regex.kt new file mode 100644 index 000000000..60111e774 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/Regex.kt @@ -0,0 +1,292 @@ +package io.ksmt.expr + +import io.ksmt.KContext +import io.ksmt.cache.hash +import io.ksmt.cache.structurallyEqual +import io.ksmt.decl.KRegexConcatDecl +import io.ksmt.decl.KRegexUnionDecl +import io.ksmt.decl.KRegexIntersectionDecl +import io.ksmt.decl.KRegexStarDecl +import io.ksmt.decl.KRegexCrossDecl +import io.ksmt.decl.KRegexDifferenceDecl +import io.ksmt.decl.KRegexComplementDecl +import io.ksmt.decl.KRegexOptionDecl +import io.ksmt.decl.KRegexRangeDecl +import io.ksmt.decl.KRegexPowerDecl +import io.ksmt.decl.KRegexLoopDecl +import io.ksmt.decl.KRegexEpsilonDecl +import io.ksmt.decl.KRegexAllDecl +import io.ksmt.decl.KRegexAllCharDecl +import io.ksmt.expr.transformer.KTransformerBase +import io.ksmt.sort.KRegexSort +import io.ksmt.sort.KStringSort + +class KRegexConcatExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.mkRegexSort() + + override val decl: KRegexConcatDecl + get() = ctx.mkRegexConcatDecl() + + override val args: List> + get() = listOf(arg0, arg1) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KRegexUnionExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.mkRegexSort() + + override val decl: KRegexUnionDecl + get() = ctx.mkRegexUnionDecl() + + override val args: List> + get() = listOf(arg0, arg1) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KRegexIntersectionExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.mkRegexSort() + + override val decl: KRegexIntersectionDecl + get() = ctx.mkRegexIntersectionDecl() + + override val args: List> + get() = listOf(arg0, arg1) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KRegexStarExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val decl: KRegexStarDecl + get() = ctx.mkRegexStarDecl() + + override val args: List> + get() = listOf(arg) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KRegexCrossExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val decl: KRegexCrossDecl + get() = ctx.mkRegexCrossDecl() + + override val args: List> + get() = listOf(arg) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KRegexDifferenceExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.mkRegexSort() + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KRegexDifferenceDecl + get() = ctx.mkRegexDifferenceDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KRegexComplementExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val decl: KRegexComplementDecl + get() = ctx.mkRegexComplementDecl() + + override val args: List> + get() = listOf(arg) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KRegexOptionExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val decl: KRegexOptionDecl + get() = ctx.mkRegexOptionDecl() + + override val args: List> + get() = listOf(arg) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KRegexRangeExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.mkRegexSort() + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KRegexRangeDecl + get() = ctx.mkRegexRangeDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KRegexPowerExpr internal constructor( + ctx: KContext, + val power: Int, + val arg: KExpr, +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val decl: KRegexPowerDecl + get() = ctx.mkRegexPowerDecl(power) + + override val args: List> + get() = listOf(arg) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg, power) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg }, { power }) +} + +class KRegexLoopExpr internal constructor( + ctx: KContext, + val from: Int, + val to: Int, + val arg: KExpr, +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val decl: KRegexLoopDecl + get() = ctx.mkRegexLoopDecl(from, to) + + override val args: List> + get() = listOf(arg) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg, from, to) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg }, { from }, { to }) +} + +class KRegexEpsilon(ctx: KContext) : KInterpretedValue(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val decl: KRegexEpsilonDecl + get() = ctx.mkRegexEpsilonDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash() + override fun internEquals(other: Any): Boolean = structurallyEqual(other) +} + +class KRegexAll(ctx: KContext) : KInterpretedValue(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val decl: KRegexAllDecl + get() = ctx.mkRegexAllDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash() + override fun internEquals(other: Any): Boolean = structurallyEqual(other) +} + +class KRegexAllChar(ctx: KContext) : KInterpretedValue(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val decl: KRegexAllCharDecl + get() = ctx.mkRegexAllCharDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash() + override fun internEquals(other: Any): Boolean = structurallyEqual(other) +} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/String.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/String.kt new file mode 100644 index 000000000..1f96a4b65 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/String.kt @@ -0,0 +1,632 @@ +package io.ksmt.expr + +import io.ksmt.KContext +import io.ksmt.cache.hash +import io.ksmt.cache.structurallyEqual +import io.ksmt.decl.KStringConcatDecl +import io.ksmt.decl.KStringLenDecl +import io.ksmt.decl.KStringSuffixOfDecl +import io.ksmt.decl.KStringPrefixOfDecl +import io.ksmt.decl.KStringLtDecl +import io.ksmt.decl.KStringLeDecl +import io.ksmt.decl.KStringGtDecl +import io.ksmt.decl.KStringGeDecl +import io.ksmt.decl.KStringToRegexDecl +import io.ksmt.decl.KStringInRegexDecl +import io.ksmt.decl.KStringContainsDecl +import io.ksmt.decl.KStringSingletonSubDecl +import io.ksmt.decl.KStringSubDecl +import io.ksmt.decl.KStringIndexOfDecl +import io.ksmt.decl.KStringIndexOfRegexDecl +import io.ksmt.decl.KStringReplaceDecl +import io.ksmt.decl.KStringReplaceAllDecl +import io.ksmt.decl.KStringReplaceWithRegexDecl +import io.ksmt.decl.KStringReplaceAllWithRegexDecl +import io.ksmt.decl.KStringToLowerDecl +import io.ksmt.decl.KStringToUpperDecl +import io.ksmt.decl.KStringReverseDecl +import io.ksmt.decl.KStringIsDigitDecl +import io.ksmt.decl.KStringToCodeDecl +import io.ksmt.decl.KStringFromCodeDecl +import io.ksmt.decl.KStringToIntDecl +import io.ksmt.decl.KStringFromIntDecl +import io.ksmt.decl.KStringLiteralDecl +import io.ksmt.expr.printer.ExpressionPrinter +import io.ksmt.expr.transformer.KTransformerBase +import io.ksmt.sort.KSort +import io.ksmt.sort.KBoolSort +import io.ksmt.sort.KIntSort +import io.ksmt.sort.KRegexSort +import io.ksmt.sort.KStringSort +import io.ksmt.utils.cast + +class KStringConcatExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.mkStringSort() + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KStringConcatDecl + get() = ctx.mkStringConcatDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringLenExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KIntSort + get() = ctx.intSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringLenDecl + get() = ctx.mkStringLenDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KStringToRegexExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KRegexSort + get() = ctx.regexSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringToRegexDecl + get() = ctx.mkStringToRegexDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KStringInRegexExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + override val args: List> + get() = listOf(arg0.cast(), arg1.cast()) + + override val decl: KStringInRegexDecl + get() = ctx.mkStringInRegexDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringSuffixOfExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KStringSuffixOfDecl + get() = ctx.mkStringSuffixOfDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringPrefixOfExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KStringPrefixOfDecl + get() = ctx.mkStringPrefixOfDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringLtExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KStringLtDecl + get() = ctx.mkStringLtDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringLeExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KStringLeDecl + get() = ctx.mkStringLeDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringGtExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KStringGtDecl + get() = ctx.mkStringGtDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringGeExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KStringGeDecl + get() = ctx.mkStringGeDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringContainsExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + override val args: List> + get() = listOf(arg0, arg1) + + override val decl: KStringContainsDecl + get() = ctx.mkStringContainsDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringSingletonSubExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg0.cast(), arg1.cast()) + + override val decl: KStringSingletonSubDecl + get() = ctx.mkStringSingletonSubDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }) +} + +class KStringSubExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr, + val arg2: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg0.cast(), arg1.cast(), arg2.cast()) + + override val decl: KStringSubDecl + get() = ctx.mkStringSubDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1, arg2) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }, { arg2 }) +} + +class KStringIndexOfExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr, + val arg2: KExpr +) : KApp(ctx) { + override val sort: KIntSort + get() = ctx.intSort + + override val args: List> + get() = listOf(arg0.cast(), arg1.cast(), arg2.cast()) + + override val decl: KStringIndexOfDecl + get() = ctx.mkStringIndexOfDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1, arg2) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }, { arg2 }) +} + +class KStringIndexOfRegexExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr, + val arg2: KExpr +) : KApp(ctx) { + override val sort: KIntSort + get() = ctx.intSort + + override val args: List> + get() = listOf(arg0.cast(), arg1.cast(), arg2.cast()) + + override val decl: KStringIndexOfRegexDecl + get() = ctx.mkStringIndexOfRegexDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1, arg2) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }, { arg2 }) +} + +class KStringReplaceExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr, + val arg2: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg0, arg1, arg2) + + override val decl: KStringReplaceDecl + get() = ctx.mkStringReplaceDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1, arg2) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }, { arg2 }) +} + +class KStringReplaceAllExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr, + val arg2: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg0, arg1, arg2) + + override val decl: KStringReplaceAllDecl + get() = ctx.mkStringReplaceAllDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1, arg2) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }, { arg2 }) +} + +class KStringReplaceWithRegexExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr, + val arg2: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg0.cast(), arg1.cast(), arg2.cast()) + + override val decl: KStringReplaceWithRegexDecl + get() = ctx.mkStringReplaceWithRegexDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1, arg2) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }, { arg2 }) +} + +class KStringReplaceAllWithRegexExpr internal constructor( + ctx: KContext, + val arg0: KExpr, + val arg1: KExpr, + val arg2: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg0.cast(), arg1.cast(), arg2.cast()) + + override val decl: KStringReplaceAllWithRegexDecl + get() = ctx.mkStringReplaceAllWithRegexDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg0, arg1, arg2) + override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 }, { arg2 }) +} + +class KStringToLowerExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringToLowerDecl + get() = ctx.mkStringToLowerDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KStringToUpperExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringToUpperDecl + get() = ctx.mkStringToUpperDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KStringReverseExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringReverseDecl + get() = ctx.mkStringReverseDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +/* + Maps to and from integers. + */ + +class KStringIsDigitExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringIsDigitDecl + get() = ctx.mkStringIsDigitDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KStringToCodeExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KIntSort + get() = ctx.intSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringToCodeDecl + get() = ctx.mkStringToCodeDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KStringFromCodeExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringFromCodeDecl + get() = ctx.mkStringFromCodeDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KStringToIntExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KIntSort + get() = ctx.intSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringToIntDecl + get() = ctx.mkStringToIntDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +class KStringFromIntExpr internal constructor( + ctx: KContext, + val arg: KExpr +) : KApp(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val args: List> + get() = listOf(arg) + + override val decl: KStringFromIntDecl + get() = ctx.mkStringFromIntDecl() + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun internHashCode(): Int = hash(arg) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg } +} + +/* + Literals + */ + +class KStringLiteralExpr internal constructor( + ctx: KContext, + val value: String +) : KInterpretedValue(ctx) { + override val sort: KStringSort + get() = ctx.stringSort + + override val decl: KStringLiteralDecl + get() = ctx.mkStringLiteralDecl(value) + + override fun accept(transformer: KTransformerBase): KExpr = + transformer.transform(this) + + override fun print(printer: ExpressionPrinter) = with(printer) { append("\"$value\"") } + + override fun internHashCode(): Int = hash(value) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { value } +} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/RegexSimplification.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/RegexSimplification.kt new file mode 100644 index 000000000..0bc248fa4 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/RegexSimplification.kt @@ -0,0 +1,58 @@ +package io.ksmt.expr.rewrite.simplify + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.sort.KRegexSort +import io.ksmt.sort.KStringSort + +fun KContext.simplifyRegexConcat( + arg0: KExpr, + arg1: KExpr +): KExpr = mkRegexConcatNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyRegexUnion( + arg0: KExpr, + arg1: KExpr +): KExpr = mkRegexUnionNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyRegexIntersection( + arg0: KExpr, + arg1: KExpr +): KExpr = mkRegexIntersectionNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyRegexStar( + arg: KExpr +): KExpr = mkRegexStarNoSimplify(arg) // Temporarily + +fun KContext.simplifyRegexCross( + arg: KExpr +): KExpr = mkRegexCrossNoSimplify(arg) // Temporarily + +fun KContext.simplifyRegexDifference( + arg0: KExpr, + arg1: KExpr +): KExpr = mkRegexDifferenceNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyRegexComplement( + arg: KExpr +): KExpr = mkRegexComplementNoSimplify(arg) // Temporarily + +fun KContext.simplifyRegexOption( + arg: KExpr +): KExpr = mkRegexOptionNoSimplify(arg) // Temporarily + +fun KContext.simplifyRegexRange( + arg0: KExpr, + arg1: KExpr +): KExpr = mkRegexRangeNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyRegexPower( + power: Int, + arg: KExpr, +): KExpr = mkRegexPowerNoSimplify(power, arg) // Temporarily + +fun KContext.simplifyRegexLoop( + from: Int, + to: Int, + arg: KExpr, +): KExpr = mkRegexLoopNoSimplify(from, to, arg) // Temporarily diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/RegexSimplificationRules.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/RegexSimplificationRules.kt new file mode 100644 index 000000000..a8eda57c9 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/RegexSimplificationRules.kt @@ -0,0 +1,2 @@ +package io.ksmt.expr.rewrite.simplify + diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplification.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplification.kt new file mode 100644 index 000000000..d84c5cc44 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplification.kt @@ -0,0 +1,140 @@ +package io.ksmt.expr.rewrite.simplify + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.sort.KBoolSort +import io.ksmt.sort.KIntSort +import io.ksmt.sort.KRegexSort +import io.ksmt.sort.KStringSort + +fun KContext.simplifyStringConcat( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringConcatNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringLen( + arg: KExpr +): KExpr = mkStringLenNoSimplify(arg) // Temporarily + +fun KContext.simplifyStringToRegex( + arg: KExpr +): KExpr = mkStringToRegexNoSimplify(arg) // Temporarily + +fun KContext.simplifyStringInRegex( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringInRegexNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringSuffixOf( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringSuffixOfNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringPrefixOf( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringPrefixOfNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringLt( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringLtNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringLe( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringLeNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringGt( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringGtNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringGe( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringGeNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringContains( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringContainsNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringSingletonSub( + arg0: KExpr, + arg1: KExpr +): KExpr = mkStringSingletonSubNoSimplify(arg0, arg1) // Temporarily + +fun KContext.simplifyStringSub( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr +): KExpr = mkStringSubNoSimplify(arg0, arg1, arg2) // Temporarily + +fun KContext.simplifyStringIndexOf( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr +): KExpr = mkStringIndexOfNoSimplify(arg0, arg1, arg2) // Temporarily + +fun KContext.simplifyStringIndexOfRegex( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr +): KExpr = mkStringIndexOfRegexNoSimplify(arg0, arg1, arg2) // Temporarily + +fun KContext.simplifyStringReplace( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr +): KExpr = mkStringReplaceNoSimplify(arg0, arg1, arg2) // Temporarily + +fun KContext.simplifyStringReplaceAll( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr +): KExpr = mkStringReplaceAllNoSimplify(arg0, arg1, arg2) // Temporarily + +fun KContext.simplifyStringReplaceWithRegex( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr +): KExpr = mkStringReplaceWithRegexNoSimplify(arg0, arg1, arg2) // Temporarily + +fun KContext.simplifyStringReplaceAllWithRegex( + arg0: KExpr, + arg1: KExpr, + arg2: KExpr +): KExpr = mkStringReplaceAllWithRegexNoSimplify(arg0, arg1, arg2) // Temporarily + +fun KContext.simplifyStringToLower( + arg: KExpr +): KExpr = mkStringToLowerNoSimplify(arg) // Temporarily + +fun KContext.simplifyStringToUpper( + arg: KExpr +): KExpr = mkStringToUpperNoSimplify(arg) // Temporarily + +fun KContext.simplifyStringReverse( + arg: KExpr +): KExpr = mkStringReverseNoSimplify(arg) // Temporarily + +fun KContext.simplifyStringIsDigit( + arg: KExpr +): KExpr = mkStringIsDigitNoSimplify(arg) // Temporarily + +fun KContext.simplifyStringToCode( + arg: KExpr +): KExpr = mkStringToCodeNoSimplify(arg) // Temporarily + +fun KContext.simplifyStringFromCode( + arg: KExpr +): KExpr = mkStringFromCodeNoSimplify(arg) // Temporarily + +fun KContext.simplifyStringToInt( + arg: KExpr +): KExpr = mkStringToIntNoSimplify(arg) // Temporarily + +fun KContext.simplifyStringFromInt( + arg: KExpr +): KExpr = mkStringFromIntNoSimplify(arg) // Temporarily diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplificationRules.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplificationRules.kt new file mode 100644 index 000000000..a8eda57c9 --- /dev/null +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplificationRules.kt @@ -0,0 +1,2 @@ +package io.ksmt.expr.rewrite.simplify + diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformer.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformer.kt index 5d5b1a272..0b1a229da 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformer.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveTransformer.kt @@ -124,6 +124,44 @@ import io.ksmt.expr.KToRealIntExpr import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr import io.ksmt.sort.KArithSort import io.ksmt.sort.KArray2Sort import io.ksmt.sort.KArray3Sort @@ -136,6 +174,8 @@ import io.ksmt.sort.KBvSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.utils.uncheckedCast @@ -661,6 +701,198 @@ abstract class KNonRecursiveTransformer(override val ctx: KContext) : KNonRecurs override fun transform(expr: KIsIntRealExpr): KExpr = transformExprAfterTransformedDefault(expr, expr.arg, ::transformApp, KContext::mkRealIsInt) + // string transformers + override fun transform(expr: KStringConcatExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringConcat + ) + + override fun transform(expr: KStringLenExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringLen + ) + + override fun transform(expr: KStringToRegexExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringToRegex + ) + + override fun transform(expr: KStringInRegexExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringInRegex + ) + + override fun transform(expr: KStringSuffixOfExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringSuffixOf + ) + + override fun transform(expr: KStringPrefixOfExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringPrefixOf + ) + + override fun transform(expr: KStringLtExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringLt + ) + + override fun transform(expr: KStringLeExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringLe + ) + + override fun transform(expr: KStringGtExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringGt + ) + + override fun transform(expr: KStringGeExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringGe + ) + + override fun transform(expr: KStringContainsExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringContains + ) + + override fun transform(expr: KStringSingletonSubExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkStringSingletonSub + ) + + override fun transform(expr: KStringSubExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, expr.arg2, ::transformApp, KContext::mkStringSub + ) + + override fun transform(expr: KStringIndexOfExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, expr.arg2, ::transformApp, KContext::mkStringIndexOf + ) + + override fun transform(expr: KStringIndexOfRegexExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, expr.arg2, ::transformApp, KContext::mkStringIndexOfRegex + ) + + override fun transform(expr: KStringReplaceExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, expr.arg2, ::transformApp, KContext::mkStringReplace + ) + + override fun transform(expr: KStringReplaceAllExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, expr.arg2, ::transformApp, KContext::mkStringReplaceAll + ) + + override fun transform(expr: KStringReplaceWithRegexExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, expr.arg2, ::transformApp, KContext::mkStringReplaceWithRegex + ) + + override fun transform(expr: KStringReplaceAllWithRegexExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, expr.arg2, ::transformApp, KContext::mkStringReplaceAllWithRegex + ) + + override fun transform(expr: KStringToLowerExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringToLower + ) + + override fun transform(expr: KStringToUpperExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringToUpper + ) + + override fun transform(expr: KStringReverseExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringReverse + ) + + override fun transform(expr: KStringIsDigitExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringIsDigit + ) + + override fun transform(expr: KStringToCodeExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringToCode + ) + + override fun transform(expr: KStringFromCodeExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringFromCode + ) + + override fun transform(expr: KStringToIntExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringToCode + ) + + override fun transform(expr: KStringFromIntExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkStringFromCode + ) + + // regex transformers + override fun transform(expr: KRegexConcatExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkRegexConcat + ) + + override fun transform(expr: KRegexUnionExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkRegexUnion + ) + + override fun transform(expr: KRegexIntersectionExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkRegexIntersection + ) + + override fun transform(expr: KRegexStarExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkRegexStar + ) + + override fun transform(expr: KRegexCrossExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkRegexCross + ) + + override fun transform(expr: KRegexDifferenceExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkRegexDifference + ) + + override fun transform(expr: KRegexComplementExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkRegexComplement + ) + + override fun transform(expr: KRegexOptionExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg, ::transformApp, KContext::mkRegexOption + ) + + override fun transform(expr: KRegexRangeExpr): KExpr = + transformExprAfterTransformedDefault( + expr, expr.arg0, expr.arg1, ::transformApp, KContext::mkRegexRange + ) + + override fun transform(expr: KRegexPowerExpr): KExpr = + transformExprAfterTransformedDefault(expr, expr.arg, ::transformApp) { + arg -> mkRegexPower(expr.power, arg) + } + + override fun transform(expr: KRegexLoopExpr): KExpr = + transformExprAfterTransformedDefault(expr, expr.arg, ::transformApp) { + arg -> mkRegexLoop(expr.from, expr.to, arg) + } + // quantified expressions override fun transform(expr: KExistentialQuantifier): KExpr = transformExprAfterTransformedDefault(expr, expr.body, ::transformExpr) { body -> 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 index 35bd4d57b..50510ba64 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitor.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KNonRecursiveVisitor.kt @@ -124,6 +124,44 @@ import io.ksmt.expr.KToRealIntExpr import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr import io.ksmt.sort.KArithSort import io.ksmt.sort.KArraySortBase import io.ksmt.sort.KBvSort @@ -629,6 +667,122 @@ abstract class KNonRecursiveVisitor( override fun visit(expr: KIsIntRealExpr): KExprVisitResult = visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + // string visitors + override fun visit(expr: KStringConcatExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringLenExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KStringToRegexExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KStringInRegexExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringSuffixOfExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringPrefixOfExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringLtExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringLeExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringGtExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringGeExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringContainsExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringSingletonSubExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KStringSubExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, expr.arg2, ::visitApp) + + override fun visit(expr: KStringIndexOfExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, expr.arg2, ::visitApp) + + override fun visit(expr: KStringIndexOfRegexExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, expr.arg2, ::visitApp) + + override fun visit(expr: KStringReplaceExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, expr.arg2, ::visitApp) + + override fun visit(expr: KStringReplaceAllExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, expr.arg2, ::visitApp) + + override fun visit(expr: KStringReplaceWithRegexExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, expr.arg2, ::visitApp) + + override fun visit(expr: KStringReplaceAllWithRegexExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, expr.arg2, ::visitApp) + + override fun visit(expr: KStringToLowerExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KStringToUpperExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KStringReverseExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KStringIsDigitExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KStringToCodeExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KStringFromCodeExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KStringToIntExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KStringFromIntExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + // regex visitors + override fun visit(expr: KRegexConcatExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KRegexUnionExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KRegexIntersectionExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KRegexStarExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KRegexCrossExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KRegexDifferenceExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KRegexComplementExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KRegexOptionExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KRegexRangeExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg0, expr.arg1, ::visitApp) + + override fun visit(expr: KRegexPowerExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + + override fun visit(expr: KRegexLoopExpr): KExprVisitResult = + visitExprAfterVisitedDefault(expr, expr.arg, ::visitApp) + // quantified expressions override fun visit(expr: KExistentialQuantifier): KExprVisitResult = visitExprAfterVisitedDefault(expr, expr.body, ::visitExpr) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KTransformer.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KTransformer.kt index dc68dd567..7d90e3299 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KTransformer.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KTransformer.kt @@ -150,6 +150,48 @@ import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar import io.ksmt.sort.KArithSort import io.ksmt.sort.KArray2Sort import io.ksmt.sort.KArray3Sort @@ -171,6 +213,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort @@ -412,6 +456,52 @@ interface KTransformer : KTransformerBase { override fun transform(expr: KIsIntRealExpr): KExpr = transformApp(expr) override fun transform(expr: KRealNumExpr): KExpr = transformValue(expr) + // string transformers + override fun transform(expr: KStringConcatExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringLenExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringToRegexExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringInRegexExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringSuffixOfExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringPrefixOfExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringLtExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringLeExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringGtExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringGeExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringContainsExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringSingletonSubExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringSubExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringIndexOfExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringIndexOfRegexExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringReplaceExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringReplaceAllExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringReplaceWithRegexExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringReplaceAllWithRegexExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringToLowerExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringToUpperExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringReverseExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringIsDigitExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringToCodeExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringFromCodeExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringToIntExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringFromIntExpr): KExpr = transformApp(expr) + override fun transform(expr: KStringLiteralExpr): KExpr = transformValue(expr) + + // regex transformers + override fun transform(expr: KRegexConcatExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexUnionExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexIntersectionExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexStarExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexCrossExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexDifferenceExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexComplementExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexOptionExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexRangeExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexPowerExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexLoopExpr): KExpr = transformApp(expr) + override fun transform(expr: KRegexEpsilon): KExpr = transformValue(expr) + override fun transform(expr: KRegexAll): KExpr = transformValue(expr) + override fun transform(expr: KRegexAllChar): KExpr = transformValue(expr) + // quantifier transformers override fun transform(expr: KExistentialQuantifier): KExpr = with(ctx) { val body = expr.body.accept(this@KTransformer) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KTransformerBase.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KTransformerBase.kt index 8178548b6..ffaef6a28 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KTransformerBase.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KTransformerBase.kt @@ -141,6 +141,48 @@ import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar import io.ksmt.sort.KArithSort import io.ksmt.sort.KArray2Sort import io.ksmt.sort.KArray3Sort @@ -162,10 +204,11 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort - interface KTransformerBase { fun apply(expr: KExpr): KExpr = expr.accept(this) @@ -341,6 +384,52 @@ interface KTransformerBase { fun transform(expr: KIsIntRealExpr): KExpr fun transform(expr: KRealNumExpr): KExpr + // string transformers + fun transform(expr: KStringConcatExpr): KExpr + fun transform(expr: KStringLenExpr): KExpr + fun transform(expr: KStringToRegexExpr): KExpr + fun transform(expr: KStringInRegexExpr): KExpr + fun transform(expr: KStringSuffixOfExpr): KExpr + fun transform(expr: KStringPrefixOfExpr): KExpr + fun transform(expr: KStringLtExpr): KExpr + fun transform(expr: KStringLeExpr): KExpr + fun transform(expr: KStringGtExpr): KExpr + fun transform(expr: KStringGeExpr): KExpr + fun transform(expr: KStringContainsExpr): KExpr + fun transform(expr: KStringSingletonSubExpr): KExpr + fun transform(expr: KStringSubExpr): KExpr + fun transform(expr: KStringIndexOfExpr): KExpr + fun transform(expr: KStringIndexOfRegexExpr): KExpr + fun transform(expr: KStringReplaceExpr): KExpr + fun transform(expr: KStringReplaceAllExpr): KExpr + fun transform(expr: KStringReplaceWithRegexExpr): KExpr + fun transform(expr: KStringReplaceAllWithRegexExpr): KExpr + fun transform(expr: KStringToLowerExpr): KExpr + fun transform(expr: KStringToUpperExpr): KExpr + fun transform(expr: KStringReverseExpr): KExpr + fun transform(expr: KStringIsDigitExpr): KExpr + fun transform(expr: KStringToCodeExpr): KExpr + fun transform(expr: KStringFromCodeExpr): KExpr + fun transform(expr: KStringToIntExpr): KExpr + fun transform(expr: KStringFromIntExpr): KExpr + fun transform(expr: KStringLiteralExpr): KExpr + + // regex transformers + fun transform(expr: KRegexConcatExpr): KExpr + fun transform(expr: KRegexUnionExpr): KExpr + fun transform(expr: KRegexIntersectionExpr): KExpr + fun transform(expr: KRegexStarExpr): KExpr + fun transform(expr: KRegexCrossExpr): KExpr + fun transform(expr: KRegexDifferenceExpr): KExpr + fun transform(expr: KRegexComplementExpr): KExpr + fun transform(expr: KRegexOptionExpr): KExpr + fun transform(expr: KRegexRangeExpr): KExpr + fun transform(expr: KRegexPowerExpr): KExpr + fun transform(expr: KRegexLoopExpr): KExpr + fun transform(expr: KRegexEpsilon): KExpr + fun transform(expr: KRegexAll): KExpr + fun transform(expr: KRegexAllChar): KExpr + // quantifier transformers fun transform(expr: KExistentialQuantifier): KExpr fun transform(expr: KUniversalQuantifier): KExpr 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 index 3f114a9e1..0c7a1e140 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KVisitor.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/transformer/KVisitor.kt @@ -149,6 +149,48 @@ import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar import io.ksmt.sort.KArithSort import io.ksmt.sort.KArray2Sort import io.ksmt.sort.KArray3Sort @@ -170,6 +212,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort @@ -614,6 +658,96 @@ interface KVisitor : KTransformer { override fun transform(expr: KIsIntRealExpr): KExpr = visitExpr(expr, ::visit) override fun transform(expr: KRealNumExpr): KExpr = visitExpr(expr, ::visit) + // string visitors + fun visit(expr: KStringConcatExpr): V = visitApp(expr) + fun visit(expr: KStringLenExpr): V = visitApp(expr) + fun visit(expr: KStringToRegexExpr): V = visitApp(expr) + fun visit(expr: KStringInRegexExpr): V = visitApp(expr) + fun visit(expr: KStringSuffixOfExpr): V = visitApp(expr) + fun visit(expr: KStringPrefixOfExpr): V = visitApp(expr) + fun visit(expr: KStringLtExpr): V = visitApp(expr) + fun visit(expr: KStringLeExpr): V = visitApp(expr) + fun visit(expr: KStringGtExpr): V = visitApp(expr) + fun visit(expr: KStringGeExpr): V = visitApp(expr) + fun visit(expr: KStringContainsExpr): V = visitApp(expr) + fun visit(expr: KStringSingletonSubExpr): V = visitApp(expr) + fun visit(expr: KStringSubExpr): V = visitApp(expr) + fun visit(expr: KStringIndexOfExpr): V = visitApp(expr) + fun visit(expr: KStringIndexOfRegexExpr): V = visitApp(expr) + fun visit(expr: KStringReplaceExpr): V = visitApp(expr) + fun visit(expr: KStringReplaceAllExpr): V = visitApp(expr) + fun visit(expr: KStringReplaceWithRegexExpr): V = visitApp(expr) + fun visit(expr: KStringReplaceAllWithRegexExpr): V = visitApp(expr) + fun visit(expr: KStringToLowerExpr): V = visitApp(expr) + fun visit(expr: KStringToUpperExpr): V = visitApp(expr) + fun visit(expr: KStringReverseExpr): V = visitApp(expr) + fun visit(expr: KStringIsDigitExpr): V = visitApp(expr) + fun visit(expr: KStringToCodeExpr): V = visitApp(expr) + fun visit(expr: KStringFromCodeExpr): V = visitApp(expr) + fun visit(expr: KStringToIntExpr): V = visitApp(expr) + fun visit(expr: KStringFromIntExpr): V = visitApp(expr) + fun visit(expr: KStringLiteralExpr): V = visitValue(expr) + + override fun transform(expr: KStringConcatExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringLenExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringToRegexExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringInRegexExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringSuffixOfExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringPrefixOfExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringLtExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringLeExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringGtExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringGeExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringContainsExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringSingletonSubExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringSubExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringIndexOfExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringIndexOfRegexExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringReplaceExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringReplaceAllExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringReplaceWithRegexExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringReplaceAllWithRegexExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringToLowerExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringToUpperExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringReverseExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringIsDigitExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringToCodeExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringFromCodeExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringToIntExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringFromIntExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KStringLiteralExpr): KExpr = visitExpr(expr, ::visit) + + // regex visitors + fun visit(expr: KRegexConcatExpr): V = visitApp(expr) + fun visit(expr: KRegexUnionExpr): V = visitApp(expr) + fun visit(expr: KRegexIntersectionExpr): V = visitApp(expr) + fun visit(expr: KRegexStarExpr): V = visitApp(expr) + fun visit(expr: KRegexCrossExpr): V = visitApp(expr) + fun visit(expr: KRegexDifferenceExpr): V = visitApp(expr) + fun visit(expr: KRegexComplementExpr): V = visitApp(expr) + fun visit(expr: KRegexOptionExpr): V = visitApp(expr) + fun visit(expr: KRegexRangeExpr): V = visitApp(expr) + fun visit(expr: KRegexPowerExpr): V = visitApp(expr) + fun visit(expr: KRegexLoopExpr): V = visitApp(expr) + fun visit(expr: KRegexEpsilon): V = visitValue(expr) + fun visit(expr: KRegexAll): V = visitValue(expr) + fun visit(expr: KRegexAllChar): V = visitValue(expr) + + override fun transform(expr: KRegexConcatExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexUnionExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexIntersectionExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexStarExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexCrossExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexDifferenceExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexComplementExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexOptionExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexRangeExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexPowerExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexLoopExpr): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexEpsilon): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexAll): KExpr = visitExpr(expr, ::visit) + override fun transform(expr: KRegexAllChar): KExpr = visitExpr(expr, ::visit) + // quantifier visitors fun visit(expr: KExistentialQuantifier): V = visitExpr(expr) fun visit(expr: KUniversalQuantifier): V = visitExpr(expr) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/solver/KTheory.kt b/ksmt-core/src/main/kotlin/io/ksmt/solver/KTheory.kt index bee24e454..679348a25 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/solver/KTheory.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/solver/KTheory.kt @@ -8,13 +8,15 @@ import io.ksmt.solver.KTheory.LRA import io.ksmt.solver.KTheory.NIA import io.ksmt.solver.KTheory.NRA import io.ksmt.solver.KTheory.UF +import io.ksmt.solver.KTheory.S /** * SMT theory * */ enum class KTheory { UF, BV, FP, Array, - LIA, NIA, LRA, NRA + LIA, NIA, LRA, NRA, + S } @Suppress("ComplexMethod", "ComplexCondition") @@ -55,6 +57,10 @@ fun Set?.smtLib2String(quantifiersAllowed: Boolean = false): String = b append("FP") } + if (S in theories) { + append("S") + } + if (LIA in theories || NIA in theories || LRA in theories || NRA in theories) { val hasNonLinear = NIA in theories || NRA in theories val hasReal = LRA in theories || NRA in theories @@ -76,4 +82,5 @@ fun Set?.smtLib2String(quantifiersAllowed: Boolean = false): String = b append("A") } + } diff --git a/ksmt-core/src/main/kotlin/io/ksmt/sort/KSort.kt b/ksmt-core/src/main/kotlin/io/ksmt/sort/KSort.kt index 75f00a0b4..43843efca 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/sort/KSort.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/sort/KSort.kt @@ -46,6 +46,30 @@ class KRealSort internal constructor(ctx: KContext) : KArithSort(ctx) { override fun equals(other: Any?): Boolean = this === other || other is KRealSort } +class KStringSort internal constructor(ctx: KContext) : KSort(ctx) { + override fun accept(visitor: KSortVisitor): T = visitor.visit(this) + + override fun print(builder: StringBuilder) { + builder.append("String") + } + + override fun hashCode(): Int = hash(javaClass) + + override fun equals(other: Any?): Boolean = this === other || other is KStringSort +} + +class KRegexSort internal constructor(ctx: KContext) : KSort(ctx) { + override fun accept(visitor: KSortVisitor): T = visitor.visit(this) + + override fun print(builder: StringBuilder) { + builder.append("Regex") + } + + override fun hashCode(): Int = hash(javaClass) + + override fun equals(other: Any?): Boolean = this === other || other is KRegexSort +} + sealed class KArraySortBase(ctx: KContext) : KSort(ctx) { abstract val domainSorts: List abstract val range: R diff --git a/ksmt-core/src/main/kotlin/io/ksmt/sort/KSortVisitor.kt b/ksmt-core/src/main/kotlin/io/ksmt/sort/KSortVisitor.kt index d44cb63a0..2260ed936 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/sort/KSortVisitor.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/sort/KSortVisitor.kt @@ -5,6 +5,8 @@ interface KSortVisitor { fun visit(sort: KBoolSort): T fun visit(sort: KIntSort): T fun visit(sort: KRealSort): T + fun visit(sort: KStringSort): T + fun visit(sort: KRegexSort): T fun visit(sort: S): T fun visit(sort: S): T fun visit(sort: KArraySort): T diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/DefaultValueSampler.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/DefaultValueSampler.kt index f4df37e27..e17464256 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/utils/DefaultValueSampler.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/utils/DefaultValueSampler.kt @@ -2,18 +2,20 @@ package io.ksmt.utils import io.ksmt.KContext import io.ksmt.expr.KExpr -import io.ksmt.sort.KArray2Sort -import io.ksmt.sort.KArray3Sort -import io.ksmt.sort.KArrayNSort -import io.ksmt.sort.KArraySort +import io.ksmt.sort.KSortVisitor +import io.ksmt.sort.KSort import io.ksmt.sort.KBoolSort -import io.ksmt.sort.KBvSort -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.KSortVisitor +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort +import io.ksmt.sort.KBvSort +import io.ksmt.sort.KFpSort +import io.ksmt.sort.KFpRoundingModeSort +import io.ksmt.sort.KArraySort +import io.ksmt.sort.KArray2Sort +import io.ksmt.sort.KArray3Sort +import io.ksmt.sort.KArrayNSort import io.ksmt.sort.KUninterpretedSort open class DefaultValueSampler(val ctx: KContext) : KSortVisitor> { @@ -26,6 +28,12 @@ open class DefaultValueSampler(val ctx: KContext) : KSortVisitor> { override fun visit(sort: KRealSort): KExpr<*> = ctx.realSortDefaultValue() + override fun visit(sort: KStringSort): KExpr<*> = + ctx.stringSortDefaultValue() + + override fun visit(sort: KRegexSort): KExpr<*> = + ctx.regexSortDefaultValue() + override fun visit(sort: S): KExpr<*> = ctx.bvSortDefaultValue(sort) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/utils/KExprTheoryRequirement.kt b/ksmt-core/src/main/kotlin/io/ksmt/utils/KExprTheoryRequirement.kt index eeb205f10..c9bd6ccc5 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/utils/KExprTheoryRequirement.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/utils/KExprTheoryRequirement.kt @@ -18,19 +18,22 @@ import io.ksmt.solver.KTheory.LRA import io.ksmt.solver.KTheory.NIA import io.ksmt.solver.KTheory.NRA import io.ksmt.solver.KTheory.UF +import io.ksmt.solver.KTheory.S +import io.ksmt.sort.KSortVisitor +import io.ksmt.sort.KSort +import io.ksmt.sort.KBoolSort import io.ksmt.sort.KArithSort +import io.ksmt.sort.KIntSort +import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort +import io.ksmt.sort.KBvSort +import io.ksmt.sort.KFpSort +import io.ksmt.sort.KFpRoundingModeSort +import io.ksmt.sort.KArraySort import io.ksmt.sort.KArray2Sort import io.ksmt.sort.KArray3Sort import io.ksmt.sort.KArrayNSort -import io.ksmt.sort.KArraySort -import io.ksmt.sort.KBoolSort -import io.ksmt.sort.KBvSort -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.KSortVisitor import io.ksmt.sort.KUninterpretedSort class KExprTheoryRequirement(ctx: KContext) : KNonRecursiveTransformer(ctx) { @@ -90,6 +93,14 @@ class KExprTheoryRequirement(ctx: KContext) : KNonRecursiveTransformer(ctx) { usedTheories += LRA } + override fun visit(sort: KStringSort) { + usedTheories += S + } + + override fun visit(sort: KRegexSort) { + usedTheories += S + } + override fun visit(sort: S) { usedTheories += BV } diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt index 124227a45..b91f348e4 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5Context.kt @@ -27,6 +27,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -373,6 +375,10 @@ class KCvc5Context( override fun visit(sort: KRealSort) = Unit + override fun visit(sort: KStringSort) = Unit + + override fun visit(sort: KRegexSort) = Unit + override fun visit(sort: S) = Unit override fun visit(sort: S) = Unit diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5DeclInternalizer.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5DeclInternalizer.kt index 38c765b58..5364120c6 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5DeclInternalizer.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5DeclInternalizer.kt @@ -3,8 +3,11 @@ package io.ksmt.solver.cvc5 import io.github.cvc5.Solver import io.github.cvc5.Term import io.ksmt.decl.KConstDecl +import io.ksmt.decl.KDecl import io.ksmt.decl.KDeclVisitor import io.ksmt.decl.KFuncDecl +import io.ksmt.solver.KSolverUnsupportedFeatureException +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort open class KCvc5DeclInternalizer( @@ -29,9 +32,16 @@ open class KCvc5DeclInternalizer( } override fun visit(decl: KConstDecl): Term = cvc5Ctx.internalizeDecl(decl) { + checkConstDeclSort(decl) cvc5Ctx.addDeclaration(decl) val sort = decl.sort.accept(sortInternalizer) tm.builder { mkConst(sort, decl.name) } } + + private fun checkConstDeclSort(decl: KDecl) { + if (decl.sort is KRegexSort) { + throw KSolverUnsupportedFeatureException("Regex constants unsupported in cvc5") + } + } } diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt index 0084e0686..7b9728edd 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprConverter.kt @@ -26,6 +26,7 @@ import io.ksmt.sort.KArraySortBase import io.ksmt.sort.KBoolSort import io.ksmt.sort.KBv1Sort import io.ksmt.sort.KBvSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort @@ -82,6 +83,7 @@ open class KCvc5ExprConverter( Kind.CONST_ARRAY -> convertNativeConstArrayExpr(expr) Kind.CONST_INTEGER -> convertNativeConstIntegerExpr(expr) Kind.CONST_RATIONAL -> convertNativeConstRealExpr(expr) + Kind.CONST_STRING -> convertNativeConstStringExpr(expr) Kind.CONSTANT -> convert { expr.convertDecl().apply(emptyList()) } Kind.UNINTERPRETED_SORT_VALUE -> convert { model ?: error("Uninterpreted value without model") @@ -378,6 +380,56 @@ open class KCvc5ExprConverter( Kind.SELECT -> convertNativeArraySelect(expr) Kind.STORE -> convertNativeArrayStore(expr) + // strings + Kind.STRING_CONCAT -> expr.convert(::mkStringConcat) + Kind.STRING_LENGTH -> expr.convert(::mkStringLen) + Kind.STRING_TO_REGEXP -> expr.convert(::mkStringToRegex) + Kind.STRING_IN_REGEXP -> expr.convert(::mkStringInRegex) + Kind.STRING_SUFFIX -> expr.convert(::mkStringSuffixOf) + Kind.STRING_PREFIX -> expr.convert(::mkStringPrefixOf) + Kind.STRING_LT -> expr.convert(::mkStringLt) + Kind.STRING_LEQ -> expr.convert(::mkStringLe) + Kind.STRING_CONTAINS -> expr.convert(::mkStringContains) + Kind.STRING_CHARAT -> expr.convert(::mkStringSingletonSub) + Kind.STRING_SUBSTR -> expr.convert(::mkStringSub) + Kind.STRING_INDEXOF -> expr.convert(::mkStringIndexOf) + Kind.STRING_REPLACE -> expr.convert(::mkStringReplace) + Kind.STRING_REPLACE_ALL -> expr.convert(::mkStringReplaceAll) + Kind.STRING_REPLACE_RE -> expr.convert(::mkStringReplaceWithRegex) + Kind.STRING_REPLACE_RE_ALL -> expr.convert(::mkStringReplaceAllWithRegex) + Kind.STRING_IS_DIGIT -> expr.convert(::mkStringIsDigit) + Kind.STRING_TO_CODE -> expr.convert(::mkStringToCode) + Kind.STRING_FROM_CODE -> expr.convert(::mkStringFromCode) + Kind.STRING_TO_INT -> expr.convert(::mkStringToInt) + Kind.STRING_FROM_INT -> expr.convert(::mkStringFromInt) + Kind.STRING_INDEXOF_RE -> expr.convert(::mkStringIndexOfRegex) + Kind.STRING_TO_LOWER -> expr.convert(::mkStringToLower) + Kind.STRING_TO_UPPER -> expr.convert(::mkStringToUpper) + Kind.STRING_REV -> expr.convert(::mkStringReverse) + Kind.STRING_UPDATE -> throw KSolverUnsupportedFeatureException( + "No direct mapping of ${Kind.STRING_UPDATE} in ksmt" + ) + + // regex + Kind.REGEXP_CONCAT -> expr.convert(::mkRegexConcat) + Kind.REGEXP_UNION -> expr.convert(::mkRegexUnion) + Kind.REGEXP_INTER -> expr.convert(::mkRegexIntersection) + Kind.REGEXP_STAR -> expr.convert(::mkRegexStar) + Kind.REGEXP_PLUS -> expr.convert(::mkRegexCross) + Kind.REGEXP_DIFF -> expr.convert(::mkRegexDifference) + Kind.REGEXP_COMPLEMENT -> expr.convert(::mkRegexComplement) + Kind.REGEXP_OPT -> expr.convert(::mkRegexOption) + Kind.REGEXP_NONE -> convert { mkRegexEpsilon() } + Kind.REGEXP_ALL -> convert { mkRegexAll() } + Kind.REGEXP_ALLCHAR -> convert { mkRegexAllChar() } + Kind.REGEXP_RANGE -> expr.convert(::mkRegexRange) + Kind.REGEXP_REPEAT -> expr.convert { regexExpr: KExpr -> + mkRegexPower(expr.regexRepeatTime, regexExpr) + } + Kind.REGEXP_LOOP -> expr.convert { regexExpr: KExpr -> + mkRegexLoop(expr.regexLoopFrom, expr.regexLoopTo, regexExpr) + } + Kind.EQ_RANGE -> throw KSolverUnsupportedFeatureException("EQ_RANGE is not supported") Kind.APPLY_CONSTRUCTOR, @@ -452,51 +504,6 @@ open class KCvc5ExprConverter( Kind.TABLE_JOIN, Kind.TABLE_GROUP -> throw KSolverUnsupportedFeatureException("currently ksmt does not support tables") - Kind.STRING_CONCAT, - Kind.STRING_IN_REGEXP, - Kind.STRING_LENGTH, - Kind.STRING_SUBSTR, - Kind.STRING_UPDATE, - Kind.STRING_CHARAT, - Kind.STRING_CONTAINS, - Kind.STRING_INDEXOF, - Kind.STRING_INDEXOF_RE, - Kind.STRING_REPLACE, - Kind.STRING_REPLACE_ALL, - Kind.STRING_REPLACE_RE, - Kind.STRING_REPLACE_RE_ALL, - Kind.STRING_TO_LOWER, - Kind.STRING_TO_UPPER, - Kind.STRING_REV, - Kind.STRING_TO_CODE, - Kind.STRING_FROM_CODE, - Kind.STRING_LT, - Kind.STRING_LEQ, - Kind.STRING_PREFIX, - Kind.STRING_SUFFIX, - Kind.STRING_IS_DIGIT, - Kind.STRING_FROM_INT, - Kind.STRING_TO_INT, - Kind.CONST_STRING, - Kind.STRING_TO_REGEXP -> throw KSolverUnsupportedFeatureException("currently ksmt does not support strings") - - Kind.REGEXP_CONCAT, - Kind.REGEXP_UNION, - Kind.REGEXP_INTER, - Kind.REGEXP_DIFF, - Kind.REGEXP_STAR, - Kind.REGEXP_PLUS, - Kind.REGEXP_OPT, - Kind.REGEXP_RANGE, - Kind.REGEXP_REPEAT, - Kind.REGEXP_LOOP, - Kind.REGEXP_NONE, - Kind.REGEXP_ALL, - Kind.REGEXP_ALLCHAR, - Kind.REGEXP_COMPLEMENT -> throw KSolverUnsupportedFeatureException( - "currently ksmt does not support regular expressions" - ) - Kind.SEQ_CONCAT, Kind.SEQ_LENGTH, Kind.SEQ_EXTRACT, @@ -710,6 +717,12 @@ open class KCvc5ExprConverter( } } + private fun convertNativeConstStringExpr(expr: Term): ExprConversionResult = with(ctx) { + convert { + mkStringLiteral(expr.stringValue) + } + } + private fun convertNativeBitvectorConstExpr(expr: Term): ExprConversionResult = with(ctx) { convert { mkBv(expr.bitVectorValue, expr.bitVectorValue.length.toUInt()) } } @@ -807,6 +820,8 @@ open class KCvc5ExprConverter( sort.isBitVector -> mkBvSort(sort.bitVectorSize.toUInt()) sort.isInteger -> intSort sort.isReal -> realSort + sort.isString -> stringSort + sort.isRegExp -> regexSort sort.isArray -> mkArrayAnySort( domain = convertArrayDomainSort(tm.sortOp(sort) { arrayIndexSort }), range = tm.sortOp(sort) { arrayElementSort }.convertSort() @@ -1009,4 +1024,28 @@ open class KCvc5ExprConverter( require(kind == Kind.DIVISIBLE) { "Required op is ${Kind.DIVISIBLE}, but was $kind" } return termOpArg(this, 0).integerValue.toInt() } + + private val Term.regexRepeatTime: Int + get() { + require(kind == Kind.REGEXP_REPEAT) { + "Required op is ${Kind.REGEXP_REPEAT}, but was $kind" + } + return termOpArg(this, 0).integerValue.toInt() + } + + private val Term.regexLoopFrom: Int + get() { + require(kind == Kind.REGEXP_LOOP) { + "Required op is ${Kind.REGEXP_LOOP}, but was $kind" + } + return termOpArg(this, 0).integerValue.toInt() + } + + private val Term.regexLoopTo: Int + get() { + require(kind == Kind.REGEXP_LOOP) { + "Required op is ${Kind.REGEXP_LOOP}, but was $kind" + } + return termOpArg(this, 1).integerValue.toInt() + } } diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt index 39dae685d..2b26a96f5 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5ExprInternalizer.kt @@ -155,6 +155,48 @@ import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoOverflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoUnderflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvDivNoOverflowExpr @@ -181,6 +223,8 @@ import io.ksmt.sort.KFp64Sort import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort import io.ksmt.utils.powerOfTwo @@ -1141,6 +1185,255 @@ class KCvc5ExprInternalizer( } } + // strings + override fun transform(expr: KStringConcatExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_CONCAT, arg0, arg1) + } + } + + override fun transform(expr: KStringLenExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_LENGTH, arg) + } + } + + override fun transform(expr: KStringToRegexExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_TO_REGEXP, arg) + } + } + + override fun transform(expr: KStringInRegexExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_IN_REGEXP, arg0, arg1) + } + } + + override fun transform(expr: KStringSuffixOfExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_SUFFIX, arg0, arg1) + } + } + + override fun transform(expr: KStringPrefixOfExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_PREFIX, arg0, arg1) + } + } + + override fun transform(expr: KStringLtExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_LT, arg0, arg1) + } + } + + override fun transform(expr: KStringLeExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_LEQ, arg0, arg1) + } + } + + override fun transform(expr: KStringGtExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_LT, arg1, arg0) + } + } + + override fun transform(expr: KStringGeExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_LEQ, arg1, arg0) + } + } + + override fun transform(expr: KStringContainsExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_CONTAINS, arg0, arg1) + } + } + + override fun transform(expr: KStringSingletonSubExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.STRING_CHARAT, arg0, arg1) + } + } + + override fun transform(expr: KStringSubExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0: Term, arg1: Term, arg2: Term -> + tm.mkTerm(Kind.STRING_SUBSTR, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringIndexOfExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0: Term, arg1: Term, arg2: Term -> + tm.mkTerm(Kind.STRING_INDEXOF, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringIndexOfRegexExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0: Term, arg1: Term, arg2: Term -> + tm.mkTerm(Kind.STRING_INDEXOF_RE, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringReplaceExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0: Term, arg1: Term, arg2: Term -> + tm.mkTerm(Kind.STRING_REPLACE, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringReplaceAllExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0: Term, arg1: Term, arg2: Term -> + tm.mkTerm(Kind.STRING_REPLACE_ALL, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringReplaceWithRegexExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0: Term, arg1: Term, arg2: Term -> + tm.mkTerm(Kind.STRING_REPLACE_RE, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringReplaceAllWithRegexExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0: Term, arg1: Term, arg2: Term -> + tm.mkTerm(Kind.STRING_REPLACE_RE_ALL, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringToLowerExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_TO_LOWER, arg) + } + } + + override fun transform(expr: KStringToUpperExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_TO_UPPER, arg) + } + } + + override fun transform(expr: KStringReverseExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_REV, arg) + } + } + + override fun transform(expr: KStringIsDigitExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_IS_DIGIT, arg) + } + } + + override fun transform(expr: KStringToCodeExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_TO_CODE, arg) + } + } + + override fun transform(expr: KStringFromCodeExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_FROM_CODE, arg) + } + } + + override fun transform(expr: KStringToIntExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_TO_INT, arg) + } + } + + override fun transform(expr: KStringFromIntExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.STRING_FROM_INT, arg) + } + } + + override fun transform(expr: KStringLiteralExpr) = with(expr) { + transform { tm.builder { mkString(expr.value) } } + } + + // regex + override fun transform(expr: KRegexConcatExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.REGEXP_CONCAT, arg0, arg1) + } + } + + override fun transform(expr: KRegexUnionExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.REGEXP_UNION, arg0, arg1) + } + } + + override fun transform(expr: KRegexIntersectionExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.REGEXP_INTER, arg0, arg1) + } + } + + override fun transform(expr: KRegexStarExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.REGEXP_STAR, arg) + } + } + + override fun transform(expr: KRegexCrossExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.REGEXP_PLUS, arg) + } + } + + override fun transform(expr: KRegexDifferenceExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.REGEXP_DIFF, arg0, arg1) + } + } + + override fun transform(expr: KRegexComplementExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.REGEXP_COMPLEMENT, arg) + } + } + + override fun transform(expr: KRegexOptionExpr) = with(expr) { + transform(arg) { arg: Term -> + tm.mkTerm(Kind.REGEXP_OPT, arg) + } + } + + override fun transform(expr: KRegexRangeExpr) = with(expr) { + transform(arg0, arg1) { arg0: Term, arg1: Term -> + tm.mkTerm(Kind.REGEXP_RANGE, arg0, arg1) + } + } + + override fun transform(expr: KRegexPowerExpr) = with(expr) { + transform(arg) { arg: Term -> + val extractOp = tm.mkOp(Kind.REGEXP_REPEAT, power) + tm.mkTerm(extractOp, arg) + } + } + + override fun transform(expr: KRegexLoopExpr) = with(expr) { + transform(arg) { arg: Term -> + val extractOp = tm.mkOp(Kind.REGEXP_LOOP, from, to) + tm.mkTerm(extractOp, arg) + } + } + + override fun transform(expr: KRegexEpsilon) = with(expr) { + transform { tm.mkTerm(Kind.REGEXP_NONE) } + } + + override fun transform(expr: KRegexAll) = with(expr) { + transform { tm.mkTerm(Kind.REGEXP_ALL) } + } + + override fun transform(expr: KRegexAllChar) = with(expr) { + transform { tm.mkTerm(Kind.REGEXP_ALLCHAR) } + } + + // Quantifiers override fun transform(expr: KExistentialQuantifier) = expr.transformQuantifiedExpression(expr.bounds, expr.body, isUniversal = false) diff --git a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5SortInternalizer.kt b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5SortInternalizer.kt index 88a5a8e66..43a93d5f3 100644 --- a/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5SortInternalizer.kt +++ b/ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/ksmt/solver/cvc5/KCvc5SortInternalizer.kt @@ -11,6 +11,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -33,6 +35,14 @@ open class KCvc5SortInternalizer( tm.builder { realSort } } + override fun visit(sort: KStringSort): Sort = cvc5Ctx.internalizeSort(sort) { + tm.builder { stringSort } + } + + override fun visit(sort: KRegexSort): Sort = cvc5Ctx.internalizeSort(sort) { + tm.builder { regExpSort } + } + override fun visit(sort: KArraySort): Sort = cvc5Ctx.internalizeSort(sort) { val domain = sort.domain.internalizeCvc5Sort() diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstDeserializer.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstDeserializer.kt index 722c62d79..766b65c1f 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstDeserializer.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstDeserializer.kt @@ -12,6 +12,7 @@ import io.ksmt.sort.KArraySortBase import io.ksmt.sort.KBoolSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort import io.ksmt.utils.uncheckedCast @@ -87,11 +88,14 @@ class AstDeserializer( mkFreshFuncDecl(name, sort, argSorts as List) } + @Suppress("ComplexMethod") private fun AbstractBuffer.deserializeSort(sortKind: SortKind): KSort = with(serializationCtx.ctx) { when (sortKind) { SortKind.Bool -> boolSort SortKind.Int -> intSort SortKind.Real -> realSort + SortKind.String -> stringSort + SortKind.Regex -> regexSort SortKind.FpRM -> mkFpRoundingModeSort() SortKind.Bv -> mkBvSort(readUInt()) SortKind.Fp -> mkFpSort(readUInt(), readUInt()) @@ -276,6 +280,57 @@ class AstDeserializer( ExprKind.ToIntRealExpr -> deserialize(::mkRealToIntNoSimplify) ExprKind.IsIntRealExpr -> deserialize(::mkRealIsIntNoSimplify) ExprKind.RealNumExpr -> mkRealNum(readExpr() as KIntNumExpr, readExpr() as KIntNumExpr) + ExprKind.StringConcatExpr -> deserialize(::mkStringConcatNoSimplify) + ExprKind.StringLenExpr -> deserialize(::mkStringLenNoSimplify) + ExprKind.StringToRegexExpr -> deserialize(::mkStringToRegexNoSimplify) + ExprKind.StringInRegexExpr -> deserialize(::mkStringInRegexNoSimplify) + ExprKind.StringSuffixOfExpr -> deserialize(::mkStringSuffixOfNoSimplify) + ExprKind.StringPrefixOfExpr -> deserialize(::mkStringPrefixOfNoSimplify) + ExprKind.StringLtExpr -> deserialize(::mkStringLtNoSimplify) + ExprKind.StringLeExpr -> deserialize(::mkStringLeNoSimplify) + ExprKind.StringGtExpr -> deserialize(::mkStringGtNoSimplify) + ExprKind.StringGeExpr -> deserialize(::mkStringGeNoSimplify) + ExprKind.StringContainsExpr -> deserialize(::mkStringContainsNoSimplify) + ExprKind.StringSingletonSubExpr -> deserialize(::mkStringSingletonSubNoSimplify) + ExprKind.StringSubExpr -> deserialize(::mkStringSubNoSimplify) + ExprKind.StringIndexOfExpr -> deserialize(::mkStringIndexOfNoSimplify) + ExprKind.StringIndexOfRegexExpr -> deserialize(::mkStringIndexOfRegexNoSimplify) + ExprKind.StringReplaceExpr -> deserialize(::mkStringReplaceNoSimplify) + ExprKind.StringReplaceAllExpr -> deserialize(::mkStringReplaceAllNoSimplify) + ExprKind.StringReplaceWithRegexExpr -> deserialize(::mkStringReplaceWithRegexNoSimplify) + ExprKind.StringReplaceAllWithRegexExpr -> deserialize(::mkStringReplaceAllWithRegexNoSimplify) + ExprKind.StringToLowerExpr -> deserialize(::mkStringToLowerNoSimplify) + ExprKind.StringToUpperExpr -> deserialize(::mkStringToUpperNoSimplify) + ExprKind.StringReverseExpr -> deserialize(::mkStringReverseNoSimplify) + ExprKind.StringIsDigitExpr -> deserialize(::mkStringIsDigitNoSimplify) + ExprKind.StringToCodeExpr -> deserialize(::mkStringToCodeNoSimplify) + ExprKind.StringFromCodeExpr -> deserialize(::mkStringFromCodeNoSimplify) + ExprKind.StringToIntExpr -> deserialize(::mkStringToIntNoSimplify) + ExprKind.StringFromIntExpr -> deserialize(::mkStringFromIntNoSimplify) + ExprKind.StringLiteralExpr -> mkStringLiteral(readString()) + ExprKind.RegexConcatExpr -> deserialize(::mkRegexConcatNoSimplify) + ExprKind.RegexUnionExpr -> deserialize(::mkRegexUnionNoSimplify) + ExprKind.RegexIntersectionExpr -> deserialize(::mkRegexIntersectionNoSimplify) + ExprKind.RegexStarExpr -> deserialize(::mkRegexStarNoSimplify) + ExprKind.RegexCrossExpr -> deserialize(::mkRegexCrossNoSimplify) + ExprKind.RegexDifferenceExpr -> deserialize(::mkRegexDifferenceNoSimplify) + ExprKind.RegexComplementExpr -> deserialize(::mkRegexComplementNoSimplify) + ExprKind.RegexOptionExpr -> deserialize(::mkRegexOptionNoSimplify) + ExprKind.RegexRangeExpr -> deserialize(::mkRegexRangeNoSimplify) + ExprKind.RegexPowerExpr -> { + val expr = readExpr() + val power = readInt() + mkRegexPower(power, expr) + } + ExprKind.RegexLoopExpr -> { + val expr = readExpr() + val from = readInt() + val to = readInt() + mkRegexLoop(from, to, expr) + } + ExprKind.RegexEpsilonExpr -> mkRegexEpsilon() + ExprKind.RegexAllExpr -> mkRegexAll() + ExprKind.RegexAllCharExpr -> mkRegexAllChar() ExprKind.ExistentialQuantifier -> { val bounds = readAstArray() mkExistentialQuantifier(readExpr(), bounds as List>) diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstSerializer.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstSerializer.kt index c17d79e3c..89c3ba77e 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstSerializer.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/AstSerializer.kt @@ -147,6 +147,48 @@ import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar import io.ksmt.solver.util.KExprIntInternalizerBase import io.ksmt.sort.KArithSort import io.ksmt.sort.KArray2Sort @@ -164,6 +206,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -230,6 +274,14 @@ class AstSerializer( serializeSort(sort, SortKind.Real) {} } + override fun visit(sort: KStringSort) { + serializeSort(sort, SortKind.String) {} + } + + override fun visit(sort: KRegexSort) { + serializeSort(sort, SortKind.Regex) {} + } + override fun visit(sort: S) { serializeSort(sort, SortKind.Bv) { writeUInt(sort.sizeBits) @@ -1098,6 +1150,187 @@ class AstSerializer( serialize(numerator, denominator) } + override fun transform(expr: KStringConcatExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringLenExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringToRegexExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringInRegexExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringSuffixOfExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringPrefixOfExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringLtExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringLeExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringGtExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringGeExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringContainsExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringSingletonSubExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KStringSubExpr) = with(expr) { + serialize(arg0, arg1, arg2) + } + + override fun transform(expr: KStringIndexOfExpr) = with(expr) { + serialize(arg0, arg1, arg2) + } + + override fun transform(expr: KStringIndexOfRegexExpr) = with(expr) { + serialize(arg0, arg1, arg2) + } + + override fun transform(expr: KStringReplaceExpr) = with(expr) { + serialize(arg0, arg1, arg2) + } + + override fun transform(expr: KStringReplaceAllExpr) = with(expr) { + serialize(arg0, arg1, arg2) + } + + override fun transform(expr: KStringReplaceWithRegexExpr) = with(expr) { + serialize(arg0, arg1, arg2) + } + + override fun transform(expr: KStringReplaceAllWithRegexExpr) = with(expr) { + serialize(arg0, arg1, arg2) + } + + override fun transform(expr: KStringToLowerExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringToUpperExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringReverseExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringIsDigitExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringToCodeExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringFromCodeExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringToIntExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringFromIntExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KStringLiteralExpr) = with(expr) { + transform { + writeExpr { writeString(value) } + } + } + + override fun transform(expr: KRegexConcatExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KRegexUnionExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KRegexIntersectionExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KRegexStarExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KRegexCrossExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KRegexDifferenceExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KRegexComplementExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KRegexOptionExpr) = with(expr) { + serialize(arg) + } + + override fun transform(expr: KRegexRangeExpr) = with(expr) { + serialize(arg0, arg1) + } + + override fun transform(expr: KRegexPowerExpr) = with(expr) { + transform(arg) { idx -> + writeExpr { + writeAst(idx) + writeInt(power) + } + } + } + + override fun transform(expr: KRegexLoopExpr) = with(expr) { + transform(arg) { idx -> + writeExpr { + writeAst(idx) + writeInt(from) + writeInt(to) + } + } + } + + override fun transform(expr: KRegexEpsilon) = with(expr) { + serialize() + } + + override fun transform(expr: KRegexAll) = with(expr) { + serialize() + } + + override fun transform(expr: KRegexAllChar) = with(expr) { + serialize() + } + override fun transform(expr: KExistentialQuantifier) = with(expr) { transform(body) { body: Int -> val bounds = bounds.map { it.serializeDecl() } diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/ExprKind.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/ExprKind.kt index a284a4f5c..ee1dcccb7 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/ExprKind.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/ExprKind.kt @@ -138,6 +138,48 @@ enum class ExprKind { ToIntRealExpr, IsIntRealExpr, RealNumExpr, + StringConcatExpr, + StringLenExpr, + StringToRegexExpr, + StringInRegexExpr, + StringSuffixOfExpr, + StringPrefixOfExpr, + StringLtExpr, + StringLeExpr, + StringGtExpr, + StringGeExpr, + StringContainsExpr, + StringSingletonSubExpr, + StringSubExpr, + StringIndexOfExpr, + StringIndexOfRegexExpr, + StringReplaceExpr, + StringReplaceAllExpr, + StringReplaceWithRegexExpr, + StringReplaceAllWithRegexExpr, + StringToLowerExpr, + StringToUpperExpr, + StringReverseExpr, + StringIsDigitExpr, + StringToCodeExpr, + StringFromCodeExpr, + StringToIntExpr, + StringFromIntExpr, + StringLiteralExpr, + RegexConcatExpr, + RegexUnionExpr, + RegexIntersectionExpr, + RegexStarExpr, + RegexCrossExpr, + RegexDifferenceExpr, + RegexComplementExpr, + RegexOptionExpr, + RegexRangeExpr, + RegexPowerExpr, + RegexLoopExpr, + RegexEpsilonExpr, + RegexAllExpr, + RegexAllCharExpr, ExistentialQuantifier, UniversalQuantifier, UninterpretedSortValue, diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/ExprKindMapper.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/ExprKindMapper.kt index 555ad49af..4fd2c1e92 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/ExprKindMapper.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/ExprKindMapper.kt @@ -141,6 +141,48 @@ import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar import io.ksmt.expr.transformer.KTransformerBase import io.ksmt.sort.KArithSort import io.ksmt.sort.KArray2Sort @@ -163,6 +205,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort @@ -627,6 +671,132 @@ class ExprKindMapper: KTransformerBase { override fun transform(expr: KRealNumExpr): KExpr = expr.kind(ExprKind.RealNumExpr) + override fun transform(expr: KStringConcatExpr): KExpr = expr.kind(ExprKind.StringConcatExpr) + + + override fun transform(expr: KStringLenExpr): KExpr = expr.kind(ExprKind.StringLenExpr) + + + override fun transform(expr: KStringToRegexExpr): KExpr = expr.kind(ExprKind.StringToRegexExpr) + + + override fun transform(expr: KStringInRegexExpr): KExpr = expr.kind(ExprKind.StringInRegexExpr) + + + override fun transform(expr: KStringSuffixOfExpr): KExpr = expr.kind(ExprKind.StringSuffixOfExpr) + + + override fun transform(expr: KStringPrefixOfExpr): KExpr = expr.kind(ExprKind.StringPrefixOfExpr) + + + override fun transform(expr: KStringLtExpr): KExpr = expr.kind(ExprKind.StringLtExpr) + + + override fun transform(expr: KStringLeExpr): KExpr = expr.kind(ExprKind.StringLeExpr) + + + override fun transform(expr: KStringGtExpr): KExpr = expr.kind(ExprKind.StringGtExpr) + + + override fun transform(expr: KStringGeExpr): KExpr = expr.kind(ExprKind.StringGeExpr) + + + override fun transform(expr: KStringContainsExpr): KExpr = expr.kind(ExprKind.StringContainsExpr) + + + override fun transform(expr: KStringSingletonSubExpr): KExpr = expr.kind(ExprKind.StringSingletonSubExpr) + + + override fun transform(expr: KStringSubExpr): KExpr = expr.kind(ExprKind.StringSubExpr) + + + override fun transform(expr: KStringIndexOfExpr): KExpr = expr.kind(ExprKind.StringIndexOfExpr) + + + override fun transform(expr: KStringIndexOfRegexExpr): KExpr = expr.kind(ExprKind.StringIndexOfRegexExpr) + + + override fun transform(expr: KStringReplaceExpr): KExpr = expr.kind(ExprKind.StringReplaceExpr) + + + override fun transform(expr: KStringReplaceAllExpr): KExpr = expr.kind(ExprKind.StringReplaceAllExpr) + + + override fun transform(expr: KStringReplaceWithRegexExpr): KExpr = expr.kind(ExprKind.StringReplaceWithRegexExpr) + + + override fun transform(expr: KStringReplaceAllWithRegexExpr): KExpr = expr.kind(ExprKind.StringReplaceAllWithRegexExpr) + + + override fun transform(expr: KStringToLowerExpr): KExpr = expr.kind(ExprKind.StringToLowerExpr) + + + override fun transform(expr: KStringToUpperExpr): KExpr = expr.kind(ExprKind.StringToUpperExpr) + + + override fun transform(expr: KStringReverseExpr): KExpr = expr.kind(ExprKind.StringReverseExpr) + + + override fun transform(expr: KStringIsDigitExpr): KExpr = expr.kind(ExprKind.StringIsDigitExpr) + + + override fun transform(expr: KStringToCodeExpr): KExpr = expr.kind(ExprKind.StringToCodeExpr) + + + override fun transform(expr: KStringFromCodeExpr): KExpr = expr.kind(ExprKind.StringFromCodeExpr) + + + override fun transform(expr: KStringToIntExpr): KExpr = expr.kind(ExprKind.StringToIntExpr) + + + override fun transform(expr: KStringFromIntExpr): KExpr = expr.kind(ExprKind.StringFromIntExpr) + + + override fun transform(expr: KStringLiteralExpr): KExpr = expr.kind(ExprKind.StringLiteralExpr) + + + override fun transform(expr: KRegexConcatExpr): KExpr = expr.kind(ExprKind.RegexConcatExpr) + + + override fun transform(expr: KRegexUnionExpr): KExpr = expr.kind(ExprKind.RegexUnionExpr) + + + override fun transform(expr: KRegexIntersectionExpr): KExpr = expr.kind(ExprKind.RegexIntersectionExpr) + + + override fun transform(expr: KRegexStarExpr): KExpr = expr.kind(ExprKind.RegexStarExpr) + + + override fun transform(expr: KRegexCrossExpr): KExpr = expr.kind(ExprKind.RegexCrossExpr) + + + override fun transform(expr: KRegexComplementExpr): KExpr = expr.kind(ExprKind.RegexComplementExpr) + + + override fun transform(expr: KRegexDifferenceExpr): KExpr = expr.kind(ExprKind.RegexDifferenceExpr) + + + override fun transform(expr: KRegexOptionExpr): KExpr = expr.kind(ExprKind.RegexOptionExpr) + + + override fun transform(expr: KRegexRangeExpr): KExpr = expr.kind(ExprKind.RegexRangeExpr) + + + override fun transform(expr: KRegexPowerExpr): KExpr = expr.kind(ExprKind.RegexPowerExpr) + + + override fun transform(expr: KRegexLoopExpr): KExpr = expr.kind(ExprKind.RegexLoopExpr) + + + override fun transform(expr: KRegexEpsilon): KExpr = expr.kind(ExprKind.RegexEpsilonExpr) + + + override fun transform(expr: KRegexAll): KExpr = expr.kind(ExprKind.RegexAllExpr) + + + override fun transform(expr: KRegexAllChar): KExpr = expr.kind(ExprKind.RegexAllCharExpr) + + override fun transform(expr: KExistentialQuantifier): KExpr = expr.kind(ExprKind.ExistentialQuantifier) diff --git a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/SortKind.kt b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/SortKind.kt index cdfac3d24..a24f38c70 100644 --- a/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/SortKind.kt +++ b/ksmt-runner/src/main/kotlin/io/ksmt/runner/serializer/SortKind.kt @@ -1,5 +1,6 @@ package io.ksmt.runner.serializer enum class SortKind { - Bool, Int, Real, Bv, Fp, Array, Array2, Array3, ArrayN, FpRM, Uninterpreted + Bool, Int, Real, Bv, Fp, Array, Array2, Array3, ArrayN, FpRM, Uninterpreted, + String, Regex } diff --git a/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/FpToBvTransformer.kt b/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/FpToBvTransformer.kt index be044b27f..bd76840bc 100644 --- a/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/FpToBvTransformer.kt +++ b/ksmt-symfpu/src/main/kotlin/io/ksmt/symfpu/solver/FpToBvTransformer.kt @@ -69,6 +69,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -595,6 +597,8 @@ class FpToBvTransformer(ctx: KContext, private val packedBvOptimization: Boolean override fun visit(sort: KBoolSort): Boolean = false override fun visit(sort: KIntSort): Boolean = false override fun visit(sort: KRealSort): Boolean = false + override fun visit(sort: KStringSort): Boolean = false + override fun visit(sort: KRegexSort): Boolean = false override fun visit(sort: S): Boolean = false } @@ -636,6 +640,8 @@ class FpToBvTransformer(ctx: KContext, private val packedBvOptimization: Boolean override fun visit(sort: KBoolSort): KSort = sort override fun visit(sort: KIntSort): KSort = sort override fun visit(sort: KRealSort): KSort = sort + override fun visit(sort: KStringSort): KSort = sort + override fun visit(sort: KRegexSort): KSort = sort override fun visit(sort: S): KSort = sort } } diff --git a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesExprInternalizer.kt b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesExprInternalizer.kt index 64c23a232..9e4af22ad 100644 --- a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesExprInternalizer.kt +++ b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesExprInternalizer.kt @@ -145,6 +145,48 @@ import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoOverflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoUnderflowExpr import io.ksmt.expr.rewrite.simplify.rewriteBvDivNoOverflowExpr @@ -176,6 +218,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KUninterpretedSort import java.math.BigInteger @@ -964,6 +1008,174 @@ open class KYicesExprInternalizer( } } + override fun transform(expr: KStringConcatExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringLenExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringToRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringInRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringSuffixOfExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringPrefixOfExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringLtExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringLeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringGtExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringGeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringContainsExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringSingletonSubExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringSubExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringIndexOfExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringIndexOfRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringReplaceExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringReplaceAllExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringReplaceWithRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringReplaceAllWithRegexExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringToLowerExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringToUpperExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringReverseExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringIsDigitExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringToCodeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringFromCodeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringToIntExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringFromIntExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KStringLiteralExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexConcatExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexUnionExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexIntersectionExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexStarExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexCrossExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexDifferenceExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexComplementExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexOptionExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexRangeExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexPowerExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexLoopExpr): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexEpsilon): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexAll): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + + override fun transform(expr: KRegexAllChar): KExpr { + throw KSolverUnsupportedFeatureException("string theory is not supported in Yices") + } + private inline fun > E.internalizeQuantifiedBody( quantifiedDecls: List>, quantifierBody: KExpr<*>, diff --git a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesModel.kt b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesModel.kt index 9e968796b..66ff311c3 100644 --- a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesModel.kt +++ b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesModel.kt @@ -26,6 +26,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -228,6 +230,8 @@ class KYicesModel( override fun visit(sort: KBoolSort) = Unit override fun visit(sort: KIntSort) = Unit override fun visit(sort: KRealSort) = Unit + override fun visit(sort: KStringSort) = Unit + override fun visit(sort: KRegexSort) = Unit override fun visit(sort: S) = Unit override fun visit(sort: S) = Unit override fun visit(sort: KFpRoundingModeSort) = Unit diff --git a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolverConfiguration.kt b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolverConfiguration.kt index 669a56a4b..793dc72e9 100644 --- a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolverConfiguration.kt +++ b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSolverConfiguration.kt @@ -7,6 +7,7 @@ import io.ksmt.solver.KSolverUnsupportedFeatureException import io.ksmt.solver.KSolverUnsupportedParameterException import io.ksmt.solver.KTheory import io.ksmt.solver.KTheory.FP +import io.ksmt.solver.KTheory.S import io.ksmt.solver.KTheory.LIA import io.ksmt.solver.KTheory.LRA import io.ksmt.solver.KTheory.NIA @@ -41,6 +42,10 @@ class KYicesSolverConfigurationImpl(private val config: Config) : KYicesSolverCo throw KSolverUnsupportedFeatureException("Unsupported theory $FP") } + if (S in theories) { + throw KSolverUnsupportedFeatureException("Unsupported theory $S") + } + // Yices requires MCSAT for the arithmetic theories if (setOf(LIA, LRA, NIA, NRA).intersect(theories).isNotEmpty()) { return diff --git a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSortInternalizer.kt b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSortInternalizer.kt index fddfbf1f4..9bcc868ea 100644 --- a/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSortInternalizer.kt +++ b/ksmt-yices/ksmt-yices-core/src/main/kotlin/io/ksmt/solver/yices/KYicesSortInternalizer.kt @@ -12,6 +12,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -74,13 +76,17 @@ open class KYicesSortInternalizer( internalizedSort = yicesCtx.newUninterpretedType(sort.name) } - override fun visit(sort: S) { + override fun visit(sort: S) = throw KSolverUnsupportedFeatureException("Unsupported sort $sort") - } - override fun visit(sort: KFpRoundingModeSort) { + override fun visit(sort: KFpRoundingModeSort) = + throw KSolverUnsupportedFeatureException("Unsupported sort $sort") + + override fun visit(sort: KStringSort) = + throw KSolverUnsupportedFeatureException("Unsupported sort $sort") + + override fun visit(sort: KRegexSort) = throw KSolverUnsupportedFeatureException("Unsupported sort $sort") - } fun internalizeYicesSort(sort: KSort): YicesSort = yicesCtx.internalizeSort(sort) { sort.accept(this) diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt index 1bd9097e7..67ae4a9e4 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprConverter.kt @@ -22,6 +22,7 @@ import io.ksmt.expr.KFpRoundingModeExpr import io.ksmt.expr.KIntNumExpr import io.ksmt.expr.KInterpretedValue import io.ksmt.expr.KRealNumExpr +import io.ksmt.expr.KStringLiteralExpr import io.ksmt.expr.rewrite.KExprUninterpretedDeclCollector import io.ksmt.solver.KSolverUnsupportedFeatureException import io.ksmt.solver.util.ExprConversionResult @@ -116,6 +117,9 @@ open class KZ3ExprConverter( Z3_sort_kind.Z3_BOOL_SORT -> boolSort Z3_sort_kind.Z3_INT_SORT -> intSort Z3_sort_kind.Z3_REAL_SORT -> realSort + // Currently, KSMT supports the only type of sequences - strings. + Z3_sort_kind.Z3_SEQ_SORT -> stringSort + Z3_sort_kind.Z3_RE_SORT -> regexSort Z3_sort_kind.Z3_ARRAY_SORT -> convertNativeArraySort(sort) Z3_sort_kind.Z3_BV_SORT -> mkBvSort(Native.getBvSortSize(nCtx, sort).toUInt()) Z3_sort_kind.Z3_FLOATING_POINT_SORT -> @@ -128,8 +132,6 @@ open class KZ3ExprConverter( Z3_sort_kind.Z3_DATATYPE_SORT, Z3_sort_kind.Z3_RELATION_SORT, Z3_sort_kind.Z3_FINITE_DOMAIN_SORT, - Z3_sort_kind.Z3_SEQ_SORT, - Z3_sort_kind.Z3_RE_SORT, Z3_sort_kind.Z3_CHAR_SORT, Z3_sort_kind.Z3_TYPE_VAR, Z3_sort_kind.Z3_UNKNOWN_SORT -> TODO("$sort is not supported yet") @@ -412,6 +414,58 @@ open class KZ3ExprConverter( throw KSolverUnsupportedFeatureException("Fp $declKind is not supported") } + // Currently, KSMT supports the only type of sequences - strings + Z3_decl_kind.Z3_OP_SEQ_CONCAT -> expr.convert(::mkStringConcat) + Z3_decl_kind.Z3_OP_SEQ_LENGTH -> expr.convert(::mkStringLen) + Z3_decl_kind.Z3_OP_SEQ_TO_RE -> expr.convert(::mkStringToRegex) + Z3_decl_kind.Z3_OP_SEQ_IN_RE -> expr.convert(::mkStringInRegex) + Z3_decl_kind.Z3_OP_SEQ_SUFFIX -> expr.convert(::mkStringSuffixOf) + Z3_decl_kind.Z3_OP_SEQ_PREFIX -> expr.convert(::mkStringPrefixOf) + Z3_decl_kind.Z3_OP_STRING_LT -> expr.convert(::mkStringLt) + Z3_decl_kind.Z3_OP_STRING_LE -> expr.convert(::mkStringLe) + Z3_decl_kind.Z3_OP_SEQ_CONTAINS -> expr.convert(::mkStringContains) + Z3_decl_kind.Z3_OP_SEQ_AT -> expr.convert(::mkStringSingletonSub) + Z3_decl_kind.Z3_OP_SEQ_EXTRACT -> expr.convert(::mkStringSub) + Z3_decl_kind.Z3_OP_SEQ_INDEX -> { + var args = getAppArgs(nCtx, expr) + if (args.size == 2) { + args += Native.mkInt(nCtx, 0, Native.mkIntSort(nCtx)) + } + expr.convert(args, ::mkStringIndexOf) + } + Z3_decl_kind.Z3_OP_SEQ_REPLACE -> expr.convert(::mkStringReplace) + Z3_decl_kind.Z3_OP_SEQ_REPLACE_ALL -> expr.convert(::mkStringReplaceAll) + Z3_decl_kind.Z3_OP_SEQ_REPLACE_RE -> expr.convert(::mkStringReplaceWithRegex) + Z3_decl_kind.Z3_OP_SEQ_REPLACE_RE_ALL -> expr.convert(::mkStringReplaceAllWithRegex) + Z3_decl_kind.Z3_OP_CHAR_IS_DIGIT -> expr.convert(::mkStringIsDigit) + Z3_decl_kind.Z3_OP_STR_TO_CODE -> expr.convert(::mkStringToCode) + Z3_decl_kind.Z3_OP_STR_FROM_CODE -> expr.convert(::mkStringFromCode) + Z3_decl_kind.Z3_OP_STR_TO_INT -> expr.convert(::mkStringToInt) + Z3_decl_kind.Z3_OP_INT_TO_STR -> expr.convert(::mkStringFromInt) + Z3_decl_kind.Z3_OP_RE_CONCAT -> expr.convert(::mkRegexConcat) + Z3_decl_kind.Z3_OP_RE_UNION -> expr.convert(::mkRegexUnion) + Z3_decl_kind.Z3_OP_RE_INTERSECT -> expr.convert(::mkRegexIntersection) + Z3_decl_kind.Z3_OP_RE_STAR -> expr.convert(::mkRegexStar) + Z3_decl_kind.Z3_OP_RE_PLUS -> expr.convert(::mkRegexCross) + Z3_decl_kind.Z3_OP_RE_DIFF -> expr.convert(::mkRegexDifference) + Z3_decl_kind.Z3_OP_RE_COMPLEMENT -> expr.convert(::mkRegexComplement) + Z3_decl_kind.Z3_OP_RE_OPTION -> expr.convert(::mkRegexOption) + Z3_decl_kind.Z3_OP_RE_RANGE -> expr.convert(::mkRegexRange) + Z3_decl_kind.Z3_OP_RE_POWER -> { + val args = getAppArgs(nCtx, expr) + val power = Native.getDeclIntParameter(nCtx, decl, 0) + expr.convert(args) { arg -> mkRegexPower(power, arg) } + } + Z3_decl_kind.Z3_OP_RE_LOOP -> { + val args = getAppArgs(nCtx, expr) + val from = Native.getDeclIntParameter(nCtx, decl, 0) + val to = Native.getDeclIntParameter(nCtx, decl, 1) + expr.convert(args) { arg -> mkRegexLoop(from, to, arg) } + } + Z3_decl_kind.Z3_OP_RE_EMPTY_SET -> ExprConversionResult(mkRegexEpsilon()) + Z3_decl_kind.Z3_OP_RE_FULL_SET -> ExprConversionResult(mkRegexAll()) + Z3_decl_kind.Z3_OP_RE_FULL_CHAR_SET -> ExprConversionResult(mkRegexAllChar()) + Z3_decl_kind.Z3_OP_INTERNAL -> tryConvertInternalAppExpr(expr, decl) Z3_decl_kind.Z3_OP_RECURSIVE -> { @@ -525,6 +579,8 @@ open class KZ3ExprConverter( Z3_sort_kind.Z3_BV_SORT -> convert { convertBvNumeral(expr, sort) } Z3_sort_kind.Z3_ROUNDING_MODE_SORT -> convert { convertFpRmNumeral(expr) } Z3_sort_kind.Z3_FLOATING_POINT_SORT -> convertFpNumeral(expr, sort) + // Currently, KSMT supports the only type of sequences - strings. + Z3_sort_kind.Z3_SEQ_SORT -> convert { convertStringLiteral(expr) } else -> TODO("numerals with ${Native.sortToString(nCtx, sort)} are not supported") } } @@ -547,6 +603,12 @@ open class KZ3ExprConverter( } } + @Suppress("MemberVisibilityCanBePrivate") + fun convertStringLiteral(expr: Long): KStringLiteralExpr = with(ctx) { + val value = Native.getString(nCtx, expr) + mkStringLiteral(value) + } + @Suppress("MemberVisibilityCanBePrivate") fun convertBvNumeral(expr: Long, sort: Long): KBitVecValue<*> = with(ctx) { val sizeBits = Native.getBvSortSize(nCtx, sort).toUInt() @@ -603,6 +665,9 @@ open class KZ3ExprConverter( mkFpToBvExpr(rm, fp, size, isSigned = false) } + "String" -> convertNumeral(expr) + "str.is_digit" -> expr.convert(::mkStringIsDigit) + else -> throw KSolverUnsupportedFeatureException("Z3 internal decl $internalDeclName is not supported") } } diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt index 75cdfc558..d99ff3f01 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3ExprInternalizer.kt @@ -149,6 +149,49 @@ import io.ksmt.expr.KUnaryMinusArithExpr import io.ksmt.expr.KUninterpretedSortValue import io.ksmt.expr.KUniversalQuantifier import io.ksmt.expr.KXorExpr +import io.ksmt.expr.KStringConcatExpr +import io.ksmt.expr.KStringLenExpr +import io.ksmt.expr.KStringToRegexExpr +import io.ksmt.expr.KStringInRegexExpr +import io.ksmt.expr.KStringSuffixOfExpr +import io.ksmt.expr.KStringPrefixOfExpr +import io.ksmt.expr.KStringLtExpr +import io.ksmt.expr.KStringLeExpr +import io.ksmt.expr.KStringGtExpr +import io.ksmt.expr.KStringGeExpr +import io.ksmt.expr.KStringContainsExpr +import io.ksmt.expr.KStringSingletonSubExpr +import io.ksmt.expr.KStringSubExpr +import io.ksmt.expr.KStringIndexOfExpr +import io.ksmt.expr.KStringIndexOfRegexExpr +import io.ksmt.expr.KStringReplaceExpr +import io.ksmt.expr.KStringReplaceAllExpr +import io.ksmt.expr.KStringReplaceWithRegexExpr +import io.ksmt.expr.KStringReplaceAllWithRegexExpr +import io.ksmt.expr.KStringToLowerExpr +import io.ksmt.expr.KStringToUpperExpr +import io.ksmt.expr.KStringReverseExpr +import io.ksmt.expr.KStringIsDigitExpr +import io.ksmt.expr.KStringToCodeExpr +import io.ksmt.expr.KStringFromCodeExpr +import io.ksmt.expr.KStringToIntExpr +import io.ksmt.expr.KStringFromIntExpr +import io.ksmt.expr.KStringLiteralExpr +import io.ksmt.expr.KRegexConcatExpr +import io.ksmt.expr.KRegexUnionExpr +import io.ksmt.expr.KRegexIntersectionExpr +import io.ksmt.expr.KRegexStarExpr +import io.ksmt.expr.KRegexCrossExpr +import io.ksmt.expr.KRegexDifferenceExpr +import io.ksmt.expr.KRegexComplementExpr +import io.ksmt.expr.KRegexOptionExpr +import io.ksmt.expr.KRegexRangeExpr +import io.ksmt.expr.KRegexPowerExpr +import io.ksmt.expr.KRegexLoopExpr +import io.ksmt.expr.KRegexEpsilon +import io.ksmt.expr.KRegexAll +import io.ksmt.expr.KRegexAllChar +import io.ksmt.solver.KSolverUnsupportedFeatureException import io.ksmt.solver.util.KExprLongInternalizerBase import io.ksmt.sort.KArithSort import io.ksmt.sort.KArray2Sort @@ -825,6 +868,269 @@ open class KZ3ExprInternalizer( } } + // strings + override fun transform(expr: KStringConcatExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkSeqConcat(nCtx, 2, longArrayOf(arg0, arg1)) + } + } + + override fun transform(expr: KStringLenExpr) = with(expr) { + transform(arg) { arg -> + Native.mkSeqLength(nCtx, arg) + } + } + + override fun transform(expr: KStringToRegexExpr) = with(expr) { + transform(arg) { arg -> + Native.mkSeqToRe(nCtx, arg) + } + } + + override fun transform(expr: KStringInRegexExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkSeqInRe(nCtx, arg0, arg1) + } + } + + override fun transform(expr: KStringSuffixOfExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkSeqSuffix(nCtx, arg0, arg1) + } + } + + override fun transform(expr: KStringPrefixOfExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkSeqPrefix(nCtx, arg0, arg1) + } + } + + override fun transform(expr: KStringLtExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkStrLt(nCtx, arg0, arg1) + } + } + + override fun transform(expr: KStringLeExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkStrLe(nCtx, arg0, arg1) + } + } + + override fun transform(expr: KStringGtExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkStrLt(nCtx, arg1, arg0) + } + } + + override fun transform(expr: KStringGeExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkStrLe(nCtx, arg1, arg0) + } + } + + override fun transform(expr: KStringContainsExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkSeqContains(nCtx, arg0, arg1) + } + } + + override fun transform(expr: KStringSingletonSubExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkSeqAt(nCtx, arg0, arg1) + } + } + + override fun transform(expr: KStringSubExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0, arg1, arg2 -> + Native.mkSeqExtract(nCtx, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringIndexOfExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0, arg1, arg2 -> + Native.mkSeqIndex(nCtx, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringIndexOfRegexExpr) = + throw KSolverUnsupportedFeatureException( + "${expr::class.simpleName} is not supported in z3" + ) + + override fun transform(expr: KStringReplaceExpr) = with(expr) { + transform(arg0, arg1, arg2) { arg0, arg1, arg2 -> + Native.mkSeqReplace(nCtx, arg0, arg1, arg2) + } + } + + override fun transform(expr: KStringReplaceAllExpr) = + throw KSolverUnsupportedFeatureException( + "${expr::class.simpleName} is not supported in z3" + ) + + override fun transform(expr: KStringReplaceWithRegexExpr) = + throw KSolverUnsupportedFeatureException( + "${expr::class.simpleName} is not supported in z3" + ) + + override fun transform(expr: KStringReplaceAllWithRegexExpr) = + throw KSolverUnsupportedFeatureException( + "${expr::class.simpleName} is not supported in z3" + ) + + override fun transform(expr: KStringToLowerExpr) = + throw KSolverUnsupportedFeatureException( + "${expr::class.simpleName} is not supported in z3" + ) + + override fun transform(expr: KStringToUpperExpr) = + throw KSolverUnsupportedFeatureException( + "${expr::class.simpleName} is not supported in z3" + ) + + override fun transform(expr: KStringReverseExpr) = + throw KSolverUnsupportedFeatureException( + "${expr::class.simpleName} is not supported in z3" + ) + + override fun transform(expr: KStringIsDigitExpr) = with(expr) { + transform(arg) { arg -> + Native.mkCharIsDigit(nCtx, arg) + } + } + + override fun transform(expr: KStringToCodeExpr) = with(expr) { + transform(arg) { arg -> + Native.mkStringToCode(nCtx, arg) + } + } + + override fun transform(expr: KStringFromCodeExpr) = with(expr) { + transform(arg) { arg -> + Native.mkStringFromCode(nCtx, arg) + } + } + + override fun transform(expr: KStringToIntExpr) = with(expr) { + transform(arg) { arg -> + Native.mkStrToInt(nCtx, arg) + } + } + + override fun transform(expr: KStringFromIntExpr) = with(expr) { + transform(arg) { arg -> + Native.mkIntToStr(nCtx, arg) + } + } + + override fun transform(expr: KStringLiteralExpr) = with(expr) { + transform { Native.mkString(nCtx, value) } + } + + // regex + override fun transform(expr: KRegexConcatExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkReConcat(nCtx, 2, longArrayOf(arg0, arg1)) + } + } + + override fun transform(expr: KRegexUnionExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkReUnion(nCtx, 2, longArrayOf(arg0, arg1)) + } + } + + override fun transform(expr: KRegexIntersectionExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkReIntersect(nCtx, 2, longArrayOf(arg0, arg1)) + } + } + + override fun transform(expr: KRegexStarExpr) = with(expr) { + transform(arg) { arg -> + Native.mkReStar(nCtx, arg) + } + } + + override fun transform(expr: KRegexCrossExpr) = with(expr) { + transform(arg) { arg -> + Native.mkRePlus(nCtx, arg) + } + } + + override fun transform(expr: KRegexDifferenceExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkReDiff(nCtx, arg0, arg1) + } + } + + override fun transform(expr: KRegexComplementExpr) = with(expr) { + transform(arg) { arg -> + Native.mkReComplement(nCtx, arg) + } + } + + override fun transform(expr: KRegexOptionExpr) = with(expr) { + transform(arg) { arg -> + Native.mkReOption(nCtx, arg) + } + } + + override fun transform(expr: KRegexRangeExpr) = with(expr) { + transform(arg0, arg1) { arg0, arg1 -> + Native.mkReRange(nCtx, arg0, arg1) + } + } + + override fun transform(expr: KRegexPowerExpr) = with(expr) { + transform(arg) { arg -> + Native.mkRePower(nCtx, arg, power) + } + } + + override fun transform(expr: KRegexLoopExpr) = with(expr) { + transform(arg) { arg -> + Native.mkReLoop(nCtx, arg, from, to) + } + } + + override fun transform(expr: KRegexEpsilon) = with(expr) { + transform { + Native.mkReEmpty( + nCtx, + Native.mkReSort( + nCtx, + Native.mkStringSort(nCtx) + ) + ) + } + } + + override fun transform(expr: KRegexAll) = with(expr) { + transform { + Native.mkReFull( + nCtx, + Native.mkReSort( + nCtx, + Native.mkStringSort(nCtx) + ) + ) + } + } + + override fun transform(expr: KRegexAllChar) = with(expr) { + transform { + Native.mkReAllchar( + nCtx, + Native.mkReSort( + nCtx, + Native.mkStringSort(nCtx) + ) + ) + } + } + private fun transformQuantifier(expr: KQuantifier, isUniversal: Boolean) = with(expr) { val boundConstants = bounds.map { ctx.mkConstApp(it) } transformArray(boundConstants + body) { args -> diff --git a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3SortInternalizer.kt b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3SortInternalizer.kt index 614cb8225..bbfc72248 100644 --- a/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3SortInternalizer.kt +++ b/ksmt-z3/ksmt-z3-core/src/main/kotlin/io/ksmt/solver/z3/KZ3SortInternalizer.kt @@ -17,6 +17,8 @@ import io.ksmt.sort.KFpRoundingModeSort import io.ksmt.sort.KFpSort import io.ksmt.sort.KIntSort import io.ksmt.sort.KRealSort +import io.ksmt.sort.KStringSort +import io.ksmt.sort.KRegexSort import io.ksmt.sort.KSort import io.ksmt.sort.KSortVisitor import io.ksmt.sort.KUninterpretedSort @@ -40,6 +42,14 @@ open class KZ3SortInternalizer( internalizedSort = Native.mkRealSort(nCtx) } + override fun visit(sort: KStringSort) { + internalizedSort = Native.mkStringSort(nCtx) + } + + override fun visit(sort: KRegexSort) { + internalizedSort = Native.mkReSort(nCtx, Native.mkStringSort(nCtx)) + } + override fun visit(sort: KArraySort) { val domain = internalizeZ3Sort(sort.domain) val range = internalizeZ3Sort(sort.range)