Skip to content

Commit ee0ff54

Browse files
committed
Syntactic sugar for strings literals and length expr
1 parent f9da6a6 commit ee0ff54

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1948,6 +1948,9 @@ open class KContext(
19481948
KStringLiteralExpr(this, value)
19491949
}
19501950

1951+
val String.expr
1952+
get() = mkStringLiteral(this)
1953+
19511954
private val stringConcatExprCache = mkAstInterner<KStringConcatExpr>()
19521955

19531956
/**
@@ -1987,6 +1990,12 @@ open class KContext(
19871990
KStringLenExpr(this, arg)
19881991
}
19891992

1993+
val KExpr<KStringSort>.len
1994+
get() = mkStringLen(this)
1995+
1996+
val String.len
1997+
get() = mkStringLen(this.expr)
1998+
19901999
private val suffixOfExprCache = mkAstInterner<KSuffixOfExpr>()
19912000

19922001
/**

0 commit comments

Comments
 (0)