mk_forall method

Z3_ast mk_forall(Z3_context c, 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 forall formula. It takes an expression \c body that contains bound variables of the same sorts as the sorts listed in the array \c sorts. The bound variables are de-Bruijn indices created using #Z3_mk_bound. The array \c decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the \c decl_names and \c sorts array refers to the variable with index 0, the second to last element of \c decl_names and \c sorts refers to the variable with index 1, etc.

\param c logical context. \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 the 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_exists

def_API('Z3_mk_forall', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, PATTERN), _in(UINT), _in_array(4, SORT), _in_array(4, SYMBOL), _in(AST)))

Implementation

Z3_ast mk_forall(
  Z3_context c,
  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_forall(
    c,
    weight,
    num_patterns,
    patterns,
    num_decls,
    sorts,
    decl_names,
    body,
  );
}