mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
52 lines
1.4 KiB
ReStructuredText
52 lines
1.4 KiB
ReStructuredText
Sort
|
|
====
|
|
|
|
The :cpp:class:`Sort <cvc5::Sort>` class represents the sort of a
|
|
:cpp:class:`Term <cvc5::Term>`.
|
|
|
|
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:`Sort <cvc5::Sort>` offers the default constructor
|
|
only to create a null Sort. Instead, the :cpp:class:`Solver <cvc5::Solver>`
|
|
class provides factory functions for all other sorts, e.g.,
|
|
:cpp:func:`cvc5::Solver::getBooleanSort()` for Sort Bool 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* (Multiset)
|
|
|
|
- Created with :cpp:func:`cvc5::Solver::mkBagSort()`
|
|
|
|
- *Set* (:ref:`Theory of Sets and Relations <theory_reference_sets>`)
|
|
|
|
- Created with :cpp:func:`cvc5::Solver::mkSetSort()`
|
|
|
|
- *Relation* (:ref:`Theory of Sets and Relations <theory_reference_sets>`)
|
|
|
|
- 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
|
|
|
|
.. doxygenclass:: cvc5::Sort
|
|
:project: cvc5
|
|
:members:
|
|
:undoc-members:
|
|
|
|
.. doxygenfunction:: cvc5::operator<<(std::ostream& out, const Sort& s)
|
|
|
|
.. doxygenstruct:: std::hash< cvc5::Sort >
|
|
:project: std
|
|
:members:
|
|
:undoc-members:
|
|
|