mk_fresh_func_decl method

Z3_func_decl mk_fresh_func_decl(
  1. Z3_context c,
  2. Z3_string prefix,
  3. int domain_size,
  4. Pointer<Z3_sort> domain,
  5. Z3_sort range,
)

\brief Declare a fresh constant or function.

Z3 will generate an unique name for this function declaration. If prefix is different from \c NULL, then the name generate by Z3 will start with \c prefix.

\remark If \c prefix is \c NULL, then it is assumed to be the empty string.

\sa Z3_mk_func_decl

def_API('Z3_mk_fresh_func_decl', FUNC_DECL, (_in(CONTEXT), _in(STRING), _in(UINT), _in_array(2, SORT), _in(SORT)))

Implementation

Z3_func_decl mk_fresh_func_decl(
  Z3_context c,
  Z3_string prefix,
  int domain_size,
  ffi.Pointer<Z3_sort> domain,
  Z3_sort range,
) {
  return _mk_fresh_func_decl(
    c,
    prefix,
    domain_size,
    domain,
    range,
  );
}