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. |
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. |
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)
private Term applyOnSubterms(Term t)
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.
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
)private void applyOnSubterm(int varInd, ImmutableArray<QuantifiableVariable> boundVars, QuantifiableVariable[] newBoundVars, int subInd, Term subTerm, Term[] newSubterms)
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..
private void applyOnSubterm1(int varInd, ImmutableArray<QuantifiableVariable> boundVars, QuantifiableVariable[] newBoundVars, int subInd, Term subTerm, Term[] newSubterms)
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}.
private boolean nameNewInSet(java.lang.String n, ImmutableSet<QuantifiableVariable> qvars)
n
in the
set s