Implement basic simplifications for suffixOf and prefixOf expressions

Author: raf-nr

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

@@ -30,12 +30,12 @@ fun KContext.simplifyStringInRegex(
 fun KContext.simplifyStringSuffixOf(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>
-): KExpr<KBoolSort> = mkStringSuffixOfNoSimplify(arg0, arg1) // Temporarily
+): KExpr<KBoolSort> = simplifyStringBasicSuffixOfExpr(arg0, arg1, ::mkStringSuffixOfNoSimplify)
 
 fun KContext.simplifyStringPrefixOf(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>
-): KExpr<KBoolSort> = mkStringPrefixOfNoSimplify(arg0, arg1) // Temporarily
+): KExpr<KBoolSort> = simplifyStringBasicPrefixOfExpr(arg0, arg1, ::mkStringPrefixOfNoSimplify)
 
 fun KContext.simplifyStringLt(
     arg0: KExpr<KStringSort>,

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

@@ -5,6 +5,7 @@ import io.ksmt.expr.KExpr
 import io.ksmt.expr.KInterpretedValue
 import io.ksmt.expr.KStringConcatExpr
 import io.ksmt.expr.KStringLiteralExpr
+import io.ksmt.sort.KBoolSort
 import io.ksmt.sort.KIntSort
 import io.ksmt.sort.KSort
 import io.ksmt.sort.KStringSort
@@ -70,6 +71,8 @@ inline fun KContext.simplifyStringNestedConcat(
 * String length expression simplification
 * */
 
+/**
+ * Eval length of string constant. */
 inline fun KContext.simplifyStringLenExpr(
     arg: KExpr<KStringSort>,
     cont: (KExpr<KStringSort>) -> KExpr<KIntSort>
@@ -80,6 +83,32 @@ inline fun KContext.simplifyStringLenExpr(
         cont(arg)
     }
 
+/*
+* SuffixOf and PrefixOf expression simplifications
+* */
+
+/** Simplifies string suffix checking expressions
+ * (str_suffix_of strConst1 strConst2) ==> boolConst */
+inline fun KContext.simplifyStringBasicSuffixOfExpr(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KBoolSort>
+): KExpr<KBoolSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, { a0, a1 -> StringUtils.isStringSuffix(a0, a1) }) {
+        cont(arg0, arg1)
+    }
+
+/** Simplifies string prefix checking expressions
+ * (str_prefix_of strConst1 strConst2) ==> boolConst */
+inline fun KContext.simplifyStringBasicPrefixOfExpr(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KBoolSort>
+): KExpr<KBoolSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, { a0, a1 -> StringUtils.isStringPrefix(a0, a1) }) {
+        cont(arg0, arg1)
+    }
+
 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,23 @@
 package io.ksmt.utils
 
+import io.ksmt.expr.KInterpretedValue
 import io.ksmt.expr.KStringLiteralExpr
+import io.ksmt.sort.KBoolSort
 
 object StringUtils {
 
     @JvmStatic
     fun concatStrings(lhs: KStringLiteralExpr, rhs: KStringLiteralExpr): KStringLiteralExpr = with (lhs.ctx) {
         mkStringLiteral(lhs.value + rhs.value)
     }
+
+    @JvmStatic
+    fun isStringSuffix(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
+        mkBool(arg1.value.endsWith(arg0.value)).uncheckedCast()
+    }
+
+    @JvmStatic
+    fun isStringPrefix(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
+        mkBool(arg1.value.startsWith(arg0.value)).uncheckedCast()
+    }
 }