Package io.github.cvc5

Class Datatype

java.lang.Object

io.github.cvc5.Datatype

All Implemented Interfaces:

java.lang.Iterable<DatatypeConstructor>

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

A cvc5 datatype.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
class	Datatype.ConstIterator

Field Summary

Fields

Modifier and Type	Field	Description
protected long	pointer
protected Solver	solver

Method Summary

Modifier and Type	Method	Description
protected void	deletePointer(long pointer)
DatatypeConstructor	getConstructor(int idx)	Get the datatype constructor at a given index.
DatatypeConstructor	getConstructor(java.lang.String name)	Get the datatype constructor with the given name.
java.lang.String	getName()
int	getNumConstructors()
Sort[]	getParameters()
long	getPointer()
DatatypeSelector	getSelector(java.lang.String name)	Get the datatype constructor with the given name.
Solver	getSolver()
boolean	isCodatatype()
boolean	isFinite()
boolean	isNull()
boolean	isParametric()
boolean	isRecord()
boolean	isTuple()
boolean	isWellFounded()	Is this datatype well-founded? If this datatype is not a codatatype, this returns false if there are no values of this datatype that are of finite size.
java.util.Iterator<DatatypeConstructor>	iterator()
java.lang.String	toString()
protected java.lang.String	toString(long pointer)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

solver

protected final Solver solver

pointer

protected long pointer

Method Detail

deletePointer

protected void deletePointer(long pointer)

getPointer

public long getPointer()

getConstructor

public DatatypeConstructor getConstructor(int idx)

Get the datatype constructor at a given index.

Parameters:

idx - The index of the datatype constructor to return.

Returns:

The datatype constructor with the given index.

getConstructor

public DatatypeConstructor getConstructor(java.lang.String name)

Get the datatype constructor with the given name. This is a linear search through the constructors, so in case of multiple, similarly-named constructors, the first is returned.

Parameters:

name - The name of the datatype constructor.

Returns:

The datatype constructor with the given name.

getSelector

public DatatypeSelector getSelector(java.lang.String name)

Get the datatype constructor with the given name. This is a linear search through the constructors and their selectors, so in case of multiple, similarly-named selectors, the first is returned.

Parameters:

name - The name of the datatype selector.

Returns:

The datatype selector with the given name.

getName

public java.lang.String getName()

Returns:

The name of this Datatype.

getNumConstructors

public int getNumConstructors()

Returns:

The number of constructors for this Datatype.

getParameters

public Sort[] getParameters()

Returns:

The parameters of this datatype, if it is parametric. An exception. is thrown if this datatype is not parametric.

Note:

This method is experimental and may change in future versions.

isParametric

public boolean isParametric()

Returns:

True if this datatype is parametric.

Note:

This method is experimental and may change in future versions.

isCodatatype

public boolean isCodatatype()

Returns:

True if this datatype corresponds to a co-datatype

isTuple

public boolean isTuple()

Returns:

True if this datatype corresponds to a tuple

isRecord

public boolean isRecord()

Returns:

True if this datatype corresponds to a record.

Note:

This method is experimental and may change in future versions.

isFinite

public boolean isFinite()

Returns:

True if this datatype is finite

isWellFounded

public boolean isWellFounded()

Is this datatype well-founded? If this datatype is not a codatatype, this returns false if there are no values of this datatype that are of finite size.

Returns:

True if this datatype is well-founded.

isNull

public boolean isNull()

Returns:

True if this Datatype is a null object.

toString

protected java.lang.String toString(long pointer)

Returns:

A string representation of this datatype.

iterator

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

Specified by:

iterator in interface java.lang.Iterable<DatatypeConstructor>

getSolver

public Solver getSolver()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object