Implement basic simplifications for string comparison expr

Author: raf-nr

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

@@ -40,22 +40,22 @@ fun KContext.simplifyStringPrefixOf(
 fun KContext.simplifyStringLt(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>
-): KExpr<KBoolSort> = mkStringLtNoSimplify(arg0, arg1) // Temporarily
+): KExpr<KBoolSort> = simplifyStringBasicLtExpr(arg0, arg1, ::mkStringLtNoSimplify)
 
 fun KContext.simplifyStringLe(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>
-): KExpr<KBoolSort> = mkStringLeNoSimplify(arg0, arg1) // Temporarily
+): KExpr<KBoolSort> = simplifyStringBasicLeExpr(arg0, arg1, ::mkStringLeNoSimplify)
 
 fun KContext.simplifyStringGt(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>
-): KExpr<KBoolSort> = mkStringGtNoSimplify(arg0, arg1) // Temporarily
+): KExpr<KBoolSort> = simplifyStringBasicGtExpr(arg0, arg1, ::mkStringGtNoSimplify)
 
 fun KContext.simplifyStringGe(
     arg0: KExpr<KStringSort>,
     arg1: KExpr<KStringSort>
-): KExpr<KBoolSort> = mkStringGeNoSimplify(arg0, arg1) // Temporarily
+): KExpr<KBoolSort> = simplifyStringBasicGeExpr(arg0, arg1, ::mkStringGeNoSimplify)
 
 fun KContext.simplifyStringContains(
     arg0: KExpr<KStringSort>,

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

@@ -109,6 +109,54 @@ inline fun KContext.simplifyStringBasicPrefixOfExpr(
         cont(arg0, arg1)
     }
 
+/*
+* String comparison expression simplifications
+* */
+
+/** Simplifies string "less than" comparison expressions
+ * (str_lt strConst1 strConst2) ==> boolConst */
+inline fun KContext.simplifyStringBasicLtExpr(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KBoolSort>
+): KExpr<KBoolSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, { a0, a1 -> StringUtils.stringLt(a0, a1) }) {
+        cont(arg0, arg1)
+    }
+
+/** Simplifies string "less than or equal" comparison expressions
+ * (str_le strConst1 strConst2) ==> boolConst */
+inline fun KContext.simplifyStringBasicLeExpr(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KBoolSort>
+): KExpr<KBoolSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, { a0, a1 -> StringUtils.stringLe(a0, a1) }) {
+        cont(arg0, arg1)
+    }
+
+/** Simplifies string "greater than" comparison expressions
+ * (str_gt strConst1 strConst2) ==> boolConst */
+inline fun KContext.simplifyStringBasicGtExpr(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KBoolSort>
+): KExpr<KBoolSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, { a0, a1 -> StringUtils.stringGt(a0, a1) }) {
+        cont(arg0, arg1)
+    }
+
+/** Simplifies string "greater than or equal" comparison expressions
+ * (str_ge strConst1 strConst2) ==> boolConst */
+inline fun KContext.simplifyStringBasicGeExpr(
+    arg0: KExpr<KStringSort>,
+    arg1: KExpr<KStringSort>,
+    cont: (KExpr<KStringSort>, KExpr<KStringSort>) -> KExpr<KBoolSort>
+): KExpr<KBoolSort> =
+    tryEvalStringLiteralOperation(arg0, arg1, { a0, a1 -> StringUtils.stringGe(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

@@ -20,4 +20,24 @@ object StringUtils {
     fun isStringPrefix(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
         mkBool(arg1.value.startsWith(arg0.value)).uncheckedCast()
     }
+
+    @JvmStatic
+    fun stringLt(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
+        mkBool(arg0.value < arg1.value).uncheckedCast()
+    }
+
+    @JvmStatic
+    fun stringLe(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
+        mkBool(arg0.value <= arg1.value).uncheckedCast()
+    }
+
+    @JvmStatic
+    fun stringGt(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
+        mkBool(arg0.value > arg1.value).uncheckedCast()
+    }
+
+    @JvmStatic
+    fun stringGe(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
+        mkBool(arg0.value >= arg1.value).uncheckedCast()
+    }
 }