Package io.github.cvc5
Enum SortKind
- java.lang.Object
-
- java.lang.Enum<SortKind>
-
- io.github.cvc5.SortKind
-
-
Enum Constant Summary
Enum Constants Enum Constant Description ABSTRACT_SORT
An abstract sort.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.LAST_SORT_KIND
Marks the upper-bound of this enumeration.NULL_SORT
Null kind.NULLABLE_SORT
A nullable sort, whose argument sort denotes the sort of the direct child of the nullable.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.UNINTERPRETED_SORT
An uninterpreted sort.
-
Method Summary
All Methods Static Methods Instance Methods Concrete Methods Modifier and Type Method Description static SortKind
fromInt(int value)
int
getValue()
static SortKind
valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.static SortKind[]
values()
Returns an array containing the constants of this enum type, in the order they are declared.
-
-
-
Enum Constant Detail
-
INTERNAL_SORT_KIND
public static final SortKind 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
public static final SortKind UNDEFINED_SORT_KIND
Undefined kind.- Note:
- Should never be exposed or created via the API.
-
NULL_SORT
public static final SortKind 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
public static final SortKind 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
public static final SortKind 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
public static final SortKind BAG_SORT
A bag sort, whose argument sort is the element sort of the bag.- Create Sort of this Kind with:
-
BOOLEAN_SORT
public static final SortKind BOOLEAN_SORT
The Boolean sort.- Create Sort of this Kind with:
-
BITVECTOR_SORT
public static final SortKind BITVECTOR_SORT
A bit-vector sort, parameterized by an integer denoting its bit-width.- Create Sort of this Kind with:
-
DATATYPE_SORT
public static final SortKind DATATYPE_SORT
A datatype sort.- Create Sort of this Kind with:
-
FINITE_FIELD_SORT
public static final SortKind FINITE_FIELD_SORT
A finite field sort, parameterized by a size.- Create Sort of this Kind with:
-
FLOATINGPOINT_SORT
public static final SortKind 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
public static final SortKind FUNCTION_SORT
A function sort with given domain sorts and codomain sort.- Create Sort of this Kind with:
-
INTEGER_SORT
public static final SortKind INTEGER_SORT
The integer sort.- Create Sort of this Kind with:
-
REAL_SORT
public static final SortKind REAL_SORT
The real sort.- Create Sort of this Kind with:
-
REGLAN_SORT
public static final SortKind REGLAN_SORT
The regular language sort.- Create Sort of this Kind with:
-
ROUNDINGMODE_SORT
public static final SortKind ROUNDINGMODE_SORT
The rounding mode sort.- Create Sort of this Kind with:
-
SEQUENCE_SORT
public static final SortKind SEQUENCE_SORT
A sequence sort, whose argument sort is the element sort of the sequence.- Create Sort of this Kind with:
-
SET_SORT
public static final SortKind SET_SORT
A set sort, whose argument sort is the element sort of the set.- Create Sort of this Kind with:
-
STRING_SORT
public static final SortKind STRING_SORT
The string sort.- Create Sort of this Kind with:
-
TUPLE_SORT
public static final SortKind 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
public static final SortKind 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
public static final SortKind UNINTERPRETED_SORT
An uninterpreted sort.- Create Sort of this Kind with:
-
LAST_SORT_KIND
public static final SortKind LAST_SORT_KIND
Marks the upper-bound of this enumeration.
-
-
Method Detail
-
values
public static SortKind[] values()
Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:for (SortKind c : SortKind.values()) System.out.println(c);
- Returns:
- an array containing the constants of this enum type, in the order they are declared
-
valueOf
public static SortKind valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (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:
java.lang.IllegalArgumentException
- if this enum type has no constant with the specified namejava.lang.NullPointerException
- if the argument is null
-
fromInt
public static SortKind fromInt(int value) throws CVC5ApiException
- Throws:
CVC5ApiException
-
getValue
public int getValue()
-
-