Datatype
-
class
cvc5
::
Datatype
-
A cvc5 datatype.
Public Functions
-
Datatype
(
)
-
Constructor.
-
~Datatype
(
)
-
Destructor.
-
DatatypeConstructor
operator
[]
(
size_t
idx
)
const
-
Get the datatype constructor at a given index.
- Parameters
-
idx – The index of the datatype constructor to return.
- Returns
-
The datatype constructor with the given index.
-
DatatypeConstructor
operator
[]
(
const
std
::
string
&
name
)
const
-
Get the datatype constructor with the given name. This is a linear search through the constructors, so in case of multiple, similarly-named constructors, the first is returned.
- Parameters
-
name – The name of the datatype constructor.
- Returns
-
The datatype constructor with the given name.
-
DatatypeConstructor
getConstructor
(
const
std
::
string
&
name
)
const
-
DatatypeSelector
getSelector
(
const
std
::
string
&
name
)
const
-
Get the datatype constructor with the given name. This is a linear search through the constructors and their selectors, so in case of multiple, similarly-named selectors, the first is returned.
- Parameters
-
name – The name of the datatype selector.
- Returns
-
The datatype selector with the given name.
-
std
::
vector
<
Sort
>
getParameters
(
)
const
-
Get the parameters of this datatype, if it is parametric.
Note
Asserts that this datatype is parametric.
Warning
This method is experimental and may change in future versions.
- Returns
-
The parameters of this datatype.
-
bool
isParametric
(
)
const
-
Warning
This method is experimental and may change in future versions.
- Returns
-
True if this datatype is parametric.
-
bool
isCodatatype
(
)
const
-
- Returns
-
True if this datatype corresponds to a co-datatype
-
bool
isTuple
(
)
const
-
- Returns
-
True if this datatype corresponds to a tuple
-
bool
isRecord
(
)
const
-
Warning
This method is experimental and may change in future versions.
- Returns
-
True if this datatype corresponds to a record.
-
bool
isFinite
(
)
const
-
- Returns
-
True if this datatype is finite
-
bool
isWellFounded
(
)
const
-
Determine if this datatype is well-founded.
If this datatype is not a codatatype, this returns false if there are no values of this datatype that are of finite size.
- Returns
-
True if this datatype is well-founded.
-
std
::
string
toString
(
)
const
-
- Returns
-
A string representation of this datatype.
-
const_iterator
begin
(
)
const
-
- Returns
-
An iterator to the first constructor of this datatype.
-
const_iterator
end
(
)
const
-
- Returns
-
An iterator to one-off-the-last constructor of this datatype.
-
class
const_iterator
-
Iterator for the constructors of a datatype.
Public Types
-
using
iterator_category
=
std
::
forward_iterator_tag
-
Iterator tag
-
using
difference_type
=
std
::
ptrdiff_t
-
The type returned when two iterators are subtracted
Public Functions
-
const_iterator
(
)
-
Nullary constructor (required for Cython).
-
const_iterator
&
operator
=
(
const
const_iterator
&
it
)
-
Assignment operator.
- Parameters
-
it – The iterator to assign to.
- Returns
-
The reference to the iterator after assignment.
-
bool
operator
==
(
const
const_iterator
&
it
)
const
-
Equality operator.
- Parameters
-
it – The iterator to compare to for equality.
- Returns
-
True if the iterators are equal.
-
bool
operator
!=
(
const
const_iterator
&
it
)
const
-
Disequality operator.
- Parameters
-
it – The iterator to compare to for disequality.
- Returns
-
True if the iterators are disequal.
-
const_iterator
&
operator
++
(
)
-
Increment operator (prefix).
- Returns
-
A reference to the iterator after incrementing by one.
-
const_iterator
operator
++
(
int
)
-
Increment operator (postfix).
- Returns
-
A reference to the iterator after incrementing by one.
-
const
DatatypeConstructor
&
operator
*
(
)
const
-
Dereference operator.
- Returns
-
A reference to the constructor this iterator points to.
-
const
DatatypeConstructor
*
operator
->
(
)
const
-
Dereference operator.
- Returns
-
A pointer to the constructor this iterator points to.
-
using
iterator_category
=
std
::
forward_iterator_tag
-
Datatype
(
)