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
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 |
equalsModRenaming(Term o)
Compares if two terms are equal modulo bound renaming
|
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
|
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)
boolean hasLabels()
boolean containsLabel(TermLabel label)
label
- the TermLabel for which to look (must not be null)ImmutableArray<TermLabel> getLabels()
null
int serialNumber()