SortKind

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



enum class cvc5 :: SortKind

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.

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.

enumerator BITVECTOR_SORT

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

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.

enumerator FLOATINGPOINT_SORT

A floating-point sort, parameterized by two integers denoting its exponent and significand bit-widths.

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.

enumerator REAL_SORT

The real sort.

enumerator REGLAN_SORT

The regular language sort.

enumerator ROUNDINGMODE_SORT

The rounding mode sort.

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.

enumerator TUPLE_SORT

A tuple sort, whose argument sorts denote the sorts of the direct children of the tuple.

enumerator NULLABLE_SORT

A nullable sort, whose argument sort denotes the sort of the direct child of the nullable.

enumerator UNINTERPRETED_SORT

An uninterpreted sort.

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

std :: string std :: to_string ( cvc5 :: SortKind k )

Get the string representation of a given kind.

Parameters :

k – the sort kind

Returns :

the string representation of kind k


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.