public class ClashFreeSubst
extends java.lang.Object
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.
|
Modifier and Type | Field and Description |
---|---|
protected Term |
s |
protected ImmutableSet<QuantifiableVariable> |
svars |
protected TermBuilder |
tb |
protected QuantifiableVariable |
v |
Constructor and Description |
---|
ClashFreeSubst(QuantifiableVariable v,
Term s,
TermBuilder tb) |
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. |
protected void |
applyOnSubterm(Term completeTerm,
int subtermIndex,
Term[] newSubterms,
ImmutableArray<QuantifiableVariable>[] newBoundVars)
Apply the substitution of the subterm
subtermIndex of
term/formula completeTerm . |
protected static ImmutableArray<QuantifiableVariable> |
getSingleArray(ImmutableArray<QuantifiableVariable>[] bv) |
protected Term |
getSubstitutedTerm() |
protected QuantifiableVariable |
getVariable() |
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. |
protected QuantifiableVariable v
protected Term s
protected ImmutableSet<QuantifiableVariable> svars
protected final TermBuilder tb
public ClashFreeSubst(QuantifiableVariable v, Term s, TermBuilder tb)
protected QuantifiableVariable getVariable()
protected Term getSubstitutedTerm()
public Term apply(Term t)
s
for v
in t
,
avoiding collisions by replacing bound variables in
t
if necessary.protected Term apply1(Term t)
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
.protected static ImmutableArray<QuantifiableVariable> getSingleArray(ImmutableArray<QuantifiableVariable>[] bv)
protected void applyOnSubterm(Term completeTerm, int subtermIndex, Term[] newSubterms, ImmutableArray<QuantifiableVariable>[] newBoundVars)
subtermIndex
of
term/formula completeTerm
. The result is stored in
newSubterms
and newBoundVars
(at index
subtermIndex
)protected boolean subTermChanges(ImmutableArray<QuantifiableVariable> boundVars, Term subTerm)
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
.protected QuantifiableVariable newVarFor(QuantifiableVariable var, ImmutableSet<QuantifiableVariable> usedVars)
var
, that is different from any of the names of
variables in usedVars
.
Assumes that var
is a @link{LogicVariable}.
Copyright © 2003-2019 The KeY-Project.