Function z3_sys::Z3_algebraic_roots [−][src]
pub unsafe extern "C" fn Z3_algebraic_roots(
c: Z3_context,
p: Z3_ast,
n: c_uint,
a: *mut Z3_ast
) -> Z3_ast_vector
Expand description
Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n)
, returns the
roots of the univariate polynomial p(a[0], ..., a[n-1], x_n)
.
Preconditions:
p
is a Z3 expression that contains only arithmetic terms and free variables.forall i in [0, n) Z3_algebraic_is_value(c, a[i])
Postconditions:
forall r in result Z3_algebraic_is_value(c, result)