001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic;
012:
013: import java.util.HashMap;
014: import java.util.Map;
015:
016: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
017: import de.uka.ilkd.key.logic.op.LogicVariable;
018: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
019: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
020: import de.uka.ilkd.key.util.Debug;
021:
022: /**
023: * Some generally useful tools for dealing with arrays of bound variables
024: */
025: public class BoundVariableTools {
026:
027: public final static BoundVariableTools DEFAULT = new BoundVariableTools();
028:
029: private BoundVariableTools() {
030: }
031:
032: private final TermFactory tf = TermFactory.DEFAULT;
033:
034: /**
035: * Compare the arrays <code>oldBoundVars</code> and
036: * <code>newBoundVars</code> component-wise, and in case of differences
037: * substitute variables from the former array with the ones of the latter
038: * array (in <code>originalTerm</code>)
039: */
040: public Term renameVariables(Term originalTerm,
041: ArrayOfQuantifiableVariable oldBoundVars,
042: ArrayOfQuantifiableVariable newBoundVars) {
043: Term res = originalTerm;
044: for (int i = 0; i != oldBoundVars.size(); ++i) {
045: if (oldBoundVars.getQuantifiableVariable(i) != newBoundVars
046: .getQuantifiableVariable(i)) {
047: final Term newVarTerm = tf
048: .createVariableTerm((LogicVariable) newBoundVars
049: .getQuantifiableVariable(i));
050: final ClashFreeSubst subst = new ClashFreeSubst(
051: oldBoundVars.getQuantifiableVariable(i),
052: newVarTerm);
053: res = subst.apply(res);
054: }
055: }
056:
057: return res;
058: }
059:
060: public Term[] renameVariables(Term[] originalTerms,
061: ArrayOfQuantifiableVariable oldBoundVars,
062: ArrayOfQuantifiableVariable newBoundVars) {
063: final Term[] res = new Term[originalTerms.length];
064: for (int i = 0; i != res.length; ++i)
065: res[i] = renameVariables(originalTerms[i], oldBoundVars,
066: newBoundVars);
067: return res;
068: }
069:
070: /**
071: * Replace all variables of <code>oldVars</code> that also turn up in
072: * <code>criticalPairs</code> with new variables (currently just with the
073: * same name).
074: *
075: * @param oldVars
076: * variables to be checked
077: * @param newVars
078: * array in which either the original variables (if a variable is
079: * not an element of <code>criticalVars</code>) or newly
080: * created variables are stored
081: * @param criticalVars
082: * variables that must not turn up in the resulting array
083: * <code>newVars</code>
084: * @return <code>true</code> iff it was necessary to create at least one
085: * new variable
086: */
087: public boolean resolveCollisions(
088: ArrayOfQuantifiableVariable oldVars,
089: QuantifiableVariable[] newVars,
090: SetOfQuantifiableVariable criticalVars) {
091: boolean changedVar = false;
092:
093: for (int i = 0; i != newVars.length; ++i) {
094: final QuantifiableVariable oldVar = oldVars
095: .getQuantifiableVariable(i);
096: if (criticalVars.contains(oldVar)) {
097: // rename the bound variable
098: newVars[i] = new LogicVariable(oldVar.name(), oldVar
099: .sort());
100: changedVar = true;
101: } else {
102: newVars[i] = oldVar;
103: }
104: }
105:
106: return changedVar;
107: }
108:
109: /**
110: * Ensure that none of the variables <code>criticalVars</code> is bound by
111: * the top-level operator of <code>t</code> (by bound renaming)
112: */
113: public Term resolveCollisions(Term t,
114: SetOfQuantifiableVariable criticalVars) {
115: final ArrayOfQuantifiableVariable[] newBoundVars = new ArrayOfQuantifiableVariable[t
116: .arity()];
117: final Term[] newSubs = new Term[t.arity()];
118:
119: if (!resolveCollisions(t, criticalVars, newBoundVars, newSubs))
120: return t;
121:
122: return tf.createTerm(t.op(), newSubs, newBoundVars, t
123: .javaBlock());
124: }
125:
126: /**
127: * Ensure that none of the variables <code>criticalVars</code> is bound by
128: * the top-level operator of <code>t</code> (by bound renaming). The
129: * resulting subterms and arrays of bound variables are stored in
130: * <code>newSubs</code> and <code>newBoundVars</code> (resp.)
131: *
132: * @return <code>true</code> if it was necessary to rename a variable,
133: * i.e. to changed anything in the term <code>originalTerm</code>
134: */
135: public boolean resolveCollisions(Term originalTerm,
136: SetOfQuantifiableVariable criticalVars,
137: ArrayOfQuantifiableVariable[] newBoundVars, Term[] newSubs) {
138: boolean changed = false;
139:
140: for (int i = 0; i != originalTerm.arity(); ++i) {
141: final ArrayOfQuantifiableVariable oldVars = originalTerm
142: .varsBoundHere(i);
143:
144: final QuantifiableVariable[] newVars = new QuantifiableVariable[oldVars
145: .size()];
146: if (resolveCollisions(oldVars, newVars, criticalVars)) {
147: changed = true;
148: newBoundVars[i] = new ArrayOfQuantifiableVariable(
149: newVars);
150: newSubs[i] = renameVariables(originalTerm.sub(i),
151: oldVars, newBoundVars[i]);
152: } else {
153: newBoundVars[i] = oldVars;
154: newSubs[i] = originalTerm.sub(i);
155: }
156: }
157:
158: return changed;
159: }
160:
161: /**
162: * Ensure that for the subterms with indexes [<code>subtermsBegin</code>,
163: * <code>subtermsEnd</code>) the same variables are bound. In case of
164: * differences bound renaming is applied (existing variables are renamed to
165: * new ones)
166: *
167: * @param boundVarsPerSub bound variables per subterms
168: * @param subs subterms (in which variables are renamed if necessary)
169: * @param subtermsBegin first subterm that is supposed to be considered
170: * @param subtermsEnd subterm after the last subterm to be consider
171: *
172: * PRE: <code>subtermsEnd > subtermsBegin</code>
173: */
174: public ArrayOfQuantifiableVariable unifyBoundVariables(
175: ArrayOfQuantifiableVariable[] boundVarsPerSub, Term[] subs,
176: int subtermsBegin, int subtermsEnd) {
177: // at least one subterms belongs to the entry (value)
178: ArrayOfQuantifiableVariable unifiedVariable = boundVarsPerSub[subtermsBegin];
179:
180: final Map variableRenamings = new HashMap();
181: for (int i = subtermsBegin + 1; i < subtermsEnd; ++i) {
182: // check that numbers and sorts of the quantified variables are
183: // consistent
184: Debug
185: .assertTrue(consistentVariableArrays(
186: unifiedVariable, boundVarsPerSub[i]),
187: "Inconsistent bound variables");
188:
189: unifiedVariable = unifyVariableArrays(unifiedVariable,
190: boundVarsPerSub[i], variableRenamings);
191: }
192:
193: // substitute variables where necessary
194: for (int i = subtermsBegin; i < subtermsEnd; ++i)
195: subs[i] = renameVariables(subs[i], boundVarsPerSub[i],
196: unifiedVariable);
197:
198: return unifiedVariable;
199: }
200:
201: /**
202: * @return <code>true</code> iff the two given arrays have the same size
203: * and the contained variables have the same sorts
204: */
205: public boolean consistentVariableArrays(
206: ArrayOfQuantifiableVariable ar0,
207: ArrayOfQuantifiableVariable ar1) {
208: if (ar0.size() != ar1.size())
209: return false;
210: for (int i = 0; i != ar0.size(); ++i) {
211: if (ar0.getQuantifiableVariable(i).sort() != ar1
212: .getQuantifiableVariable(i).sort())
213: return false;
214: }
215: return true;
216: }
217:
218: /**
219: * @return <code>true</code> iff the two arrays of variables are
220: * compatible (<code>compatibleVariableArrays()</code>) and the
221: * two given terms are equal modulo renaming after unification of
222: * the two arrays (of variables occurring free in the terms)
223: */
224: public boolean equalsModRenaming(ArrayOfQuantifiableVariable vars0,
225: Term term0, ArrayOfQuantifiableVariable vars1, Term term1) {
226: if (!consistentVariableArrays(vars0, vars1))
227: return false;
228: if (vars0.size() == 0)
229: return term0.equalsModRenaming(term1);
230:
231: final ArrayOfQuantifiableVariable unifiedVars = unifyVariableArrays(
232: vars0, vars1, new HashMap());
233:
234: final Term renamedTerm0 = renameVariables(term0, vars0,
235: unifiedVars);
236: final Term renamedTerm1 = renameVariables(term1, vars1,
237: unifiedVars);
238:
239: return renamedTerm0.equalsModRenaming(renamedTerm1);
240: }
241:
242: /**
243: * Unify the given arrays be replacing variables with new ones, return the
244: * unifier
245: */
246: private ArrayOfQuantifiableVariable unifyVariableArrays(
247: ArrayOfQuantifiableVariable ar0,
248: ArrayOfQuantifiableVariable ar1, Map variableRenaming) {
249: final QuantifiableVariable[] res = new QuantifiableVariable[ar0
250: .size()];
251: for (int i = 0; i != ar0.size(); ++i) {
252: QuantifiableVariable pv0 = ar0.getQuantifiableVariable(i);
253: if (variableRenaming.containsKey(pv0))
254: pv0 = (QuantifiableVariable) variableRenaming.get(pv0);
255:
256: QuantifiableVariable pv1 = ar1.getQuantifiableVariable(i);
257: if (variableRenaming.containsKey(pv1))
258: pv1 = (QuantifiableVariable) variableRenaming.get(pv1);
259:
260: if (pv0 != pv1) {
261: // introduce a new variable
262: final QuantifiableVariable newVar = new LogicVariable(
263: pv0.name(), pv0.sort());
264: variableRenaming.put(ar0.getQuantifiableVariable(i),
265: newVar);
266: variableRenaming.put(ar1.getQuantifiableVariable(i),
267: newVar);
268: variableRenaming.put(pv0, newVar);
269: variableRenaming.put(pv1, newVar);
270: pv0 = pv1 = newVar;
271: }
272:
273: res[i] = pv0;
274: }
275:
276: return new ArrayOfQuantifiableVariable(res);
277: }
278: }
|