| java.lang.Object
 de.uka.ilkd.key.logic.op.Op
de.uka.ilkd.key.logic.op.Equality
| Equality | | public class Equality extends Op (Code) | | This class represents an equality symbol for a given sort.
The system will generate automatically for each sort exactly one
equality symbol. For the special sort Formula the corresponding equality
symbol is the equivalence-junctor
Op.EQV .
|
| Constructor Summary | |
| | Equality(Name name)
generates a new equality symbol for the given target sort.
Don't call this, but
Sort.getEqualitySymbol . | | | Equality(Name name, Sort targetSort)
generates a new equality symbol for the given target sort and a
given name. |
| Method Summary | |
| public Sort | argSort(int i)
| | public int | arity()
| | public Sort | sort(Term[] term)
| | public boolean | validTopLevel(Term term)
checks if the given term is syntactically valid at its top
level assumed the top level operator were this, i.e. |
| Equality | | Equality(Name name)(Code) | | generates a new equality symbol for the given target sort.
Don't call this, but
Sort.getEqualitySymbol . In case of
schemavariables without sort on both sides (e.g. two program SVs)
Parameters:
targetSort - - sort for which the equality symbol is generated. |
| Equality | | Equality(Name name, Sort targetSort)(Code) | | generates a new equality symbol for the given target sort and a
given name.
Don't call this, but use
Op.EQV or
Op.EQUALS .
Parameters:
targetSort - - sort for which the equality symbol is generated.
Parameters:
name - - name for the equality symbol |
| argSort | | public Sort argSort(int i)(Code) | | returns the sort of the i-th argument
|
| arity | | public int arity()(Code) | | arity of the Equality as int that is 2 |
| sort | | public Sort sort(Term[] term)(Code) | | Sort of the term consisting of the given subterms if it wouldhave this operator as top level operator |
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | checks if the given term is syntactically valid at its top
level assumed the top level operator were this, i.e. if the
direct subterms can be subterms of a term with this top level
operator, the method returns true. Furthermore, it is checked
that no variables are bound for none of the subterms.
If a subterm is a schemavariable, the whole term is accepted.
Parameters:
term - the Term to be checked. true iff the given term hassubterms that are suitable for this function. |
|
|