DatatypeConstructor 

This class represents a datatype constructor. Datatype constructors are specified via cvc5::DatatypeConstructorDecl when constructing a datatype sort and can be retrieved from a cvc5::Datatype via cvc5::Datatype::getConstructor() .

• class cvc5::DatatypeConstructor

• std::ostream& cvc5::operator<< (std::ostream& out, const DatatypeConstructor& cons)

class DatatypeConstructor 

A cvc5 datatype constructor.

Public Functions

DatatypeConstructor ( ) 

Constructor.

~DatatypeConstructor ( ) 

Destructor.

std :: string getName ( ) const 

Get the name of this datatype constructor.

Returns :

The name.

Term getTerm ( ) const 

Get the constructor term of this datatype constructor.

Datatype constructors are a special class of function-like terms whose sort is datatype constructor ( Sort::isDatatypeConstructor() ). All datatype constructors, including nullary ones, should be used as the first argument to Terms whose kind is #APPLY_CONSTRUCTOR. For example, the nil list can be constructed by Solver::mkTerm ( Kind::APPLY_CONSTRUCTOR , {t}) , where t is the term returned by this function.

Note

This function should not be used for parametric datatypes. Instead, use the function DatatypeConstructor::getInstantiatedTerm() below.

Returns :

The constructor term.

Term getInstantiatedTerm ( const Sort & retSort ) const 

Get the constructor term of this datatype constructor whose return type is retSort .

This function is intended to be used on constructors of parametric datatypes and can be seen as returning the constructor term that has been explicitly cast to the given sort.

This function is required for constructors of parametric datatypes whose return type cannot be determined by type inference. For example, given:

(declare-datatype List
    (par (T) ((nil) (cons (head T) (tail (List T))))))

The type of nil terms must be provided by the user. In SMT version 2.6, this is done via the syntax for qualified identifiers:

(as nil (List Int))

This function is equivalent of applying the above, where this DatatypeConstructor is the one corresponding to nil , and retSort is (List Int) .

Note

The returned constructor term t is used to construct the above (nullary) application of nil with Solver::mkTerm ( Kind::APPLY_CONSTRUCTOR , {t}) .

Warning

This function is experimental and may change in future versions.

Parameters :

retSort – The desired return sort of the constructor.

Returns :

The constructor term.

Term getTesterTerm ( ) const 

Get the tester term of this datatype constructor.

Similar to constructors, testers are a class of function-like terms of tester sort ( Sort::isDatatypeConstructor() ) which should be used as the first argument of Terms of kind #APPLY_TESTER.

Returns :

The tester term.

size_t getNumSelectors ( ) const 

Returns :

The number of selectors (so far) of this Datatype constructor.

DatatypeSelector operator [] ( size_t index ) const 

Returns :

The i^th DatatypeSelector .

DatatypeSelector operator [] ( const std :: string & name ) const 

Get the datatype selector with the given name.

Note

This is a linear search through the selectors, so in case of multiple, similarly-named selectors, the first is returned.

Parameters :

name – The name of the datatype selector.

Returns :

The first datatype selector with the given name.

DatatypeSelector getSelector ( const std :: string & name ) const 

Get the datatype selector with the given name.

Note

This is a linear search through the selectors, so in case of multiple, similarly-named selectors, the first is returned.

Parameters :

name – The name of the datatype selector.

Returns :

The first datatype selector with the given name.

bool isNull ( ) const 

Returns :

True if this DatatypeConstructor is a null object.

std :: string toString ( ) const 

Get a string representation of this datatype constructor.

Returns :

The string representation.

const_iterator begin ( ) const 

Returns :

An iterator to the first selector of this constructor.

const_iterator end ( ) const 

Returns :

An iterator to one-off-the-last selector of this constructor.

class const_iterator 

Iterator for the selectors of a datatype constructor.

Public Types

using iterator_category = std :: forward_iterator_tag 

Iterator tag

using value_type = DatatypeConstructor 

The type of the item

using pointer = const DatatypeConstructor * 

The pointer type of the item

using reference = const DatatypeConstructor & 

The reference type of the item

using difference_type = std :: ptrdiff_t 

The type returned when two iterators are subtracted

Public Functions

const_iterator ( ) 

Nullary constructor (required for Cython).

const_iterator & operator = ( const const_iterator & it ) 

Assignment operator.

Parameters :

it – The iterator to assign to.

Returns :

The reference to the iterator after assignment.

bool operator == ( const const_iterator & it ) const 

Equality operator.

Parameters :

it – The iterator to compare to for equality.

Returns :

True if the iterators are equal.

bool operator != ( const const_iterator & it ) const 

Disequality operator.

Parameters :

it – The iterator to compare to for disequality.

Returns :

True if the iterators are disequal.

const_iterator & operator ++ ( ) 

Increment operator (prefix).

Returns :

A reference to the iterator after incrementing by one.

const_iterator operator ++ ( int ) 

Increment operator (postfix).

Returns :

A reference to the iterator after incrementing by one.

const DatatypeSelector & operator * ( ) const 

Dereference operator.

Returns :

A reference to the selector this iterator points to.

const DatatypeSelector * operator -> ( ) const 

Dereference operator.

Returns :

A pointer to the selector this iterator points to.

std :: ostream & cvc5 :: operator << ( std :: ostream & out , const DatatypeConstructor & ctor ) 

Serialize a datatype constructor to given stream.

Parameters :

• out – The output stream.

• ctor – The datatype constructor to be serialized to given stream.

Returns :

The output stream.