Syntactic sugar for strings and regex concatenation

Author: raf-nr

ksmt-core/src/main/kotlin/io/ksmt/KContext.kt

@@ -1953,18 +1953,24 @@ open class KContext(
     /**
      * Create String concatenation (`concat`) expression.
      * */
-    open fun mkStringConcatExpr(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KExpr<KStringSort> =
-        mkSimplified(arg0, arg1, KContext::mkStringConcatExprNoSimplify, ::mkStringConcatExprNoSimplify) // Add simplified version
+    open fun mkStringConcat(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KExpr<KStringSort> =
+        mkSimplified(arg0, arg1, KContext::mkStringConcatNoSimplify, ::mkStringConcatNoSimplify) // Add simplified version
 
     /**
      * Create String concatenation (`concat`) expression.
      * */
-    open fun mkStringConcatExprNoSimplify(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KStringConcatExpr =
+    open fun mkStringConcatNoSimplify(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KStringConcatExpr =
         stringConcatExprCache.createIfContextActive {
             ensureContextMatch(arg0, arg1)
             KStringConcatExpr(this, arg0, arg1)
         }
 
+    /**
+     * Create String concatenation (`concat`) expression.
+     * */
+    @JvmName("stringConcat")
+    operator fun KExpr<KStringSort>.plus(other: KExpr<KStringSort>) = mkStringConcat(this, other)
+
     private val stringLenExprCache = mkAstInterner<KStringLenExpr>()
 
     /**
@@ -2183,6 +2189,12 @@ open class KContext(
             KRegexConcatExpr(this, arg0, arg1)
         }
 
+    /**
+     * Create Regex concatenation (`concat`) expression.
+     * */
+    @JvmName("regexConcat")
+    operator fun KExpr<KRegexSort>.plus(other: KExpr<KRegexSort>) = mkRegexConcat(this, other)
+
     private val regexUnionExprCache = mkAstInterner<KRegexUnionExpr>()
 
     /**

ksmt-core/src/main/kotlin/io/ksmt/decl/Regex.kt

@@ -17,7 +17,7 @@ class KRegexConcatDecl internal constructor(
     ctx: KContext,
 ) : KFuncDecl2<KRegexSort, KRegexSort, KRegexSort>(
     ctx,
-    name = "concat",
+    name = "regex_concat",
     resultSort = ctx.mkRegexSort(),
     ctx.mkRegexSort(),
     ctx.mkRegexSort()

ksmt-core/src/main/kotlin/io/ksmt/decl/String.kt

@@ -20,7 +20,7 @@ class KStringConcatDecl internal constructor(
     ctx: KContext,
 ) : KFuncDecl2<KStringSort, KStringSort, KStringSort>(
     ctx,
-    name = "concat",
+    name = "str_concat",
     resultSort = ctx.mkStringSort(),
     ctx.mkStringSort(),
     ctx.mkStringSort()
@@ -30,7 +30,7 @@ class KStringConcatDecl internal constructor(
     override fun KContext.apply(
         arg0: KExpr<KStringSort>,
         arg1: KExpr<KStringSort>
-    ): KApp<KStringSort, *> = mkStringConcatExprNoSimplify(arg0, arg1)
+    ): KApp<KStringSort, *> = mkStringConcatNoSimplify(arg0, arg1)
 }
 
 class KStringLenDecl internal constructor(