ksmt-core/io.ksmt/KContext/mkRealNum

mkRealNum

fun mkRealNum(numerator: KIntNumExpr, denominator: KIntNumExpr): KRealNumExpr
fun mkRealNum(numerator: KIntNumExpr): KRealNumExpr
fun mkRealNum(numerator: Int): KRealNumExpr
fun mkRealNum(numerator: Int, denominator: Int): KRealNumExpr
fun mkRealNum(numerator: Long): KRealNumExpr
fun mkRealNum(numerator: Long, denominator: Long): KRealNumExpr

Create a Real value.

fun mkRealNum(value: String): KRealNumExpr

Create a Real value from a string of the form "123/456".