[−][src]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 usingZ3_mk_pattern
.num_decls
: number of variables to be bound.sorts
: the sorts of the bound variables.decl_names
: names of the bound variablesbody
: the body of the quantifier.