Sort

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

All Implemented Interfaces:: java.lang.Comparable<Sort>

public class Sort
extends java.lang.Object
implements java.lang.Comparable<Sort>

The sort of a cvc5 term.

Field Summary

Fields
Modifier and Type Field and Description

protected long pointer

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

Constructor Summary

Constructors
Constructor and Description

Sort()
Null sort

Constructors
Constructor and Description
`Sort()` Null sort

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`int`	`compareTo(Sort s)` Comparison for ordering on sorts.
`void`	`deletePointer()`
`protected void`	`deletePointer(long pointer)`
`boolean`	`equals(java.lang.Object s)` Comparison for structural equality.
`SortKind`	`getAbstractedKind()`
`Sort`	`getArrayElementSort()`
`Sort`	`getArrayIndexSort()`
`Sort`	`getBagElementSort()`
`int`	`getBitVectorSize()`
`Datatype`	`getDatatype()`
`int`	`getDatatypeArity()`
`int`	`getDatatypeConstructorArity()`
`Sort`	`getDatatypeConstructorCodomainSort()`
`Sort[]`	`getDatatypeConstructorDomainSorts()`
`Sort`	`getDatatypeSelectorCodomainSort()`
`Sort`	`getDatatypeSelectorDomainSort()`
`Sort`	`getDatatypeTesterCodomainSort()`
`Sort`	`getDatatypeTesterDomainSort()`
`java.lang.String`	`getFiniteFieldSize()`
`int`	`getFloatingPointExponentSize()`
`int`	`getFloatingPointSignificandSize()`
`int`	`getFunctionArity()`
`Sort`	`getFunctionCodomainSort()`
`Sort[]`	`getFunctionDomainSorts()`
`Sort[]`	`getInstantiatedParameters()` Get the sorts used to instantiate the sort parameters of a parametric sort (parametric datatype or uninterpreted sort constructor sort, see `instantiate(Sort[])`).
`SortKind`	`getKind()`
`Sort`	`getNullableElementSort()`
`long`	`getPointer()`
`Sort`	`getSequenceElementSort()`
`Sort`	`getSetElementSort()`
`java.lang.String`	`getSymbol()`
`int`	`getTupleLength()`
`Sort[]`	`getTupleSorts()`
`Sort`	`getUninterpretedSortConstructor()` Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.
`int`	`getUninterpretedSortConstructorArity()`
`int`	`hashCode()` Get the hash value of a sort.
`boolean`	`hasSymbol()`
`Sort`	`instantiate(Sort[] params)` Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
`boolean`	`isAbstract()` Determine if this is an abstract sort.
`boolean`	`isArray()` Determine if this is an array sort.
`boolean`	`isBag()` Determine if this is a Bag sort.
`boolean`	`isBitVector()` Determine if this is a bit-vector sort (SMT-LIB: `(_ BitVec i)`).
`boolean`	`isBoolean()` Determine if this is the Boolean sort (SMT-LIB: `Bool`).
`boolean`	`isDatatype()` Determine if this is a datatype sort.
`boolean`	`isDatatypeConstructor()` Determine if this is a datatype constructor sort.
`boolean`	`isDatatypeSelector()` Determine if this is a datatype selector sort.
`boolean`	`isDatatypeTester()` Determine if this is a datatype tester sort.
`boolean`	`isDatatypeUpdater()` Determine if this is a datatype updater sort.
`boolean`	`isFiniteField()` Determine if this is a finite field sort (SMT-LIB: `(_ FiniteField i)`).
`boolean`	`isFloatingPoint()` Determine if this is a floatingpoint sort (SMT-LIB: `(_ FloatingPoint eb sb)`).
`boolean`	`isFunction()` Determine if this is a function sort.
`boolean`	`isInstantiated()` Determine if this is an instantiated (parametric datatype or uninterpreted sort constructor) sort.
`boolean`	`isInteger()` Determine if this is the integer sort (SMT-LIB: `Int`).
`boolean`	`isNull()` Determine if this is the null sort.
`boolean`	`isNullable()` Determine if this a nullable sort.
`boolean`	`isPredicate()` Determine if this is a predicate sort.
`boolean`	`isReal()` Determine if this is the real sort (SMT-LIB: `Real`).
`boolean`	`isRecord()` Determine if this is a record sort.
`boolean`	`isRegExp()` Determine if this is the regular expression sort (SMT-LIB: `RegLan`).
`boolean`	`isRoundingMode()` Determine if this is the rounding mode sort (SMT-LIB: `RoundingMode`).
`boolean`	`isSequence()` Determine if this is a Sequence sort.
`boolean`	`isSet()` Determine if this is a Set sort.
`boolean`	`isString()` Determine if this is the string sort (SMT-LIB: `String`)..
`boolean`	`isTuple()` Determine if this a tuple sort.
`boolean`	`isUninterpretedSort()` Determine if this is an uninterpreted sort.
`boolean`	`isUninterpretedSortConstructor()` Determine if this is an uninterpreted sort constructor.
`Sort`	`substitute(Sort[] sorts, Sort[] replacements)` Simultaneous substitution of Sorts.
`Sort`	`substitute(Sort sort, Sort replacement)` Substitution of Sorts.
`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

- Field Detail
  - pointer
```
protected long pointer
```
- Constructor Detail
  - Sort
```
public Sort()
```
    Null sort
- Method Detail
  - deletePointer
```
protected void deletePointer(long pointer)
```
  - equals
```
public boolean equals(java.lang.Object s)
```
    Comparison for structural equality.
    
    Overrides:
    
    equals in class java.lang.Object
    
    Parameters:
    
    s - The sort to compare to.
    
    Returns:
    
    True if the sorts are equal.
  - compareTo
```
public int compareTo(Sort s)
```
    Comparison for ordering on sorts.
    
    Specified by:
    
    compareTo in interface java.lang.Comparable<Sort>
    
    Parameters:
    
    s - The sort to compare to.
    
    Returns:
    
    A negative integer, zero, or a positive integer as this sort is less than, equal to, or greater than the specified sort.
  - getKind
```
public SortKind getKind()
                 throws CVC5ApiException
```
    Returns:
    
    The kind of this sort.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    This method is experimental and may change in future versions.
  - hasSymbol
```
public boolean hasSymbol()
```
    Returns:
    
    True if the sort has a symbol.
  - getSymbol
```
public java.lang.String getSymbol()
```
    Returns:
    
    The raw symbol of the symbol.
    
    Note:
    
    Asserts hasSymbol().
  - isNull
```
public boolean isNull()
```
    Determine if this is the null sort.
    
    Returns:
    
    True if this Sort is the null sort.
  - isBoolean
```
public boolean isBoolean()
```
    Determine if this is the Boolean sort (SMT-LIB: Bool).
    
    Returns:
    
    True if this sort is the Boolean sort.
  - isInteger
```
public boolean isInteger()
```
    Determine if this is the integer sort (SMT-LIB: Int).
    
    Returns:
    
    True if this sort is the integer sort.
  - isReal
```
public boolean isReal()
```
    Determine if this is the real sort (SMT-LIB: Real).
    
    Returns:
    
    True if this sort is the real sort.
  - isString
```
public boolean isString()
```
    Determine if this is the string sort (SMT-LIB: String)..
    
    Returns:
    
    True if this sort is the string sort.
  - isRegExp
```
public boolean isRegExp()
```
    Determine if this is the regular expression sort (SMT-LIB: RegLan).
    
    Returns:
    
    True if this sort is the regular expression sort.
  - isRoundingMode
```
public boolean isRoundingMode()
```
    Determine if this is the rounding mode sort (SMT-LIB: RoundingMode).
    
    Returns:
    
    True if this sort is the rounding mode sort.
  - isBitVector
```
public boolean isBitVector()
```
    Determine if this is a bit-vector sort (SMT-LIB: (_ BitVec i)).
    
    Returns:
    
    True if this sort is a bit-vector sort.
  - isFiniteField
```
public boolean isFiniteField()
```
    Determine if this is a finite field sort (SMT-LIB: (_ FiniteField i)).
    
    Returns:
    
    True if this sort is a finite field sort.
  - isFloatingPoint
```
public boolean isFloatingPoint()
```
    Determine if this is a floatingpoint sort (SMT-LIB: (_ FloatingPoint eb sb)).
    
    Returns:
    
    True if this sort is a floating-point sort.
  - isDatatype
```
public boolean isDatatype()
```
    Determine if this is a datatype sort.
    
    Returns:
    
    True if this sort is a datatype sort.
  - isDatatypeConstructor
```
public boolean isDatatypeConstructor()
```
    Determine if this is a datatype constructor sort.
    
    Returns:
    
    True if this sort is a datatype constructor sort.
  - isDatatypeSelector
```
public boolean isDatatypeSelector()
```
    Determine if this is a datatype selector sort.
    
    Returns:
    
    True if this sort is a datatype selector sort.
  - isDatatypeTester
```
public boolean isDatatypeTester()
```
    Determine if this is a datatype tester sort.
    
    Returns:
    
    True if this sort is a datatype tester sort.
  - isDatatypeUpdater
```
public boolean isDatatypeUpdater()
```
    Determine if this is a datatype updater sort.
    
    Returns:
    
    True if this sort is a datatype updater sort.
  - isFunction
```
public boolean isFunction()
```
    Determine if this is a function sort.
    
    Returns:
    
    True if this sort is a function sort.
  - isPredicate
```
public boolean isPredicate()
```
    Determine if this is a predicate sort. A predicate sort is a function sort that maps to the Boolean sort. All predicate sorts are also function sorts.
    
    Returns:
    
    True if this sort is a predicate sort.
  - isTuple
```
public boolean isTuple()
```
    Determine if this a tuple sort.
    
    Returns:
    
    True if this sort is a tuple sort.
  - isNullable
```
public boolean isNullable()
```
    Determine if this a nullable sort.
    
    Returns:
    
    True if this sort is a nullable sort.
  - isRecord
```
public boolean isRecord()
```
    Determine if this is a record sort.
    
    Returns:
    
    True if the sort is a record sort.
    
    Note:
    
    This method is experimental and may change in future versions.
  - isArray
```
public boolean isArray()
```
    Determine if this is an array sort.
    
    Returns:
    
    True if the sort is an array sort.
  - isSet
```
public boolean isSet()
```
    Determine if this is a Set sort.
    
    Returns:
    
    True if the sort is a Set sort.
  - isBag
```
public boolean isBag()
```
    Determine if this is a Bag sort.
    
    Returns:
    
    True if the sort is a Bag sort.
  - isSequence
```
public boolean isSequence()
```
    Determine if this is a Sequence sort.
    
    Returns:
    
    True if the sort is a Sequence sort.
  - isAbstract
```
public boolean isAbstract()
```
    Determine if this is an abstract sort.
    
    Returns:
    
    True if the sort is a abstract sort.
    
    Note:
    
    This method is experimental and may change in future versions.
  - isUninterpretedSort
```
public boolean isUninterpretedSort()
```
    Determine if this is an uninterpreted sort.
    
    Returns:
    
    True if this is an uninterpreted sort.
  - isUninterpretedSortConstructor
```
public boolean isUninterpretedSortConstructor()
```
    Determine if this is an uninterpreted sort constructor. An uninterpreted sort constructor has arity > 0 and can be instantiated to construct uninterpreted sorts with given sort parameters.
    
    Returns:
    
    True if this is a sort constructor kind.
  - isInstantiated
```
public boolean isInstantiated()
```
    Determine if this is an instantiated (parametric datatype or uninterpreted sort constructor) sort. An instantiated sort is a sort that has been constructed from instantiating a sort with sort arguments (see instantiate(Sort[])).
    
    Returns:
    
    True if this is an instantiated sort.
  - getUninterpretedSortConstructor
```
public Sort getUninterpretedSortConstructor()
```
    Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.
    
    Returns:
    
    The uninterpreted sort constructor sort.
  - getDatatype
```
public Datatype getDatatype()
```
    Returns:
    
    The underlying datatype of a datatype sort.
  - instantiate
```
public Sort instantiate(Sort[] params)
```
    Instantiate a parameterized datatype sort or uninterpreted sort constructor sort. Create sorts parameter with Solver.mkParamSort(String)).
    
    Parameters:
    
    params - The list of sort parameters to instantiate with.
    
    Returns:
    
    The instantiated sort.
    
    Note:
    
    This method is experimental and may change in future versions.
  - getInstantiatedParameters
```
public Sort[] getInstantiatedParameters()
```
    Get the sorts used to instantiate the sort parameters of a parametric sort (parametric datatype or uninterpreted sort constructor sort, see instantiate(Sort[])).
    
    Returns:
    
    The sorts used to instantiate the sort parameters of a parametric sort.
  - substitute
```
public Sort substitute(Sort sort,
                       Sort replacement)
```
    Substitution of Sorts.
    
    Parameters:
    
    sort - The subsort to be substituted within this sort.
    
    replacement - The sort replacing the substituted subsort.
    
    Returns:
    
    The sort yielded by substituting the replacement sort within the given sort.
    
    Note:
    
    This replacement is applied during a pre-order traversal and only once to the sort. It is not run until fix point., This method is experimental and may change in future versions.
  - substitute
```
public Sort substitute(Sort[] sorts,
                       Sort[] replacements)
```
    Simultaneous substitution of Sorts. Note that this replacement is applied during a pre-order traversal and only once to the sort. It is not run until fix point. In the case that sorts contains duplicates, the replacement earliest in the list takes priority. For example, (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will return (Array (Array C D) B).
    
    Parameters:
    
    sorts - The subsorts to be substituted within this sort.
    
    replacements - The sort replacing the substituted subsorts.
    
    Returns:
    
    The sorts yielded by substituting the replacement sort within the given sorts.
    
    Note:
    
    This method is experimental and may change in future versions.
  - toString
```
protected java.lang.String toString(long pointer)
```
    Returns:
    
    A string representation of this sort.
  - getDatatypeConstructorArity
```
public int getDatatypeConstructorArity()
```
    Returns:
    
    The arity of a datatype constructor sort.
  - getDatatypeConstructorDomainSorts
```
public Sort[] getDatatypeConstructorDomainSorts()
```
    Returns:
    
    The domain sorts of a datatype constructor sort.
  - getDatatypeConstructorCodomainSort
```
public Sort getDatatypeConstructorCodomainSort()
```
    Returns:
    
    The codomain sort of a datatype constructor sort.
  - getDatatypeSelectorDomainSort
```
public Sort getDatatypeSelectorDomainSort()
```
    Returns:
    
    The domain sort of a datatype selector sort.
  - getDatatypeSelectorCodomainSort
```
public Sort getDatatypeSelectorCodomainSort()
```
    Returns:
    
    The codomain sort of a datatype selector sort.
  - getDatatypeTesterDomainSort
```
public Sort getDatatypeTesterDomainSort()
```
    Returns:
    
    The domain sort of a datatype tester sort.
  - getDatatypeTesterCodomainSort
```
public Sort getDatatypeTesterCodomainSort()
```
    Returns:
    
    The codomain sort of a datatype tester sort, which is the Boolean sort.
  - getFunctionArity
```
public int getFunctionArity()
```
    Returns:
    
    The arity of a function sort.
  - getFunctionDomainSorts
```
public Sort[] getFunctionDomainSorts()
```
    Returns:
    
    The domain sorts of a function sort.
  - getFunctionCodomainSort
```
public Sort getFunctionCodomainSort()
```
    Returns:
    
    The codomain sort of a function sort.
  - getArrayIndexSort
```
public Sort getArrayIndexSort()
```
    Returns:
    
    The array index sort of an array sort.
  - getArrayElementSort
```
public Sort getArrayElementSort()
```
    Returns:
    
    The array element sort of an array element sort.
  - getSetElementSort
```
public Sort getSetElementSort()
```
    Returns:
    
    The element sort of a set sort.
  - getBagElementSort
```
public Sort getBagElementSort()
```
    Returns:
    
    The element sort of a bag sort.
  - getSequenceElementSort
```
public Sort getSequenceElementSort()
```
    Returns:
    
    The element sort of a sequence sort.
  - getAbstractedKind
```
public SortKind getAbstractedKind()
                           throws CVC5ApiException
```
    Returns:
    
    The sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.
    
    Throws:
    
    CVC5ApiException - on error
    
    Note:
    
    This method is experimental and may change in future versions.
  - getUninterpretedSortConstructorArity
```
public int getUninterpretedSortConstructorArity()
```
    Returns:
    
    The arity of an uninterpreted sort constructor sort.
  - getBitVectorSize
```
public int getBitVectorSize()
```
    Returns:
    
    The bit-width of the bit-vector sort.
  - getFiniteFieldSize
```
public java.lang.String getFiniteFieldSize()
```
    Returns:
    
    The bit-width of the bit-vector sort.
  - getFloatingPointExponentSize
```
public int getFloatingPointExponentSize()
```
    Returns:
    
    The bit-width of the exponent of the floating-point sort.
  - getFloatingPointSignificandSize
```
public int getFloatingPointSignificandSize()
```
    Returns:
    
    The width of the significand of the floating-point sort.
  - getDatatypeArity
```
public int getDatatypeArity()
```
    Returns:
    
    The arity of a datatype sort.
  - getTupleLength
```
public int getTupleLength()
```
    Returns:
    
    The length of a tuple sort.
  - getTupleSorts
```
public Sort[] getTupleSorts()
```
    Returns:
    
    The element sorts of a tuple sort.
  - getNullableElementSort
```
public Sort getNullableElementSort()
```
    Returns:
    
    The element sort of a nullable sort.
  - hashCode
```
public int hashCode()
```
    Get the hash value of a sort.
    
    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

Class Sort

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

pointer

Constructor Detail

Sort

Method Detail

deletePointer

equals

compareTo

getKind

hasSymbol

getSymbol

isNull

isBoolean

isInteger

isReal

isString

isRegExp

isRoundingMode

isBitVector

isFiniteField

isFloatingPoint

isDatatype

isDatatypeConstructor

isDatatypeSelector

isDatatypeTester

isDatatypeUpdater

isFunction

isPredicate

isTuple

isNullable

isRecord

isArray

isSet

isBag

isSequence

isAbstract

isUninterpretedSort

isUninterpretedSortConstructor

isInstantiated

getUninterpretedSortConstructor

getDatatype

instantiate

getInstantiatedParameters

substitute

substitute

toString

getDatatypeConstructorArity

getDatatypeConstructorDomainSorts

getDatatypeConstructorCodomainSort

getDatatypeSelectorDomainSort

getDatatypeSelectorCodomainSort

getDatatypeTesterDomainSort

getDatatypeTesterCodomainSort

getFunctionArity

getFunctionDomainSorts

getFunctionCodomainSort

getArrayIndexSort

getArrayElementSort

getSetElementSort

getBagElementSort

getSequenceElementSort

getAbstractedKind

getUninterpretedSortConstructorArity

getBitVectorSize

getFiniteFieldSize

getFloatingPointExponentSize

getFloatingPointSignificandSize

getDatatypeArity

getTupleLength

getTupleSorts

getNullableElementSort

hashCode

getPointer

deletePointer

toString