| java.lang.Object
 de.uka.ilkd.key.logic.op.TermSymbol
de.uka.ilkd.key.logic.op.SchemaVariableAdapter
All known Subclasses: de.uka.ilkd.key.logic.op.SortedSchemaVariable, de.uka.ilkd.key.logic.op.OperatorSV, de.uka.ilkd.key.logic.op.NameSV, de.uka.ilkd.key.logic.op.ListSV,
| SchemaVariableAdapter | | abstract public class SchemaVariableAdapter extends TermSymbol implements SchemaVariable(Code) | | This class represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms. Schema variables
are used in Taclets where they act as placeholders for other
TermSymbols. The TermSymbols a SchemaVariable is allowed to match
is specified by their type and sort. If a match fits these
conditions can be checked using the method isCompatible(TermSymbol t)
|
| SchemaVariableAdapter | | protected SchemaVariableAdapter(Name name, Class matchType, Sort sort, boolean listSV)(Code) | | creates a new SchemaVariable. That is used as placeholder for
TermSymbols of a certain type.
Parameters:
name - the Name of the SchemaVariable
Parameters:
matchType - Class representing the type of symbols thatcan be matched
Parameters:
sort - the Sort of the SchemaVariable and the matched type
Parameters:
listSV - a boolean which is true iff the schemavariable is allowedto match a list of syntactical elements |
| SchemaVariableAdapter | | protected SchemaVariableAdapter(Name name, Class matchType)(Code) | | |
| arity | | public int arity()(Code) | | arity of the Variable as int |
| isFormulaSV | | public boolean isFormulaSV()(Code) | | returns true iff this SchemaVariable is used to match
a formula
true iff this SchemaVariable is used to matcha formula |
| isListSV | | public boolean isListSV()(Code) | | returns true if the schemavariable can match a list of syntactical
elements
true if the schemavariable can match a list of syntacticalelements |
| isNameSV | | public boolean isNameSV()(Code) | | |
| isOperatorSV | | public boolean isOperatorSV()(Code) | | true iff this SchemaVariable is used to matchmodal operators |
| isProgramSV | | public boolean isProgramSV()(Code) | | returns true iff this SchemaVariable is used to match
a part of a program
true iff this SchemaVariable is used to matcha part of a program |
| isRigid | | public boolean isRigid(Term term)(Code) | | true if the value of "term" having this operator astop-level operator and may not be changed by modalities |
| isRigid | | public boolean isRigid()(Code) | | |
| isSkolemTermSV | | public boolean isSkolemTermSV()(Code) | | returns true iff this SchemaVariable is used to match (create)
a skolem term
true iff this SchemaVariable is used to match (create)a skolem term |
| isStrict | | public boolean isStrict()(Code) | | true if the schemavariable has the strict modifier which forces the instantiation to have exact the same sortas the schemavariable (or if the sv is of generic sort - the instantiation of the generic sort) |
| isTermSV | | public boolean isTermSV()(Code) | | returns true iff this SchemaVariable is used to match
a term but not a formula
true iff this SchemaVariable is used to matcha term but not a formula |
| isVariableSV | | public boolean isVariableSV()(Code) | | returns true iff this SchemaVariable is used to match
bound (quantifiable) variables
true iff this SchemaVariable is used to matchbound (quantifiable) variables |
|
|