Function z3_sys::Z3_mk_numeral

source · 
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.

See also: