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
Return the nonzero subresultants of p
and q
with respect to the "variable" x
.
- Precondition:
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 polynomialf(a)*f(a) + 2*f(a) + 1