[−][src]Function z3_sys::Z3_algebraic_eval
pub unsafe extern "C" fn Z3_algebraic_eval(
c: Z3_context,
p: Z3_ast,
n: c_uint,
a: *mut Z3_ast
) -> c_int
Given a multivariate polynomial p(x_0, ..., x_{n-1})
, return the
sign of p(a[0], ..., a[n-1])
.
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])