Go to the source code of this file.
Functions | |
Polynomials | |
Z3_ast_vector Z3_API | Z3_polynomial_subresultants (Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) |
Return the nonzero subresultants of p and q with respect to the "variable" x . More... | |
Z3_ast_vector Z3_API Z3_polynomial_subresultants | ( | Z3_context | c, |
Z3_ast | p, | ||
Z3_ast | q, | ||
Z3_ast | x | ||
) |
Return the nonzero subresultants of p
and q
with respect to the "variable" x
.
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