Implement prefixOf and suffixOf strings' operations

Author: raf-nr

ksmt-core/src/main/kotlin/io/ksmt/KContext.kt

@@ -133,6 +133,8 @@ import io.ksmt.decl.KStringLiteralDecl
 import io.ksmt.decl.KStringConcatDecl
 import io.ksmt.decl.KStringLenDecl
 import io.ksmt.decl.KStringToRegexDecl
+import io.ksmt.decl.KSuffixOfDecl
+import io.ksmt.decl.KPrefixOfDecl
 import io.ksmt.decl.KRegexLiteralDecl
 import io.ksmt.decl.KRegexConcatDecl
 import io.ksmt.decl.KRegexUnionDecl
@@ -287,6 +289,8 @@ import io.ksmt.expr.KStringLiteralExpr
 import io.ksmt.expr.KStringConcatExpr
 import io.ksmt.expr.KStringLenExpr
 import io.ksmt.expr.KStringToRegexExpr
+import io.ksmt.expr.KSuffixOfExpr
+import io.ksmt.expr.KPrefixOfExpr
 import io.ksmt.expr.KRegexLiteralExpr
 import io.ksmt.expr.KRegexConcatExpr
 import io.ksmt.expr.KRegexUnionExpr
@@ -1971,6 +1975,41 @@ open class KContext(
         KStringToRegexExpr(this, arg)
     }
 
+    private val suffixOfExprCache = mkAstInterner<KSuffixOfExpr>()
+
+    /**
+     * Check if first string is a suffix of second.
+     * */
+    open fun mkSuffixOf(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KExpr<KBoolSort> =
+        mkSimplified(arg0, arg1, KContext::mkSuffixOfNoSimplify, ::mkSuffixOfNoSimplify) // Add simplified version
+
+    /**
+     * Check if first string is a suffix of second.
+     * */
+    open fun mkSuffixOfNoSimplify(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KSuffixOfExpr =
+        suffixOfExprCache.createIfContextActive {
+            ensureContextMatch(arg0, arg1)
+            KSuffixOfExpr(this, arg0, arg1)
+        }
+
+    private val prefixOfExprCache = mkAstInterner<KPrefixOfExpr>()
+
+    /**
+     * Check if first string is a prefix of second.
+     * */
+    open fun mkPrefixOf(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KExpr<KBoolSort> =
+        mkSimplified(arg0, arg1, KContext::mkPrefixOfNoSimplify, ::mkPrefixOfNoSimplify) // Add simplified version
+
+    /**
+     * Check if first string is a prefix of second.
+     * */
+    open fun mkPrefixOfNoSimplify(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KPrefixOfExpr =
+        prefixOfExprCache.createIfContextActive {
+            ensureContextMatch(arg0, arg1)
+            KPrefixOfExpr(this, arg0, arg1)
+        }
+
+
     private val regexLiteralCache = mkAstInterner<KRegexLiteralExpr>()
 
     /**
@@ -4688,6 +4727,10 @@ open class KContext(
 
     fun mkStringToRegexDecl(): KStringToRegexDecl = KStringToRegexDecl(this)
 
+    fun mkSuffixOfDecl(): KSuffixOfDecl = KSuffixOfDecl(this)
+
+    fun mkPrefixOfDecl(): KPrefixOfDecl = KPrefixOfDecl(this)
+
     // regex
     fun mkRegexLiteralDecl(value: String): KRegexLiteralDecl = KRegexLiteralDecl(this, value)
 

ksmt-core/src/main/kotlin/io/ksmt/decl/String.kt

@@ -46,3 +46,37 @@ class KStringToRegexDecl internal constructor(
     override fun KContext.apply(arg: KExpr<KStringSort>): KApp<KRegexSort, KStringSort> = mkStringToRegexNoSimplify(arg)
     override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
 }
+
+class KSuffixOfDecl internal constructor(
+    ctx: KContext,
+) : KFuncDecl2<KBoolSort, KStringSort, KStringSort>(
+    ctx,
+    name = "suffix_of",
+    resultSort = ctx.mkBoolSort(),
+    ctx.mkStringSort(),
+    ctx.mkStringSort()
+) {
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+
+    override fun KContext.apply(
+        arg0: KExpr<KStringSort>,
+        arg1: KExpr<KStringSort>
+    ): KApp<KBoolSort, *> = mkSuffixOfNoSimplify(arg0, arg1)
+}
+
+class KPrefixOfDecl internal constructor(
+    ctx: KContext,
+) : KFuncDecl2<KBoolSort, KStringSort, KStringSort>(
+    ctx,
+    name = "prefix_of",
+    resultSort = ctx.mkBoolSort(),
+    ctx.mkStringSort(),
+    ctx.mkStringSort()
+) {
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+
+    override fun KContext.apply(
+        arg0: KExpr<KStringSort>,
+        arg1: KExpr<KStringSort>
+    ): KApp<KBoolSort, *> = mkPrefixOfNoSimplify(arg0, arg1)
+}

ksmt-core/src/main/kotlin/io/ksmt/expr/String.kt

@@ -5,6 +5,7 @@ import io.ksmt.cache.hash
 import io.ksmt.cache.structurallyEqual
 import io.ksmt.decl.*
 import io.ksmt.expr.transformer.KTransformerBase
+import io.ksmt.sort.KBoolSort
 import io.ksmt.sort.KIntSort
 import io.ksmt.sort.KRegexSort
 import io.ksmt.sort.KStringSort
@@ -87,3 +88,45 @@ class KStringToRegexExpr internal constructor(
     override fun internHashCode(): Int = hash(arg)
     override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg }
 }
+
+class KSuffixOfExpr internal constructor(
+    ctx: KContext,
+    val arg0: KExpr<KStringSort>,
+    val arg1: KExpr<KStringSort>
+) : KApp<KBoolSort, KStringSort>(ctx) {
+    override val sort: KBoolSort = ctx.mkBoolSort()
+
+    override val args: List<KExpr<KStringSort>>
+        get() = listOf(arg0, arg1)
+
+    override val decl: KDecl<KBoolSort>
+        get() = ctx.mkSuffixOfDecl()
+
+    override fun accept(transformer: KTransformerBase): KExpr<KBoolSort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun internHashCode(): Int = hash(arg0, arg1)
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 })
+}
+
+class KPrefixOfExpr internal constructor(
+    ctx: KContext,
+    val arg0: KExpr<KStringSort>,
+    val arg1: KExpr<KStringSort>
+) : KApp<KBoolSort, KStringSort>(ctx) {
+    override val sort: KBoolSort = ctx.mkBoolSort()
+
+    override val args: List<KExpr<KStringSort>>
+        get() = listOf(arg0, arg1)
+
+    override val decl: KDecl<KBoolSort>
+        get() = ctx.mkPrefixOfDecl()
+
+    override fun accept(transformer: KTransformerBase): KExpr<KBoolSort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun internHashCode(): Int = hash(arg0, arg1)
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 })
+}