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 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 a DatatypeDecl using:

Public Functions

DatatypeDecl()

Constructor.

~DatatypeDecl()

Destructor.

bool operator==(const DatatypeDecl &decl) const

Equality operator.

Parameters:

decl – The datatype declaration to compare to for equality.

Returns:

True if the datatype declarations are equal.

void addConstructor(const DatatypeConstructorDecl &ctor)

Add datatype constructor declaration.

Parameters:

ctor – The datatype constructor declaration to add.

size_t getNumConstructors() const

Get the number of constructors (so far) for this Datatype declaration.

Returns:

The number of constructors.

bool isParametric() const

Determine if this Datatype declaration is parametric.

Warning

This function is experimental and may change in future versions.

Returns:

True if this datatype declaration is parametric.

bool isResolved() const

Determine if this datatype declaration is resolved (has already been used to declare a datatype).

Returns:

True if this datatype declaration is resolved.

bool isNull() const

Determine if this datatype declaration is nullary.

Returns:

True if this DatatypeDecl is a null object.

std::string toString() const

Get a string representation of this datatype declaration.

Returns:

A string representation.

std::string getName() const

Get the name of this datatype declaration.

Returns:

The name.

Friends

friend struct std::hash< DatatypeDecl >
std::ostream &cvc5::operator<<(std::ostream &out, const DatatypeDecl &dtdecl)

Serialize a datatype declaration to given stream.

Parameters:

  • out – The output stream.

  • dtdecl – The datatype declaration to be serialized to the given stream.

Returns:

The output stream.