de.uni_freiburg.informatik.ultimate.logic

Class ApplicationTerm

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.Term

de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm

public class ApplicationTerm
extends Term

Represents a function application term. This consists of a function symbol and zero or more sub-terms (the parameters of the function). A constant is represented as function application with zero parameters. An application term is created by Script.term(String, Term...) or for indexed function symbols or for symbols with generic return sort by Script.term(String, java.math.BigInteger[], Sort, Term...).

Author:

hoenicke

Field Summary

Fields inherited from class de.uni_freiburg.informatik.ultimate.logic.Term

mTmpCtr

Method Summary

Modifier and Type	Method and Description
FunctionSymbol	getFunction() Get the function symbol.
Term[]	getParameters() Get the parameters of the function application.
Sort	getSort() Returns the SMTLIB sort of this term.
void	toStringHelper(java.util.ArrayDeque<java.lang.Object> mTodo) Convert a term to a string in a stack based fashion.

Methods inherited from class de.uni_freiburg.informatik.ultimate.logic.Term

getFreeVars, getTheory, hashCode, toString, toStringDirect

Methods inherited from class java.lang.Object

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

Method Detail

getFunction

public FunctionSymbol getFunction()

Get the function symbol.

Returns:

the function symbol.

See Also:

FunctionSymbol.getName()

getParameters

public Term[] getParameters()

Get the parameters of the function application.

Returns:

the parameters. For constants this array is empty. Never write to this array!

getSort

public Sort getSort()

Returns the SMTLIB sort of this term.

Specified by:

getSort in class Term

Returns:

the sort of the term.

toStringHelper

public void toStringHelper(java.util.ArrayDeque<java.lang.Object> mTodo)

Convert a term to a string in a stack based fashion. This is used for internal purposes. External users can just use toString() or toStringDirect().

Specified by:

toStringHelper in class Term

Parameters:

mTodo - The stack where to put the strings and sub terms.

See Also:

PrintTerm