1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Kind
================
Every :py:obj:`Term <cvc5.Term>` has an associated kind, represented
as enum class :py:obj:`cvc5.Kind`.
This kind distinguishes if the Term is a value, constant, variable or operator,
and what kind of each.
For example, a bit-vector value has kind
:py:obj:`CONST_BITVECTOR <cvc5.Kind.CONST_BITVECTOR>`,
a free constant symbol has kind
:py:obj:`CONSTANT <cvc5.Kind.CONSTANT>`,
an equality over terms of any sort has kind
:py:obj:`EQUAL <cvc5.Kind.EQUAL>`, and a universally
quantified formula has kind :py:obj:`FORALL <cvc5.Kind.FORALL>`.
The kinds below directly correspond to the enum values of the C++
:cpp:enum:`Kind <cvc5::Kind>` enum.
----
.. autoclass:: cvc5.Kind
:members:
:undoc-members:
|
