de.uka.ilkd.key.logic

Class ClashFreeSubst

java.lang.Object

de.uka.ilkd.key.logic.ClashFreeSubst

Direct Known Subclasses:

WaryClashFreeSubst

public class ClashFreeSubst
extends java.lang.Object

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	ClashFreeSubst.VariableCollectVisitor A Visitor class to collect all (not just the free) variables occurring in a term.

Field Summary

Fields

Modifier and Type	Field and Description
protected Term	s
protected ImmutableSet<QuantifiableVariable>	svars
protected TermBuilder	tb
protected QuantifiableVariable	v

Constructor Summary

Constructors

Constructor and Description
ClashFreeSubst(QuantifiableVariable v, Term s, TermBuilder tb)

Method Summary

Modifier and Type	Method and Description
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.
private void	applyOnSubterm(int varInd, ImmutableArray<QuantifiableVariable> boundVars, QuantifiableVariable[] newBoundVars, int subInd, Term subTerm, Term[] newSubterms) Perform the substitution on subTerm bound by the variables in boundVars, starting with the variable at index varInd.
protected void	applyOnSubterm(Term completeTerm, int subtermIndex, Term[] newSubterms, ImmutableArray<QuantifiableVariable>[] newBoundVars) Apply the substitution of the subterm subtermIndex of term/formula completeTerm.
private void	applyOnSubterm1(int varInd, ImmutableArray<QuantifiableVariable> boundVars, QuantifiableVariable[] newBoundVars, int subInd, Term subTerm, Term[] newSubterms) Same as applyOnSubterm, but v doesn't have to occurr free in the considered quantified subterm.
private Term	applyOnSubterms(Term t) substitute s for v in every subterm of t, and build a new term.
protected static ImmutableArray<QuantifiableVariable>	getSingleArray(ImmutableArray<QuantifiableVariable>[] bv)
protected Term	getSubstitutedTerm()
protected QuantifiableVariable	getVariable()
private boolean	nameNewInSet(java.lang.String n, ImmutableSet<QuantifiableVariable> qvars) returns true if there is no object named n in the set s
protected QuantifiableVariable	newVarFor(QuantifiableVariable var, ImmutableSet<QuantifiableVariable> 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(ImmutableArray<QuantifiableVariable> boundVars, Term subTerm) returns true if subTerm bound by boundVars would change under application of this substitution.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

v

protected QuantifiableVariable v

s

protected Term s

svars

protected ImmutableSet<QuantifiableVariable> svars

tb

protected final TermBuilder tb

Constructor Detail

ClashFreeSubst

public ClashFreeSubst(QuantifiableVariable v,
                      Term s,
                      TermBuilder tb)

Method Detail

getVariable

protected QuantifiableVariable getVariable()

getSubstitutedTerm

protected Term getSubstitutedTerm()

apply

public Term apply(Term t)

substitute s for v in t, avoiding collisions by replacing bound variables in t if necessary.

apply1

protected Term apply1(Term t)

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.

getSingleArray

protected static ImmutableArray<QuantifiableVariable> getSingleArray(ImmutableArray<QuantifiableVariable>[] bv)

applyOnSubterms

private Term applyOnSubterms(Term t)

substitute s for v in every subterm of t, and build a new term. It is assumed, that one of the subterms contains a free occurrence of v, and that the case v==t is already handled.

applyOnSubterm

protected void applyOnSubterm(Term completeTerm,
                              int subtermIndex,
                              Term[] newSubterms,
                              ImmutableArray<QuantifiableVariable>[] newBoundVars)

Apply the substitution of the subterm subtermIndex of term/formula completeTerm. The result is stored in newSubterms and newBoundVars (at index subtermIndex)

applyOnSubterm

private void applyOnSubterm(int varInd,
                            ImmutableArray<QuantifiableVariable> boundVars,
                            QuantifiableVariable[] newBoundVars,
                            int subInd,
                            Term subTerm,
                            Term[] newSubterms)

Perform the substitution on subTerm bound by the variables in boundVars, starting with the variable at index varInd. Put the resulting bound variables (which might be new) into newBoundVars, starting from position varInd, and the resulting subTerm into newSubterms[subInd].

It is assumed that v occurrs free in in this quantified subterm, i.e. it occurrs free in subTerm, but does not occurr in boundVars from varInd upwards..

applyOnSubterm1

private void applyOnSubterm1(int varInd,
                             ImmutableArray<QuantifiableVariable> boundVars,
                             QuantifiableVariable[] newBoundVars,
                             int subInd,
                             Term subTerm,
                             Term[] newSubterms)

Same as applyOnSubterm, but v doesn't have to occurr free in the considered quantified subterm. It is however assumed that no more clash can occurr.

subTermChanges

protected boolean subTermChanges(ImmutableArray<QuantifiableVariable> boundVars,
                                 Term subTerm)

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.

newVarFor

protected QuantifiableVariable newVarFor(QuantifiableVariable var,
                                         ImmutableSet<QuantifiableVariable> 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.

Assumes that var is a @link{LogicVariable}.

nameNewInSet

private boolean nameNewInSet(java.lang.String n,
                             ImmutableSet<QuantifiableVariable> qvars)

returns true if there is no object named n in the set s