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 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.