[−][src]Function z3_sys::Z3_mk_forall_const

pub unsafe extern "C" fn Z3_mk_forall_const(
    c: Z3_context, 
    weight: c_uint, 
    num_bound: c_uint, 
    bound: *const Z3_app, 
    num_patterns: c_uint, 
    patterns: *const Z3_pattern, 
    body: Z3_ast
) -> Z3_ast

Create a universal quantifier using a list of constants that will form the set of bound variables.

  • 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_bound: number of constants to be abstracted into bound variables.
  • bound: array of constants to be abstracted into bound variables.
  • num_patterns: number of patterns.
  • patterns: array containing the patterns created using Z3_mk_pattern.
  • body: the body of the quantifier.

See also: