Function z3_sys::Z3_mk_exists [−][src]
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
Expand description
Create an exists formula. Similar to Z3_mk_forall
.