Syntactic sugar for suffixOf, prefixOf, contains operations

UnitTestBot · Dec 8, 2024 · eb068cc · eb068cc
1 parent ee0ff54
commit eb068cc
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt
@@ -2013,6 +2013,11 @@ open class KContext(
             KSuffixOfExpr(this, arg0, arg1)
         }
 
+    /**
+     * Check if first string is a suffix of second.
+     * */
+    infix fun KExpr<KStringSort>.isSuffixOf(other: KExpr<KStringSort>) = mkSuffixOf(this, other)
+
     private val prefixOfExprCache = mkAstInterner<KPrefixOfExpr>()
 
     /**
@@ -2030,6 +2035,11 @@ open class KContext(
             KPrefixOfExpr(this, arg0, arg1)
         }
 
+    /**
+     * Check if first string is a prefix of second.
+     * */
+    infix fun KExpr<KStringSort>.isPrefixOf(other: KExpr<KStringSort>) = mkPrefixOf(this, other)
+
     private val stringLtCache = mkAstInterner<KStringLtExpr>()
 
     /**
@@ -2139,6 +2149,11 @@ open class KContext(
             KStringContainsExpr(this, lhs, rhs)
         }
 
+    /**
+     * Check if first string contains second one.
+     * */
+    infix fun KExpr<KStringSort>.contains(other: KExpr<KStringSort>) = mkStringContains(this, other)
+
     private val stringToRegexExprCache = mkAstInterner<KStringToRegexExpr>()
 
     /**