Function z3_sys::Z3_polynomial_subresultants

pub unsafe extern "C" fn Z3_polynomial_subresultants(
    c: Z3_context, 
    p: Z3_ast, 
    q: Z3_ast, 
    x: Z3_ast
) -> Z3_ast_vector

Return the nonzero subresultants of p and q with respect to the “variable” x.

Preconditions:

• p, q and x are Z3 expressions where p and q are arithmetic terms.

Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable. Example: f(a) is a considered to be a variable in the polynomial f(a)*f(a) + 2*f(a) + 1