de.uni_freiburg.informatik.ultimate.logic

Class TermVariable

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.Term

de.uni_freiburg.informatik.ultimate.logic.TermVariable

public class TermVariable
extends Term

Represents a term variable that is used in a lets, quantified formulas, and define-fun. Term variables are created by Script.variable(String, Sort).

Author:

Juergen Christ

Field Summary

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

mTmpCtr

Method Summary

Modifier and Type	Method and Description
Sort	getDeclaredSort() Return the declared sort of the variable.
java.lang.String	getName() Return the name of the variable.
Sort	getSort() Return the (expanded) sort of the variable.
java.lang.String	toString() The SMTLIB representation of the 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, toStringDirect

Methods inherited from class java.lang.Object

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

Method Detail

getName

public java.lang.String getName()

Return the name of the variable.

Returns:

the name of the variable.

getDeclaredSort

public Sort getDeclaredSort()

Return the declared sort of the variable.

Returns:

the sort of the variable that was used to declare the variable. This is not expanded if the sort is a defined sort.

getSort

public Sort getSort()

Return the (expanded) sort of the variable.

Specified by:

getSort in class Term

Returns:

the expanded sort of the variable.

toString

public java.lang.String toString()

The SMTLIB representation of the term.

Overrides:

toString in class Term

Returns:

an SMTLIB representation.

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