Cvc5SortKind

Every Cvc5Sort has an associated kind, represented as enum Cvc5SortKind.

enum Cvc5SortKind

The kind of a cvc5 Sort.

Values:

enumerator CVC5_SORT_KIND_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 CVC5_SORT_KIND_UNDEFINED_SORT_KIND

Undefined kind.

Note

Should never be exposed or created via the API.

enumerator CVC5_SORT_KIND_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 CVC5_SORT_KIND_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 CVC5_SORT_KIND_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 CVC5_SORT_KIND_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 CVC5_SORT_KIND_BOOLEAN_SORT

The Boolean sort.

• Create Sort of this Kind with:

  • Solver::getBooleanSort() const

enumerator CVC5_SORT_KIND_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 CVC5_SORT_KIND_DATATYPE_SORT

A datatype sort.

• Create Sort of this Kind with:

  • Solver::mkDatatypeSort(DatatypeDecl)

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

enumerator CVC5_SORT_KIND_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 CVC5_SORT_KIND_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 CVC5_SORT_KIND_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 CVC5_SORT_KIND_INTEGER_SORT

The integer sort.

• Create Sort of this Kind with:

  • Solver::getIntegerSort() const

enumerator CVC5_SORT_KIND_REAL_SORT

The real sort.

• Create Sort of this Kind with:

  • Solver::getRealSort() const

enumerator CVC5_SORT_KIND_REGLAN_SORT

The regular language sort.

• Create Sort of this Kind with:

  • Solver::getRegExpSort() const

enumerator CVC5_SORT_KIND_ROUNDINGMODE_SORT

The rounding mode sort.

• Create Sort of this Kind with:

  • Solver::getRoundingModeSort() const

enumerator CVC5_SORT_KIND_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 CVC5_SORT_KIND_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 CVC5_SORT_KIND_STRING_SORT

The string sort.

• Create Sort of this Kind with:

  • Solver::getStringSort() const

enumerator CVC5_SORT_KIND_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 CVC5_SORT_KIND_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 CVC5_SORT_KIND_UNINTERPRETED_SORT

An uninterpreted sort.

• Create Sort of this Kind with:

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

enumerator CVC5_SORT_KIND_LAST_SORT_KIND

Marks the upper-bound of this enumeration.

const char *cvc5_sort_kind_to_string(Cvc5SortKind kind)

Get a string representation of a Cvc5SortKind.

Parameters:

kind – The sort kind.

Returns:

The string representation.

size_t cvc5_sort_kind_hash(Cvc5SortKind kind)

Hash function for Cvc5SortKinds.

Parameters:

kind – The kind.

Returns:

The hash value.