Function z3_sys::Z3_mk_exists_const [−][src]
pub unsafe extern "C" fn Z3_mk_exists_const(
c: Z3_context,
weight: c_uint,
num_bound: c_uint,
bound: *const Z3_app,
num_patterns: c_uint,
patterns: *const Z3_pattern,
body: Z3_ast
) -> Z3_ast
Expand description
Similar to Z3_mk_forall_const
.
Create an existential quantifier using a list of constants that will form the set of bound variables.
c
: logical context.weight
: quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.num_bound
: number of constants to be abstracted into bound variables.bound
: array of constants to be abstracted into bound variables.num_patterns
: number of patterns.patterns
: array containing the patterns created usingZ3_mk_pattern
.body
: the body of the quantifier.