Skip to content

Commit fd259a5

Browse files
raf-nrraf-nr
committed
Implement operation to check whether a string belongs to a regex
1 parent 5a139cd commit fd259a5

4 files changed

Lines changed: 80 additions & 25 deletions

File tree

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

Lines changed: 36 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -133,6 +133,7 @@ import io.ksmt.decl.KStringLiteralDecl
133133
import io.ksmt.decl.KStringConcatDecl
134134
import io.ksmt.decl.KStringLenDecl
135135
import io.ksmt.decl.KStringToRegexDecl
136+
import io.ksmt.decl.KStringInRegexDecl
136137
import io.ksmt.decl.KSuffixOfDecl
137138
import io.ksmt.decl.KPrefixOfDecl
138139
import io.ksmt.decl.KRegexLiteralDecl
@@ -289,6 +290,7 @@ import io.ksmt.expr.KStringLiteralExpr
289290
import io.ksmt.expr.KStringConcatExpr
290291
import io.ksmt.expr.KStringLenExpr
291292
import io.ksmt.expr.KStringToRegexExpr
293+
import io.ksmt.expr.KStringInRegexExpr
292294
import io.ksmt.expr.KSuffixOfExpr
293295
import io.ksmt.expr.KPrefixOfExpr
294296
import io.ksmt.expr.KRegexLiteralExpr
@@ -1959,22 +1961,6 @@ open class KContext(
19591961
KStringLenExpr(this, arg)
19601962
}
19611963

1962-
private val stringToRegexExprCache = mkAstInterner<KStringToRegexExpr>()
1963-
1964-
/**
1965-
* Create a regular expression based on a string expression.
1966-
* */
1967-
open fun mkStringToRegex(arg: KExpr<KStringSort>): KExpr<KRegexSort> =
1968-
mkSimplified(arg, KContext::mkStringToRegexNoSimplify, ::mkStringToRegexNoSimplify) // Add simplified version
1969-
1970-
/**
1971-
* Create a regular expression based on a string expression.
1972-
* */
1973-
open fun mkStringToRegexNoSimplify(arg: KExpr<KStringSort>): KStringToRegexExpr = stringToRegexExprCache.createIfContextActive {
1974-
ensureContextMatch(arg)
1975-
KStringToRegexExpr(this, arg)
1976-
}
1977-
19781964
private val suffixOfExprCache = mkAstInterner<KSuffixOfExpr>()
19791965

19801966
/**
@@ -2009,6 +1995,38 @@ open class KContext(
20091995
KPrefixOfExpr(this, arg0, arg1)
20101996
}
20111997

1998+
private val stringToRegexExprCache = mkAstInterner<KStringToRegexExpr>()
1999+
2000+
/**
2001+
* Create a regular expression based on a string expression.
2002+
* */
2003+
open fun mkStringToRegex(arg: KExpr<KStringSort>): KExpr<KRegexSort> =
2004+
mkSimplified(arg, KContext::mkStringToRegexNoSimplify, ::mkStringToRegexNoSimplify) // Add simplified version
2005+
2006+
/**
2007+
* Create a regular expression based on a string expression.
2008+
* */
2009+
open fun mkStringToRegexNoSimplify(arg: KExpr<KStringSort>): KStringToRegexExpr = stringToRegexExprCache.createIfContextActive {
2010+
ensureContextMatch(arg)
2011+
KStringToRegexExpr(this, arg)
2012+
}
2013+
2014+
private val stringInRegexExprCache = mkAstInterner<KStringInRegexExpr>()
2015+
2016+
/**
2017+
* Check if a string belongs to the language defined by the regular expression.
2018+
* */
2019+
open fun mkStringInRegex(arg0: KExpr<KStringSort>, arg1: KExpr<KRegexSort>): KExpr<KBoolSort> =
2020+
mkSimplified(arg0, arg1, KContext::mkStringInRegexNoSimplify, ::mkStringInRegexNoSimplify) // Add simplified version
2021+
2022+
/**
2023+
* Check if a string belongs to the language defined by the regular expression.
2024+
* */
2025+
open fun mkStringInRegexNoSimplify(arg0: KExpr<KStringSort>, arg1: KExpr<KRegexSort>): KStringInRegexExpr =
2026+
stringInRegexExprCache.createIfContextActive {
2027+
ensureContextMatch(arg0, arg1)
2028+
KStringInRegexExpr(this, arg0, arg1)
2029+
}
20122030

20132031
private val regexLiteralCache = mkAstInterner<KRegexLiteralExpr>()
20142032

@@ -4727,6 +4745,8 @@ open class KContext(
47274745

47284746
fun mkStringToRegexDecl(): KStringToRegexDecl = KStringToRegexDecl(this)
47294747

4748+
fun mkStringInRegexDecl(): KStringInRegexDecl = KStringInRegexDecl(this)
4749+
47304750
fun mkSuffixOfDecl(): KSuffixOfDecl = KSuffixOfDecl(this)
47314751

47324752
fun mkPrefixOfDecl(): KPrefixOfDecl = KPrefixOfDecl(this)

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ package io.ksmt.decl
33
import io.ksmt.KContext
44
import io.ksmt.expr.KApp
55
import io.ksmt.expr.KExpr
6+
import io.ksmt.sort.KSort
67
import io.ksmt.sort.KBoolSort
78
import io.ksmt.sort.KIntSort
89
import io.ksmt.sort.KRegexSort
@@ -47,6 +48,23 @@ class KStringToRegexDecl internal constructor(
4748
override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
4849
}
4950

51+
class KStringInRegexDecl internal constructor(
52+
ctx: KContext,
53+
) : KFuncDecl2<KBoolSort, KStringSort, KRegexSort>(
54+
ctx,
55+
name = "in_regex",
56+
resultSort = ctx.mkBoolSort(),
57+
ctx.mkStringSort(),
58+
ctx.mkRegexSort()
59+
) {
60+
override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
61+
62+
override fun KContext.apply(
63+
arg0: KExpr<KStringSort>,
64+
arg1: KExpr<KRegexSort>
65+
): KApp<KBoolSort, *> = mkStringInRegexNoSimplify(arg0, arg1)
66+
}
67+
5068
class KSuffixOfDecl internal constructor(
5169
ctx: KContext,
5270
) : KFuncDecl2<KBoolSort, KStringSort, KStringSort>(

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

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,10 @@ package io.ksmt.expr
33
import io.ksmt.KContext
44
import io.ksmt.cache.hash
55
import io.ksmt.cache.structurallyEqual
6-
import io.ksmt.decl.KDecl
7-
import io.ksmt.decl.KRegexKleeneClosureDecl
8-
import io.ksmt.decl.KRegexKleeneCrossDecl
9-
import io.ksmt.decl.KRegexLiteralDecl
6+
import io.ksmt.decl.*
107
import io.ksmt.expr.transformer.KTransformerBase
118
import io.ksmt.sort.KRegexSort
9+
import io.ksmt.sort.KStringSort
1210

1311
class KRegexLiteralExpr internal constructor(
1412
ctx: KContext,
@@ -150,4 +148,4 @@ class KRegexDifferenceExpr internal constructor(
150148

151149
override fun internHashCode(): Int = hash(arg0, arg1)
152150
override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 })
153-
}
151+
}

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

Lines changed: 23 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,8 @@ import io.ksmt.cache.hash
55
import io.ksmt.cache.structurallyEqual
66
import io.ksmt.decl.*
77
import io.ksmt.expr.transformer.KTransformerBase
8-
import io.ksmt.sort.KBoolSort
9-
import io.ksmt.sort.KIntSort
10-
import io.ksmt.sort.KRegexSort
11-
import io.ksmt.sort.KStringSort
8+
import io.ksmt.sort.*
9+
import io.ksmt.utils.cast
1210

1311
class KStringLiteralExpr internal constructor(
1412
ctx: KContext,
@@ -89,6 +87,27 @@ class KStringToRegexExpr internal constructor(
8987
override fun internEquals(other: Any): Boolean = structurallyEqual(other) { arg }
9088
}
9189

90+
class KStringInRegexExpr internal constructor(
91+
ctx: KContext,
92+
val arg0: KExpr<KStringSort>,
93+
val arg1: KExpr<KRegexSort>
94+
) : KApp<KBoolSort, KSort>(ctx) {
95+
override val sort: KBoolSort = ctx.mkBoolSort()
96+
97+
override val args: List<KExpr<KSort>>
98+
get() = listOf(arg0.cast(), arg1.cast())
99+
100+
override val decl: KDecl<KBoolSort>
101+
get() = ctx.mkStringInRegexDecl()
102+
103+
override fun accept(transformer: KTransformerBase): KExpr<KBoolSort> {
104+
TODO("Not yet implemented")
105+
}
106+
107+
override fun internHashCode(): Int = hash(arg0, arg1)
108+
override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 })
109+
}
110+
92111
class KSuffixOfExpr internal constructor(
93112
ctx: KContext,
94113
val arg0: KExpr<KStringSort>,

0 commit comments

Comments
 (0)