Implement basic and nested string concat simplification

Author: raf-nr

ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplification.kt

@@ -10,7 +10,9 @@ import io.ksmt.sort.KStringSort
 fun KContext.simplifyStringConcat(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>
-): KExpr<KStringSort> = mkStringConcatNoSimplify(arg0, arg1) // Temporarily
+): KExpr<KStringSort> = simplifyStringBasicConcat(arg0, arg1) {arg2, arg3 ->
+    simplifyStringNestedConcat(arg2, arg3, KContext::simplifyStringConcat, ::mkStringConcatNoSimplify)
+}
 
 fun KContext.simplifyStringLen(
     arg: KExpr<KStringSort>

ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplificationRules.kt

@@ -1,8 +1,54 @@
 package io.ksmt.expr.rewrite.simplify
 
+import io.ksmt.KContext
 import io.ksmt.expr.KExpr
+import io.ksmt.expr.KStringConcatExpr
 import io.ksmt.expr.KStringLiteralExpr
 import io.ksmt.sort.KStringSort
+import io.ksmt.utils.StringUtils
+
+inline fun KContext.simplifyStringBasicConcat(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KStringSort>
+): KExpr<KStringSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, { a1, a2 -> StringUtils.concatStrings(a1, a2) }) {
+        cont(arg0, arg1)
+    }
+
+inline fun KContext.simplifyStringNestedConcat(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    rewriteStringConcatExpr: KContext.(KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KStringSort>
+): KExpr<KStringSort> {
+    if (arg0 is KStringLiteralExpr && arg1 is KStringConcatExpr) {
+        val arg1Left = arg1.arg0
+        if (arg1Left is KStringLiteralExpr) {
+            return rewriteStringConcatExpr(StringUtils.concatStrings(arg0, arg1Left), arg1.arg1)
+        }
+    }
+
+    if (arg1 is KStringLiteralExpr && arg0 is KStringConcatExpr) {
+        val arg0Right = arg0.arg1
+        if (arg0Right is KStringLiteralExpr) {
+            return rewriteStringConcatExpr(arg0.arg0, StringUtils.concatStrings(arg0Right, arg1))
+        }
+    }
+
+    if (arg0 is KStringConcatExpr && arg1 is KStringConcatExpr) {
+        val arg0Right = arg0.arg1
+        val arg1Left = arg1.arg0
+        if (arg0Right is KStringLiteralExpr && arg1Left is KStringLiteralExpr) {
+            return rewriteStringConcatExpr(
+                arg0.arg0,
+                mkStringConcat(StringUtils.concatStrings(arg0Right, arg1Left), arg1.arg1)
+            )
+        }
+    }
+
+    return cont(arg0, arg1)
+}
 
 inline fun tryEvalStringLiteralOperation(
     lhs: KExpr<KStringSort>,