Package io.github.cvc5

Class Sort

java.lang.Object
io.github.cvc5.Sort
All Implemented Interfaces:
Comparable<Sort>
public class Sort extends Object implements Comparable<Sort>
The sort of a cvc5 term.

  • Field Details

    • pointer

      protected long pointer
      The raw native pointer value.

  • Constructor Details

    • Sort

      public Sort()
      Null sort

  • Method Details

    • deletePointer

      protected void deletePointer(long pointer)
      Delete the native resource associated with the specified pointer.

      Subclasses must implement this method to provide resource-specific cleanup logic.

      Parameters:
      pointer - the native pointer to delete

    • equals

      public boolean equals(Object s)
      Comparison for structural equality.
      Overrides:
      equals in class 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 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
      Get the kind of this sort.
      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()
      Determine if the sort has a symbol.
      Returns:
      True if the sort has a symbol.

    • getSymbol

      public String getSymbol()
      Get the raw symbol of the symbol.
      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()
      Get the underlying datatype of a datatype sort.
      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 TermManager.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 String toString(long pointer)
      Return a string representation of the specified native pointer.

      Subclasses must implement this method to convert the native pointer into a meaningful string.

      Parameters:
      pointer - the native pointer
      Returns:
      A string representation of this sort.

    • getDatatypeConstructorArity

      public int getDatatypeConstructorArity()
      Get the arity of a datatype constructor sort.
      Returns:
      The arity of a datatype constructor sort.

    • getDatatypeConstructorDomainSorts

      public Sort[] getDatatypeConstructorDomainSorts()
      Get the domain sorts of a datatype constructor sort.
      Returns:
      The domain sorts of a datatype constructor sort.

    • getDatatypeConstructorCodomainSort

      public Sort getDatatypeConstructorCodomainSort()
      Get the codomain sort of a datatype constructor sort.
      Returns:
      The codomain sort of a datatype constructor sort.

    • getDatatypeSelectorDomainSort

      public Sort getDatatypeSelectorDomainSort()
      Get the domain sort of a datatype selector sort.
      Returns:
      The domain sort of a datatype selector sort.

    • getDatatypeSelectorCodomainSort

      public Sort getDatatypeSelectorCodomainSort()
      Get the codomain sort of a datatype selector sort.
      Returns:
      The codomain sort of a datatype selector sort.

    • getDatatypeTesterDomainSort

      public Sort getDatatypeTesterDomainSort()
      Get the domain sort of a datatype tester sort.
      Returns:
      The domain sort of a datatype tester sort.

    • getDatatypeTesterCodomainSort

      public Sort getDatatypeTesterCodomainSort()
      Get the codomain sort of a datatype tester sort, which is the Boolean sort.
      Returns:
      The codomain sort of a datatype tester sort, which is the Boolean sort.

    • getFunctionArity

      public int getFunctionArity()
      Get the arity of a function sort.
      Returns:
      The arity of a function sort.

    • getFunctionDomainSorts

      public Sort[] getFunctionDomainSorts()
      Get the domain sorts of a function sort.
      Returns:
      The domain sorts of a function sort.

    • getFunctionCodomainSort

      public Sort getFunctionCodomainSort()
      Get the codomain sort of a function sort.
      Returns:
      The codomain sort of a function sort.

    • getArrayIndexSort

      public Sort getArrayIndexSort()
      Get the array index sort of an array sort.
      Returns:
      The array index sort of an array sort.

    • getArrayElementSort

      public Sort getArrayElementSort()
      Get the array element sort of an array element sort.
      Returns:
      The array element sort of an array element sort.

    • getSetElementSort

      public Sort getSetElementSort()
      Get the element sort of a set sort.
      Returns:
      The element sort of a set sort.

    • getBagElementSort

      public Sort getBagElementSort()
      Get the element sort of a bag sort.
      Returns:
      The element sort of a bag sort.

    • getSequenceElementSort

      public Sort getSequenceElementSort()
      Get the element sort of a sequence sort.
      Returns:
      The element sort of a sequence sort.

    • getAbstractedKind

      public SortKind getAbstractedKind() throws CVC5ApiException
      Get the sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.
      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()
      Get the arity of an uninterpreted sort constructor sort.
      Returns:
      The arity of an uninterpreted sort constructor sort.

    • getBitVectorSize

      public int getBitVectorSize()
      Get the bit-width of the bit-vector sort.
      Returns:
      The bit-width of the bit-vector sort.

    • getFiniteFieldSize

      public String getFiniteFieldSize()
      Get the bit-width of the bit-vector sort.
      Returns:
      The bit-width of the bit-vector sort.

    • getFloatingPointExponentSize

      public int getFloatingPointExponentSize()
      Get the bit-width of the exponent of the floating-point sort.
      Returns:
      The bit-width of the exponent of the floating-point sort.

    • getFloatingPointSignificandSize

      public int getFloatingPointSignificandSize()
      Get the width of the significand of the floating-point sort.
      Returns:
      The width of the significand of the floating-point sort.

    • getDatatypeArity

      public int getDatatypeArity()
      Get the arity of a datatype sort.
      Returns:
      The arity of a datatype sort.

    • getTupleLength

      public int getTupleLength()
      Get the length of a tuple sort.
      Returns:
      The length of a tuple sort.

    • getTupleSorts

      public Sort[] getTupleSorts()
      Get the element sorts of a tuple sort.
      Returns:
      The element sorts of a tuple sort.

    • getNullableElementSort

      public Sort getNullableElementSort()
      Get the element sort of a nullable sort.
      Returns:
      The element sort of a nullable sort.

    • hashCode

      public int hashCode()
      Get the hash value of a sort.
      Overrides:
      hashCode in class Object
      Returns:
      The hash value.

    • getPointer

      public long getPointer()
      Return the raw native pointer.
      Returns:
      the pointer value

    • deletePointer

      public void deletePointer()
      Free the native resource associated with this pointer.

      This method should be called to explicitly clean up the underlying native resource. It removes this instance from the Context, then invokes the subclass-defined deletePointer(long) method to perform the actual cleanup.

    • toString

      public String toString()
      Return a string representation of the pointer.
      Overrides:
      toString in class Object
      Returns:
      a string representation of the pointer