DatatypeConstructorDecl

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

• class cvc5::DatatypeConstructorDecl

• std::ostream& cvc5::operator<< (std::ostream& out, const DatatypeConstructorDecl& decl)

• std::ostream& cvc5::operator<< (std::ostream& out, const std::vector<DatatypeConstructorDecl>& vector)

class DatatypeConstructorDecl

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

Public Functions

DatatypeConstructorDecl()

Constructor.

~DatatypeConstructorDecl()

Destructor.

bool operator==(const DatatypeConstructorDecl &decl) const

Equality operator.

Parameters:

decl – The datatype constructor declaration to compare to for equality.

Returns:

True if the datatype constructor declarations are equal.

void addSelector(const std::string &name, const 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.

void addSelectorSelf(const std::string &name)

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

Parameters:

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

void addSelectorUnresolved(const std::string &name, const std::string &unresDataypeName)

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.

bool isNull() const

Returns:

True if this DatatypeConstructorDecl is a null declaration.

std::string toString() const

Returns:

A string representation of this datatype constructor declaration.

Friends

friend struct std::hash< DatatypeConstructorDecl >

std::ostream &cvc5::operator<<(std::ostream &out, const DatatypeConstructorDecl &ctordecl)

Serialize a datatype constructor declaration to given stream.

Parameters:

• out – The output stream.

• ctordecl – The datatype constructor declaration to be serialized.

Returns:

The output stream.

std::ostream &cvc5::operator<<(std::ostream &out, const std::vector<DatatypeConstructorDecl> &vector)

Serialize a vector of datatype constructor declarations to given stream.

Parameters:

• out – The output stream.

• vector – The vector of datatype constructor declarations to be. serialized to the given stream

Returns:

The output stream.