mk_map method

Z3_ast mk_map(
  1. Z3_context c,
  2. Z3_func_decl f,
  3. int n,
  4. Pointer<Z3_ast> args,
)

\brief Map f on the argument arrays.

The \c n nodes \c args must be of array sorts \ccode{domain_i -> range_i}. The function declaration \c f must have type \ccode{ range_1 .. range_n -> range}. \c v must have sort range. The sort of the result is \ccode{domain_i -> range}.

\sa Z3_mk_array_sort \sa Z3_mk_store \sa Z3_mk_select

def_API('Z3_mk_map', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT), _in_array(2, AST)))

Implementation

Z3_ast mk_map(
  Z3_context c,
  Z3_func_decl f,
  int n,
  ffi.Pointer<Z3_ast> args,
) {
  return _mk_map(
    c,
    f,
    n,
    args,
  );
}