de.uni_freiburg.informatik.ultimate.logic

Class SortSymbol

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.SortSymbol

public class SortSymbol
extends java.lang.Object

A sort symbol is the name of an SMTLIB sort. In SMTLIB, sorts can be parametric over other sorts, e.g., the array sort Array IndexSort ElemSort is parametric over the index and element sort. The sort symbol represents only the name, i.e., Array and stores the number of sort parameters. Then several objects of type Sort can be instantiated with different sort parameters.

Author:

Jochen Hoenicke

Method Summary

Modifier and Type	Method and Description
void	checkArity(java.math.BigInteger[] indices, int arity) Checks whether the indices and the arity match and the sort can be created.
java.lang.String	getName() Returns the name of this sort.
Sort	getSort(java.math.BigInteger[] indices, Sort... args)
int	hashCode()
boolean	isArray() Check if this sort symbol corresponds to an array sort.
boolean	isIntern() Checks if the sort is internal, i.e., defined by the logic.
boolean	isNumeric() Check if this sort symbol corresponds to a numeric sort.
boolean	isParametric() Checks if this is a sort variable.
java.lang.String	toString() Returns a string representation of the sort symbol, as it would be used for declare-sort command.

Methods inherited from class java.lang.Object

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

Method Detail

isIntern

public boolean isIntern()

Checks if the sort is internal, i.e., defined by the logic.

Returns:

true, if the sort is an internal sort.

getName

public java.lang.String getName()

Returns the name of this sort. The | symbols used for quoting are not part of the name.

Returns:

the name of the sort.

toString

public java.lang.String toString()

Returns a string representation of the sort symbol, as it would be used for declare-sort command.

Overrides:

toString in class java.lang.Object

Returns:

the string representation.

checkArity

public void checkArity(java.math.BigInteger[] indices,
                       int arity)

Checks whether the indices and the arity match and the sort can be created. This function is called when a sort expression is parsed. Override this function if your sort expects indices.

Parameters:

indices - The indices.

arity - The number of sort parameters.

Throws:

java.lang.IllegalArgumentException - if the sort parameters or the index do not match.

getSort

public Sort getSort(java.math.BigInteger[] indices,
                    Sort... args)

isParametric

public boolean isParametric()

Checks if this is a sort variable.

Returns:

true if this is a sort variable.

isNumeric

public boolean isNumeric()

Check if this sort symbol corresponds to a numeric sort.

Returns:

true if this sort is numeric.

isArray

public boolean isArray()

Check if this sort symbol corresponds to an array sort.

Returns:

true if this sort is an array sort.

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object