| java.lang.Object
 de.uka.ilkd.key.logic.op.TermSymbol
de.uka.ilkd.key.logic.op.Function
de.uka.ilkd.key.logic.op.NonRigidFunction
de.uka.ilkd.key.logic.op.NRFunctionWithExplicitDependencies
| NRFunctionWithExplicitDependencies | | public class NRFunctionWithExplicitDependencies extends NonRigidFunction (Code) | | Non Rigid Fucntion with explicit dependencies. This means a list of
location of whose and only whose value the interpretation of the
function symbol depends.
(May be generalized to more than locations in future)
The list of dependencies may be partitioned into several lists.
|
| Method Summary | |
| public String | classifier()
| | public ArrayOfLocation | dependencies()
| | public ArrayOfLocation | getDependencies(int i)
| | public int | getNumPartitions()
| | public static NRFunctionWithExplicitDependencies | getSymbol(Name name, ArrayOfLocation dependencies)
| | public static NRFunctionWithExplicitDependencies | getSymbol(Name name, Sort sort, Sort[] argSorts, Location[] dependencies)
| | public static NRFunctionWithExplicitDependencies | getSymbol(Name name, Sort sort, ArrayOfSort argSorts, List depList)
| | public static NRFunctionWithExplicitDependencies | getSymbol(Name name, Sort sort, ArrayOfSort argSorts, ArrayOfLocation dependencies)
| | public MatchConditions | match(SVSubstitute subst, MatchConditions mc, Services services)
| | public String | toString()
|
| DEPENDENCY_ELEMENT_SEPARATOR | | final public static char DEPENDENCY_ELEMENT_SEPARATOR(Code) | | |
| DEPENDENCY_LIST_END | | final public static char DEPENDENCY_LIST_END(Code) | | |
| DEPENDENCY_LIST_SEPARATOR | | final public static char DEPENDENCY_LIST_SEPARATOR(Code) | | |
| DEPENDENCY_LIST_STARTER | | final public static char DEPENDENCY_LIST_STARTER(Code) | | |
| dependencies | | public ArrayOfLocation dependencies()(Code) | | returns an array of all locations this function depends on
the array of locations this function depends on |
| getDependencies | | public ArrayOfLocation getDependencies(int i)(Code) | | returns the i-th partition of the locations this function depends on
|
| getNumPartitions | | public int getNumPartitions()(Code) | | |
| getSymbol | | public static NRFunctionWithExplicitDependencies getSymbol(Name name, ArrayOfLocation dependencies)(Code) | | retrieves the non-rigid function with the given name and dependencies
or returns null if no such function symbol exists
Parameters:
name - the Name of the function symbol to look for
Parameters:
dependencies - the ArrayOfLocation with the dependencies the non-rigid function symbol |
| getSymbol | | public static NRFunctionWithExplicitDependencies getSymbol(Name name, Sort sort, Sort[] argSorts, Location[] dependencies)(Code) | | retrieves the non-rigid function with the given name and dependencies
and creates one if not available
Parameters:
name - the Name of the function symbol to look for
Parameters:
sort - the Sort of the function symbol
Parameters:
argSorts - the array of Sorts for the arguments
Parameters:
dependencies - the array of Locations describing the dependencies the non-rigid function symbol |
| getSymbol | | public static NRFunctionWithExplicitDependencies getSymbol(Name name, Sort sort, ArrayOfSort argSorts, List depList)(Code) | | retrieves the non-rigid function with the given name and dependencies
and creates one if not available
Parameters:
name - the Name of the function symbol to look for
Parameters:
sort - the Sort of the function symbol
Parameters:
argSorts - the ArrayOfSort for the arguments
Parameters:
depList - partitioned dependencies as a list of ArrayOfLocation the non-rigid function symbol |
| getSymbol | | public static NRFunctionWithExplicitDependencies getSymbol(Name name, Sort sort, ArrayOfSort argSorts, ArrayOfLocation dependencies)(Code) | | retrieves the non-rigid function with the given name and dependencies
and creates one if not available
Parameters:
name - the Name of the function symbol to look for
Parameters:
sort - the Sort of the function symbol
Parameters:
argSorts - the ArrayOfSort for the arguments
Parameters:
dependencies - the ArrayOfLocation with the dependencies the non-rigid function symbol |
|
|