Function z3_sys::Z3_mk_quantifier_ex
[−]
[src]
pub unsafe extern "C" fn Z3_mk_quantifier_ex(
c: Z3_context,
is_forall: Z3_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 quantifierskolem_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 usingZ3_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: