Function z3_sys::Z3_polynomial_subresultants [−][src]
pub unsafe extern "C" fn Z3_polynomial_subresultants(
c: Z3_context,
p: Z3_ast,
q: Z3_ast,
x: Z3_ast
) -> Z3_ast_vector
Expand description
Return the nonzero subresultants of p
and q
with respect to the “variable” x
.
Preconditions:
p
,q
andx
are Z3 expressions wherep
andq
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