Function z3_sys::Z3_mk_forall

pub unsafe extern "C" fn Z3_mk_forall(
    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 a forall formula. It takes an expression body that contains bound variables of the same sorts as the sorts listed in the array sorts. The bound variables are de-Bruijn indices created using Z3_mk_bound. The array decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the decl_names and sorts array refers to the variable with index 0, the second to last element of decl_names and sorts refers to the variable with index 1, etc.

• 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_patterns: number of patterns.
• patterns: array containing the patterns created using Z3_mk_pattern.
• num_decls: number of variables to be bound.
• sorts: the 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_exists