de.uni_freiburg.informatik.ultimate.logic

Class Sort

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.Sort

public final class Sort
extends java.lang.Object

Represents an SMTLIB sort. We distinguish real sorts (which are declared with declare-sort or pre-defined in the logic) from defined sort (which are defined with define-sort to some other sort. For a real sort, getRealSort() == this holds. A sort has a sort symbol and as many sort arguments as the sort symbol specifies. There are also parametric sorts used for declaring polymorphic function symbols. A parametric sort (or sort variable) has a position (used for substitution) and a name, both stored in the SortSymbol. Every term has a closed real sort, which can be obtained by term.getSort(). Defined sorts may occur only in function symbols and the declared sort of a term variable. Sorts that are not closed may only occur in polymorphic function symbols and in sort definitions in SortSymbol.

Author:

Jochen Hoenicke

Method Summary

Modifier and Type	Method and Description
Sort[]	getArguments() Get the sort arguments for a sort.
java.lang.String	getIndexedName() Get the indexed name of this sort in smtlib representation.
java.math.BigInteger[]	getIndices() Get the indices, if this is an indexed sort like (_ bv 5).
java.lang.String	getName() Get the name of this sort.
Sort	getRealSort() Get the real sort.
de.uni_freiburg.informatik.ultimate.logic.Theory	getTheory()
int	hashCode()
boolean	isArraySort() Returns true if this is an array sort.
boolean	isInternal() Returns true if this sort is internal, i.e., defined by an SMTLIB theory.
boolean	isNumericSort() Returns true if this is a numeric sort.
boolean	isParametric() This returns true if and only if the sort was created with Script.sortVariables(String...).
java.lang.String	toString() This returns the SMTLIB string represenation of this sort.

Methods inherited from class java.lang.Object

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

Method Detail

getName

public java.lang.String getName()

Get the name of this sort.

Returns:

the name.

getIndexedName

public java.lang.String getIndexedName()

Get the indexed name of this sort in smtlib representation.

Returns:

the name.

getIndices

public java.math.BigInteger[] getIndices()

Get the indices, if this is an indexed sort like (_ bv 5).

Returns:

the indices, null if this sort is not indexed.

getArguments

public Sort[] getArguments()

Get the sort arguments for a sort. This is used for a sort, whose sort symbol was declared with declare-sort(name, int) where the second parameter is not zero. In that case the sort is created with sort arguments and these arguments are returned by this method.

Returns:

An array containing the sort arguments for this sort. You must never write to this array.

getRealSort

public Sort getRealSort()

Get the real sort. This is used for sorts that are defined with define-sort. For other sorts this just returns this.

Returns:

the sort representation where all sort definitions are expanded.

isParametric

public boolean isParametric()

This returns true if and only if the sort was created with Script.sortVariables(String...). These are only used for a later define-sort command.

Returns:

true iff this is a sort variable.

toString

public java.lang.String toString()

This returns the SMTLIB string represenation of this sort.

Overrides:

toString in class java.lang.Object

Returns:

the SMTLIB string representation.

getTheory

public de.uni_freiburg.informatik.ultimate.logic.Theory getTheory()

isArraySort

public boolean isArraySort()

Returns true if this is an array sort. This is any instantiation of the parametric sort Array defined by the SMTLIB array theory.

Returns:

true if this is an array sort.

isNumericSort

public boolean isNumericSort()

Returns true if this is a numeric sort. Numeric sorts are only the sorts Int and Real defined by the corresponding SMTLIB theories.

Returns:

true if this is a numeric sort.

isInternal

public boolean isInternal()

Returns true if this sort is internal, i.e., defined by an SMTLIB theory.

Returns:

true if the sort is internal, false if it is user defined.

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object