Skip to content

Commit f5bd81b

Browse files
raf-nrraf-nr
committed
Implement basic simplifications for mapping between str/int expressions
1 parent c98613a commit f5bd81b

4 files changed

Lines changed: 121 additions & 18 deletions

File tree

‎ksmt-core/src/main/kotlin/Main.kt‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
import io.ksmt.KContext
2+
import io.ksmt.utils.getValue
3+
4+
fun main() {
5+
val ctx = KContext(simplificationMode = KContext.SimplificationMode.SIMPLIFY)
6+
with(ctx) {
7+
println(mkStringFromInt( 2147483643337.expr))
8+
// val a by stringSort
9+
// val b by stringSort
10+
// println((a + "k".expr) + ("ok".expr + b))
11+
// println("aaaa".expr.len)
12+
}
13+
}

‎ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplification.kt‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -123,20 +123,20 @@ fun KContext.simplifyStringReverse(
123123

124124
fun KContext.simplifyStringIsDigit(
125125
arg: KExpr<KStringSort>
126-
): KExpr<KBoolSort> = mkStringIsDigitNoSimplify(arg) // Temporarily
126+
): KExpr<KBoolSort> = simplifyStringIsDigitExprBasic(arg, ::mkStringIsDigitNoSimplify)
127127

128128
fun KContext.simplifyStringToCode(
129129
arg: KExpr<KStringSort>
130-
): KExpr<KIntSort> = mkStringToCodeNoSimplify(arg) // Temporarily
130+
): KExpr<KIntSort> = simplifyStringToCodeExprBasic(arg, ::mkStringToCodeNoSimplify)
131131

132132
fun KContext.simplifyStringFromCode(
133133
arg: KExpr<KIntSort>
134-
): KExpr<KStringSort> = mkStringFromCodeNoSimplify(arg) // Temporarily
134+
): KExpr<KStringSort> = simplifyStringFromCodeExprBasic(arg, ::mkStringFromCodeNoSimplify)
135135

136136
fun KContext.simplifyStringToInt(
137137
arg: KExpr<KStringSort>
138-
): KExpr<KIntSort> = mkStringToIntNoSimplify(arg) // Temporarily
138+
): KExpr<KIntSort> = simplifyStringToIntExprBasic(arg, ::mkStringToIntNoSimplify)
139139

140140
fun KContext.simplifyStringFromInt(
141141
arg: KExpr<KIntSort>
142-
): KExpr<KStringSort> = mkStringFromIntNoSimplify(arg) // Temporarily
142+
): KExpr<KStringSort> = simplifyStringFromIntExprBasic(arg, ::mkStringFromIntNoSimplify)

‎ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/StringSimplificationRules.kt‎

Lines changed: 70 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import io.ksmt.sort.KIntSort
77
import io.ksmt.sort.KSort
88
import io.ksmt.sort.KStringSort
99
import io.ksmt.utils.StringUtils
10+
import io.ksmt.utils.StringUtils.STRING_FROM_CODE_UPPER_BOUND
1011

1112
/*
1213
* String concatenation simplification
@@ -191,7 +192,7 @@ inline fun KContext.simplifyStringBasicToUpperExpr(
191192
cont(arg)
192193
}
193194

194-
/** Reverses a string constant */
195+
/** Reverses a string constan.t */
195196
inline fun KContext.simplifyStringBasicReverseExpr(
196197
arg: KExpr<KStringSort>,
197198
cont: (KExpr<KStringSort>) -> KExpr<KStringSort>
@@ -200,6 +201,74 @@ inline fun KContext.simplifyStringBasicReverseExpr(
200201
cont(arg)
201202
}
202203

204+
/*
205+
* Mapping between strings and integers simplifications
206+
* */
207+
208+
/** Eval constants: if string literal consist of one digit - return true, otherwise false. */
209+
inline fun KContext.simplifyStringIsDigitExprBasic(
210+
arg: KExpr<KStringSort>,
211+
cont: (KExpr<KStringSort>) -> KExpr<KBoolSort>
212+
): KExpr<KBoolSort> =
213+
tryEvalStringLiteralOperation(arg, { a -> StringUtils.stringIsDigit(a) }) {
214+
cont(arg)
215+
}
216+
217+
/** Eval constants: if string literal consist of one character - return its code, otherwise return -1. */
218+
inline fun KContext.simplifyStringToCodeExprBasic(
219+
arg: KExpr<KStringSort>,
220+
cont: (KExpr<KStringSort>) -> KExpr<KIntSort>
221+
): KExpr<KIntSort> =
222+
tryEvalStringLiteralOperation(arg, { a -> StringUtils.stringToCode(a) }) {
223+
cont(arg)
224+
}
225+
226+
/** Eval constants: if int constant is in the range [0; STRING_FROM_CODE_UPPER_BOUND], then
227+
* return code point of constant, otherwise return empty string. */
228+
inline fun KContext.simplifyStringFromCodeExprBasic(
229+
arg: KExpr<KIntSort>,
230+
cont: (KExpr<KIntSort>) -> KExpr<KStringSort>
231+
): KExpr<KStringSort> {
232+
val value = when (arg) {
233+
is KInt32NumExpr -> arg.value.toLong()
234+
is KInt64NumExpr -> arg.value
235+
is KIntBigNumExpr -> arg.value.toLong()
236+
else -> return cont(arg)
237+
}
238+
239+
return if (value in 0..STRING_FROM_CODE_UPPER_BOUND) {
240+
mkStringLiteral(value.toInt().toChar().toString())
241+
} else {
242+
mkStringLiteral("")
243+
}
244+
}
245+
246+
/** Eval constants: if string literal consist of digits, then
247+
* return the positive integer denoted by literal;
248+
* otherwise, return -1. */
249+
inline fun KContext.simplifyStringToIntExprBasic(
250+
arg: KExpr<KStringSort>,
251+
cont: (KExpr<KStringSort>) -> KExpr<KIntSort>
252+
): KExpr<KIntSort> =
253+
tryEvalStringLiteralOperation(arg, { a -> StringUtils.stringToInt(a) }) {
254+
cont(arg)
255+
}
256+
257+
/** Eval constants: if the integer is non-negative, return its string representation;
258+
* otherwise, return an empty string. */
259+
inline fun KContext.simplifyStringFromIntExprBasic(
260+
arg: KExpr<KIntSort>,
261+
cont: (KExpr<KIntSort>) -> KExpr<KStringSort>
262+
): KExpr<KStringSort> {
263+
val intValue = when (arg) {
264+
is KInt32NumExpr -> arg.value.toLong()
265+
is KInt64NumExpr -> arg.value
266+
is KIntBigNumExpr -> arg.value.toLong()
267+
else -> return cont(arg)
268+
}
269+
return mkStringLiteral(if (intValue >= 0) intValue.toString() else "")
270+
}
271+
203272
inline fun <K : KSort> tryEvalStringLiteralOperation(
204273
arg: KExpr<KStringSort>,
205274
operation: (KStringLiteralExpr) -> KInterpretedValue<K>,

‎ksmt-core/src/main/kotlin/io/ksmt/utils/StringUtils.kt‎

Lines changed: 33 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -7,67 +7,88 @@ import io.ksmt.expr.KIntNumExpr
77
import io.ksmt.expr.KInterpretedValue
88
import io.ksmt.expr.KStringLiteralExpr
99
import io.ksmt.sort.KBoolSort
10+
import io.ksmt.sort.KStringSort
1011

1112
object StringUtils {
1213

14+
const val STRING_FROM_CODE_UPPER_BOUND: Int = 196607
15+
1316
@JvmStatic
14-
fun getStringLen(arg: KStringLiteralExpr): KIntNumExpr = with (arg.ctx) {
17+
fun getStringLen(arg: KStringLiteralExpr): KIntNumExpr = with(arg.ctx) {
1518
mkIntNum(arg.value.length)
1619
}
1720

1821
@JvmStatic
19-
fun concatStrings(lhs: KStringLiteralExpr, rhs: KStringLiteralExpr): KStringLiteralExpr = with (lhs.ctx) {
22+
fun concatStrings(lhs: KStringLiteralExpr, rhs: KStringLiteralExpr): KStringLiteralExpr = with(lhs.ctx) {
2023
mkStringLiteral(lhs.value + rhs.value)
2124
}
2225

2326
@JvmStatic
24-
fun isStringSuffix(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
27+
fun isStringSuffix(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with(arg0.ctx) {
2528
mkBool(arg1.value.endsWith(arg0.value)).uncheckedCast()
2629
}
2730

2831
@JvmStatic
29-
fun isStringPrefix(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
32+
fun isStringPrefix(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with(arg0.ctx) {
3033
mkBool(arg1.value.startsWith(arg0.value)).uncheckedCast()
3134
}
3235

3336
@JvmStatic
34-
fun stringLt(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
37+
fun stringLt(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with(arg0.ctx) {
3538
mkBool(arg0.value < arg1.value).uncheckedCast()
3639
}
3740

3841
@JvmStatic
39-
fun stringLe(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
42+
fun stringLe(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with(arg0.ctx) {
4043
mkBool(arg0.value <= arg1.value).uncheckedCast()
4144
}
4245

4346
@JvmStatic
44-
fun stringGt(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
47+
fun stringGt(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with(arg0.ctx) {
4548
mkBool(arg0.value > arg1.value).uncheckedCast()
4649
}
4750

4851
@JvmStatic
49-
fun stringGe(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
52+
fun stringGe(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with(arg0.ctx) {
5053
mkBool(arg0.value >= arg1.value).uncheckedCast()
5154
}
5255

5356
@JvmStatic
54-
fun stringContains(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with (arg0.ctx) {
57+
fun stringContains(arg0: KStringLiteralExpr, arg1: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with(arg0.ctx) {
5558
mkBool(arg0.value.contains(arg1.value)).uncheckedCast()
5659
}
5760

5861
@JvmStatic
59-
fun stringToLowerCase(arg: KStringLiteralExpr): KStringLiteralExpr = with (arg.ctx) {
62+
fun stringToLowerCase(arg: KStringLiteralExpr): KStringLiteralExpr = with(arg.ctx) {
6063
mkStringLiteral(arg.value.lowercase())
6164
}
6265

6366
@JvmStatic
64-
fun stringToUpperCase(arg: KStringLiteralExpr): KStringLiteralExpr = with (arg.ctx) {
67+
fun stringToUpperCase(arg: KStringLiteralExpr): KStringLiteralExpr = with(arg.ctx) {
6568
mkStringLiteral(arg.value.uppercase())
6669
}
6770

6871
@JvmStatic
69-
fun stringReverse(arg: KStringLiteralExpr): KStringLiteralExpr = with (arg.ctx) {
72+
fun stringReverse(arg: KStringLiteralExpr): KStringLiteralExpr = with(arg.ctx) {
7073
mkStringLiteral(arg.value.reversed())
7174
}
7275

76+
@JvmStatic
77+
fun stringIsDigit(arg: KStringLiteralExpr): KInterpretedValue<KBoolSort> = with(arg.ctx) {
78+
mkBool(arg.value.length == 1 && arg.value[0].isDigit()).uncheckedCast()
79+
}
80+
81+
@JvmStatic
82+
fun stringToCode(arg: KStringLiteralExpr): KIntNumExpr = with(arg.ctx) {
83+
mkIntNum(arg.value.singleOrNull()?.code ?: -1)
84+
}
85+
86+
@JvmStatic
87+
fun stringToInt(arg: KStringLiteralExpr): KIntNumExpr = with(arg.ctx) {
88+
return if (arg.value.isNotEmpty() && arg.value.all { it.isDigit() }) {
89+
mkIntNum(arg.value.toLongOrNull() ?: -1)
90+
} else {
91+
mkIntNum(-1)
92+
}
93+
}
7394
}

0 commit comments

Comments
 (0)