Function z3_sys::Z3_mk_real

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

See also: