solver_get_levels method

void solver_get_levels(
  1. Z3_context c,
  2. Z3_solver s,
  3. Z3_ast_vector literals,
  4. int sz,
  5. Pointer<UnsignedInt> levels,
)

\brief retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat call and no other calls (to extract models) have been invoked.

def_API('Z3_solver_get_levels', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(UINT), _in_array(3, UINT)))

Implementation

void solver_get_levels(
  Z3_context c,
  Z3_solver s,
  Z3_ast_vector literals,
  int sz,
  ffi.Pointer<ffi.UnsignedInt> levels,
) {
  return _solver_get_levels(
    c,
    s,
    literals,
    sz,
    levels,
  );
}