Skip to main content

mk_abstract_sort

Function mk_abstract_sort 

Source
pub unsafe extern "C" fn mk_abstract_sort(
    tm: *mut TermManager,
    k: SortKind,
) -> Sort
Expand 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.