DatatypeDecl 

This class encapsulates a datatype declaration. A datatype declaration is constructed via cvc5::Solver::mkDatatypeDecl() . This is not a datatype itself (see Datatype ), but the representation of the specification for creating a datatype Sort (see cvc5::Solver::mkDatatypeSort() and cvc5::Solver::mkDatatypeSorts() ).

• class cvc5::DatatypeDecl

• std::ostream& cvc5::operator<< (std::ostream& out, const DatatypeDecl& decl)

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 a DatatypeDecl using:

• Solver::mkDatatypeSort()

• Solver::mkDatatypeSorts()

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.

Returns :

The number of constructors.

bool isParametric ( ) const 

Determine if this Datatype declaration is parametric.

Warning

This function is experimental and may change in future versions.

Returns :

True if this datatype declaration is parametric.

bool isResolved ( ) const 

Determine if this datatype declaration is resolved (has already been used to declare a datatype).

Returns :

True if this datatype declaration is resolved.

bool isNull ( ) const 

Determine if this datatype declaration is nullary.

Returns :

True if this DatatypeDecl is a null object.

std :: string toString ( ) const 

Get a string representation of this datatype declaration.

Returns :

A string representation.

std :: string getName ( ) const 

Get the name of this datatype declaration.

Returns :

The name.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const DatatypeDecl & dtdecl ) 

Serialize a datatype declaration to given stream.

Parameters :

• out – The output stream.

• dtdecl – The datatype declaration to be serialized to the given stream.

Returns :

The output stream.