SortKind

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

• enum class cvc5::SortKind

• std::ostream& cvc5::operator<< (std::ostream& out, SortKind kind)

• std::hash<cvc5::SortKind>

enum class cvc5::SortKind : int32_t

The kind of a cvc5 Sort.

Values:

enumerator 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.

enumerator UNDEFINED_SORT_KIND

Undefined kind.

Note

Should never be exposed or created via the API.

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

enumerator 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) const

enumerator 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) const

enumerator BAG_SORT

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

• Create Sort of this Kind with:

  • Solver::mkBagSort(Sort) const

enumerator BOOLEAN_SORT

The Boolean sort.

• Create Sort of this Kind with:

  • Solver::getBooleanSort() const

enumerator BITVECTOR_SORT

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

• Create Sort of this Kind with:

  • Solver::mkBitVectorSort(uint32_t) const

enumerator DATATYPE_SORT

A datatype sort.

• Create Sort of this Kind with:

  • Solver::mkDatatypeSort(DatatypeDecl)

  • Solver::mkDatatypeSorts(const std::vector<DatatypeDecl>&)

enumerator FINITE_FIELD_SORT

A finite field sort, parameterized by a size.

• Create Sort of this Kind with:

  • Solver::mkFiniteFieldSort(const std::string&, uint32_t base) const

enumerator 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(uint32_t, uint32_t) const

enumerator FUNCTION_SORT

A function sort with given domain sorts and codomain sort.

• Create Sort of this Kind with:

  • Solver::mkFunctionSort(const std::vector<Sort>&, Sort) const

enumerator INTEGER_SORT

The integer sort.

• Create Sort of this Kind with:

  • Solver::getIntegerSort() const

enumerator REAL_SORT

The real sort.

• Create Sort of this Kind with:

  • Solver::getRealSort() const

enumerator REGLAN_SORT

The regular language sort.

• Create Sort of this Kind with:

  • Solver::getRegExpSort() const

enumerator ROUNDINGMODE_SORT

The rounding mode sort.

• Create Sort of this Kind with:

  • Solver::getRoundingModeSort() const

enumerator SEQUENCE_SORT

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

• Create Sort of this Kind with:

  • Solver::mkSequenceSort(Sort) const

enumerator SET_SORT

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

• Create Sort of this Kind with:

  • Solver::mkSetSort(Sort) const

enumerator STRING_SORT

The string sort.

• Create Sort of this Kind with:

  • Solver::getStringSort() const

enumerator 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(const std::vector<Sort>&) const

enumerator 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(const Sort&) const

enumerator UNINTERPRETED_SORT

An uninterpreted sort.

• Create Sort of this Kind with:

  • Solver::mkUninterpretedSort(const std::optional<std::string>&) const

enumerator LAST_SORT_KIND

Marks the upper-bound of this enumeration.

std::ostream &cvc5::operator<<(std::ostream &out, SortKind k)

Serialize a kind to given stream.

Parameters:

• out – the output stream

• k – the sort kind to be serialized to the given output stream

Returns:

the output stream

template<>
struct hash<cvc5::SortKind>

Hash function for SortKinds.

Public Functions

size_t operator()(cvc5::SortKind kind) const

Hashes a SortKind to a size_t.

Parameters:

kind – The kind.

Returns:

The hash value.