public class BoundVariableTools
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static BoundVariableTools |
DEFAULT |
Modifier | Constructor and Description |
---|---|
private |
BoundVariableTools() |
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
|
public static final BoundVariableTools DEFAULT
public Term renameVariables(Term originalTerm, ImmutableArray<QuantifiableVariable> oldBoundVars, ImmutableArray<QuantifiableVariable> newBoundVars, TermServices services)
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
)services
- the Servicespublic Term[] renameVariables(Term[] originalTerms, ImmutableArray<QuantifiableVariable> oldBoundVars, ImmutableArray<QuantifiableVariable> newBoundVars, TermServices services)
public boolean resolveCollisions(ImmutableArray<QuantifiableVariable> oldVars, QuantifiableVariable[] newVars, ImmutableSet<QuantifiableVariable> criticalVars)
oldVars
that also turn up in
criticalPairs
with new variables (currently just with the
same name).oldVars
- variables to be checkednewVars
- array in which either the original variables (if a variable is
not an element of criticalVars
) or newly
created variables are storedcriticalVars
- variables that must not turn up in the resulting array
newVars
true
iff it was necessary to create at least one
new variablepublic boolean resolveCollisions(Term originalTerm, ImmutableSet<QuantifiableVariable> criticalVars, ImmutableArray<QuantifiableVariable>[] newBoundVars, Term[] newSubs, TermServices services)
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.)services
- TODOtrue
if it was necessary to rename a variable,
i.e. to changed anything in the term originalTerm
public ImmutableArray<QuantifiableVariable> unifyBoundVariables(ImmutableArray<QuantifiableVariable>[] boundVarsPerSub, Term[] subs, int subtermsBegin, int subtermsEnd, TermServices services)
subtermsBegin
,
subtermsEnd
) the same variables are bound. In case of
differences bound renaming is applied (existing variables are renamed to
new ones)boundVarsPerSub
- bound variables per subtermssubs
- subterms (in which variables are renamed if necessary)subtermsBegin
- first subterm that is supposed to be consideredsubtermsEnd
- subterm after the last subterm to be consider
PRE: subtermsEnd > subtermsBegin
services
- TODOpublic boolean consistentVariableArrays(ImmutableArray<QuantifiableVariable> ar0, ImmutableArray<QuantifiableVariable> ar1)
true
iff the two given arrays have the same size
and the contained variables have the same sortspublic boolean equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0, Term term0, ImmutableArray<QuantifiableVariable> vars1, Term term1, TermServices services)
services
- TODOtrue
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)private ImmutableArray<QuantifiableVariable> unifyVariableArrays(ImmutableArray<QuantifiableVariable> ar0, ImmutableArray<QuantifiableVariable> ar1, java.util.Map<QuantifiableVariable,QuantifiableVariable> variableRenaming)