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`