Function Z3_mk_quantifier_ex 

pub unsafe extern "C" fn Z3_mk_quantifier_ex(
    c: Z3_context,
    is_forall: bool,
    weight: c_uint,
    quantifier_id: Z3_symbol,
    skolem_id: Z3_symbol,
    num_patterns: c_uint,
    patterns: *const Z3_pattern,
    num_no_patterns: c_uint,
    no_patterns: *const Z3_ast,
    num_decls: c_uint,
    sorts: *const Z3_sort,
    decl_names: *const Z3_symbol,
    body: Z3_ast,
) -> Z3_ast

Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes

• c: logical context.
• is_forall: flag to indicate if this is a universal or existential quantifier.
• quantifier_id: identifier to identify quantifier
• skolem_id: identifier to identify skolem constants introduced by quantifier.
• weight: quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
• num_patterns: number of patterns.
• patterns: array containing the patterns created using Z3_mk_pattern.
• num_no_patterns: number of no_patterns.
• no_patterns: array containing subexpressions to be excluded from inferred patterns.
• num_decls: number of variables to be bound.
• sorts: array of sorts of the bound variables.
• decl_names: names of the bound variables.
• body: the body of the quantifier.

See also:

• Z3_mk_pattern
• Z3_mk_bound
• Z3_mk_forall
• Z3_mk_exists