Package io.github.cvc5

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

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

      • getPointer

        public long getPointer()

      • deletePointer

        public void deletePointer()

      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object