Function z3_sys::Z3_mk_exists

pub unsafe extern "C" fn Z3_mk_exists(
    c: Z3_context,
    weight: c_uint,
    num_patterns: c_uint,
    patterns: *const Z3_pattern,
    num_decls: c_uint,
    sorts: *const Z3_sort,
    decl_names: *const Z3_symbol,
    body: Z3_ast
) -> Z3_ast

Create an exists formula. Similar to Z3_mk_forall.

See also:

• Z3_mk_pattern
• Z3_mk_bound
• Z3_mk_forall
• Z3_mk_quantifier