mk_exists method

Z3_ast mk_exists(
  1. Z3_context c,
  2. int weight,
  3. int num_patterns,
  4. Pointer<Z3_pattern> patterns,
  5. int num_decls,
  6. Pointer<Z3_sort> sorts,
  7. Pointer<Z3_symbol> decl_names,
  8. Z3_ast body,
)

\brief Create an exists formula. Similar to #Z3_mk_forall.

\sa Z3_mk_pattern \sa Z3_mk_bound \sa Z3_mk_forall \sa Z3_mk_quantifier

def_API('Z3_mk_exists', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, PATTERN), _in(UINT), _in_array(4, SORT), _in_array(4, SYMBOL), _in(AST)))

Implementation

Z3_ast mk_exists(
  Z3_context c,
  int weight,
  int num_patterns,
  ffi.Pointer<Z3_pattern> patterns,
  int num_decls,
  ffi.Pointer<Z3_sort> sorts,
  ffi.Pointer<Z3_symbol> decl_names,
  Z3_ast body,
) {
  return _mk_exists(
    c,
    weight,
    num_patterns,
    patterns,
    num_decls,
    sorts,
    decl_names,
    body,
  );
}