[][src]Function z3_sys::Z3_rcf_get_numerator_denominator

pub unsafe extern "C" fn Z3_rcf_get_numerator_denominator(
    c: Z3_context,
    a: Z3_rcf_num,
    n: *mut Z3_rcf_num,
    d: *mut Z3_rcf_num
)

Extract the "numerator" and "denominator" of the given RCF numeral.

We have that a = n/d, moreover n and d are not represented using rational functions.