public final class PosInOccurrence
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private class |
PosInOccurrence.PIOPathIteratorImpl |
Modifier and Type | Field and Description |
---|---|
private short |
hashCode |
private boolean |
inAntec
is true iff the position is in the antecedent of a sequent.
|
private PosInTerm |
posInTerm
the position in sequentFormula.formula()
|
private SequentFormula |
sequentFormula
the constrained formula the pos in occurrence describes
|
private Term |
subTermCache
The subterm this object points to, or
null |
Constructor and Description |
---|
PosInOccurrence(SequentFormula sequentFormula,
PosInTerm posInTerm,
boolean inAntec) |
Modifier and Type | Method and Description |
---|---|
int |
depth() |
PosInOccurrence |
down(int i)
creates a new PosInOccurrence that has exactly the same state as this
object except the PosInTerm is new and walked down the specified
subterm, as specified in method down of
PosInTerm . |
boolean |
eqEquals(java.lang.Object obj)
compares this PosInOccurrence with another PosInOccurrence
and returns true if both describe the same occurrence
|
boolean |
equals(java.lang.Object obj)
Contrary to
eqEquals , this method returns true only for pio
objects that point to the same (identical) formula |
private boolean |
equalsHelp(PosInOccurrence cmp) |
static PosInOccurrence |
findInSequent(Sequent seq,
int formulaNumber,
PosInTerm pos) |
int |
getIndex() |
int |
hashCode() |
boolean |
isInAntec()
returns true iff the occurrence is in the
antecedent of a sequent.
|
boolean |
isTopLevel() |
PIOPathIterator |
iterator()
List all subterms between the root and the position this
objects points to; the first term is the whole term
constrainedFormula().formula() , the last one
subTerm() |
PosInTerm |
posInTerm()
The usage of this method is strongly discouraged, use
iterator() instead. |
PosInOccurrence |
replaceConstrainedFormula(SequentFormula p_newFormula)
Replace the formula this object points to with the new formula given
|
SequentFormula |
sequentFormula()
returns the SequentFormula that determines the occurrence of
this PosInOccurrence
|
Term |
subTerm()
returns the subterm this object points to
|
PosInOccurrence |
topLevel()
Ascend to the top node of the formula this object points to
|
java.lang.String |
toString()
toString
|
PosInOccurrence |
up()
Ascend to the parent node
|
private final SequentFormula sequentFormula
private final short hashCode
private final boolean inAntec
private final PosInTerm posInTerm
private volatile Term subTermCache
null
public PosInOccurrence(SequentFormula sequentFormula, PosInTerm posInTerm, boolean inAntec)
public static PosInOccurrence findInSequent(Sequent seq, int formulaNumber, PosInTerm pos)
public SequentFormula sequentFormula()
public int depth()
isTopLevel()
have depth zeropublic PosInOccurrence down(int i)
PosInTerm
.public boolean eqEquals(java.lang.Object obj)
public boolean equals(java.lang.Object obj)
eqEquals
, this method returns true only for pio
objects that point to the same (identical) formulaequals
in class java.lang.Object
obj
- private boolean equalsHelp(PosInOccurrence cmp)
public int getIndex()
PosInOccurrence
points to. If the position is
top-level, the result will be -1
public int hashCode()
hashCode
in class java.lang.Object
public boolean isInAntec()
public boolean isTopLevel()
public PIOPathIterator iterator()
constrainedFormula().formula()
, the last one
subTerm()
PosInOccurrence
-object points topublic PosInTerm posInTerm()
iterator()
instead.
describes the exact occurrence of the referred term inside
SequentFormula.formula()
public PosInOccurrence replaceConstrainedFormula(SequentFormula p_newFormula)
p_newFormula
- the new formulaPosInOccurrence
object that points to the same
position within the formula p_newFormula
as this
object does within the formula constrainedFormula()
.
It is not tested whether this position exists within p_newFormula
public Term subTerm()
public PosInOccurrence topLevel()
public java.lang.String toString()
toString
in class java.lang.Object
public PosInOccurrence up()