Z3
z3_polynomial.h File Reference

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...
 

Function Documentation

◆ Z3_polynomial_subresultants()

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.

Precondition
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