Implement regular expression complement operation

Author: raf-nr

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

@@ -147,6 +147,7 @@ import io.ksmt.decl.KRegexIntersectionDecl
 import io.ksmt.decl.KRegexKleeneClosureDecl
 import io.ksmt.decl.KRegexKleeneCrossDecl
 import io.ksmt.decl.KRegexDifferenceDecl
+import io.ksmt.decl.KRegexComplementDecl
 import io.ksmt.decl.KIteDecl
 import io.ksmt.decl.KNotDecl
 import io.ksmt.decl.KOrDecl
@@ -308,6 +309,7 @@ import io.ksmt.expr.KRegexIntersectionExpr
 import io.ksmt.expr.KRegexKleeneClosureExpr
 import io.ksmt.expr.KRegexKleeneCrossExpr
 import io.ksmt.expr.KRegexDifferenceExpr
+import io.ksmt.expr.KRegexComplementExpr
 import io.ksmt.expr.KIteExpr
 import io.ksmt.expr.KLeArithExpr
 import io.ksmt.expr.KLtArithExpr
@@ -2213,6 +2215,22 @@ open class KContext(
             KRegexDifferenceExpr(this, arg0, arg1)
         }
 
+    private val regexComplementExprCache = mkAstInterner<KRegexComplementExpr>()
+
+    /**
+     * Create regular expression's complement.
+     * */
+    open fun mkRegexComplement(arg: KExpr<KRegexSort>): KExpr<KRegexSort> =
+        mkSimplified(arg, KContext::mkRegexComplementNoSimplify, ::mkRegexComplementNoSimplify) // Add simplified version
+
+    /**
+     * Create regular expression's complement.
+     * */
+    open fun mkRegexComplementNoSimplify(arg: KExpr<KRegexSort>): KRegexComplementExpr = regexComplementExprCache.createIfContextActive {
+        ensureContextMatch(arg)
+        KRegexComplementExpr(this, arg)
+    }
+
     // bitvectors
     private val bv1Cache = mkAstInterner<KBitVec1Value>()
     private val bv8Cache = mkAstInterner<KBitVec8Value>()
@@ -4850,6 +4868,8 @@ open class KContext(
 
     fun mkRegexDifferenceDecl(): KRegexDifferenceDecl = KRegexDifferenceDecl(this)
 
+    fun mkRegexComplementDecl(): KRegexComplementDecl = KRegexComplementDecl(this)
+
     // Bit vectors
     fun mkBvDecl(value: Boolean): KDecl<KBv1Sort> =
         KBitVec1ValueDecl(this, value)

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

@@ -95,3 +95,9 @@ class KRegexDifferenceDecl internal constructor(
     ): KApp<KRegexSort, *> = mkRegexDifferenceNoSimplify(arg0, arg1)
 }
 
+class KRegexComplementDecl internal constructor(
+    ctx: KContext
+) : KFuncDecl1<KRegexSort, KRegexSort>(ctx, "comp", ctx.mkRegexSort(), ctx.mkRegexSort()) {
+    override fun KContext.apply(arg: KExpr<KRegexSort>): KApp<KRegexSort, KRegexSort> = mkRegexComplementNoSimplify(arg)
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}

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

@@ -7,6 +7,7 @@ import io.ksmt.decl.KDecl
 import io.ksmt.decl.KRegexKleeneClosureDecl
 import io.ksmt.decl.KRegexLiteralDecl
 import io.ksmt.decl.KRegexKleeneCrossDecl
+import io.ksmt.decl.KRegexComplementDecl
 import io.ksmt.expr.transformer.KTransformerBase
 import io.ksmt.sort.KRegexSort
 
@@ -151,3 +152,23 @@ class KRegexDifferenceExpr internal constructor(
     override fun internHashCode(): Int = hash(arg0, arg1)
     override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 })
 }
+
+class KRegexComplementExpr internal constructor(
+    ctx: KContext,
+    val arg: KExpr<KRegexSort>
+) : KApp<KRegexSort, KRegexSort>(ctx) {
+    override val sort: KRegexSort = ctx.regexSort
+
+    override val decl: KRegexComplementDecl
+        get() = ctx.mkRegexComplementDecl()
+
+    override val args: List<KExpr<KRegexSort>>
+        get() = listOf(arg)
+
+    override fun accept(transformer: KTransformerBase): KExpr<KRegexSort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun internHashCode(): Int = hash(arg)
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg }
+}