DatatypeDecl ¶

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 ( self , DatatypeConstructorDecl ctor ) ¶

Add a datatype constructor declaration.

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

getName ( self ) ¶

Returns :: The name of this datatype declaration.

getNumConstructors ( self ) ¶

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

isNull ( self ) ¶

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

isParametric ( self ) ¶

Warning

This method is experimental and may change in future versions.

Returns :: True if this datatype declaration is parametric.