Function z3_sys::Z3_mk_quantifier [−][src]
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
Expand description
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 usingZ3_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.