|
| |
|
| java.lang.Object
 de.uka.ilkd.key.logic.op.Op
de.uka.ilkd.key.logic.op.AccessOp
de.uka.ilkd.key.logic.op.ArrayOp
All known Subclasses: de.uka.ilkd.key.logic.op.ShadowArrayOp,
| sort | | final protected Sort sort(Code) | | Sort of the array this operator addresses
|
| arity | | public int arity()(Code) | | the arity of an array access operator is 2 where the
first sub term denotes the array object itself and the second one
the accessed index
arity of the Operator as int |
| arraySort | | public Sort arraySort()(Code) | | the array sort on which this operator is applied |
| arraySortAliased | | protected boolean arraySortAliased(Sort as1, Sort as2)(Code) | | |
| getArrayOp | | public static ArrayOp getArrayOp(Sort arraySort)(Code) | | returns and if neccessary creates the shadowed array access operator for
the given array sort
Parameters:
arraySort - the Sort to which this operator is applicablemust be of kind ArraySort or ProgramSVSort the array access operator for the given array sort |
| getSortDependingOn | | public Sort getSortDependingOn()(Code) | | |
| index | | public Term index(Term t)(Code) | | the top level operator of t must be this
returns the index of this array access for the given term
|
| isShadowed | | public boolean isShadowed()(Code) | | true if the operator is a shadowed |
| referencePrefix | | public Term referencePrefix(Term t)(Code) | | the top level operator of t must be this
returns the reference prefix of this array access for the given term
|
| sort | | public Sort sort(Term[] term)(Code) | | determines the sort of the
Term if it would be created using this
Operator as top level operator and the given terms as sub terms. The
assumption that the constructed term would be allowed is not checked.
Parameters:
term - an array of Term containing the subterms of a (potential)term with this operator as top level operator sort of the term with this operator as top level operator of thegiven substerms |
| sort | | public Sort sort()(Code) | | the sort of this operator |
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | checks whether the top level structure of the given @link Term
is syntactically valid, given the assumption that the top level
operator of the term is the same as this Operator. The
assumption that the top level operator and the term are equal
is NOT checked.
true iff the top level structure ofthe @link Term is valid. |
|
|
|