mk_quantifier method

Z3_ast mk_quantifier(Z3_context c, bool is_forall, int weight, int num_patterns, Pointer<Z3_pattern> patterns, int num_decls, Pointer<Z3_sort> sorts, Pointer<Z3_symbol> decl_names, Z3_ast body,)

\brief Create a quantifier - universal or existential, with pattern hints. See the documentation for #Z3_mk_forall for an explanation of the parameters.

\param c logical context. \param is_forall flag to indicate if this is a universal or existential quantifier. \param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. \param num_patterns number of patterns. \param patterns array containing the patterns created using #Z3_mk_pattern. \param num_decls number of variables to be bound. \param sorts array of sorts of the bound variables. \param decl_names names of the bound variables. \param body the body of the quantifier.

\sa Z3_mk_pattern \sa Z3_mk_bound \sa Z3_mk_forall \sa Z3_mk_exists

def_API('Z3_mk_quantifier', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(UINT), _in_array(3, PATTERN), _in(UINT), _in_array(5, SORT), _in_array(5, SYMBOL), _in(AST)))

Implementation

Z3_ast mk_quantifier(
  Z3_context c,
  bool is_forall,
  int weight,
  int num_patterns,
  ffi.Pointer<Z3_pattern> patterns,
  int num_decls,
  ffi.Pointer<Z3_sort> sorts,
  ffi.Pointer<Z3_symbol> decl_names,
  Z3_ast body,
) {
  return _mk_quantifier(
    c,
    is_forall,
    weight,
    num_patterns,
    patterns,
    num_decls,
    sorts,
    decl_names,
    body,
  );
}