Function z3_sys::Z3_mk_numeral [−][src]
pub unsafe extern "C" fn Z3_mk_numeral(
c: Z3_context,
numeral: Z3_string,
ty: Z3_sort
) -> Z3_ast
Expand description
Create a numeral of a given sort.
c
: logical context.numeral
: A string representing the numeral value in decimal notation. The string may be of the form[num]*[.[num]*][E[+|-][num]+]
. If the given sort is a real, then the numeral can be a rational, that is, a string of the form[num]* / [num]*
.ty
: The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size.