pub unsafe extern "C" fn mk_abstract_sort(
tm: *mut TermManager,
k: SortKind,
) -> SortExpand description
Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified.
The kind k must be the kind of a sort that can be abstracted, i.e., a
sort that has indices or argument sorts. For example,
#CVC5_SORT_KIND_ARRAY_SORT and #CVC5_SORT_KIND_BITVECTOR_SORT can be passed
as the kind k to this function, while #CVC5_SORT_KIND_INTEGER_SORT and
#CVC5_SORT_KIND_STRING_SORT cannot.
@note Providing the kind #CVC5_SORT_KIND_ABSTRACT_SORT as an argument to
this function returns the (fully) unspecified sort, denoted ?.
@note Providing a kind k that has no indices and a fixed arity
of argument sorts will return the sort of kind k whose arguments are
the unspecified sort. For example,
cvc5_mk_abstract_sort(tm, CVC5_SORT_KIND_ARRAY_SORT) will return the
sort (ARRAY_SORT ? ?) instead of the abstract sort whose abstract
kind is #CVC5_SORT_KIND_ARRAY_SORT.
@warning This function is experimental and may change in future versions.
@param tm The term manager instance. @param k The kind of the abstract sort @return The abstract sort.