io.github.cvc5

Class DatatypeConstructor

java.lang.Object

io.github.cvc5.DatatypeConstructor

All Implemented Interfaces:

java.lang.Iterable<DatatypeSelector>

public class DatatypeConstructor
extends java.lang.Object
implements java.lang.Iterable<DatatypeSelector>

A cvc5 datatype constructor.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
class	DatatypeConstructor.ConstIterator

Field Summary

Fields

Modifier and Type	Field and Description
protected long	pointer

Method Summary

Modifier and Type	Method and Description
void	deletePointer()
protected void	deletePointer(long pointer)
boolean	equals(java.lang.Object c) Syntactic equality operator.
Term	getInstantiatedTerm(Sort retSort) Get the constructor term of this datatype constructor whose return type is retSort.
java.lang.String	getName()
int	getNumSelectors()
long	getPointer()
DatatypeSelector	getSelector(int index) Get the DatatypeSelector at the given index
DatatypeSelector	getSelector(java.lang.String name) Get the datatype selector with the given name.
Term	getTerm() Get the constructor term of this datatype constructor.
Term	getTesterTerm() Get the tester term of this datatype constructor.
int	hashCode() Get the hash value of a datatype constructor.
boolean	isNull()
java.util.Iterator<DatatypeSelector>	iterator()
java.lang.String	toString()
protected java.lang.String	toString(long pointer)

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

pointer

protected long pointer

Method Detail

deletePointer

protected void deletePointer(long pointer)

equals

public boolean equals(java.lang.Object c)

Syntactic equality operator.

Overrides:

equals in class java.lang.Object

Parameters:

c - The datatype constructor to compare to for equality.

Returns:

True if the datatype constructors are equal.

getName

public java.lang.String getName()

Returns:

The name of this Datatype constructor.

getTerm

public Term 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 Kind.APPLY_CONSTRUCTOR. For example, the nil list is represented by the term (APPLY_CONSTRUCTOR nil), where nil is the term returned by this method.

Returns:

The constructor term.

Note:

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

getInstantiatedTerm

public Term getInstantiatedTerm(Sort retSort)

Get the constructor term of this datatype constructor whose return type is retSort. This method 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 method 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 need to be provided by the user. In SMT version 2.6, this is done via the syntax for qualified identifiers: (as nil (List Int)) This method is equivalent of applying the above, where this DatatypeConstructor is the one corresponding to nil, and retSort is (List Int).

Parameters:

retSort - The desired return sort of the constructor.

Returns:

The constructor term.

Note:

The returned constructor term t is used to construct the above (nullary) application of nil with Solver.mkTerm(APPLY_CONSTRUCTOR, new Term[] {t})., This method is experimental and may change in future versions.

getTesterTerm

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

getNumSelectors

public int getNumSelectors()

Returns:

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

getSelector

public DatatypeSelector getSelector(int index)

Get the DatatypeSelector at the given index

Parameters:

index - The given index i.

Returns:

The i^th DatatypeSelector.

getSelector

public DatatypeSelector getSelector(java.lang.String name)

Get the datatype selector with the given name. 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.

isNull

public boolean isNull()

Returns:

True if this DatatypeConstructor is a null object.

toString

protected java.lang.String toString(long pointer)

Returns:

A string representation of this datatype constructor.

iterator

public java.util.Iterator<DatatypeSelector> iterator()

Specified by:

iterator in interface java.lang.Iterable<DatatypeSelector>

hashCode

public int hashCode()

Get the hash value of a datatype constructor.

Overrides:

hashCode in class java.lang.Object

Returns:

The hash value.

getPointer

public long getPointer()

deletePointer

public void deletePointer()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object