public interface Term extends SVSubstitute, Sorted
Sort.FORMULA
. Terms of a different sort are terms in the
customary logic sense. A term of sort formula is allowed exact there, where a
formuala in logic is allowed to appear, same for terms of different sorts.
Some words about other design decisions:
TermFactory
and
_not_ by using the constructors itself.
TermFactory
know only the class
Term and its interface. Even most classes of the logic package.
Visitor
pattern. Two different visit strategies are
currently supported: execPostOrder(Visitor)
and
execPreOrder(Visitor)
.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.
|
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 |
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
|
default java.lang.String |
getOrigin()
Returns an human-readable source of this term.
|
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.
|
Sort |
sort()
The sort of the term.
|
Term |
sub(int n)
The
n -th direct subterm. |
ImmutableArray<Term> |
subs()
The subterms.
|
ImmutableArray<QuantifiableVariable> |
varsBoundHere(int n)
The logical variables bound by the top level operator for the nth
subterm.
|
Operator op()
<T> T op(java.lang.Class<T> opClass) throws java.lang.IllegalArgumentException
java.lang.IllegalArgumentException
ImmutableArray<Term> subs()
Term sub(int n)
n
-th direct subterm.ImmutableArray<QuantifiableVariable> boundVars()
ImmutableArray<QuantifiableVariable> varsBoundHere(int n)
JavaBlock javaBlock()
int arity()
int depth()
boolean isRigid()
ImmutableSet<QuantifiableVariable> freeVars()
void execPostOrder(Visitor visitor)
visitor
- the Visitorvoid execPreOrder(Visitor visitor)
visitor
- the Visitorboolean equalsModRenaming(Term o)
o
- another term,boolean hasLabels()
boolean containsLabel(TermLabel label)
label
- the TermLabel for which to look (must not be null)ImmutableArray<TermLabel> getLabels()
null
int serialNumber()
boolean containsJavaBlockRecursive()
boolean equalsModIrrelevantTermLabels(java.lang.Object o)
o
is a term syntactically equal to this one,
except for some irrelevant labels.o
- an objecttrue
iff o
is a term syntactically equal to this one,
except for their labels.TermLabel#isStrategyRelevant
boolean equalsModTermLabels(java.lang.Object o)
o
is a term syntactically equal to this one, ignoring all term
labels.o
- an objecttrue
iff o
is a term syntactically equal to this ignoring term labels@Nullable default java.lang.String getOrigin()
Copyright © 2003-2019 The KeY-Project.