Package io.github.cvc5
Enum Class SortKind
- All Implemented Interfaces:
Serializable,Comparable<SortKind>,Constable
Enum representing the set of possible values for SortKind.
-
Nested Class Summary
Nested classes/interfaces inherited from class java.lang.Enum
Enum.EnumDesc<E extends Enum<E>> -
Enum Constant Summary
Enum ConstantsEnum ConstantDescriptionAn abstract sort.An array sort, whose argument sorts are the index and element sorts of the array.A bag sort, whose argument sort is the element sort of the bag.A bit-vector sort, parameterized by an integer denoting its bit-width.The Boolean sort.A datatype sort.A finite field sort, parameterized by a size.A floating-point sort, parameterized by two integers denoting its exponent and significand bit-widths.A function sort with given domain sorts and codomain sort.The integer sort.Internal kind.Marks the upper-bound of this enumeration.Null kind.A nullable sort, whose argument sort denotes the sort of the direct child of the nullable.The real sort.The regular language sort.The rounding mode sort.A sequence sort, whose argument sort is the element sort of the sequence.A set sort, whose argument sort is the element sort of the set.The string sort.A tuple sort, whose argument sorts denote the sorts of the direct children of the tuple.Undefined kind.An uninterpreted sort. -
Method Summary
Modifier and TypeMethodDescriptionstatic SortKindfromInt(int value) Converts an integer value to the corresponding enum constant.intgetValue()Get the integer value associated with this enum constant.static SortKindReturns the enum constant of this class with the specified name.static SortKind[]values()Returns an array containing the constants of this enum class, in the order they are declared.
-
Enum Constant Details
-
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.
-
UNDEFINED_SORT_KIND
Undefined kind.- Note:
- Should never be exposed or created via the API.
-
NULL_SORT
Null kind. The kind of a null sort (Sort()).- Note:
- May not be explicitly created via API functions other than
Sort().
-
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.- Create Sort of this Kind with:
-
ARRAY_SORT
An array sort, whose argument sorts are the index and element sorts of the array.- Create Sort of this Kind with:
-
BAG_SORT
A bag sort, whose argument sort is the element sort of the bag.- Create Sort of this Kind with:
-
BOOLEAN_SORT
The Boolean sort.- Create Sort of this Kind with:
-
BITVECTOR_SORT
A bit-vector sort, parameterized by an integer denoting its bit-width.- Create Sort of this Kind with:
-
DATATYPE_SORT
A datatype sort.- Create Sort of this Kind with:
-
FINITE_FIELD_SORT
A finite field sort, parameterized by a size.- Create Sort of this Kind with:
-
FLOATINGPOINT_SORT
A floating-point sort, parameterized by two integers denoting its exponent and significand bit-widths.- Create Sort of this Kind with:
-
FUNCTION_SORT
A function sort with given domain sorts and codomain sort.- Create Sort of this Kind with:
-
INTEGER_SORT
The integer sort.- Create Sort of this Kind with:
-
REAL_SORT
The real sort.- Create Sort of this Kind with:
-
REGLAN_SORT
The regular language sort.- Create Sort of this Kind with:
-
ROUNDINGMODE_SORT
The rounding mode sort.- Create Sort of this Kind with:
-
SEQUENCE_SORT
A sequence sort, whose argument sort is the element sort of the sequence.- Create Sort of this Kind with:
-
SET_SORT
A set sort, whose argument sort is the element sort of the set.- Create Sort of this Kind with:
-
STRING_SORT
The string sort.- Create Sort of this Kind with:
-
TUPLE_SORT
A tuple sort, whose argument sorts denote the sorts of the direct children of the tuple.- Create Sort of this Kind with:
-
NULLABLE_SORT
A nullable sort, whose argument sort denotes the sort of the direct child of the nullable.- Create Sort of this Kind with:
-
UNINTERPRETED_SORT
An uninterpreted sort.- Create Sort of this Kind with:
-
LAST_SORT_KIND
Marks the upper-bound of this enumeration.
-
-
Method Details
-
values
Returns an array containing the constants of this enum class, in the order they are declared.- Returns:
- an array containing the constants of this enum class, in the order they are declared
-
valueOf
Returns the enum constant of this class with the specified name. The string must match exactly an identifier used to declare an enum constant in this class. (Extraneous whitespace characters are not permitted.)- Parameters:
name- the name of the enum constant to be returned.- Returns:
- the enum constant with the specified name
- Throws:
IllegalArgumentException- if this enum class has no constant with the specified nameNullPointerException- if the argument is null
-
fromInt
Converts an integer value to the corresponding enum constant.- Parameters:
value- the integer representation of the enum constant.- Returns:
- the corresponding enum constant for the given integer value.
- Throws:
CVC5ApiException- if the value is outside the valid range, or if no corresponding enum constant exists.
-
getValue
public int getValue()Get the integer value associated with this enum constant.- Returns:
- the integer representation of the enum constant.
-