Function z3_sys::Z3_algebraic_eval

source · 
pub unsafe extern "C" fn Z3_algebraic_eval(
    c: Z3_context,
    p: Z3_ast,
    n: c_uint,
    a: *mut Z3_ast
) -> c_int
Expand description

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

See also: