Function z3_sys::Z3_mk_quantifier

pub unsafe extern "C" fn Z3_mk_quantifier(
    c: Z3_context, 
    is_forall: bool, 
    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 a quantifier - universal or existential, with pattern hints. See the documentation for Z3_mk_forall for an explanation of the parameters.

• c: logical context.
• is_forall: flag to indicate if this is a universal or existential 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_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