DatatypeConstructorDecl

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.

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.