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 de.uka.ilkd.key.logic.op.*;
014:
015: public class ClashFreeSubst {
016: protected TermFactory tf = TermFactory.DEFAULT;
017:
018: QuantifiableVariable v;
019: Term s;
020: SetOfQuantifiableVariable svars;
021:
022: public ClashFreeSubst(QuantifiableVariable v, Term s) {
023: this .v = v;
024: this .s = s;
025: svars = s.freeVars();
026: }
027:
028: protected QuantifiableVariable getVariable() {
029: return v;
030: }
031:
032: protected Term getSubstitutedTerm() {
033: return s;
034: }
035:
036: /** substitute <code>s</code> for <code>v</code> in <code>t</code>,
037: * avoiding collisions by replacing bound variables in
038: * <code>t</code> if necessary.
039: */
040: public Term apply(Term t) {
041: if (!t.freeVars().contains(v)) {
042: return t;
043: } else
044: return apply1(t);
045: }
046:
047: /** substitute <code>s</code> for <code>v</code> in
048: * <code>t</code>, avoiding collisions by replacing bound
049: * variables in <code>t</code> if necessary. It is
050: * assumed, that <code>t</code> contains a free occurrence of
051: * <code>v</code>. */
052: protected Term apply1(Term t) {
053: if (t.op() == v) {
054: return s;
055: } else {
056: return applyOnSubterms(t);
057: }
058: }
059:
060: /** substitute <code>s</code> for <code>v</code> in
061: * every subterm of <code>t</code>, and build a new term.
062: * It is assumed, that one of the subterms contains a free occurrence
063: * of <code>v</code>, and that the case <code>v==t<code> is already
064: * handled. */
065: private Term applyOnSubterms(Term t) {
066: final int arity = t.arity();
067: final Term[] newSubterms = new Term[arity];
068: final ArrayOfQuantifiableVariable[] newBoundVars = new ArrayOfQuantifiableVariable[arity];
069: for (int i = 0; i < arity; i++) {
070: applyOnSubterm(t, i, newSubterms, newBoundVars);
071: }
072: return tf.createTerm(t.op(), newSubterms, newBoundVars, t
073: .javaBlock());
074: }
075:
076: /**
077: * Apply the substitution of the subterm <code>subtermIndex</code> of
078: * term/formula <code>completeTerm</code>. The result is stored in
079: * <code>newSubterms</code> and <code>newBoundVars</code> (at index
080: * <code>subtermIndex</code>)
081: */
082: protected void applyOnSubterm(Term completeTerm, int subtermIndex,
083: Term[] newSubterms,
084: ArrayOfQuantifiableVariable[] newBoundVars) {
085: if (subTermChanges(completeTerm.varsBoundHere(subtermIndex),
086: completeTerm.sub(subtermIndex))) {
087: final QuantifiableVariable[] nbv = new QuantifiableVariable[completeTerm
088: .varsBoundHere(subtermIndex).size()];
089: applyOnSubterm(0, completeTerm.varsBoundHere(subtermIndex),
090: nbv, subtermIndex, completeTerm.sub(subtermIndex),
091: newSubterms);
092: newBoundVars[subtermIndex] = new ArrayOfQuantifiableVariable(
093: nbv);
094: } else {
095: newBoundVars[subtermIndex] = completeTerm
096: .varsBoundHere(subtermIndex);
097: newSubterms[subtermIndex] = completeTerm.sub(subtermIndex);
098: }
099: }
100:
101: /** Perform the substitution on <code>subTerm</code> bound by the
102: * variables in <code>boundVars</code>, starting with the variable
103: * at index <code>varInd</code>. Put the resulting bound
104: * variables (which might be new) into <code>newBoundVars</code>,
105: * starting from position <code>varInd</code>, and the resulting
106: * subTerm into <code>newSubterms[subInd]</code>.
107: * <P> It is assumed that <code>v</code> occurrs free in
108: * in this quantified subterm, i.e. it occurrs free in
109: * <code>subTerm</code>, but does not occurr in
110: * <code>boundVars</code> from <code>varInd</code> upwards..
111: */
112: private void applyOnSubterm(int varInd,
113: ArrayOfQuantifiableVariable boundVars,
114: QuantifiableVariable[] newBoundVars, int subInd,
115: Term subTerm, Term[] newSubterms) {
116: if (varInd >= boundVars.size()) {
117: newSubterms[subInd] = apply1(subTerm);
118: } else {
119: QuantifiableVariable qv = boundVars
120: .getQuantifiableVariable(varInd);
121: if (svars.contains(qv)) {
122: /* Here is the clash case all this is about! Hurrah! */
123:
124: // Determine Variable names to avoid
125: VariableCollectVisitor vcv = new VariableCollectVisitor();
126: SetOfQuantifiableVariable usedVars;
127: subTerm.execPostOrder(vcv);
128: usedVars = svars;
129: usedVars = usedVars.union(vcv.vars());
130: for (int i = varInd + 1; i < boundVars.size(); i++) {
131: usedVars = usedVars.add(boundVars
132: .getQuantifiableVariable(i));
133: }
134: // Get a new variable with a fitting name.
135: QuantifiableVariable qv1 = newVarFor(qv, usedVars);
136:
137: // Substitute that for the old one.
138: newBoundVars[varInd] = qv1;
139: new ClashFreeSubst(qv, tf
140: .createVariableTerm((LogicVariable) qv1))
141: .applyOnSubterm1(varInd + 1, boundVars,
142: newBoundVars, subInd, subTerm,
143: newSubterms);
144: // then continue recursively, on the result.
145: applyOnSubterm(varInd + 1,
146: new ArrayOfQuantifiableVariable(newBoundVars),
147: newBoundVars, subInd, newSubterms[subInd],
148: newSubterms);
149: } else {
150: newBoundVars[varInd] = qv;
151: applyOnSubterm(varInd + 1, boundVars, newBoundVars,
152: subInd, subTerm, newSubterms);
153: }
154: }
155: }
156:
157: /** Same as applyOnSubterm, but v doesn't have to occurr free in the
158: * considered quantified subterm. It is however assumed that no more
159: * clash can occurr. */
160: private void applyOnSubterm1(int varInd,
161: ArrayOfQuantifiableVariable boundVars,
162: QuantifiableVariable[] newBoundVars, int subInd,
163: Term subTerm, Term[] newSubterms) {
164: if (varInd >= boundVars.size()) {
165: newSubterms[subInd] = apply(subTerm);
166: } else {
167: QuantifiableVariable qv = boundVars
168: .getQuantifiableVariable(varInd);
169: newBoundVars[varInd] = qv;
170: if (qv == v) {
171: newSubterms[subInd] = subTerm;
172: for (int i = varInd; i < boundVars.size(); i++) {
173: newBoundVars[i] = boundVars
174: .getQuantifiableVariable(varInd);
175: }
176: } else {
177: applyOnSubterm1(varInd + 1, boundVars, newBoundVars,
178: subInd, subTerm, newSubterms);
179: }
180: }
181: }
182:
183: /** returns true if <code>subTerm</code> bound by
184: * <code>boundVars</code> would change under application of this
185: * substitution. This is the case, if <code>v</code> occurrs free
186: * in <code>subTerm</code>, but does not occurr in <code>boundVars</code>.
187: * @returns true if <code>subTerm</code> bound by
188: * <code>boundVars</code> would change under application of this
189: * substitution
190: */
191: protected boolean subTermChanges(
192: ArrayOfQuantifiableVariable boundVars, Term subTerm) {
193: if (!subTerm.freeVars().contains(v)) {
194: return false;
195: } else {
196: for (int i = 0; i < boundVars.size(); i++) {
197: if (v == boundVars.getQuantifiableVariable(i)) {
198: return false;
199: }
200: }
201: }
202: return true;
203: }
204:
205: /** returns a new variable that has a name derived from that of
206: * <code>var</code>, that is different from any of the names of
207: * variables in <code>usedVars</code>.
208: * <P> Assumes that <code>var</code> is a @link{LogicVariable}. */
209: protected QuantifiableVariable newVarFor(QuantifiableVariable var,
210: SetOfQuantifiableVariable usedVars) {
211: LogicVariable lv = (LogicVariable) var;
212: String stem = var.name().toString();
213: int i = 1;
214: while (!nameNewInSet((stem + i), usedVars)) {
215: i++;
216: }
217: return new LogicVariable(new Name(stem + i), lv.sort());
218: }
219:
220: /** returns true if there is no object named <code>n</code> in the
221: * set <code>s</code> */
222: private boolean nameNewInSet(String n,
223: SetOfQuantifiableVariable qvars) {
224: IteratorOfQuantifiableVariable it = qvars.iterator();
225: while (it.hasNext()) {
226: if (it.next().name().toString().equals(n)) {
227: return false;
228: }
229: }
230: return true;
231: }
232:
233: /** A Visitor class to collect all (not just the free) variables
234: * occurring in a term. */
235: protected static class VariableCollectVisitor extends Visitor {
236: /** the collected variables */
237: private SetOfQuantifiableVariable vars;
238:
239: /** creates the Variable collector */
240: public VariableCollectVisitor() {
241: vars = SetAsListOfQuantifiableVariable.EMPTY_SET;
242: }
243:
244: public void visit(Term t) {
245: if (t.op() instanceof QuantifiableVariable) {
246: vars = vars.add((QuantifiableVariable) t.op());
247: } else {
248: for (int i = 0; i < t.arity(); i++) {
249: ArrayOfQuantifiableVariable vbh = t
250: .varsBoundHere(i);
251: for (int j = 0; j < vbh.size(); j++) {
252: vars = vars.add(vbh.getQuantifiableVariable(j));
253: }
254: }
255: }
256: }
257:
258: /** the set of all occurring variables.*/
259: public SetOfQuantifiableVariable vars() {
260: return vars;
261: }
262: }
263:
264: }
|