mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
67 lines
1.8 KiB
ReStructuredText
67 lines
1.8 KiB
ReStructuredText
Sort
|
|
====
|
|
|
|
The :cpp:class:`Sort <cvc5::Sort>` class represents the sort of a
|
|
:cpp:class:`Term <cvc5::Term>`.
|
|
Its kind is represented as enum class :cpp:enum:`cvc5::SortKind`.
|
|
|
|
A :cpp:class:`Sort <cvc5::Sort>` can be hashed (using
|
|
:cpp:class:`std::hash\<cvc5::Sort>`) and serialized to an output stream
|
|
(using :cpp:func:`cvc5::operator<<()`).
|
|
|
|
Class :cpp:class:`cvc5::Sort` only provides the default constructor
|
|
to create a null Sort. Class :cpp:class:`Solver <cvc5::Solver>`
|
|
provides factory functions for all other sorts, e.g.,
|
|
:cpp:func:`cvc5::Solver::getBooleanSort()` for the Boolean sort and
|
|
:cpp:func:`cvc5::Solver::mkBitVectorSort()` for bit-vector
|
|
sorts.
|
|
|
|
Sorts are defined as standardized in the SMT-LIB standard for standardized
|
|
theories. Additionally, we introduce the following sorts for non-standardized
|
|
theories:
|
|
|
|
- *Bag* (:doc:`Theory of Bags <../../theories/bags>`)
|
|
|
|
- Created with :cpp:func:`cvc5::Solver::mkBagSort()`
|
|
|
|
- *Set* (:doc:`Theory of Sets and Relations <../../theories/sets-and-relations>`)
|
|
|
|
- Created with :cpp:func:`cvc5::Solver::mkSetSort()`
|
|
|
|
- *Relation* (:doc:`Theory of Sets and Relations <../../theories/sets-and-relations>`)
|
|
|
|
- Created with :cpp:func:`cvc5::Solver::mkSetSort()` as a set of tuple
|
|
sorts
|
|
|
|
- *Table*
|
|
|
|
- Created with :cpp:func:`cvc5::Solver::mkBagSort()` as a bag of tuple
|
|
sorts
|
|
|
|
----
|
|
|
|
- class :cpp:class:`cvc5::Sort`
|
|
- :cpp:func:`std::ostream& cvc5::operator<< (std::ostream& out, const Sort& s)`
|
|
- :cpp:struct:`std::hash\<cvc5::Sort>`
|
|
|
|
----
|
|
|
|
.. doxygenclass:: cvc5::Sort
|
|
:project: cvc5
|
|
:members:
|
|
:undoc-members:
|
|
|
|
----
|
|
|
|
.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const Sort& s)
|
|
:project: cvc5
|
|
|
|
----
|
|
|
|
|
|
.. doxygenstruct:: std::hash< cvc5::Sort >
|
|
:project: std
|
|
:members:
|
|
:undoc-members:
|
|
|