mk_datatype_sort method
\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,
);
}