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