public final class PosInTerm
extends java.lang.Object
down(int)
to keep track of the current position. Pass as argument the
position of the subterm to be taken. Attention: Each invocation creates a new position in term
object which has to be used for further navigation. The original one remains unchanged.Modifier and Type | Class and Description |
---|---|
static class |
PosInTerm.PiTIterator |
Modifier and Type | Field and Description |
---|---|
private boolean |
copy |
private char |
hash |
private char[] |
positions |
private char |
size |
private static PosInTerm |
TOP_LEVEL |
Modifier | Constructor and Description |
---|---|
private |
PosInTerm()
only used once to create the singleton for the top level position
|
private |
PosInTerm(char[] positions,
char size,
boolean copy)
creates an instance representing the position
positions[0..size-1] |
Modifier and Type | Method and Description |
---|---|
int |
depth()
the depth of the sub term described by this position
|
PosInTerm |
down(int i)
returns the position for the
i -th subterm of the subterm described by this position |
boolean |
equals(java.lang.Object o) |
PosInTerm |
firstN(int n)
returns the position of the
depth-n parent term |
int |
getIndex()
equivalent to
getIndexAt(depth() - 1) |
int |
getIndexAt(int i)
returns the index of the subterm at depth
i |
Term |
getSubTerm(Term t)
navigate to the subterm described by this position and return it
if the described position does not exist in the term an
IndexOutOfBoundsException
is thrown |
static PosInTerm |
getTopLevel()
returns the instance representing the top level position
|
int |
hashCode() |
java.lang.String |
integerList(IntIterator it)
returns a comma separated list of integers enclosed in brackets (the list contains all integers
in the order as returned by the iterator)
|
boolean |
isPrefixOf(PosInTerm pit)
Checks whether this pit is the prefix of a given pit.
|
boolean |
isTopLevel()
true if the position describes the top level position, i.e., the term as a whole
|
IntIterator |
iterator()
iterates through all indices in top to bottom order
|
static PosInTerm |
parseReverseString(java.lang.String s)
create a position from the string
The string contains a comma separated list of integers.
|
IntIterator |
reverseIterator()
iterates through all indices in bottom to top order
|
java.lang.String |
toString() |
PosInTerm |
up()
returns the position of the enclosing term
|
private static final PosInTerm TOP_LEVEL
private final char[] positions
private final char size
private volatile char hash
private volatile boolean copy
private PosInTerm()
private PosInTerm(char[] positions, char size, boolean copy)
positions[0..size-1]
positions
- the integer array where each element describes the position to be taken (in top-to-bottom order)size
- the size of the integer list (attention: might be shorter than the length of the position array)copy
- indicates (i.e. true) if the position array has to be copied when going downwardspublic static PosInTerm parseReverseString(java.lang.String s)
s
- the String with the list of integers to be interpreted as term indices in
reverse orderpublic static PosInTerm getTopLevel()
public int depth()
public boolean isTopLevel()
public PosInTerm up()
public PosInTerm firstN(int n)
depth-n
parent termn
- the integer specifying the length of the prefixn
java.lang.IndexOutOfBoundsException
- if n
is greater than the depth of this positionpublic PosInTerm down(int i)
i
-th subterm of the subterm described by this positioni
- the index of the subtermpublic int getIndexAt(int i)
i
i
- the depth of the subterm whose index it to be returnedterm.subAt(this).sub(getIndex(i)) == term.subAt(firstN(i+1))
public int getIndex()
getIndexAt(depth() - 1)
public Term getSubTerm(Term t)
IndexOutOfBoundsException
is thrownt
- the Term
t
at this positionan
- IndexOutOfBoundsException
if no subterm exists at this positionpublic int hashCode()
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public java.lang.String integerList(IntIterator it)
it
- the iteratorpublic IntIterator iterator()
public IntIterator reverseIterator()
public java.lang.String toString()
toString
in class java.lang.Object
public boolean isPrefixOf(PosInTerm pit)
pit
- the given pit