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
Create a real from a fraction.
-
c
: logical context. -
num
: numerator of rational. -
den
: denominator of rational.
- Precondition:
den != 0
See also: