| java.lang.Object
 de.uka.ilkd.key.logic.op.TermSymbol
de.uka.ilkd.key.logic.op.Function
de.uka.ilkd.key.logic.op.RigidFunction
de.uka.ilkd.key.logic.op.SortDependingFunction
All known Subclasses: de.uka.ilkd.key.logic.op.ExactInstanceSymbol, de.uka.ilkd.key.logic.op.InstanceofSymbol, de.uka.ilkd.key.logic.op.CastFunctionSymbol,
| SortDependingFunction | | public class SortDependingFunction extends RigidFunction implements SortDependingSymbol(Code) | | A sort depending function is a function symbol.
The following invariant has to hold:
given two sort depending functions f1 and f2 then
from f1.isSimilar(f2) and f1.getSortDependingOn() == f2.getSortDependingOn()
follows f1 == f2
|
| SortDependingFunction | | public SortDependingFunction(Name name, Sort sort, Sort[] argSorts, Name kind, Sort sortDependingOn)(Code) | | creates a Function
Parameters:
name - String with name of the function
Parameters:
sort - the Sort of the function (result type)
Parameters:
kind - name of the kind this object belongs to
Parameters:
sortDependingOn - sort this object is depending on, thisis the difference between various objects of the same kind |
| SortDependingFunction | | public SortDependingFunction(Name name, Sort sort, ArrayOfSort argSorts, Name kind, Sort sortDependingOn)(Code) | | |
| getInstanceFor | | public SortDependingSymbol getInstanceFor(SortDefiningSymbols p_sort)(Code) | | Get the instance of this term symbol defined by the given sort
"p_sort"
a term symbol similar to this one, or null if thissymbol is not defined by "p_sort"POSTCONDITION: result==null || (this.isSimilar(result) &&result.getSortDependingOn()==p_sort) |
| getKind | | public Name getKind()(Code) | | Assign a name to this term symbol, independant of concrete
instantiations for different sorts
the kind of term symbol this object is an instantiationfor |
| getSortDependingOn | | public Sort getSortDependingOn()(Code) | | the sort this object has been instantiated for |
| isSimilar | | public boolean isSimilar(SortDependingSymbol p)(Code) | | Compares "this" and "p"
Parameters:
p - object to compare true iff this and p are instances of the same kind ofsymbol, but possibly instantiated for different sorts |
| match | | public MatchConditions match(SVSubstitute subst, MatchConditions mc, Services services)(Code) | | Taking this sortdepending function as template to be matched against op,
the necessary conditions are returned or null if not unifiable (matchable).
A sortdepending function is matched successfull against another sortdepending function
if the sorts can be matched and they are of same kind.
|
|
|