Skip to content

Commit cefcd15

Browse files
committed
Fix old and add new helper function for eval str literal operations
1 parent 33a862f commit cefcd15

1 file changed

Lines changed: 16 additions & 4 deletions

File tree

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

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -90,13 +90,25 @@ inline fun <K : KSort> tryEvalStringLiteralOperation(
9090
cont()
9191
}
9292

93-
inline fun tryEvalStringLiteralOperation(
93+
inline fun <K: KSort> tryEvalStringLiteralOperation(
9494
arg0: KExpr<KStringSort>,
9595
arg1: KExpr<KStringSort>,
96-
operation: (KStringLiteralExpr, KStringLiteralExpr) -> KStringLiteralExpr,
97-
cont: () -> KExpr<KStringSort>
98-
): KExpr<KStringSort> = if (arg0 is KStringLiteralExpr && arg1 is KStringLiteralExpr) {
96+
operation: (KStringLiteralExpr, KStringLiteralExpr) -> KInterpretedValue<K>,
97+
cont: () -> KExpr<K>
98+
): KExpr<K> = if (arg0 is KStringLiteralExpr && arg1 is KStringLiteralExpr) {
9999
operation(arg0, arg1)
100100
} else {
101101
cont()
102102
}
103+
104+
inline fun <K: KSort> tryEvalStringLiteralOperation(
105+
arg0: KExpr<KStringSort>,
106+
arg1: KExpr<KStringSort>,
107+
arg2: KExpr<KStringSort>,
108+
operation: (KStringLiteralExpr, KStringLiteralExpr, KStringLiteralExpr) -> KInterpretedValue<K>,
109+
cont: () -> KExpr<K>
110+
): KExpr<K> = if (arg0 is KStringLiteralExpr && arg1 is KStringLiteralExpr && arg2 is KStringLiteralExpr) {
111+
operation(arg0, arg1, arg2)
112+
} else {
113+
cont()
114+
}

0 commit comments

Comments
 (0)