mk_quantifier_ex method

Z3_ast mk_quantifier_ex(Z3_context c, bool is_forall, int weight, Z3_symbol quantifier_id, Z3_symbol skolem_id, int num_patterns, Pointer<Z3_pattern> patterns, int num_no_patterns, Pointer<Z3_ast> no_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, no patterns, and attributes

\param c logical context. \param is_forall flag to indicate if this is a universal or existential quantifier. \param quantifier_id identifier to identify quantifier \param skolem_id identifier to identify skolem constants introduced by 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_no_patterns number of no_patterns. \param no_patterns array containing subexpressions to be excluded from inferred patterns. \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_ex', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(5, PATTERN), _in(UINT), _in_array(7, AST), _in(UINT), _in_array(9, SORT), _in_array(9, SYMBOL), _in(AST)))

Implementation

Z3_ast mk_quantifier_ex(
  Z3_context c,
  bool is_forall,
  int weight,
  Z3_symbol quantifier_id,
  Z3_symbol skolem_id,
  int num_patterns,
  ffi.Pointer<Z3_pattern> patterns,
  int num_no_patterns,
  ffi.Pointer<Z3_ast> no_patterns,
  int num_decls,
  ffi.Pointer<Z3_sort> sorts,
  ffi.Pointer<Z3_symbol> decl_names,
  Z3_ast body,
) {
  return _mk_quantifier_ex(
    c,
    is_forall,
    weight,
    quantifier_id,
    skolem_id,
    num_patterns,
    patterns,
    num_no_patterns,
    no_patterns,
    num_decls,
    sorts,
    decl_names,
    body,
  );
}