de.uka.ilkd.key.logic

Class LabeledTermImpl

java.lang.Object

de.uka.ilkd.key.logic.TermImpl

de.uka.ilkd.key.logic.LabeledTermImpl

All Implemented Interfaces:

SVSubstitute, Sorted, Term

class LabeledTermImpl
extends TermImpl

The labeled term class is used for terms that have a label attached. Two labeled terms are equal if they have equal term structure and equal annotations. In contrast the method Term#equalsModRenaming(Object) does not care about annotations and will just compare the term structure alone modula renaming.

See Also:

Term, TermImpl

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableArray<TermLabel>	labels

Constructor Summary

Constructors

Constructor and Description
LabeledTermImpl(Operator op, ImmutableArray<Term> subs, ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock, ImmutableArray<TermLabel> labels) creates an instance of a labeled term.

Method Summary

Modifier and Type	Method and Description
int	computeHashCode() performs the actual computation of the hashcode and can be overwritten by subclasses if necessary
boolean	containsLabel(TermLabel label) returns true if the given label is attached
boolean	equals(java.lang.Object o) true iff o is syntactically equal to this term
TermLabel	getLabel(Name termLabelName) Returns the first TermLabel with the given Name.
ImmutableArray<TermLabel>	getLabels() returns the labels attached to this term
boolean	hasLabels() returns true if the term is labeled
java.lang.String	toString() returns a linearized textual representation of this term

Methods inherited from class de.uka.ilkd.key.logic.TermImpl

arity, boundVars, checked, containsJavaBlockRecursive, depth, equalsModRenaming, execPostOrder, execPreOrder, freeVars, hashCode, isRigid, javaBlock, op, op, serialNumber, sort, sub, subs, varsBoundHere

Methods inherited from class java.lang.Object

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

Field Detail

labels

private final ImmutableArray<TermLabel> labels

Constructor Detail

LabeledTermImpl

public LabeledTermImpl(Operator op,
                       ImmutableArray<Term> subs,
                       ImmutableArray<QuantifiableVariable> boundVars,
                       JavaBlock javaBlock,
                       ImmutableArray<TermLabel> labels)

creates an instance of a labeled term.

Parameters:

op - the top level operator

subs - the Term that are the subterms of this term

boundVars - logic variables bound by the operator

javaBlock - contains the program part of the term (if any)

labels - the terms labels (must not be null or empty)

Method Detail

hasLabels

public boolean hasLabels()

returns true if the term is labeled

Specified by:

hasLabels in interface Term

Overrides:

hasLabels in class TermImpl

getLabels

public ImmutableArray<TermLabel> getLabels()

returns the labels attached to this term

Specified by:

getLabels in interface Term

Overrides:

getLabels in class TermImpl

Returns:

list of labels (maybe be empty but never null

getLabel

public TermLabel getLabel(Name termLabelName)

Description copied from interface: Term

Returns the first TermLabel with the given Name.

Specified by:

getLabel in interface Term

Overrides:

getLabel in class TermImpl

Parameters:

termLabelName - The Name of the TermLabel to search.

Returns:

The first found TermLabel or null if not available.

containsLabel

public boolean containsLabel(TermLabel label)

returns true if the given label is attached

Specified by:

containsLabel in interface Term

Overrides:

containsLabel in class TermImpl

Parameters:

label - the TermLabel for which to look (must not be null)

Returns:

true iff. the label is attached to this term

equals

public boolean equals(java.lang.Object o)

true iff o is syntactically equal to this term

Overrides:

equals in class TermImpl

computeHashCode

public int computeHashCode()

performs the actual computation of the hashcode and can be overwritten by subclasses if necessary

Overrides:

computeHashCode in class TermImpl

toString

public java.lang.String toString()

returns a linearized textual representation of this term

Overrides:

toString in class TermImpl