DatatypeDecl

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

class cvc5.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 DatatypeDecl using the methods:

Solver.mkDatatypeSort()

Solver.mkDatatypeSorts()

Wrapper class for cvc5::DatatypeDecl.

addConstructor()

Add a datatype constructor declaration.

Parameters:: ctor – The datatype constructor declaration to add.

getName()

Returns:: The name of this datatype declaration.

getNumConstructors()

Returns:: The number of constructors (so far) for this datatype declaration.

isNull()

Returns:: True if this DatatypeDecl is a null object.

isParametric()

Warning

This function is experimental and may change in future versions.

Returns:: True if this datatype declaration is parametric.