| java.lang.Object
 de.uka.ilkd.key.logic.BoundVariableTools
| BoundVariableTools | | public class BoundVariableTools (Code) | | Some generally useful tools for dealing with arrays of bound variables
|
| Method Summary | |
| public boolean | consistentVariableArrays(ArrayOfQuantifiableVariable ar0, ArrayOfQuantifiableVariable ar1)
| | public boolean | equalsModRenaming(ArrayOfQuantifiableVariable vars0, Term term0, ArrayOfQuantifiableVariable vars1, Term term1)
| | public Term | renameVariables(Term originalTerm, ArrayOfQuantifiableVariable oldBoundVars, ArrayOfQuantifiableVariable newBoundVars)
| | public Term[] | renameVariables(Term[] originalTerms, ArrayOfQuantifiableVariable oldBoundVars, ArrayOfQuantifiableVariable newBoundVars)
| | public boolean | resolveCollisions(ArrayOfQuantifiableVariable oldVars, QuantifiableVariable[] newVars, SetOfQuantifiableVariable criticalVars)
Replace all variables of oldVars that also turn up in
criticalPairs with new variables (currently just with the
same name). | | public Term | resolveCollisions(Term t, SetOfQuantifiableVariable criticalVars)
| | public boolean | resolveCollisions(Term originalTerm, SetOfQuantifiableVariable criticalVars, ArrayOfQuantifiableVariable[] newBoundVars, Term[] newSubs)
Ensure that none of the variables criticalVars is bound by
the top-level operator of t (by bound renaming). | | public ArrayOfQuantifiableVariable | unifyBoundVariables(ArrayOfQuantifiableVariable[] boundVarsPerSub, Term[] subs, int subtermsBegin, int subtermsEnd)
Ensure that for the subterms with indexes [subtermsBegin,
subtermsEnd) the same variables are bound. |
| consistentVariableArrays | | public boolean consistentVariableArrays(ArrayOfQuantifiableVariable ar0, ArrayOfQuantifiableVariable ar1)(Code) | | true iff the two given arrays have the same sizeand the contained variables have the same sorts |
| equalsModRenaming | | public boolean equalsModRenaming(ArrayOfQuantifiableVariable vars0, Term term0, ArrayOfQuantifiableVariable vars1, Term term1)(Code) | | true iff the two arrays of variables arecompatible (compatibleVariableArrays()) and thetwo given terms are equal modulo renaming after unification ofthe two arrays (of variables occurring free in the terms) |
| renameVariables | | public Term renameVariables(Term originalTerm, ArrayOfQuantifiableVariable oldBoundVars, ArrayOfQuantifiableVariable newBoundVars)(Code) | | Compare the arrays oldBoundVars and
newBoundVars component-wise, and in case of differences
substitute variables from the former array with the ones of the latter
array (in originalTerm)
|
| renameVariables | | public Term[] renameVariables(Term[] originalTerms, ArrayOfQuantifiableVariable oldBoundVars, ArrayOfQuantifiableVariable newBoundVars)(Code) | | |
| resolveCollisions | | public boolean resolveCollisions(ArrayOfQuantifiableVariable oldVars, QuantifiableVariable[] newVars, SetOfQuantifiableVariable criticalVars)(Code) | | Replace all variables of oldVars that also turn up in
criticalPairs with new variables (currently just with the
same name).
Parameters:
oldVars - variables to be checked
Parameters:
newVars - array in which either the original variables (if a variable isnot an element of criticalVars) or newlycreated variables are stored
Parameters:
criticalVars - variables that must not turn up in the resulting arraynewVars true iff it was necessary to create at least onenew variable |
| resolveCollisions | | public Term resolveCollisions(Term t, SetOfQuantifiableVariable criticalVars)(Code) | | Ensure that none of the variables criticalVars is bound by
the top-level operator of t (by bound renaming)
|
| resolveCollisions | | public boolean resolveCollisions(Term originalTerm, SetOfQuantifiableVariable criticalVars, ArrayOfQuantifiableVariable[] newBoundVars, Term[] newSubs)(Code) | | Ensure that none of the variables criticalVars is bound by
the top-level operator of t (by bound renaming). The
resulting subterms and arrays of bound variables are stored in
newSubs and newBoundVars (resp.)
true if it was necessary to rename a variable,i.e. to changed anything in the term originalTerm |
| unifyBoundVariables | | public ArrayOfQuantifiableVariable unifyBoundVariables(ArrayOfQuantifiableVariable[] boundVarsPerSub, Term[] subs, int subtermsBegin, int subtermsEnd)(Code) | | Ensure that for the subterms with indexes [subtermsBegin,
subtermsEnd) the same variables are bound. In case of
differences bound renaming is applied (existing variables are renamed to
new ones)
Parameters:
boundVarsPerSub - bound variables per subterms
Parameters:
subs - subterms (in which variables are renamed if necessary)
Parameters:
subtermsBegin - first subterm that is supposed to be considered
Parameters:
subtermsEnd - subterm after the last subterm to be considerPRE: subtermsEnd > subtermsBegin |
|
|