class TermImpl extends java.lang.Object implements Term
Modifier and Type | Class and Description |
---|---|
private static class |
TermImpl.ThreeValuedTruth |
Modifier and Type | Field and Description |
---|---|
private ImmutableArray<QuantifiableVariable> |
boundVars |
private TermImpl.ThreeValuedTruth |
containsJavaBlockRecursive
|
private int |
depth |
private static ImmutableArray<TermLabel> |
EMPTY_LABEL_LIST |
private static ImmutableArray<Term> |
EMPTY_TERM_LIST |
private static ImmutableArray<QuantifiableVariable> |
EMPTY_VAR_LIST |
private static NameAbstractionTable |
FAILED
used to encode that handleJava results in an unsatisfiable
constraint (faster than using exceptions)
|
private ImmutableSet<QuantifiableVariable> |
freeVars |
private int |
hashcode |
private JavaBlock |
javaBlock |
private Operator |
op |
private TermImpl.ThreeValuedTruth |
rigid |
private int |
serialNumber |
private static java.util.concurrent.atomic.AtomicInteger |
serialNumberCounter |
private ImmutableArray<Term> |
subs |
Constructor and Description |
---|
TermImpl(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock) |
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.
|
private static NameAbstractionTable |
checkNat(NameAbstractionTable nat) |
private static boolean |
compareBoundVariables(QuantifiableVariable ownVar,
QuantifiableVariable cmpVar,
ImmutableList<QuantifiableVariable> ownBoundVars,
ImmutableList<QuantifiableVariable> cmpBoundVars)
compare two quantifiable variables if they are equal modulo renaming
|
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.
|
private boolean |
descendRecursively(Term t0,
Term t1,
ImmutableList<QuantifiableVariable> ownBoundVars,
ImmutableList<QuantifiableVariable> cmpBoundVars,
NameAbstractionTable nat) |
private ImmutableSet<QuantifiableVariable> |
determineFreeVars() |
boolean |
equals(java.lang.Object o)
true iff
o is syntactically equal to 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
|
private static NameAbstractionTable |
handleJava(Term t0,
Term t1,
NameAbstractionTable nat) |
private boolean |
handleQuantifiableVariable(Term t0,
Term t1,
ImmutableList<QuantifiableVariable> ownBoundVars,
ImmutableList<QuantifiableVariable> cmpBoundVars) |
int |
hashCode() |
boolean |
hasLabels()
returns true if the term is labeled
|
private static int |
indexOf(QuantifiableVariable var,
ImmutableList<QuantifiableVariable> list) |
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 nr)
The
n -th direct subterm. |
ImmutableArray<Term> |
subs()
The subterms.
|
java.lang.String |
toString()
returns a linearized textual representation of this term
|
private boolean |
unifyHelp(Term t0,
Term t1,
ImmutableList<QuantifiableVariable> ownBoundVars,
ImmutableList<QuantifiableVariable> cmpBoundVars,
NameAbstractionTable nat)
Compares two terms modulo bound renaming
|
ImmutableArray<QuantifiableVariable> |
varsBoundHere(int n)
The logical variables bound by the top level operator for the nth
subterm.
|
private static final ImmutableArray<Term> EMPTY_TERM_LIST
private static final ImmutableArray<QuantifiableVariable> EMPTY_VAR_LIST
private static final ImmutableArray<TermLabel> EMPTY_LABEL_LIST
private static java.util.concurrent.atomic.AtomicInteger serialNumberCounter
private final int serialNumber
private final Operator op
private final ImmutableArray<Term> subs
private final ImmutableArray<QuantifiableVariable> boundVars
private final JavaBlock javaBlock
private int depth
private TermImpl.ThreeValuedTruth rigid
private ImmutableSet<QuantifiableVariable> freeVars
private int hashcode
private TermImpl.ThreeValuedTruth containsJavaBlockRecursive
private static NameAbstractionTable FAILED
public TermImpl(Operator op, ImmutableArray<Term> subs, ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock)
private ImmutableSet<QuantifiableVariable> determineFreeVars()
public 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
private static boolean compareBoundVariables(QuantifiableVariable ownVar, QuantifiableVariable cmpVar, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars)
ownVar
- first QuantifiableVariable to be comparedcmpVar
- second QuantifiableVariable to be comparedownBoundVars
- variables bound above the current positioncmpBoundVars
- variables bound above the current positionprivate static int indexOf(QuantifiableVariable var, ImmutableList<QuantifiableVariable> list)
var
in
list
, or -1
if the variable is not an
element of the listprivate boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars, NameAbstractionTable nat)
t0
- the first termt1
- the second termownBoundVars
- variables bound above the current positioncmpBoundVars
- variables bound above the current positiontrue
is returned iff the terms are equal modulo
bound renamingprivate boolean handleQuantifiableVariable(Term t0, Term t1, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars)
private static NameAbstractionTable handleJava(Term t0, Term t1, NameAbstractionTable nat)
private boolean descendRecursively(Term t0, Term t1, ImmutableList<QuantifiableVariable> ownBoundVars, ImmutableList<QuantifiableVariable> cmpBoundVars, NameAbstractionTable nat)
private static NameAbstractionTable checkNat(NameAbstractionTable nat)
public boolean equals(java.lang.Object o)
o
is syntactically equal to this termequals
in class java.lang.Object
public 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.