Sort Kind

enum murxla::SortKind

The kind of a sort.

Values:

enumerator SORT_ARRAY

Array sort, parameterized over index and element sort.

enumerator SORT_BAG

Bag sort, parameterized over element sort.

enumerator SORT_BOOL

Boolean sort.

enumerator SORT_BV

Bit-vector sort, parameterized over bit-width.

enumerator SORT_DT

Datatype sort.

enumerator SORT_FF

Finite-field sort, parameterized over field size.

enumerator SORT_FP

Floating-point sort, parameterized over exponent and signifcand size.

enumerator SORT_FUN

Function sort, parameterized over domain sorts.

enumerator SORT_INT

Integer sort.

enumerator SORT_REAL

Real sort.

enumerator SORT_RM

RoundingMode sort.

enumerator SORT_REGLAN

Regular language sort.

enumerator SORT_SEQ

Sequence sort, parameterized over element sort.

enumerator SORT_SET

Set sort, parameterized over element sort.

enumerator SORT_STRING

String sort.

enumerator SORT_UNINTERPRETED

Uninterpreted sort.

enumerator SORT_ANY

The kind representing any sort kind. Used to indicate, for example, that the operands of an operator can be of any sort kind.

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

Specialization of std::hash for SortKind.

Public Functions

size_t operator()(const murxla::SortKind &k) const

Operator overload to get the hash value of a sort kind.

Parameters:

k – The sort kind to compute the hash value for.

Returns:

The hash value of a sort kind.

using murxla::SortKindVector = std::vector<SortKind>

A std::vector of sort kinds.

using murxla::SortKindSet = std::unordered_set<SortKind>

A std::unordered_set of sort kinds.