Datatype (cvc5-turnkey 1.2.0 API)

java.lang.Object
- io.github.cvc5.Datatype

All Implemented Interfaces:: Iterable<DatatypeConstructor>

public class Datatype
extends Object
implements Iterable<DatatypeConstructor>

A cvc5 datatype.

Nested Class Summary

Nested Classes
Modifier and Type Class and Description

class Datatype.ConstIterator

Nested Classes
Modifier and Type	Class and Description
`class`	`Datatype.ConstIterator`

Field Summary

Fields
Modifier and Type Field and Description

protected long pointer

Fields
Modifier and Type	Field and Description
`protected long`	`pointer`

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`void`	`deletePointer()`
`protected void`	`deletePointer(long pointer)`
`boolean`	`equals(Object dt)` Syntactic equality operator.
`DatatypeConstructor`	`getConstructor(int idx)` Get the datatype constructor at a given index.
`DatatypeConstructor`	`getConstructor(String name)` Get the datatype constructor with the given name.
`String`	`getName()`
`int`	`getNumConstructors()`
`Sort[]`	`getParameters()`
`long`	`getPointer()`
`DatatypeSelector`	`getSelector(String name)` Get the datatype constructor with the given name.
`int`	`hashCode()` Get the hash value of a datatype.
`boolean`	`isCodatatype()`
`boolean`	`isFinite()`
`boolean`	`isNull()`
`boolean`	`isParametric()`
`boolean`	`isRecord()`
`boolean`	`isTuple()`
`boolean`	`isWellFounded()` Is this datatype well-founded?
`Iterator<DatatypeConstructor>`	`iterator()`
`String`	`toString()`
`protected 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(Object dt)
```
    Syntactic equality operator.
    
    Overrides:
    
    equals in class Object
    
    Parameters:
    
    dt - The datatype to compare to for equality.
    
    Returns:
    
    True if the datatypes are equal.
  - 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(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(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 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.
  - isParametric
```
public boolean isParametric()
```
    Returns:
    
    True if this datatype is parametric.
  - 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.
  - 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 String toString(long pointer)
```
    Returns:
    
    A string representation of this datatype.
  - iterator
```
public Iterator<DatatypeConstructor> iterator()
```
    Specified by:
    
    iterator in interface Iterable<DatatypeConstructor>
  - hashCode
```
public int hashCode()
```
    Get the hash value of a datatype.
    
    Overrides:
    
    hashCode in class Object
    
    Returns:
    
    The hash value.
  - getPointer
```
public long getPointer()
```
  - deletePointer
```
public void deletePointer()
```
  - toString
```
public String toString()
```
    Overrides:
    
    toString in class Object

Class Datatype

Nested Class Summary

Field Summary

Method Summary

Methods inherited from class java.lang.Object

Methods inherited from interface java.lang.Iterable

Field Detail

pointer

Method Detail

deletePointer

equals

getConstructor

getConstructor

getSelector

getName

getNumConstructors

getParameters

isParametric

isCodatatype

isTuple

isRecord

isFinite

isWellFounded

isNull

toString

iterator

hashCode

getPointer

deletePointer

toString