SortKind

Every Sort has an associated kind, represented as enum cvc5.SortKind.


class cvc5.SortKind(value)

The SortKind enum

ABSTRACT_SORT

An abstract sort.

An abstract sort represents a sort whose parameters or argument sorts are unspecified. For example, mkAbstractSort(BITVECTOR_SORT) returns a sort that represents the sort of bit-vectors whose bit-width is unspecified.

ARRAY_SORT

An array sort, whose argument sorts are the index and element sorts of the array.

BAG_SORT

A bag sort, whose argument sort is the element sort of the bag.

BITVECTOR_SORT

A bit-vector sort, parameterized by an integer denoting its bit-width.

BOOLEAN_SORT

The Boolean sort.

DATATYPE_SORT

A datatype sort.

FINITE_FIELD_SORT

A finite field sort, parameterized by a size.

FLOATINGPOINT_SORT

A floating-point sort, parameterized by two integers denoting its exponent and significand bit-widths.

FUNCTION_SORT

A function sort with given domain sorts and codomain sort.

INTEGER_SORT

The integer sort.

INTERNAL_SORT_KIND

Internal kind.

This kind serves as an abstraction for internal kinds that are not exposed via the API but may appear in terms returned by API functions, e.g., when querying the simplified form of a term.

Note

Should never be created via the API.

LAST_SORT_KIND

Marks the upper-bound of this enumeration.

NULLABLE_SORT

A nullable sort, whose argument sort denotes the sort of the direct child of the nullable.

NULL_SORT

Null kind.

The kind of a null sort (Sort::Sort()).

Note

May not be explicitly created via API functions other than Sort::Sort().

REAL_SORT

The real sort.

REGLAN_SORT

The regular language sort.

ROUNDINGMODE_SORT

The rounding mode sort.

SEQUENCE_SORT

A sequence sort, whose argument sort is the element sort of the sequence.

SET_SORT

A set sort, whose argument sort is the element sort of the set.

STRING_SORT

The string sort.

TUPLE_SORT

A tuple sort, whose argument sorts denote the sorts of the direct children of the tuple.

UNDEFINED_SORT_KIND

Undefined kind.

Note

Should never be exposed or created via the API.

UNINTERPRETED_SORT

An uninterpreted sort.