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: package de.uka.ilkd.key.rule;
010:
011: import de.uka.ilkd.key.java.Services;
012: import de.uka.ilkd.key.logic.ArrayOfTerm;
013: import de.uka.ilkd.key.logic.BoundVariableTools;
014: import de.uka.ilkd.key.logic.Term;
015: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
016: import de.uka.ilkd.key.logic.op.SetAsListOfQuantifiableVariable;
017: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
018: import de.uka.ilkd.key.logic.sort.AbstractSort;
019: import de.uka.ilkd.key.logic.sort.Sort;
020: import de.uka.ilkd.key.logic.util.TermHelper;
021: import de.uka.ilkd.key.rule.updatesimplifier.ArrayOfAssignmentPair;
022: import de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair;
023: import de.uka.ilkd.key.rule.updatesimplifier.Update;
024: import de.uka.ilkd.key.rule.updatesimplifier.UpdateSimplifierTermFactory;
025:
026: /**
027: * abstract class that must be extended by rules designed to be used
028: * by the update simplifier
029: */
030: public abstract class AbstractUpdateRule implements IUpdateRule {
031:
032: private final UpdateSimplifier updateSimplifier;
033:
034: /**
035: * creates an instance of this rule used by the given update
036: * simplifier
037: * @param updateSimplifier the UpdateSimplifier using this rule
038: */
039: public AbstractUpdateRule(UpdateSimplifier updateSimplifier) {
040: this .updateSimplifier = updateSimplifier;
041: }
042:
043: /**
044: * returns the update simplifier for which this rule has been
045: * registered
046: */
047: public UpdateSimplifier updateSimplifier() {
048: return updateSimplifier;
049: }
050:
051: /**
052: * returns true if casting term <code>newSub</code> is necessary if
053: * it should replace the <code>pos</code>-th position of <code>t</code>
054: */
055: private boolean needsCast(Term t, Term newSub, int pos,
056: Services services) {
057: if (newSub.sort().extendsTrans(t.sub(pos).sort())) {
058: return false;
059: }
060: final Sort maxSort = TermHelper.getMaxSort(t, pos, services);
061: return !newSub.sort().extendsTrans(maxSort);
062: }
063:
064: /**
065: * TODO: here we have to check for collisions!!! /PR
066: *
067: * propagates the update to the subterm of the given term
068: * @param update the Update to be propagated
069: * @param term the Term whose subterms have to be simplified
070: * @param services the Services object
071: * @return the simplified subterm, an array of bound variables
072: * and a flag indicating if one of the subterms has changed
073: */
074: protected PropagationResult propagateUpdateToSubterms(
075: Update update, Term term, Services services) {
076: final Term[] subs = new Term[term.arity()];
077: final ArrayOfQuantifiableVariable[] vars = new ArrayOfQuantifiableVariable[subs.length];
078:
079: boolean changed = BoundVariableTools.DEFAULT.resolveCollisions(
080: term, update.freeVars(), vars, subs);
081:
082: for (int i = 0; i < subs.length; i++) {
083: final Term oldSub = subs[i];
084: subs[i] = updateSimplifier().simplify(update, oldSub,
085: services);
086: if (subs[i] != oldSub) {
087: changed = true;
088: if (needsCast(term, subs[i], i, services)
089: && subs[i].sort() instanceof AbstractSort) {
090: subs[i] = UpdateSimplifierTermFactory.DEFAULT
091: .getBasicTermFactory().createCastTerm(
092: (AbstractSort) oldSub.sort(),
093: subs[i]);
094: }
095: }
096: }
097:
098: return new PropagationResult(subs, vars, changed);
099: }
100:
101: /**
102: * determines whether this rule is applicable for the pair of
103: * update and target (the term on which the update will be
104: * applied) term
105: * @param update the Update to be applied on the given term
106: * @param target the Term on which the update is applied
107: * @return true if the rule can be applied on the update, target
108: * pair
109: */
110: public abstract boolean isApplicable(Update update, Term target);
111:
112: public static class PropagationResult {
113: private final Term[] subs;
114: private final boolean changeFlag;
115: private final ArrayOfQuantifiableVariable[] vars;
116:
117: public PropagationResult(Term[] subs,
118: ArrayOfQuantifiableVariable[] vars, boolean changeFlag) {
119: this .subs = subs;
120: this .vars = vars;
121: this .changeFlag = changeFlag;
122: }
123:
124: /**
125: * @return
126: */
127: public Term[] getSimplifiedSubterms() {
128: return subs;
129: }
130:
131: public ArrayOfQuantifiableVariable[] getBoundVariables() {
132: return vars;
133: }
134:
135: /**
136: * @return
137: */
138: public boolean hasChanged() {
139: return changeFlag;
140: }
141: }
142:
143: /**
144: * @param result
145: */
146: protected void logExit(Term result) {
147: /*
148: System.out.println("result is " + result);
149: */
150: }
151:
152: /**
153: * @param update
154: * @param target
155: */
156: protected void logEnter(Update update, Term target) {
157: /*
158: System.out.println("Rule: " + this.getClass() );
159: System.out.println("apply " + update + " on " + target);
160: */
161:
162: }
163:
164: protected static abstract class IterateAssignmentPairsIfExCascade
165: implements UpdateSimplifierTermFactory.IfExCascade {
166:
167: private final UpdateSimplifierTermFactory utf = UpdateSimplifierTermFactory.DEFAULT;
168:
169: private int locNum;
170: private final ArrayOfAssignmentPair pairs;
171: private AssignmentPair currentPair;
172:
173: public IterateAssignmentPairsIfExCascade(
174: ArrayOfAssignmentPair pairs) {
175: this .pairs = pairs;
176: this .locNum = pairs.size();
177: }
178:
179: public ArrayOfQuantifiableVariable getMinimizedVars() {
180: return getCurrentPair().boundVars();
181: }
182:
183: public Term getThenBranch() {
184: return getCurrentPair().value();
185: }
186:
187: public boolean hasNext() {
188: return locNum > 0;
189: }
190:
191: public void next() {
192: --locNum;
193: currentPair = utf.resolveCollisions(pairs
194: .getAssignmentPair(locNum), criticalVars());
195: }
196:
197: protected AssignmentPair getCurrentPair() {
198: return currentPair;
199: }
200:
201: /**
202: * Variables that must not turn up as result of
203: * <code>getMinimizedVars()</code>. This method has to be overridden
204: * by subclasses to give a hint about which variables that are bound in
205: * the treated update have to be renamed
206: */
207: protected abstract SetOfQuantifiableVariable criticalVars();
208:
209: protected static SetOfQuantifiableVariable freeVars(
210: ArrayOfTerm terms) {
211: SetOfQuantifiableVariable res = SetAsListOfQuantifiableVariable.EMPTY_SET;
212: for (int i = 0; i != terms.size(); ++i)
213: res = res.union(terms.getTerm(i).freeVars());
214: return res;
215: }
216: }
217:
218: }
|