SortKind

java.lang.Object
- java.lang.Enum<SortKind>
- - io.github.cvc5.SortKind

All Implemented Interfaces:

java.io.Serializable, java.lang.Comparable<SortKind>
```
public enum SortKind
extends java.lang.Enum<SortKind>
```

Enum Constant Summary

Enum Constants
Enum Constant and 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 and 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.

Methods inherited from class java.lang.Enum
clone, compareTo, equals, finalize, getDeclaringClass, hashCode, name, ordinal, toString, valueOf

Methods inherited from class java.lang.Object
getClass, notify, notifyAll, wait, wait, wait

- 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:
      
      Solver.mkAbstractSort(SortKind)
  - 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:
      
      Solver.mkArraySort(Sort, Sort)
  - 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:
      
      Solver.mkBagSort(Sort)
  - BOOLEAN_SORT
```
public static final SortKind BOOLEAN_SORT
```
    The Boolean sort.
    - Create Sort of this Kind with:
      
      Solver.getBooleanSort()
  - 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:
      
      Solver.mkBitVectorSort(int)
  - DATATYPE_SORT
```
public static final SortKind DATATYPE_SORT
```
    A datatype sort.
    - Create Sort of this Kind with:
      
      Solver.mkDatatypeSort(DatatypeDecl)
      
      Solver.mkDatatypeSorts(DatatypeDecl[])
  - FINITE_FIELD_SORT
```
public static final SortKind FINITE_FIELD_SORT
```
    A finite field sort, parameterized by a size.
    - Create Sort of this Kind with:
      
      Solver.mkFiniteFieldSort(String, int base)
  - 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:
      
      Solver.mkFloatingPointSort(int, int)
  - FUNCTION_SORT
```
public static final SortKind FUNCTION_SORT
```
    A function sort with given domain sorts and codomain sort.
    - Create Sort of this Kind with:
      
      Solver.mkFunctionSort(Sort[], Sort)
  - INTEGER_SORT
```
public static final SortKind INTEGER_SORT
```
    The integer sort.
    - Create Sort of this Kind with:
      
      Solver.getIntegerSort()
  - REAL_SORT
```
public static final SortKind REAL_SORT
```
    The real sort.
    - Create Sort of this Kind with:
      
      Solver.getRealSort()
  - REGLAN_SORT
```
public static final SortKind REGLAN_SORT
```
    The regular language sort.
    - Create Sort of this Kind with:
      
      Solver.getRegExpSort()
  - ROUNDINGMODE_SORT
```
public static final SortKind ROUNDINGMODE_SORT
```
    The rounding mode sort.
    - Create Sort of this Kind with:
      
      Solver.getRoundingModeSort()
  - 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:
      
      Solver.mkSequenceSort(Sort)
  - 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:
      
      Solver.mkSetSort(Sort)
  - STRING_SORT
```
public static final SortKind STRING_SORT
```
    The string sort.
    - Create Sort of this Kind with:
      
      Solver.getStringSort()
  - 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:
      
      Solver.mkTupleSort(Sort[])
  - 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:
      
      Solver.mkNullableSort(Sort)
  - UNINTERPRETED_SORT
```
public static final SortKind UNINTERPRETED_SORT
```
    An uninterpreted sort.
    - Create Sort of this Kind with:
      
      Solver.mkUninterpretedSort(String)
  - 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 name
    
    java.lang.NullPointerException - if the argument is null
  - fromInt
```
public static SortKind fromInt(int value)
                        throws CVC5ApiException
```
    Throws:
    
    CVC5ApiException
  - getValue
```
public int getValue()
```

Enum SortKind

Enum Constant Summary

Method Summary

Methods inherited from class java.lang.Enum

Methods inherited from class java.lang.Object

Enum Constant Detail

INTERNAL_SORT_KIND

UNDEFINED_SORT_KIND

NULL_SORT

ABSTRACT_SORT

ARRAY_SORT

BAG_SORT

BOOLEAN_SORT

BITVECTOR_SORT

DATATYPE_SORT

FINITE_FIELD_SORT

FLOATINGPOINT_SORT

FUNCTION_SORT

INTEGER_SORT

REAL_SORT

REGLAN_SORT

ROUNDINGMODE_SORT

SEQUENCE_SORT

SET_SORT

STRING_SORT

TUPLE_SORT

NULLABLE_SORT

UNINTERPRETED_SORT

LAST_SORT_KIND

Method Detail

values

valueOf

fromInt

getValue