mk_datatype_sort method

Z3_sort mk_datatype_sort(
  1. Z3_context c,
  2. Z3_symbol name
)

\brief create a forward reference to a recursive datatype being declared. The forward reference can be used in a nested occurrence: the range of an array or as element sort of a sequence. The forward reference should only be used when used in an accessor for a recursive datatype that gets declared.

Forward references can replace the use sort references, that are unsigned integers in the \c Z3_mk_constructor call

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

Implementation

Z3_sort mk_datatype_sort(
  Z3_context c,
  Z3_symbol name,
) {
  return _mk_datatype_sort(
    c,
    name,
  );
}