Implement simplifications for replace string expressions

Author: raf-nr

ksmt-core/src/main/kotlin/Main.kt

@@ -89,13 +89,13 @@ fun KContext.simplifyStringReplace(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>,
     arg2: KExpr<KStringSort>
-): KExpr<KStringSort> = mkStringReplaceNoSimplify(arg0, arg1, arg2) // Temporarily
+): KExpr<KStringSort> = simplifyStringReplaceExprBasic(arg0, arg1, arg2, ::mkStringReplaceNoSimplify)
 
 fun KContext.simplifyStringReplaceAll(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>,
     arg2: KExpr<KStringSort>
-): KExpr<KStringSort> = mkStringReplaceAllNoSimplify(arg0, arg1, arg2) // Temporarily
+): KExpr<KStringSort> = simplifyStringReplaceAllExprBasic(arg0, arg1, arg2, ::mkStringReplaceAllNoSimplify)
 
 fun KContext.simplifyStringReplaceWithRegex(
     arg0: KExpr<KStringSort>,

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

@@ -170,6 +170,30 @@ inline fun KContext.simplifyStringBasicContainsExpr(
         cont(arg0, arg1)
     }
 
+/*
+* String replace expressions simplifications
+* */
+
+inline fun KContext.simplifyStringReplaceExprBasic(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    arg2: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KStringSort>
+): KExpr<KStringSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, arg2, { a0, a1, a2 -> StringUtils.strintReplace(a0, a1, a2) }) {
+        cont(arg0, arg1, arg2)
+    }
+
+inline fun KContext.simplifyStringReplaceAllExprBasic(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    arg2: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KStringSort>
+): KExpr<KStringSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, arg2, { a0, a1, a2 -> StringUtils.strintReplaceAll(a0, a1, a2) }) {
+        cont(arg0, arg1, arg2)
+    }
+
 /*
 * String to lower/upper case expression simplifications
 * */

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

@@ -91,4 +91,20 @@ object StringUtils {
             mkIntNum(-1)
         }
     }
+
+    @JvmStatic
+    fun strintReplace(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr, arg2: KStringLiteralExpr): KStringLiteralExpr = with(arg0.ctx) {
+        val str = arg0.value
+        val search = arg1.value
+        val replace = arg2.value
+        return mkStringLiteral(if (search.isEmpty()) (replace + str) else str.replaceFirst(search, replace))
+    }
+
+    @JvmStatic
+    fun strintReplaceAll(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr, arg2: KStringLiteralExpr): KStringLiteralExpr = with(arg0.ctx) {
+        val str = arg0.value
+        val search = arg1.value
+        val replace = arg2.value
+        return mkStringLiteral(if (search.isEmpty()) str else str.replace(search, replace))
+    }
 }