mk_list_sort method

Z3_sort mk_list_sort(
  1. Z3_context c,
  2. Z3_symbol name,
  3. Z3_sort elem_sort,
  4. Pointer<Z3_func_decl> nil_decl,
  5. Pointer<Z3_func_decl> is_nil_decl,
  6. Pointer<Z3_func_decl> cons_decl,
  7. Pointer<Z3_func_decl> is_cons_decl,
  8. Pointer<Z3_func_decl> head_decl,
  9. Pointer<Z3_func_decl> tail_decl,
)

\brief Create a list sort

A list sort over \c elem_sort This function declares the corresponding constructors and testers for lists.

\param c logical context \param name name of the list sort. \param elem_sort sort of list elements. \param nil_decl declaration for the empty list. \param is_nil_decl test for the empty list. \param cons_decl declaration for a cons cell. \param is_cons_decl cons cell test. \param head_decl list head. \param tail_decl list tail.

def_API('Z3_mk_list_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(SORT), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL), _out(FUNC_DECL)))

Implementation

Z3_sort mk_list_sort(
  Z3_context c,
  Z3_symbol name,
  Z3_sort elem_sort,
  ffi.Pointer<Z3_func_decl> nil_decl,
  ffi.Pointer<Z3_func_decl> is_nil_decl,
  ffi.Pointer<Z3_func_decl> cons_decl,
  ffi.Pointer<Z3_func_decl> is_cons_decl,
  ffi.Pointer<Z3_func_decl> head_decl,
  ffi.Pointer<Z3_func_decl> tail_decl,
) {
  return _mk_list_sort(
    c,
    name,
    elem_sort,
    nil_decl,
    is_nil_decl,
    cons_decl,
    is_cons_decl,
    head_decl,
    tail_decl,
  );
}