de.uni_freiburg.informatik.ultimate.logic

Class Term

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.Term

Direct Known Subclasses:

AnnotatedTerm, ApplicationTerm, ConstantTerm, LetTerm, QuantifiedFormula, TermVariable

public abstract class Term
extends java.lang.Object

This is the base class for representing SMTLIB 2 terms. You can assume that every term is one of the following sub-classes:

• ApplicationTerm represents a function application (name ...).
• AnnotatedTerm represents an annotated term (! term ...).
• ConstantTerm represents a numeral, decimal, bit vector, or string literal.
• LetTerm represents a let term (let ((var term)...) term).
• TermVariable represents a term variable var used in quantifier or let term. Note that constants are represented by ApplicationTerm.
• QuantifiedFormula represents a quantified formula (exists/forall ...).

In principle it is possible to write your own sub-classes, but that is dangerous and only recommend for the advanced SMTInterpol hacker.

Author:

Juergen Christ, Jochen Hoenicke

Field Summary

Fields

Modifier and Type	Field and Description
int	mTmpCtr A temporary counter used e.g. to count the number of occurrences of this term in a bigger term.

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	Term(int hash) Create a term.

Method Summary

Modifier and Type	Method and Description
TermVariable[]	getFreeVars() Computes and returns the free variables occurring in this term.
abstract Sort	getSort() Returns the SMTLIB sort of this term.
de.uni_freiburg.informatik.ultimate.logic.Theory	getTheory()
int	hashCode()
java.lang.String	toString() Prints an SMTLIB representation of this term.
java.lang.String	toStringDirect() Prints the canonical SMTLIB representation of this term.
protected abstract void	toStringHelper(java.util.ArrayDeque<java.lang.Object> mTodo) Convert a term to a string in a stack based fashion.

Methods inherited from class java.lang.Object

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

Field Detail

mTmpCtr

public int mTmpCtr

A temporary counter used e.g. to count the number of occurrences of this term in a bigger term. Don't use this!!!!

Constructor Detail

Term

protected Term(int hash)

Create a term.

Parameters:

hash - the hash code of the term. This should be stable.

Method Detail

getSort

public abstract Sort getSort()

Returns the SMTLIB sort of this term.

Returns:

the sort of the term.

getFreeVars

public TermVariable[] getFreeVars()

Computes and returns the free variables occurring in this term.

Returns:

the free variables.

getTheory

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

toString

public java.lang.String toString()

Prints an SMTLIB representation of this term. This introduces lets for common subexpressions to prevent exponential blow-up when printing a term with lots of sharing.

Overrides:

toString in class java.lang.Object

Returns:

an SMTLIB representation.

toStringDirect

public java.lang.String toStringDirect()

Prints the canonical SMTLIB representation of this term. This does not eliminate common sub-expressions and can cause exponential blow-up.

Returns:

the canonical SMTLIB representation.

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toStringHelper

protected abstract 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().

Parameters:

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

See Also:

PrintTerm