| java.lang.Object
 de.uka.ilkd.key.logic.PosInOccurrence
| PosInOccurrence | | public class PosInOccurrence (Code) | | This class describes a position in an occurrence of a term. A
ConstrainedFormula and a PosInTerm determine an object of this
class exactly.
|
| constrainedFormula | | public ConstrainedFormula constrainedFormula()(Code) | | returns the ConstrainedFormula that determines the occurrence of
this PosInOccurrence
|
| depth | | public int depth()(Code) | | Depth of the represented position within a formula; top-levelpositions (isTopLevel() have depth zero |
| eqEquals | | public boolean eqEquals(Object obj)(Code) | | compares this PosInOccurrence with another PosInOccurrence
and returns true if both describe the same occurrence
|
| equals | | public boolean equals(Object obj)(Code) | | Contrary to eqEquals, this method returns true only for pio
objects that point to the same (identical) formula
Parameters:
obj - |
| getIndex | | public int getIndex()(Code) | | the number/index of the deepest subterm that thisPosInOccurrence points to. If the position istop-level, the result will be -1 |
| hashCode | | public int hashCode()(Code) | | |
| isInAntec | | public boolean isInAntec()(Code) | | returns true iff the occurrence is in the
antecedent of a sequent.
|
| isTopLevel | | public boolean isTopLevel()(Code) | | |
| iterator | | public PIOPathIterator iterator()(Code) | | 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()
an iterator that walks from the root of the term to theposition this PosInOccurrence-object points to |
| replaceConstrainedFormula | | public PosInOccurrence replaceConstrainedFormula(ConstrainedFormula p_newFormula)(Code) | | Replace the formula this object points to with the new formula given
Parameters:
p_newFormula - the new formula a PosInOccurrence object that points to the sameposition within the formula p_newFormula as thisobject does within the formula constrainedFormula().It is not tested whether this position exists within p_newFormula |
| setTermBelowMetavariable | | public PosInOccurrence setTermBelowMetavariable(Term p_metaTerm)(Code) | | If "this" points to a metavariable, a term can be inserted at
this position, allowing to walk down the term further "inside"
the metavariable.
|
| subTerm | | public Term subTerm()(Code) | | returns the subterm this object points to
|
| topLevel | | public PosInOccurrence topLevel()(Code) | | Ascend to the top node of the formula this object points to
|
|
|