Skip to content

Commit 2a500d7

Browse files
raf-nrraf-nr
committed
Implement operations for comparing strings
1 parent fd259a5 commit 2a500d7

5 files changed

Lines changed: 211 additions & 8 deletions

File tree

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

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,10 @@ import io.ksmt.decl.KStringToRegexDecl
136136
import io.ksmt.decl.KStringInRegexDecl
137137
import io.ksmt.decl.KSuffixOfDecl
138138
import io.ksmt.decl.KPrefixOfDecl
139+
import io.ksmt.decl.KStringLtDecl
140+
import io.ksmt.decl.KStringLeDecl
141+
import io.ksmt.decl.KStringGtDecl
142+
import io.ksmt.decl.KStringGeDecl
139143
import io.ksmt.decl.KRegexLiteralDecl
140144
import io.ksmt.decl.KRegexConcatDecl
141145
import io.ksmt.decl.KRegexUnionDecl
@@ -293,6 +297,10 @@ import io.ksmt.expr.KStringToRegexExpr
293297
import io.ksmt.expr.KStringInRegexExpr
294298
import io.ksmt.expr.KSuffixOfExpr
295299
import io.ksmt.expr.KPrefixOfExpr
300+
import io.ksmt.expr.KStringLtExpr
301+
import io.ksmt.expr.KStringLeExpr
302+
import io.ksmt.expr.KStringGtExpr
303+
import io.ksmt.expr.KStringGeExpr
296304
import io.ksmt.expr.KRegexLiteralExpr
297305
import io.ksmt.expr.KRegexConcatExpr
298306
import io.ksmt.expr.KRegexUnionExpr
@@ -1995,6 +2003,74 @@ open class KContext(
19952003
KPrefixOfExpr(this, arg0, arg1)
19962004
}
19972005

2006+
private val stringLtCache = mkAstInterner<KStringLtExpr>()
2007+
2008+
/**
2009+
* Create a lexicographic ordering (`<` (less)) expression.
2010+
* */
2011+
open fun mkStringLt(lhs: KExpr<KStringSort>, rhs: KExpr<KStringSort>): KExpr<KBoolSort> =
2012+
mkSimplified(lhs, rhs, KContext::mkStringLtNoSimplify, ::mkStringLtNoSimplify)
2013+
2014+
/**
2015+
* Create a lexicographic ordering (`<` (less)) expression.
2016+
* */
2017+
open fun mkStringLtNoSimplify(lhs: KExpr<KStringSort>, rhs: KExpr<KStringSort>): KStringLtExpr =
2018+
stringLtCache.createIfContextActive {
2019+
ensureContextMatch(lhs, rhs)
2020+
KStringLtExpr(this, lhs, rhs)
2021+
}
2022+
2023+
private val stringLeCache = mkAstInterner<KStringLeExpr>()
2024+
2025+
/**
2026+
* Create a lexicographic ordering reflexive closure (`<=` (less or equal)) expression.
2027+
* */
2028+
open fun mkStringLe(lhs: KExpr<KStringSort>, rhs: KExpr<KStringSort>): KExpr<KBoolSort> =
2029+
mkSimplified(lhs, rhs, KContext::mkStringLeNoSimplify, ::mkStringLeNoSimplify)
2030+
2031+
/**
2032+
* Create a lexicographic ordering reflexive closure (`<=` (less or equal)) expression.
2033+
* */
2034+
open fun mkStringLeNoSimplify(lhs: KExpr<KStringSort>, rhs: KExpr<KStringSort>): KStringLeExpr =
2035+
stringLeCache.createIfContextActive {
2036+
ensureContextMatch(lhs, rhs)
2037+
KStringLeExpr(this, lhs, rhs)
2038+
}
2039+
2040+
private val stringGtCache = mkAstInterner<KStringGtExpr>()
2041+
2042+
/**
2043+
* Create a lexicographic ordering (`>` (greater)) expression.
2044+
* */
2045+
open fun mkStringGt(lhs: KExpr<KStringSort>, rhs: KExpr<KStringSort>): KExpr<KBoolSort> =
2046+
mkSimplified(lhs, rhs, KContext::mkStringGtNoSimplify, ::mkStringGtNoSimplify)
2047+
2048+
/**
2049+
* Create a lexicographic ordering (`>` (greater)) expression.
2050+
* */
2051+
open fun mkStringGtNoSimplify(lhs: KExpr<KStringSort>, rhs: KExpr<KStringSort>): KStringGtExpr =
2052+
stringGtCache.createIfContextActive {
2053+
ensureContextMatch(lhs, rhs)
2054+
KStringGtExpr(this, lhs, rhs)
2055+
}
2056+
2057+
private val stringGeCache = mkAstInterner<KStringGeExpr>()
2058+
2059+
/**
2060+
* Create a lexicographic ordering reflexive closure (`>=` (greater or equal)) expression.
2061+
* */
2062+
open fun mkStringGe(lhs: KExpr<KStringSort>, rhs: KExpr<KStringSort>): KExpr<KBoolSort> =
2063+
mkSimplified(lhs, rhs, KContext::mkStringGeNoSimplify, ::mkStringGeNoSimplify)
2064+
2065+
/**
2066+
* Create a lexicographic ordering reflexive closure (`>=` (greater or equal)) expression.
2067+
* */
2068+
open fun mkStringGeNoSimplify(lhs: KExpr<KStringSort>, rhs: KExpr<KStringSort>): KStringGeExpr =
2069+
stringGeCache.createIfContextActive {
2070+
ensureContextMatch(lhs, rhs)
2071+
KStringGeExpr(this, lhs, rhs)
2072+
}
2073+
19982074
private val stringToRegexExprCache = mkAstInterner<KStringToRegexExpr>()
19992075

20002076
/**
@@ -4751,6 +4827,14 @@ open class KContext(
47514827

47524828
fun mkPrefixOfDecl(): KPrefixOfDecl = KPrefixOfDecl(this)
47534829

4830+
fun mkStringLtDecl(): KStringLtDecl = KStringLtDecl(this)
4831+
4832+
fun mkStringLeDecl(): KStringLeDecl = KStringLeDecl(this)
4833+
4834+
fun mkStringGtDecl(): KStringGtDecl = KStringGtDecl(this)
4835+
4836+
fun mkStringGeDecl(): KStringGeDecl = KStringGeDecl(this)
4837+
47544838
// regex
47554839
fun mkRegexLiteralDecl(value: String): KRegexLiteralDecl = KRegexLiteralDecl(this, value)
47564840

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +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.KIntSort
76
import io.ksmt.sort.KRegexSort
8-
import io.ksmt.sort.KStringSort
97

108
class KRegexLiteralDecl internal constructor(
119
ctx: KContext,

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

Lines changed: 24 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ 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
76
import io.ksmt.sort.KBoolSort
87
import io.ksmt.sort.KIntSort
98
import io.ksmt.sort.KRegexSort
@@ -98,3 +97,27 @@ class KPrefixOfDecl internal constructor(
9897
arg1: KExpr<KStringSort>
9998
): KApp<KBoolSort, *> = mkPrefixOfNoSimplify(arg0, arg1)
10099
}
100+
101+
class KStringLtDecl internal constructor(ctx: KContext) :
102+
KFuncDecl2<KBoolSort, KStringSort, KStringSort>(ctx, "stringLt", ctx.mkBoolSort(), ctx.mkStringSort(), ctx.mkStringSort()) {
103+
override fun KContext.apply(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KApp<KBoolSort, *> = mkStringLtNoSimplify(arg0, arg1)
104+
override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
105+
}
106+
107+
class KStringLeDecl internal constructor(ctx: KContext) :
108+
KFuncDecl2<KBoolSort, KStringSort, KStringSort>(ctx, "stringLe", ctx.mkBoolSort(), ctx.mkStringSort(), ctx.mkStringSort()) {
109+
override fun KContext.apply(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KApp<KBoolSort, *> = mkStringLeNoSimplify(arg0, arg1)
110+
override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
111+
}
112+
113+
class KStringGtDecl internal constructor(ctx: KContext) :
114+
KFuncDecl2<KBoolSort, KStringSort, KStringSort>(ctx, "stringGt", ctx.mkBoolSort(), ctx.mkStringSort(), ctx.mkStringSort()) {
115+
override fun KContext.apply(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KApp<KBoolSort, *> = mkStringGtNoSimplify(arg0, arg1)
116+
override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
117+
}
118+
119+
class KStringGeDecl internal constructor(ctx: KContext) :
120+
KFuncDecl2<KBoolSort, KStringSort, KStringSort>(ctx, "stringGe", ctx.mkBoolSort(), ctx.mkStringSort(), ctx.mkStringSort()) {
121+
override fun KContext.apply(arg0: KExpr<KStringSort>, arg1: KExpr<KStringSort>): KApp<KBoolSort, *> = mkStringGeNoSimplify(arg0, arg1)
122+
override fun <R> accept(visitor: KDeclVisitor<R>): R = visitor.visit(this)
123+
}

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,12 @@ 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.*
6+
import io.ksmt.decl.KDecl
7+
import io.ksmt.decl.KRegexKleeneClosureDecl
8+
import io.ksmt.decl.KRegexLiteralDecl
9+
import io.ksmt.decl.KRegexKleeneCrossDecl
710
import io.ksmt.expr.transformer.KTransformerBase
811
import io.ksmt.sort.KRegexSort
9-
import io.ksmt.sort.KStringSort
1012

1113
class KRegexLiteralExpr internal constructor(
1214
ctx: KContext,

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

Lines changed: 99 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,21 @@ 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.*
6+
import io.ksmt.decl.KDecl
7+
import io.ksmt.decl.KStringLenDecl
8+
import io.ksmt.decl.KStringLiteralDecl
9+
import io.ksmt.decl.KStringLtDecl
10+
import io.ksmt.decl.KStringLeDecl
11+
import io.ksmt.decl.KStringGtDecl
12+
import io.ksmt.decl.KStringGeDecl
13+
import io.ksmt.decl.KStringToRegexDecl
14+
import io.ksmt.decl.KStringInRegexDecl
715
import io.ksmt.expr.transformer.KTransformerBase
8-
import io.ksmt.sort.*
16+
import io.ksmt.sort.KSort
17+
import io.ksmt.sort.KBoolSort
18+
import io.ksmt.sort.KIntSort
19+
import io.ksmt.sort.KRegexSort
20+
import io.ksmt.sort.KStringSort
921
import io.ksmt.utils.cast
1022

1123
class KStringLiteralExpr internal constructor(
@@ -97,7 +109,7 @@ class KStringInRegexExpr internal constructor(
97109
override val args: List<KExpr<KSort>>
98110
get() = listOf(arg0.cast(), arg1.cast())
99111

100-
override val decl: KDecl<KBoolSort>
112+
override val decl: KStringInRegexDecl
101113
get() = ctx.mkStringInRegexDecl()
102114

103115
override fun accept(transformer: KTransformerBase): KExpr<KBoolSort> {
@@ -149,3 +161,87 @@ class KPrefixOfExpr internal constructor(
149161
override fun internHashCode(): Int = hash(arg0, arg1)
150162
override fun internEquals(other: Any): Boolean = structurallyEqual(other, { arg0 }, { arg1 })
151163
}
164+
165+
class KStringLtExpr internal constructor(
166+
ctx: KContext,
167+
val lhs: KExpr<KStringSort>,
168+
val rhs: KExpr<KStringSort>
169+
) : KApp<KBoolSort, KStringSort>(ctx) {
170+
override val sort: KBoolSort = ctx.boolSort
171+
172+
override val decl: KStringLtDecl
173+
get() = ctx.mkStringLtDecl()
174+
175+
override val args: List<KExpr<KStringSort>>
176+
get() = listOf(lhs, rhs)
177+
178+
override fun accept(transformer: KTransformerBase): KExpr<KBoolSort> {
179+
TODO("Not yet implemented")
180+
}
181+
182+
override fun internHashCode(): Int = hash(lhs, rhs)
183+
override fun internEquals(other: Any): Boolean = structurallyEqual(other, { lhs }, { rhs })
184+
}
185+
186+
class KStringLeExpr internal constructor(
187+
ctx: KContext,
188+
val lhs: KExpr<KStringSort>,
189+
val rhs: KExpr<KStringSort>
190+
) : KApp<KBoolSort, KStringSort>(ctx) {
191+
override val sort: KBoolSort = ctx.boolSort
192+
193+
override val decl: KStringLeDecl
194+
get() = ctx.mkStringLeDecl()
195+
196+
override val args: List<KExpr<KStringSort>>
197+
get() = listOf(lhs, rhs)
198+
199+
override fun accept(transformer: KTransformerBase): KExpr<KBoolSort> {
200+
TODO("Not yet implemented")
201+
}
202+
203+
override fun internHashCode(): Int = hash(lhs, rhs)
204+
override fun internEquals(other: Any): Boolean = structurallyEqual(other, { lhs }, { rhs })
205+
}
206+
207+
class KStringGtExpr internal constructor(
208+
ctx: KContext,
209+
val lhs: KExpr<KStringSort>,
210+
val rhs: KExpr<KStringSort>
211+
) : KApp<KBoolSort, KStringSort>(ctx) {
212+
override val sort: KBoolSort = ctx.boolSort
213+
214+
override val decl: KStringGtDecl
215+
get() = ctx.mkStringGtDecl()
216+
217+
override val args: List<KExpr<KStringSort>>
218+
get() = listOf(lhs, rhs)
219+
220+
override fun accept(transformer: KTransformerBase): KExpr<KBoolSort> {
221+
TODO("Not yet implemented")
222+
}
223+
224+
override fun internHashCode(): Int = hash(lhs, rhs)
225+
override fun internEquals(other: Any): Boolean = structurallyEqual(other, { lhs }, { rhs })
226+
}
227+
228+
class KStringGeExpr internal constructor(
229+
ctx: KContext,
230+
val lhs: KExpr<KStringSort>,
231+
val rhs: KExpr<KStringSort>
232+
) : KApp<KBoolSort, KStringSort>(ctx) {
233+
override val sort: KBoolSort = ctx.boolSort
234+
235+
override val decl: KStringGeDecl
236+
get() = ctx.mkStringGeDecl()
237+
238+
override val args: List<KExpr<KStringSort>>
239+
get() = listOf(lhs, rhs)
240+
241+
override fun accept(transformer: KTransformerBase): KExpr<KBoolSort> {
242+
TODO("Not yet implemented")
243+
}
244+
245+
override fun internHashCode(): Int = hash(lhs, rhs)
246+
override fun internEquals(other: Any): Boolean = structurallyEqual(other, { lhs }, { rhs })
247+
}

0 commit comments

Comments
 (0)