| de.uka.ilkd.key.logic.op.Operator
All known Subclasses: de.uka.ilkd.key.logic.op.TermSymbol, de.uka.ilkd.key.logic.op.AccessOp, de.uka.ilkd.key.logic.op.Op,
| Operator | | public interface Operator extends Named,SVSubstitute(Code) | | All symbols acting as members of a term e.g. logical operators, predicates,
functions, variables etc. have to implement this interface.
|
| Method Summary | |
| int | arity()
| | boolean | isRigid(Term term)
| | MatchConditions | match(SVSubstitute subst, MatchConditions mc, Services services)
tests if this operator (plays role of a template) matches
the given operator with respect to the given match
conditions. | | Name | name()
| | Sort | sort(Term[] term)
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. | | boolean | validTopLevel(Term term)
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. |
| arity | | int arity()(Code) | | the arity of this operator
arity of the Operator as int |
| isRigid | | boolean isRigid(Term term)(Code) | | true if the value of "term" having this operator astop-level operator and may not be changed by modalities |
| match | | MatchConditions match(SVSubstitute subst, MatchConditions mc, Services services)(Code) | | tests if this operator (plays role of a template) matches
the given operator with respect to the given match
conditions.
If matching fails null is returned.
Parameters:
subst - the Operator to match
Parameters:
mc - the MatchConditions to pay respect to
Parameters:
services - the Services to access model information the resulting match conditions (e.g. with new addedinstantiations of schema variables) |
| name | | Name name()(Code) | | returns the name of the operator
name of the operator |
| sort | | 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 |
| validTopLevel | | 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 Term is valid. |
|
|