public class WaryClashFreeSubst extends ClashFreeSubst
ClashFreeSubst.VariableCollectVisitor
Modifier and Type | Field and Description |
---|---|
private boolean |
createQuantifier
the formula should be prepended with a quantifier
|
private int |
depth
depth of recursion of the
apply method |
private QuantifiableVariable |
newVar
variable with which the original variable should be
substituted below modalities
|
private Term |
newVarTerm |
private ImmutableSet<QuantifiableVariable> |
warysvars
variables occurring within the original term and within the
term to be substituted
|
s, svars, tb, v
Constructor and Description |
---|
WaryClashFreeSubst(QuantifiableVariable v,
Term s,
TermBuilder tb) |
Modifier and Type | Method and Description |
---|---|
private Term |
addWarySubst(Term t)
Prepend the given term with a wary substitution (substituting
newVar with getSubstitutedTerm() ) |
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 Term |
applyBelowModality(Term t)
Apply the substitution to a term/formula below a modality or update
|
private Term |
applyBelowTransformer(Term t)
Apply the substitution to a term/formula below a transformer procedure
|
private Term |
applyOnModality(Term t)
Apply the substitution (that replaces a variable with a
non-rigid term) on t, which has a modality as top-level
operator.
|
private Term |
applyOnTransformer(Term t)
Apply the substitution (that replaces a variable with a
term) on t, which has a transformer procedure as top-level
operator.
|
private Term |
applyOnUpdate(Term t)
Apply the substitution (that replaces a variable with a
non-rigid term) on t, which has an update operator as top-level
operator.
|
private void |
createVariable()
Create a new logic variable to be used for substitutions below
modalities
|
private void |
findUsedVariables(Term t)
Determine a set of variables that do already appear within
t or the substituted term, and whose names should
not be used for free variables |
private Term |
substWithNewVar(Term t)
Rename the original variable to be substituted to
newVar |
applyOnSubterm, getSingleArray, getSubstitutedTerm, getVariable, newVarFor, subTermChanges
private int depth
apply
methodprivate boolean createQuantifier
private QuantifiableVariable newVar
private Term newVarTerm
private ImmutableSet<QuantifiableVariable> warysvars
public WaryClashFreeSubst(QuantifiableVariable v, Term s, TermBuilder tb)
public Term apply(Term t)
s
for v
in t
,
avoiding collisions by replacing bound variables in
t
if necessary.apply
in class ClashFreeSubst
private void findUsedVariables(Term t)
t
or the substituted term, and whose names should
not be used for free variablesprivate void createVariable()
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
.apply1
in class ClashFreeSubst
private Term applyOnModality(Term t)
apply1
for substitutions with non-rigid terms
PRECONDITION: warysvars != null
private Term applyOnTransformer(Term t)
apply1
for substitutions with non-rigid terms
PRECONDITION: warysvars != null
private Term applyOnUpdate(Term t)
apply1
for substitutions with non-rigid terms
PRECONDITION: warysvars != null
private Term applyBelowModality(Term t)
private Term applyBelowTransformer(Term t)
private Term addWarySubst(Term t)
newVar
with getSubstitutedTerm()
)