mk_uninterpreted_sort method

Z3_sort mk_uninterpreted_sort(Z3_context c, Z3_symbol s)

\brief Create a free (uninterpreted) type using the given name (symbol).

Two free types are considered the same iff the have the same name.

def_API('Z3_mk_uninterpreted_sort', SORT, (_in(CONTEXT), _in(SYMBOL)))

Implementation

Z3_sort mk_uninterpreted_sort(
  Z3_context c,
  Z3_symbol s,
) {
  return _mk_uninterpreted_sort(
    c,
    s,
  );
}