From 1b38d128b33cda20a86cf46f49f9c836ea1b193b Mon Sep 17 00:00:00 2001 From: raf-nr Date: Sun, 8 Dec 2024 22:44:13 +0300 Subject: [PATCH] Syntactic sugar for inRegex, toRegex operations --- ksmt-core/src/main/kotlin/io/ksmt/KContext.kt | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index 66f98deb1..86f3f8728 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt @@ -2152,6 +2152,7 @@ open class KContext( /** * Check if first string contains second one. * */ + @JvmName("strContains") infix fun KExpr.contains(other: KExpr) = mkStringContains(this, other) private val stringToRegexExprCache = mkAstInterner() @@ -2170,6 +2171,16 @@ open class KContext( KStringToRegexExpr(this, arg) } + /** + * Create a regular expression based on a string expression. + * */ + fun KExpr.toRegex() = mkStringToRegex(this) + + /** + * Create a regular expression based on a string expression. + * */ + fun String.toRegex() = mkStringToRegex(this.expr) + private val stringInRegexExprCache = mkAstInterner() /** @@ -2187,6 +2198,22 @@ open class KContext( KStringInRegexExpr(this, arg0, arg1) } + /** + * Check if a string belongs to the language defined by the regular expression. + * */ + infix fun KExpr.inRegex(other: KExpr) = mkStringInRegex(this, other) + + /** + * Check if a string belongs to the language defined by the regular expression. + * */ + infix fun String.inRegex(other: KExpr) = mkStringInRegex(this.expr, other) + + /** + * Check if a string belongs to the language defined by the regular expression. + * */ + @JvmName("regexContains") + infix fun KExpr.contains(other: KExpr) = mkStringInRegex(other, this) + private val regexLiteralCache = mkAstInterner() /**