algebraic_roots method

Z3_ast_vector algebraic_roots(
  1. Z3_context c,
  2. Z3_ast p,
  3. int n,
  4. Pointer<Z3_ast> a,
)

\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polynomial p(a0, ..., an-1, x_n).

\pre p is a Z3 expression that contains only arithmetic terms and free variables. \pre forall i in [0, n) Z3_algebraic_is_value(c, ai) \post forall r in result Z3_algebraic_is_value(c, result)

def_API('Z3_algebraic_roots', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))

Implementation

Z3_ast_vector algebraic_roots(
  Z3_context c,
  Z3_ast p,
  int n,
  ffi.Pointer<Z3_ast> a,
) {
  return _algebraic_roots(
    c,
    p,
    n,
    a,
  );
}