Function z3_sys::Z3_rcf_mk_roots [−][src]
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.