Function z3_sys::Z3_rcf_mk_roots

source ·
pub unsafe extern "C" fn Z3_rcf_mk_roots(
    c: Z3_context,
    n: c_uint,
    a: *const Z3_rcf_num,
    roots: *mut Z3_rcf_num
) -> c_uint
Expand description

Store in roots the roots of the polynomial a[n-1]*x^{n-1} + ... + a[0]. The output vector roots must have size n. It returns the number of roots of the polynomial.

Preconditions:

  • The input polynomial is not the zero polynomial.