de.uka.ilkd.key.logic

Class WaryClashFreeSubst

java.lang.Object

de.uka.ilkd.key.logic.ClashFreeSubst

de.uka.ilkd.key.logic.WaryClashFreeSubst

public class WaryClashFreeSubst
extends ClashFreeSubst

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.logic.ClashFreeSubst

ClashFreeSubst.VariableCollectVisitor

Field Summary

Fields

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

Fields inherited from class de.uka.ilkd.key.logic.ClashFreeSubst

s, svars, tb, v

Constructor Summary

Constructors

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

Method Summary

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

Methods inherited from class de.uka.ilkd.key.logic.ClashFreeSubst

applyOnSubterm, getSingleArray, getSubstitutedTerm, getVariable, newVarFor, subTermChanges

Methods inherited from class java.lang.Object

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

Field Detail

depth

private int depth

depth of recursion of the apply method

createQuantifier

private boolean createQuantifier

the formula should be prepended with a quantifier

newVar

private QuantifiableVariable newVar

variable with which the original variable should be substituted below modalities

newVarTerm

private Term newVarTerm

warysvars

private ImmutableSet<QuantifiableVariable> warysvars

variables occurring within the original term and within the term to be substituted

Constructor Detail

WaryClashFreeSubst

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

Method Detail

apply

public Term apply(Term t)

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

Overrides:

apply in class ClashFreeSubst

findUsedVariables

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

createVariable

private void createVariable()

Create a new logic variable to be used for substitutions below modalities

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.

Overrides:

apply1 in class ClashFreeSubst

applyOnModality

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. This is done by creating a (top-level) existential quantifier. This method is only called from apply1 for substitutions with non-rigid terms PRECONDITION: warysvars != null

applyOnTransformer

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. This is done by creating a (top-level) existential quantifier. This method is only called from apply1 for substitutions with non-rigid terms PRECONDITION: warysvars != null

applyOnUpdate

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. This is done by creating a (top-level) existential quantifier. This method is only called from apply1 for substitutions with non-rigid terms PRECONDITION: warysvars != null

applyBelowModality

private Term applyBelowModality(Term t)

Apply the substitution to a term/formula below a modality or update

applyBelowTransformer

private Term applyBelowTransformer(Term t)

Apply the substitution to a term/formula below a transformer procedure

addWarySubst

private Term addWarySubst(Term t)

Prepend the given term with a wary substitution (substituting newVar with getSubstitutedTerm())

substWithNewVar

private Term substWithNewVar(Term t)

Rename the original variable to be substituted to newVar