public class TermImpl extends java.lang.Object implements Term
Constructor and Description |
---|
TermImpl(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock)
Constructs a term for the given operator, with the given sub terms,
bounded variables and (if applicable) the code block on this term.
|
Modifier and Type | Method and Description |
---|---|
int |
arity()
The arity of the term.
|
ImmutableArray<QuantifiableVariable> |
boundVars()
The logical variables bound by the top level operator.
|
Term |
checked()
Checks whether the Term is valid on the top level.
|
protected int |
computeHashCode()
Performs the actual computation of the hashcode and can be overwritten by subclasses
if necessary
|
boolean |
containsJavaBlockRecursive()
|
boolean |
containsLabel(TermLabel label)
checks if the given label is attached to the term
|
int |
depth()
The nesting depth of this term.
|
boolean |
equals(java.lang.Object o)
true iff
o is syntactically equal to this term |
boolean |
equalsModIrrelevantTermLabels(java.lang.Object o)
Checks if
o is a term syntactically equal to this one,
except for some irrelevant labels. |
boolean |
equalsModRenaming(Term o)
Compares if two terms are equal modulo bound renaming
|
boolean |
equalsModTermLabels(java.lang.Object o)
Checks if
o is a term syntactically equal to this one, ignoring all term
labels. |
void |
execPostOrder(Visitor visitor)
The visitor is handed through till the bottom of the tree and
then it walks upwards, while at each upstep the method visit of
the visitor is called.
|
void |
execPreOrder(Visitor visitor)
The visitor walks downwards the tree, while at each downstep the method
visit of the visitor is called.
|
ImmutableSet<QuantifiableVariable> |
freeVars()
The set of free quantifiable variables occurring in this term.
|
TermLabel |
getLabel(Name termLabelName)
|
ImmutableArray<TermLabel> |
getLabels()
returns list of labels attached to this term
|
java.lang.String |
getOrigin()
Returns an human-readable source of this term.
|
int |
hashCode() |
boolean |
hasLabels()
returns true if the term is labeled
|
boolean |
isRigid()
Whether all operators in this term are rigid.
|
JavaBlock |
javaBlock()
The Java block at top level.
|
Operator |
op()
The top operator (e.g., in "A and B" this is "and", in f(x,y) it is "f").
|
<T> T |
op(java.lang.Class<T> opClass)
The top operator (e.g., in "A and B" this is "and", in f(x,y) it is "f")
casted to the passed type.
|
int |
serialNumber()
Returns a serial number for a term.
|
void |
setOrigin(java.lang.String origin) |
Sort |
sort()
The sort of the term.
|
Term |
sub(int nr)
The
n -th direct subterm. |
ImmutableArray<Term> |
subs()
The subterms.
|
java.lang.String |
toString()
returns a linearized textual representation of this term
|
ImmutableArray<QuantifiableVariable> |
varsBoundHere(int n)
The logical variables bound by the top level operator for the nth
subterm.
|
public TermImpl(Operator op, ImmutableArray<Term> subs, ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock)
op
- the operator of the term, e.g., some arithmetic operationsubs
- the sub terms of the constructed term (whose type is
constrained by the used operator)boundVars
- the bounded variables (if applicable), e.g., for quantifiersjavaBlock
- the code block (if applicable) after which the term is evaluatedpublic Term checked()
public Operator op()
Term
public <T> T op(java.lang.Class<T> opClass) throws java.lang.IllegalArgumentException
Term
public ImmutableArray<Term> subs()
Term
public ImmutableArray<QuantifiableVariable> boundVars()
Term
public ImmutableArray<QuantifiableVariable> varsBoundHere(int n)
Term
varsBoundHere
in interface Term
public JavaBlock javaBlock()
Term
public int arity()
Term
public int depth()
Term
public boolean isRigid()
Term
public ImmutableSet<QuantifiableVariable> freeVars()
Term
public void execPostOrder(Visitor visitor)
Term
execPostOrder
in interface Term
visitor
- the Visitorpublic void execPreOrder(Visitor visitor)
Term
execPreOrder
in interface Term
visitor
- the Visitorpublic final boolean equalsModRenaming(Term o)
Term
equalsModRenaming
in interface Term
o
- another term,public boolean equals(java.lang.Object o)
o
is syntactically equal to this termequals
in class java.lang.Object
public boolean equalsModIrrelevantTermLabels(java.lang.Object o)
Term
o
is a term syntactically equal to this one,
except for some irrelevant labels.equalsModIrrelevantTermLabels
in interface Term
o
- an objecttrue
iff o
is a term syntactically equal to this one,
except for their labels.TermLabel#isStrategyRelevant
public boolean equalsModTermLabels(java.lang.Object o)
Term
o
is a term syntactically equal to this one, ignoring all term
labels.equalsModTermLabels
in interface Term
o
- an objecttrue
iff o
is a term syntactically equal to this ignoring term labelspublic final int hashCode()
hashCode
in class java.lang.Object
protected int computeHashCode()
public java.lang.String toString()
toString
in class java.lang.Object
public int serialNumber()
Term
serialNumber
in interface Term
public boolean hasLabels()
Term
public boolean containsLabel(TermLabel label)
Term
containsLabel
in interface Term
label
- the TermLabel for which to look (must not be null)public ImmutableArray<TermLabel> getLabels()
Term
public boolean containsJavaBlockRecursive()
containsJavaBlockRecursive
in interface Term
true
The Term
or one of its direct or indirect children contains a non empty JavaBlock
, false
no JavaBlock
available.@Nullable public java.lang.String getOrigin()
Term
public void setOrigin(java.lang.String origin)
Copyright © 2003-2019 The KeY-Project.