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 the declare-datatypes command.

Datatype sorts can be constructed from DatatypeDecl using the methods:

Public Functions

DatatypeDecl ( )


~DatatypeDecl ( )


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.


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.