Function z3_sys::Z3_mk_quantifier_const
source · pub unsafe extern "C" fn Z3_mk_quantifier_const(
c: Z3_context,
is_forall: Z3_bool,
weight: c_uint,
num_bound: c_uint,
bound: *const Z3_app,
num_patterns: c_uint,
patterns: *const Z3_pattern,
body: Z3_ast
) -> Z3_ast
Expand description
Create a universal or existential quantifier using a list of constants that will form the set of bound variables.