mk_func_decl method

Z3_func_decl mk_func_decl(Z3_context c, Z3_symbol s, int domain_size, Pointer<Z3_sort> domain, Z3_sort range,)

\brief Declare a constant or function.

\param c logical context. \param s name of the constant or function. \param domain_size number of arguments. It is 0 when declaring a constant. \param domain array containing the sort of each argument. The array must contain domain_size elements. It is 0 when declaring a constant. \param range sort of the constant or the return sort of the function.

After declaring a constant or function, the function #Z3_mk_app can be used to create a constant or function application.

\sa Z3_mk_app \sa Z3_mk_fresh_func_decl \sa Z3_mk_rec_func_decl

def_API('Z3_mk_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))

Implementation

Z3_func_decl mk_func_decl(
  Z3_context c,
  Z3_symbol s,
  int domain_size,
  ffi.Pointer<Z3_sort> domain,
  Z3_sort range,
) {
  return _mk_func_decl(
    c,
    s,
    domain_size,
    domain,
    range,
  );
}