From 844db5939d4acab4ef3d1c1c5dbd883ab7ab0171 Mon Sep 17 00:00:00 2001 From: raf-nr Date: Wed, 4 Dec 2024 18:59:24 +0300 Subject: [PATCH] Add regular expression constants --- ksmt-core/src/main/kotlin/io/ksmt/KContext.kt | 35 ++++++++++++++ .../src/main/kotlin/io/ksmt/decl/Regex.kt | 21 +++++++++ .../src/main/kotlin/io/ksmt/expr/Regex.kt | 47 ++++++++++++++++++- 3 files changed, 102 insertions(+), 1 deletion(-) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt index 7b0a1623b..cf4efa5a6 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/KContext.kt +++ b/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() private val bv8Cache = mkAstInterner() @@ -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 = KBitVec1ValueDecl(this, value) diff --git a/ksmt-core/src/main/kotlin/io/ksmt/decl/Regex.kt b/ksmt-core/src/main/kotlin/io/ksmt/decl/Regex.kt index d6d83a0d9..51f004a47 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/decl/Regex.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/decl/Regex.kt @@ -101,3 +101,24 @@ class KRegexComplementDecl internal constructor( override fun KContext.apply(arg: KExpr): KApp = mkRegexComplementNoSimplify(arg) override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) } + +class KEpsilonDecl internal constructor( + ctx: KContext +) : KConstDecl(ctx, "eps", ctx.mkRegexSort()) { + override fun apply(args: List>): KApp = ctx.mkEpsilon() + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KAllDecl internal constructor( + ctx: KContext +) : KConstDecl(ctx, "all", ctx.mkRegexSort()) { + override fun apply(args: List>): KApp = ctx.mkAll() + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} + +class KAllCharDecl internal constructor( + ctx: KContext +) : KConstDecl(ctx, "all_char", ctx.mkRegexSort()) { + override fun apply(args: List>): KApp = ctx.mkAllChar() + override fun accept(visitor: KDeclVisitor): R = visitor.visit(this) +} diff --git a/ksmt-core/src/main/kotlin/io/ksmt/expr/Regex.kt b/ksmt-core/src/main/kotlin/io/ksmt/expr/Regex.kt index b0c52e738..51587d19a 100644 --- a/ksmt-core/src/main/kotlin/io/ksmt/expr/Regex.kt +++ b/ksmt-core/src/main/kotlin/io/ksmt/expr/Regex.kt @@ -5,9 +5,12 @@ 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.KRegexLiteralDecl import io.ksmt.decl.KRegexComplementDecl +import io.ksmt.decl.KEpsilonDecl +import io.ksmt.decl.KAllDecl +import io.ksmt.decl.KAllCharDecl import io.ksmt.expr.transformer.KTransformerBase import io.ksmt.sort.KRegexSort @@ -172,3 +175,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(ctx) { + override val sort: KRegexSort = ctx.regexSort + + override val decl: KEpsilonDecl + get() = ctx.mkEpsilonDecl() + + override fun accept(transformer: KTransformerBase): KExpr { + TODO("Not yet implemented") + } + + override fun internHashCode(): Int = hash() + override fun internEquals(other: Any): Boolean = structurallyEqual(other) +} + +class KAll(ctx: KContext) : KInterpretedValue(ctx) { + override val sort: KRegexSort = ctx.regexSort + + override val decl: KAllDecl + get() = ctx.mkAllDecl() + + override fun accept(transformer: KTransformerBase): KExpr { + TODO("Not yet implemented") + } + + override fun internHashCode(): Int = hash() + override fun internEquals(other: Any): Boolean = structurallyEqual(other) +} + +class KAllChar(ctx: KContext) : KInterpretedValue(ctx) { + override val sort: KRegexSort = ctx.regexSort + + override val decl: KAllCharDecl + get() = ctx.mkAllCharDecl() + + override fun accept(transformer: KTransformerBase): KExpr { + TODO("Not yet implemented") + } + + override fun internHashCode(): Int = hash() + override fun internEquals(other: Any): Boolean = structurallyEqual(other) +}