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

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

Wrapper class for cvc5::DatatypeConstructorDecl.

addSelector()

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()

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

Parameters:

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

addSelectorUnresolved()

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()

Returns:

True if this DatatypeConstructorDecl is a null object.