Implement simplifiers for contains, toLower, toUpper, reverse operations

Author: raf-nr

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

@@ -60,7 +60,7 @@ fun KContext.simplifyStringGe(
 fun KContext.simplifyStringContains(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>
-): KExpr<KBoolSort> = mkStringContainsNoSimplify(arg0, arg1) // Temporarily
+): KExpr<KBoolSort> = simplifyStringBasicContainsExpr(arg0, arg1, ::mkStringContainsNoSimplify)
 
 fun KContext.simplifyStringSingletonSub(
     arg0: KExpr<KStringSort>,
@@ -111,15 +111,15 @@ fun KContext.simplifyStringReplaceAllWithRegex(
 
 fun KContext.simplifyStringToLower(
     arg: KExpr<KStringSort>
-): KExpr<KStringSort> = mkStringToLowerNoSimplify(arg) // Temporarily
+): KExpr<KStringSort> = simplifyStringBasicToLowerExpr(arg, ::mkStringToLowerNoSimplify)
 
 fun KContext.simplifyStringToUpper(
     arg: KExpr<KStringSort>
-): KExpr<KStringSort> = mkStringToUpperNoSimplify(arg) // Temporarily
+): KExpr<KStringSort> = simplifyStringBasicToUpperExpr(arg, ::mkStringToUpperNoSimplify)
 
 fun KContext.simplifyStringReverse(
     arg: KExpr<KStringSort>
-): KExpr<KStringSort> = mkStringReverseNoSimplify(arg) // Temporarily
+): KExpr<KStringSort> = simplifyStringBasicReverseExpr(arg, ::mkStringReverseNoSimplify)
 
 fun KContext.simplifyStringIsDigit(
     arg: KExpr<KStringSort>

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

@@ -1,10 +1,7 @@
 package io.ksmt.expr.rewrite.simplify
 
 import io.ksmt.KContext
-import io.ksmt.expr.KExpr
-import io.ksmt.expr.KInterpretedValue
-import io.ksmt.expr.KStringConcatExpr
-import io.ksmt.expr.KStringLiteralExpr
+import io.ksmt.expr.*
 import io.ksmt.sort.KBoolSort
 import io.ksmt.sort.KIntSort
 import io.ksmt.sort.KSort
@@ -77,8 +74,8 @@ inline fun KContext.simplifyStringLenExpr(
     arg: KExpr<KStringSort>,
     cont: (KExpr<KStringSort>) -> KExpr<KIntSort>
 ): KExpr<KIntSort> =
-    tryEvalStringLiteralOperation(arg, { literalArg ->
-        mkIntNum(literalArg.value.length)
+    tryEvalStringLiteralOperation(arg, {
+        a -> StringUtils.getStringLen(a)
     }) {
         cont(arg)
     }
@@ -157,6 +154,52 @@ inline fun KContext.simplifyStringBasicGeExpr(
         cont(arg0, arg1)
     }
 
+/*
+* String contains expression simplifications
+* */
+
+/** Basic simplify string contains expression
+ * (str_contains strConst1 strConst2) ==> boolConst */
+inline fun KContext.simplifyStringBasicContainsExpr(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KBoolSort>
+): KExpr<KBoolSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, { a0, a1 -> StringUtils.stringContains(a0, a1) }) {
+        cont(arg0, arg1)
+    }
+
+/*
+* String to lower/upper case expression simplifications
+* */
+
+/** Converting all letters of a string constant to lowercase. */
+inline fun KContext.simplifyStringBasicToLowerExpr(
+    arg: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>) -> KExpr<KStringSort>
+): KExpr<KStringSort> =
+    tryEvalStringLiteralOperation(arg, { a -> StringUtils.stringToLowerCase(a) }) {
+        cont(arg)
+    }
+
+/** Converting all letters of a string constant to uppercase. */
+inline fun KContext.simplifyStringBasicToUpperExpr(
+    arg: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>) -> KExpr<KStringSort>
+): KExpr<KStringSort> =
+    tryEvalStringLiteralOperation(arg, { a -> StringUtils.stringToUpperCase(a) }) {
+        cont(arg)
+    }
+
+/** Reverses a string constant */
+inline fun KContext.simplifyStringBasicReverseExpr(
+    arg: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>) -> KExpr<KStringSort>
+): KExpr<KStringSort> =
+    tryEvalStringLiteralOperation(arg, { a -> StringUtils.stringReverse(a) }) {
+        cont(arg)
+    }
+
 inline fun <K : KSort> tryEvalStringLiteralOperation(
     arg: KExpr<KStringSort>,
     operation: (KStringLiteralExpr) -> KInterpretedValue<K>,

ksmt-core/src/main/kotlin/io/ksmt/utils/StringUtils.kt

@@ -1,11 +1,20 @@
 package io.ksmt.utils
 
+import io.ksmt.expr.KInt32NumExpr
+import io.ksmt.expr.KInt64NumExpr
+import io.ksmt.expr.KIntBigNumExpr
+import io.ksmt.expr.KIntNumExpr
 import io.ksmt.expr.KInterpretedValue
 import io.ksmt.expr.KStringLiteralExpr
 import io.ksmt.sort.KBoolSort
 
 object StringUtils {
 
+    @JvmStatic
+    fun getStringLen(arg: KStringLiteralExpr): KIntNumExpr = with (arg.ctx) {
+        mkIntNum(arg.value.length)
+    }
+
     @JvmStatic
     fun concatStrings(lhs: KStringLiteralExpr, rhs: KStringLiteralExpr): KStringLiteralExpr = with (lhs.ctx) {
         mkStringLiteral(lhs.value + rhs.value)
@@ -40,4 +49,25 @@ object StringUtils {
     fun stringGe(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
         mkBool(arg0.value >= arg1.value).uncheckedCast()
     }
+
+    @JvmStatic
+    fun stringContains(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
+        mkBool(arg0.value.contains(arg1.value)).uncheckedCast()
+    }
+
+    @JvmStatic
+    fun stringToLowerCase(arg: KStringLiteralExpr): KStringLiteralExpr = with (arg.ctx) {
+        mkStringLiteral(arg.value.lowercase())
+    }
+
+    @JvmStatic
+    fun stringToUpperCase(arg: KStringLiteralExpr): KStringLiteralExpr = with (arg.ctx) {
+        mkStringLiteral(arg.value.uppercase())
+    }
+
+    @JvmStatic
+    fun stringReverse(arg: KStringLiteralExpr): KStringLiteralExpr = with (arg.ctx) {
+        mkStringLiteral(arg.value.reversed())
+    }
+
 }