DatatypeDecl ¶
-
class
DatatypeDecl
¶
-
A cvc5 datatype declaration. A datatype declaration is not itself a datatype (see Datatype ), but a specification for creating a datatype sort.
The interface for a datatype declaration coincides with the syntax for the SMT-LIB 2.6 command
declare-datatype, or a single datatype within thedeclare-datatypescommand.Datatype sorts can be constructed from DatatypeDecl using the methods:
Public Functions
-
DatatypeDecl
(
)
¶
-
Constructor.
-
~DatatypeDecl
(
)
¶
-
Destructor.
-
void
addConstructor
(
const
DatatypeConstructorDecl
&
ctor
)
¶
-
Add datatype constructor declaration.
- Parameters :
-
ctor – The datatype constructor declaration to add.
-
size_t
getNumConstructors
(
)
const
¶
-
Get the number of constructors (so far) for this Datatype declaration.
-
bool
isParametric
(
)
const
¶
-
Determine if this Datatype declaration is parametric.
Warning
This method is experimental and may change in future versions.
-
bool
isResolved
(
)
const
¶
-
Is this datatype declaration resolved (i.e,. has it been used to declare a datatype already)?
-
bool
isNull
(
)
const
¶
-
- Returns :
-
True if this DatatypeDecl is a null object.
-
std
::
string
toString
(
)
const
¶
-
- Returns :
-
A string representation of this datatype declaration.
-
std
::
string
getName
(
)
const
¶
-
- Returns :
-
The name of this datatype declaration.
-
DatatypeDecl
(
)
¶