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: import de.uka.ilkd.key.rule.soundness.SVSkolemFunction;
015:
016: public class WaryClashFreeSubst extends ClashFreeSubst {
017:
018: /** depth of recursion of the <code>apply</code> method */
019: private int depth = 0;
020: /** the formula should be prepended with a quantifier */
021: private boolean createQuantifier = false;
022:
023: /** variable with which the original variable should be
024: * substituted below modalities */
025: private QuantifiableVariable newVar = null;
026: private Term newVarTerm = null;
027:
028: /** variables occurring within the original term and within the
029: * term to be substituted */
030: private SetOfQuantifiableVariable warysvars = null;
031:
032: public WaryClashFreeSubst(QuantifiableVariable v, Term s) {
033: super (v, s);
034: warysvars = null;
035: }
036:
037: /**
038: * substitute <code>s</code> for <code>v</code> in <code>t</code>,
039: * avoiding collisions by replacing bound variables in
040: * <code>t</code> if necessary.
041: */
042: public Term apply(Term t) {
043: Term res;
044:
045: if (depth == 0) {
046: if (!getSubstitutedTerm().isRigid())
047: findUsedVariables(t);
048: }
049:
050: ++depth;
051: try {
052: res = super .apply(t);
053: } finally {
054: --depth;
055: }
056:
057: if (createQuantifier && depth == 0)
058: res = addWarySubst(res);
059:
060: return res;
061: }
062:
063: /**
064: * Determine a set of variables that do already appear within
065: * <code>t</code> or the substituted term, and whose names should
066: * not be used for free variables
067: */
068: private void findUsedVariables(Term t) {
069: VariableCollectVisitor vcv;
070:
071: vcv = new VariableCollectVisitor();
072: getSubstitutedTerm().execPostOrder(vcv);
073: warysvars = vcv.vars();
074:
075: vcv = new VariableCollectVisitor();
076: t.execPostOrder(vcv);
077: warysvars = warysvars.union(vcv.vars());
078: }
079:
080: /**
081: * Create a new logic variable to be used for substitutions below
082: * modalities
083: */
084: private void createVariable() {
085: if (!createQuantifier) {
086: createQuantifier = true;
087:
088: if (getSubstitutedTerm().freeVars().contains(getVariable()))
089: // in this case one might otherwise get collisions, as the
090: // substitution might be carried out partially within the scope
091: // of the original substitution operator
092: newVar = newVarFor(getVariable(), warysvars);
093: else
094: newVar = getVariable();
095: newVarTerm = tf.createVariableTerm((LogicVariable) newVar);
096: }
097: }
098:
099: /**
100: * substitute <code>s</code> for <code>v</code> in
101: * <code>t</code>, avoiding collisions by replacing bound
102: * variables in <code>t</code> if necessary. It is
103: * assumed, that <code>t</code> contains a free occurrence of
104: * <code>v</code>.
105: */
106: protected Term apply1(Term t) {
107: // don't move to a different modality level
108: if (!getSubstitutedTerm().isRigid()) {
109: if (t.op() instanceof Modality)
110: return applyOnModality(t);
111: if (t.op() instanceof IUpdateOperator)
112: return applyOnUpdate(t);
113: if (t.op() instanceof SVSkolemFunction)
114: return applyToSVSkolem(t);
115: }
116: return super .apply1(t);
117: }
118:
119: /**
120: * Apply the substitution (that replaces a variable with a
121: * non-rigid term) on t, which has a modality as top-level
122: * operator. This is done by creating a (top-level) existential
123: * quantifier. This method is only called from <code>apply1</code>
124: * for substitutions with non-rigid terms
125: *
126: * PRECONDITION: <code>warysvars != null</code>
127: */
128: private Term applyOnModality(Term t) {
129: return applyBelowModality(t);
130: }
131:
132: /**
133: * Apply the substitution (that replaces a variable with a
134: * non-rigid term) on t, which has an update operator as top-level
135: * operator. This is done by creating a (top-level) existential
136: * quantifier. This method is only called from <code>apply1</code>
137: * for substitutions with non-rigid terms
138: *
139: * PRECONDITION: <code>warysvars != null</code>
140: */
141: private Term applyOnUpdate(Term t) {
142: final IUpdateOperator updOp = (IUpdateOperator) t.op();
143:
144: // only the last child is below the update
145: final Term target = updOp.target(t);
146: if (!target.freeVars().contains(getVariable()))
147: return super .apply1(t);
148:
149: final Term[] newSubterms = new Term[t.arity()];
150: final ArrayOfQuantifiableVariable[] newBoundVars = new ArrayOfQuantifiableVariable[t
151: .arity()];
152:
153: for (int i = 0; i < t.arity(); i++) {
154: if (i != updOp.targetPos())
155: applyOnSubterm(t, i, newSubterms, newBoundVars);
156: }
157:
158: newBoundVars[updOp.targetPos()] = t.varsBoundHere(updOp
159: .targetPos());
160: final boolean addSubst = subTermChanges(t.varsBoundHere(updOp
161: .targetPos()), target);
162: newSubterms[updOp.targetPos()] = addSubst ? substWithNewVar(target)
163: : target;
164:
165: return tf.createTerm(t.op(), newSubterms, newBoundVars, t
166: .javaBlock());
167: }
168:
169: /**
170: * Apply the substitution to a term/formula below a modality or update
171: */
172: private Term applyBelowModality(Term t) {
173: return substWithNewVar(t);
174: }
175:
176: /**
177: * Prepend the given term with a wary substitution (substituting
178: * <code>newVar</code> with <code>getSubstitutedTerm()</code>)
179: */
180: private Term addWarySubst(Term t) {
181: createVariable();
182: return tf.createSubstitutionTerm(Op.SUBST, newVar,
183: getSubstitutedTerm(), t);
184: }
185:
186: /**
187: * Rename the original variable to be substituted to <code>newVar</code>
188: */
189: private Term substWithNewVar(Term t) {
190: createVariable();
191: final ClashFreeSubst cfs = new ClashFreeSubst(getVariable(),
192: newVarTerm);
193: return cfs.apply(t);
194: }
195:
196: /**
197: * Apply the substitution to a non-rigid skolem function
198: */
199: private Term applyToSVSkolem(Term t) {
200: return applyBelowModality(t);
201: }
202:
203: }
|