| java.lang.Object
 de.uka.ilkd.key.logic.ClashFreeSubst
All known Subclasses: de.uka.ilkd.key.logic.WaryClashFreeSubst,
| ClashFreeSubst | | public class ClashFreeSubst (Code) | | |
| Inner Class :protected static class VariableCollectVisitor extends Visitor | |
| Method Summary | |
| public Term | apply(Term t)
substitute s for v in t,
avoiding collisions by replacing bound variables in
t if necessary. | | protected Term | apply1(Term t)
substitute s for v in
t, avoiding collisions by replacing bound
variables in t if necessary. | | protected void | applyOnSubterm(Term completeTerm, int subtermIndex, Term[] newSubterms, ArrayOfQuantifiableVariable[] newBoundVars)
Apply the substitution of the subterm subtermIndex of
term/formula completeTerm. | | protected Term | getSubstitutedTerm()
| | protected QuantifiableVariable | getVariable()
| | protected QuantifiableVariable | newVarFor(QuantifiableVariable var, SetOfQuantifiableVariable usedVars)
returns a new variable that has a name derived from that of
var, that is different from any of the names of
variables in usedVars. | | protected boolean | subTermChanges(ArrayOfQuantifiableVariable boundVars, Term subTerm)
returns true if subTerm bound by
boundVars would change under application of this
substitution. |
| svars | | SetOfQuantifiableVariable svars(Code) | | |
| apply | | public Term apply(Term t)(Code) | | substitute s for v in t,
avoiding collisions by replacing bound variables in
t if necessary.
|
| apply1 | | protected Term apply1(Term t)(Code) | | substitute s for v in
t, avoiding collisions by replacing bound
variables in t if necessary. It is
assumed, that t contains a free occurrence of
v.
|
| applyOnSubterm | | protected void applyOnSubterm(Term completeTerm, int subtermIndex, Term[] newSubterms, ArrayOfQuantifiableVariable[] newBoundVars)(Code) | | Apply the substitution of the subterm subtermIndex of
term/formula completeTerm. The result is stored in
newSubterms and newBoundVars (at index
subtermIndex)
|
| getSubstitutedTerm | | protected Term getSubstitutedTerm()(Code) | | |
| newVarFor | | protected QuantifiableVariable newVarFor(QuantifiableVariable var, SetOfQuantifiableVariable usedVars)(Code) | | returns a new variable that has a name derived from that of
var, that is different from any of the names of
variables in usedVars.
Assumes that var is a @link{LogicVariable}.
|
| subTermChanges | | protected boolean subTermChanges(ArrayOfQuantifiableVariable boundVars, Term subTerm)(Code) | | returns true if subTerm bound by
boundVars would change under application of this
substitution. This is the case, if v occurrs free
in subTerm, but does not occurr in boundVars.
|
|
|