Function z3_sys::Z3_algebraic_roots

source · 
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)

See also: