algebraic_eval method

int algebraic_eval(
  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}), return the sign of p(a0, ..., an-1).

\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)

def_API('Z3_algebraic_eval', INT, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))

Implementation

int algebraic_eval(
  Z3_context c,
  Z3_ast p,
  int n,
  ffi.Pointer<Z3_ast> a,
) {
  return _algebraic_eval(
    c,
    p,
    n,
    a,
  );
}