DatatypeConstructor

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

class cvc5.DatatypeConstructor

A cvc5 datatype constructor.

Wrapper class for cvc5::DatatypeConstructor.

__getitem__()

Get the datatype selector with the given index, where index can be either a numeric id starting with zero, or the name of the selector. In the latter case, this is a linear search through the selectors, so in case of multiple, similarly-named selectors, the first is returned.

Parameters:

index – The id or name of the datatype selector.

Returns:

The matching datatype selector.

__iter__()

Iterate over all datatype selectors.

getInstantiatedTerm()

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 TermManager.mkTerm(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.

getName()

Returns:

The name of the constructor.

getNumSelectors()

Returns:

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

getSelector()

Parameters:

name – The name of the datatype selector.

Returns:

The first datatype selector with the given name.

getTerm()

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 via TermManager.mkTerm(APPLY_CONSTRUCTOR, [nil]), where nil is the Term returned by this method.

Note

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

Returns:

The constructor term.

getTesterTerm()

Get the tester term of this datatype constructor.

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

Returns:

The tester term for this constructor.

isNull()

Returns:

True if this DatatypeConstructor is a null object.