mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
46 lines
1.4 KiB
ReStructuredText
46 lines
1.4 KiB
ReStructuredText
Sort
|
|
================
|
|
|
|
The :py:obj:`Sort <cvc5.Sort>` class represents the sort of a
|
|
:py:obj:`Term <cvc5.Term>`.
|
|
Its kind is represented as enum class :py:obj:`cvc5.SortKind`.
|
|
|
|
A :py:obj:`Sort <cvc5.Sort>` can be hashed (using
|
|
:py:obj:`std.hash\<cvc5.Sort>`) and represented as a string
|
|
(using :py:func:`cvc5.Sort.__str__()`).
|
|
|
|
Class :py:obj:`cvc5.Sort` only provides the default constructor
|
|
to create a null Sort. Class :py:obj:`TermManager <cvc5.TermManager>`
|
|
provides factory functions for all other sorts, e.g.,
|
|
:py:func:`cvc5.TermManager.getBooleanSort()` for the Boolean sort and
|
|
:py:func:`cvc5.TermManager.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 :py:func:`cvc5.TermManager.mkBagSort()`
|
|
|
|
- *Set* (:doc:`Theory of Sets and Relations <../../../theories/sets-and-relations>`)
|
|
|
|
- Created with :py:func:`cvc5.TermManager.mkSetSort()`
|
|
|
|
- *Relation* (:doc:`Theory of Sets and Relations <../../../theories/sets-and-relations>`)
|
|
|
|
- Created with :py:func:`cvc5.TermManager.mkSetSort()` as a set of tuple
|
|
sorts
|
|
|
|
- *Table*
|
|
|
|
- Created with :py:func:`cvc5.TermManager.mkBagSort()` as a bag of tuple
|
|
sorts
|
|
|
|
----
|
|
|
|
.. autoclass:: cvc5.Sort
|
|
:members:
|
|
:undoc-members:
|