| java.lang.Object de.uka.ilkd.key.logic.op.TermSymbol de.uka.ilkd.key.logic.op.SchemaVariableAdapter de.uka.ilkd.key.logic.op.OperatorSV
All known Subclasses: de.uka.ilkd.key.logic.op.ModalOperatorSV,
OperatorSV | public class OperatorSV extends SchemaVariableAdapter (Code) | | Creates an operator schemavariable that matches a given set of operators.
All operators to be matched must have the same arity like this
schema variable.
|
OperatorSV | OperatorSV(Name name, Sort sort, int arity, HashSet set)(Code) | | creates an instance of this schemavariable kind that can match any
operator occuring in the set as long as the arities are the same
Parameters: name - the Name of the schema variable Parameters: sort - the Sort the schema variable shall have Parameters: arity - the int with the arity Parameters: set - the set of operators to be matched by this schemavariable kind |
OperatorSV | protected OperatorSV(Name name, Class matchingType, Sort sort, int arity, HashSet set)(Code) | | creates an instance of this schemavariable kind that can match any
operator occuring in the set as long as the arities are the same as long
as it is an instance of the given matching type
Parameters: name - the Name of the schema variable Parameters: matchingType - the Class whose instances (including subtypes) can be matched Parameters: sort - the Sort the schema variable shall have Parameters: arity - the int with the arity Parameters: set - the set of operators to be matched by this schemavariable kind |
arity | public int arity()(Code) | | returns the arity of this operator
|
isOperatorSV | public boolean isOperatorSV()(Code) | | returns true if the schemavariable is an operator sv
|
operators | public Set operators()(Code) | | returns an unmodifiacle set of operators this schemavariable can match
|
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 Term is valid. |
|
|