de.uka.ilkd.key.logic

Class BoundVariableTools

java.lang.Object

de.uka.ilkd.key.logic.BoundVariableTools

public class BoundVariableTools
extends java.lang.Object

Some generally useful tools for dealing with arrays of bound variables

Field Summary

Fields

Modifier and Type	Field and Description
static BoundVariableTools	DEFAULT

Constructor Summary

Constructors

Modifier	Constructor and Description
private	BoundVariableTools()

Method Summary

Modifier and Type	Method and Description
boolean	consistentVariableArrays(ImmutableArray<QuantifiableVariable> ar0, ImmutableArray<QuantifiableVariable> ar1)
boolean	equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0, Term term0, ImmutableArray<QuantifiableVariable> vars1, Term term1, TermServices services)
Term[]	renameVariables(Term[] originalTerms, ImmutableArray<QuantifiableVariable> oldBoundVars, ImmutableArray<QuantifiableVariable> newBoundVars, TermServices services)
Term	renameVariables(Term originalTerm, ImmutableArray<QuantifiableVariable> oldBoundVars, ImmutableArray<QuantifiableVariable> newBoundVars, TermServices services) Compare the arrays oldBoundVars and newBoundVars component-wise, and in case of differences substitute variables from the former array with the ones of the latter array (in originalTerm)
boolean	resolveCollisions(ImmutableArray<QuantifiableVariable> oldVars, QuantifiableVariable[] newVars, ImmutableSet<QuantifiableVariable> criticalVars) Replace all variables of oldVars that also turn up in criticalPairs with new variables (currently just with the same name).
boolean	resolveCollisions(Term originalTerm, ImmutableSet<QuantifiableVariable> criticalVars, ImmutableArray<QuantifiableVariable>[] newBoundVars, Term[] newSubs, TermServices services) Ensure that none of the variables criticalVars is bound by the top-level operator of t (by bound renaming).
ImmutableArray<QuantifiableVariable>	unifyBoundVariables(ImmutableArray<QuantifiableVariable>[] boundVarsPerSub, Term[] subs, int subtermsBegin, int subtermsEnd, TermServices services) Ensure that for the subterms with indexes [subtermsBegin, subtermsEnd) the same variables are bound.
private ImmutableArray<QuantifiableVariable>	unifyVariableArrays(ImmutableArray<QuantifiableVariable> ar0, ImmutableArray<QuantifiableVariable> ar1, java.util.Map<QuantifiableVariable,QuantifiableVariable> variableRenaming) Unify the given arrays be replacing variables with new ones, return the unifier

Methods inherited from class java.lang.Object

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

Field Detail

DEFAULT

public static final BoundVariableTools DEFAULT

Constructor Detail

BoundVariableTools

private BoundVariableTools()

Method Detail

renameVariables

public Term renameVariables(Term originalTerm,
                            ImmutableArray<QuantifiableVariable> oldBoundVars,
                            ImmutableArray<QuantifiableVariable> newBoundVars,
                            TermServices services)

Compare the arrays oldBoundVars and newBoundVars component-wise, and in case of differences substitute variables from the former array with the ones of the latter array (in originalTerm)

Parameters:

services - the Services

renameVariables

public Term[] renameVariables(Term[] originalTerms,
                              ImmutableArray<QuantifiableVariable> oldBoundVars,
                              ImmutableArray<QuantifiableVariable> newBoundVars,
                              TermServices services)

resolveCollisions

public boolean resolveCollisions(ImmutableArray<QuantifiableVariable> oldVars,
                                 QuantifiableVariable[] newVars,
                                 ImmutableSet<QuantifiableVariable> criticalVars)

Replace all variables of oldVars that also turn up in criticalPairs with new variables (currently just with the same name).

Parameters:

oldVars - variables to be checked

newVars - array in which either the original variables (if a variable is not an element of criticalVars) or newly created variables are stored

criticalVars - variables that must not turn up in the resulting array newVars

Returns:

true iff it was necessary to create at least one new variable

resolveCollisions

public boolean resolveCollisions(Term originalTerm,
                                 ImmutableSet<QuantifiableVariable> criticalVars,
                                 ImmutableArray<QuantifiableVariable>[] newBoundVars,
                                 Term[] newSubs,
                                 TermServices services)

Ensure that none of the variables criticalVars is bound by the top-level operator of t (by bound renaming). The resulting subterms and arrays of bound variables are stored in newSubs and newBoundVars (resp.)

Parameters:

services - TODO

Returns:

true if it was necessary to rename a variable, i.e. to changed anything in the term originalTerm

unifyBoundVariables

public ImmutableArray<QuantifiableVariable> unifyBoundVariables(ImmutableArray<QuantifiableVariable>[] boundVarsPerSub,
                                                                Term[] subs,
                                                                int subtermsBegin,
                                                                int subtermsEnd,
                                                                TermServices services)

Ensure that for the subterms with indexes [subtermsBegin, subtermsEnd) the same variables are bound. In case of differences bound renaming is applied (existing variables are renamed to new ones)

Parameters:

boundVarsPerSub - bound variables per subterms

subs - subterms (in which variables are renamed if necessary)

subtermsBegin - first subterm that is supposed to be considered

subtermsEnd - subterm after the last subterm to be consider PRE: subtermsEnd > subtermsBegin

services - TODO

consistentVariableArrays

public boolean consistentVariableArrays(ImmutableArray<QuantifiableVariable> ar0,
                                        ImmutableArray<QuantifiableVariable> ar1)

Returns:

true iff the two given arrays have the same size and the contained variables have the same sorts

equalsModRenaming

public boolean equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0,
                                 Term term0,
                                 ImmutableArray<QuantifiableVariable> vars1,
                                 Term term1,
                                 TermServices services)

Parameters:

services - TODO

Returns:

true iff the two arrays of variables are compatible (compatibleVariableArrays()) and the two given terms are equal modulo renaming after unification of the two arrays (of variables occurring free in the terms)

unifyVariableArrays

private ImmutableArray<QuantifiableVariable> unifyVariableArrays(ImmutableArray<QuantifiableVariable> ar0,
                                                                 ImmutableArray<QuantifiableVariable> ar1,
                                                                 java.util.Map<QuantifiableVariable,QuantifiableVariable> variableRenaming)

Unify the given arrays be replacing variables with new ones, return the unifier