Add regular expression constants

Author: raf-nr

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

@@ -140,6 +140,9 @@ import io.ksmt.decl.KStringLtDecl
 import io.ksmt.decl.KStringLeDecl
 import io.ksmt.decl.KStringGtDecl
 import io.ksmt.decl.KStringGeDecl
+import io.ksmt.decl.KEpsilonDecl
+import io.ksmt.decl.KAllDecl
+import io.ksmt.decl.KAllCharDecl
 import io.ksmt.decl.KRegexLiteralDecl
 import io.ksmt.decl.KRegexConcatDecl
 import io.ksmt.decl.KRegexUnionDecl
@@ -302,6 +305,9 @@ import io.ksmt.expr.KStringLtExpr
 import io.ksmt.expr.KStringLeExpr
 import io.ksmt.expr.KStringGtExpr
 import io.ksmt.expr.KStringGeExpr
+import io.ksmt.expr.KEpsilon
+import io.ksmt.expr.KAll
+import io.ksmt.expr.KAllChar
 import io.ksmt.expr.KRegexLiteralExpr
 import io.ksmt.expr.KRegexConcatExpr
 import io.ksmt.expr.KRegexUnionExpr
@@ -2231,6 +2237,28 @@ open class KContext(
         KRegexComplementExpr(this, arg)
     }
 
+    val epsilonExpr: KEpsilon = KEpsilon(this)
+
+    /**
+     * Create regex Epsilon constant.
+     * Epsilon regular expression denoting the empty set of strings.
+     * */
+    fun mkEpsilon(): KEpsilon = epsilonExpr
+
+    val allExpr: KAll = KAll(this)
+
+    /**
+     * Create regex constant denoting the set of all strings.
+     * */
+    fun mkAll(): KAll = allExpr
+
+    val allCharExpr: KAllChar = KAllChar(this)
+
+    /**
+     * Create regex constant denoting the set of all strings of length 1.
+     * */
+    fun mkAllChar(): KAllChar = allCharExpr
+
     // bitvectors
     private val bv1Cache = mkAstInterner<KBitVec1Value>()
     private val bv8Cache = mkAstInterner<KBitVec8Value>()
@@ -4854,6 +4882,7 @@ open class KContext(
     fun mkStringGeDecl(): KStringGeDecl = KStringGeDecl(this)
 
     // regex
+
     fun mkRegexLiteralDecl(value: String): KRegexLiteralDecl = KRegexLiteralDecl(this, value)
 
     fun mkRegexConcatDecl(): KRegexConcatDecl = KRegexConcatDecl(this)
@@ -4870,6 +4899,12 @@ open class KContext(
 
     fun mkRegexComplementDecl(): KRegexComplementDecl = KRegexComplementDecl(this)
 
+    fun mkEpsilonDecl(): KEpsilonDecl = KEpsilonDecl(this)
+
+    fun mkAllDecl(): KAllDecl = KAllDecl(this)
+
+    fun mkAllCharDecl(): KAllCharDecl = KAllCharDecl(this)
+
     // Bit vectors
     fun mkBvDecl(value: Boolean): KDecl<KBv1Sort> =
         KBitVec1ValueDecl(this, value)

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

@@ -3,6 +3,7 @@ package io.ksmt.decl
 import io.ksmt.KContext
 import io.ksmt.expr.KApp
 import io.ksmt.expr.KExpr
+import io.ksmt.sort.KBoolSort
 import io.ksmt.sort.KRegexSort
 
 class KRegexLiteralDecl internal constructor(
@@ -101,3 +102,24 @@ class KRegexComplementDecl internal constructor(
     override fun KContext.apply(arg: KExpr<KRegexSort>): KApp<KRegexSort, KRegexSort> = mkRegexComplementNoSimplify(arg)
     override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
 }
+
+class KEpsilonDecl internal constructor(
+    ctx: KContext
+) : KConstDecl<KRegexSort>(ctx, "eps", ctx.mkRegexSort()) {
+    override fun apply(args: List<KExpr<*>>): KApp<KRegexSort, *> = ctx.mkEpsilon()
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}
+
+class KAllDecl internal constructor(
+    ctx: KContext
+) : KConstDecl<KRegexSort>(ctx, "all", ctx.mkRegexSort()) {
+    override fun apply(args: List<KExpr<*>>): KApp<KRegexSort, *> = ctx.mkAll()
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}
+
+class KAllCharDecl internal constructor(
+    ctx: KContext
+) : KConstDecl<KRegexSort>(ctx, "all_char", ctx.mkRegexSort()) {
+    override fun apply(args: List<KExpr<*>>): KApp<KRegexSort, *> = ctx.mkAllChar()
+    override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
+}

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

@@ -3,12 +3,9 @@ package io.ksmt.expr
 import io.ksmt.KContext
 import io.ksmt.cache.hash
 import io.ksmt.cache.structurallyEqual
-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.decl.*
 import io.ksmt.expr.transformer.KTransformerBase
+import io.ksmt.sort.KBoolSort
 import io.ksmt.sort.KRegexSort
 
 class KRegexLiteralExpr internal constructor(
@@ -172,3 +169,45 @@ class KRegexComplementExpr internal constructor(
     override fun internHashCode(): Int = hash(arg)
     override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg }
 }
+
+class KEpsilon(ctx: KContext) : KInterpretedValue<KRegexSort>(ctx) {
+    override val sort: KRegexSort = ctx.regexSort
+
+    override val decl: KEpsilonDecl
+        get() = ctx.mkEpsilonDecl()
+
+    override fun accept(transformer: KTransformerBase): KExpr<KRegexSort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun internHashCode(): Int = hash()
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other)
+}
+
+class KAll(ctx: KContext) : KInterpretedValue<KRegexSort>(ctx) {
+    override val sort: KRegexSort = ctx.regexSort
+
+    override val decl: KAllDecl
+        get() = ctx.mkAllDecl()
+
+    override fun accept(transformer: KTransformerBase): KExpr<KRegexSort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun internHashCode(): Int = hash()
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other)
+}
+
+class KAllChar(ctx: KContext) : KInterpretedValue<KRegexSort>(ctx) {
+    override val sort: KRegexSort = ctx.regexSort
+
+    override val decl: KAllCharDecl
+        get() = ctx.mkAllCharDecl()
+
+    override fun accept(transformer: KTransformerBase): KExpr<KRegexSort> {
+        TODO("Not yet implemented")
+    }
+
+    override fun internHashCode(): Int = hash()
+    override fun internEquals(other: Any): Boolean = structurallyEqual(other)
+}