Function z3_sys::Z3_mk_real [−][src]
pub unsafe extern "C" fn Z3_mk_real(
c: Z3_context,
num: c_int,
den: c_int
) -> Z3_ast
Expand description
Create a real from a fraction.
c
: logical context.num
: numerator of rational.den
: denominator of rational.
Preconditions:
den != 0