de.uni_freiburg.informatik.ultimate.logic

Class LetTerm

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.Term

de.uni_freiburg.informatik.ultimate.logic.LetTerm

public class LetTerm
extends Term

Representation of a let term. This class represents the SMTLIB 2 construct

 (let ((var_0 val_0) ... (var_n val_n)) ...)
 

A let term is created by Script.let(TermVariable[], Term[], 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
Sort	getSort() Returns the SMTLIB sort of this term.
Term	getSubTerm()
Term[]	getValues()
TermVariable[]	getVariables()
static int	hashLet(TermVariable[] vars, Term[] values, Term subform)
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

getVariables

public TermVariable[] getVariables()

Returns:

The variables

getValues

public Term[] getValues()

Returns:

The values

getSubTerm

public Term getSubTerm()

Returns:

The subformula

getSort

public Sort getSort()

Description copied from class: Term

Returns the SMTLIB sort of this term.

Specified by:

getSort in class Term

Returns:

the sort of the term.

hashLet

public static final int hashLet(TermVariable[] vars,
                                Term[] values,
                                Term subform)

toStringHelper

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

Description copied from class: Term

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