DatatypeConstructorDecl ¶

class cvc5. DatatypeConstructorDecl ¶

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

Wrapper class for cvc5::DatatypeConstructorDecl .

addSelector ( self , unicode name , 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.

addSelectorSelf ( self , unicode name ) ¶

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

Parameters :

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

addSelectorUnresolved ( self , unicode name , unicode unresDatatypeName ) ¶

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.

isNull ( self ) ¶

Returns :

True if this DatatypeConstructorDecl is a null object.