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.

• Create Sort of this Kind with:

  • Solver.mkAbstractSort()

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()

BAG_SORT

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

• Create Sort of this Kind with:

  • Solver.mkBagSort()

BITVECTOR_SORT

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

• Create Sort of this Kind with:

  • Solver.mkBitVectorSort()

BOOLEAN_SORT

The Boolean sort.

• Create Sort of this Kind with:

  • Solver.getBooleanSort()

DATATYPE_SORT

A datatype sort.

• Create Sort of this Kind with:

  • Solver.mkDatatypeSort()

  • Solver.mkDatatypeSorts()

FINITE_FIELD_SORT

A finite field sort, parameterized by a size.

• Create Sort of this Kind with:

  • Solver.mkFiniteFieldSort()

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()

FUNCTION_SORT

A function sort with given domain sorts and codomain sort.

• Create Sort of this Kind with:

  • Solver.mkFunctionSort()

INTEGER_SORT

The integer sort.

• Create Sort of this Kind with:

  • Solver.getIntegerSort()

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.

• Create Sort of this Kind with:

  • Solver.mkNullableSort()

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.

• Create Sort of this Kind with:

  • Solver.getRealSort()

REGLAN_SORT

The regular language sort.

• Create Sort of this Kind with:

  • Solver.getRegExpSort()

ROUNDINGMODE_SORT

The rounding mode sort.

• Create Sort of this Kind with:

  • Solver.getRoundingModeSort()

SEQUENCE_SORT

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

• Create Sort of this Kind with:

  • Solver.mkSequenceSort()

SET_SORT

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

• Create Sort of this Kind with:

  • Solver.mkSetSort()

STRING_SORT

The string sort.

• Create Sort of this Kind with:

  • Solver.getStringSort()

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()

UNDEFINED_SORT_KIND

Undefined kind.

Note

Should never be exposed or created via the API.

UNINTERPRETED_SORT

An uninterpreted sort.

• Create Sort of this Kind with:

  • Solver.mkUninterpretedSort()