DatatypeConstructorDecl 

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

• class cvc5::DatatypeConstructorDecl

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

• std::ostream& cvc5::operator<< (std::ostream& out, const std::vector<DatatypeConstructorDecl>& vector)

class DatatypeConstructorDecl 

A cvc5 datatype constructor declaration. A datatype constructor declaration is a specification used for creating a datatype constructor.

Public Functions

DatatypeConstructorDecl ( ) 

Constructor.

~DatatypeConstructorDecl ( ) 

Destructor.

bool operator == ( const DatatypeConstructorDecl & decl ) const 

Equality operator.

Parameters :

decl – The datatype constructor declaration to compare to for equality.

Returns :

True if the datatype constructor declarations are equal.

void addSelector ( const std :: string & name , const Sort & sort ) 

Add datatype selector declaration.

Parameters :

• name – The name of the datatype selector declaration to add.

• sort – The codomain sort of the datatype selector declaration to add.

void addSelectorSelf ( const std :: string & name ) 

Add datatype selector declaration whose codomain type is the datatype itself.

Parameters :

name – The name of the datatype selector declaration to add.

void addSelectorUnresolved ( const std :: string & name , const std :: string & unresDataypeName ) 

Add datatype selector declaration whose codomain sort is an unresolved datatype with the given name.

Parameters :

• name – The name of the datatype selector declaration to add.

• unresDataypeName – The name of the unresolved datatype. The codomain of the selector will be the resolved datatype with the given name.

bool isNull ( ) const 

Returns :

True if this DatatypeConstructorDecl is a null declaration.

std :: string toString ( ) const 

Returns :

A string representation of this datatype constructor declaration.

Friends

friend struct std::hash< DatatypeConstructorDecl >

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const DatatypeConstructorDecl & ctordecl ) 

Serialize a datatype constructor declaration to given stream.

Parameters :

• out – The output stream.

• ctordecl – The datatype constructor declaration to be serialized.

Returns :

The output stream.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const std :: vector < DatatypeConstructorDecl > & vector ) 

Serialize a vector of datatype constructor declarations to given stream.

Parameters :

• out – The output stream.

• vector – The vector of datatype constructor declarations to be. serialized to the given stream

Returns :

The output stream.