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.java.Services;
014: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.logic.sort.Sort;
017: import de.uka.ilkd.key.rule.UpdateSimplifier;
018: import de.uka.ilkd.key.rule.updatesimplifier.*;
019:
020: /**
021: * Factory providing the update constructors that are described in "Sequential,
022: * Parallel and Quantified Updates of First-Order Structures". Don't try to use
023: * this class together with anonymous updates, this would probably screw up
024: * everything horribly.
025: *
026: * TODO: so far, updates are not simplified during construction; the factory
027: * could be optimized
028: */
029: public class UpdateFactory {
030:
031: /**
032: * Context of the updates that are produced by the factory.
033: */
034: private final Services services;
035:
036: /**
037: * the update simplifier to be used
038: */
039: private final UpdateSimplifier simplifier;
040:
041: private final TermFactory tf = TermFactory.DEFAULT;
042: private final UpdateSimplifierTermFactory utf = UpdateSimplifierTermFactory.DEFAULT;
043:
044: public UpdateFactory(Services services, UpdateSimplifier simplifier) {
045: this .services = services;
046: this .simplifier = simplifier;
047: }
048:
049: private Term wellOrder(Term t1, Term t2) {
050: // TODO: pretty hackish, better replace this with some real code /PR
051:
052: final IntegerLDT integerLDT = services.getTypeConverter()
053: .getIntegerLDT();
054:
055: if (t1.sort().extendsTrans(integerLDT.targetSort())
056: && t2.sort().extendsTrans(integerLDT.targetSort())) { // integer case
057: final Function WORelation = (Function) services
058: .getNamespaces().functions().lookup(
059: new Name("quanUpdateLeqInt"));
060: assert WORelation != null : "Update factory could not find "
061: + "well-ordering for integers";
062:
063: return tf.createFunctionTerm(WORelation, t1, t2);
064: }
065:
066: //TEST
067: System.out.println("UF: Sorts are " + t1.sort() + "("
068: + t1.sort().hashCode() + ") and " + t2.sort() + "("
069: + t2.sort().hashCode() + ")");
070: System.out.println("correct int sort is: "
071: + integerLDT.targetSort() + "("
072: + integerLDT.targetSort().hashCode() + ")");
073: System.exit(-1);
074:
075: assert false : "Update factory can currently not handle the"
076: + " sorts of the terms " + t1 + ", " + t2;
077: return null; // unreachable
078: }
079:
080: /**
081: * Apply an update to a term or a formula, without simplifying the result
082: */
083: public Term prepend(Update update, Term target) {
084: return UpdateSimplifierTermFactory.DEFAULT.createUpdateTerm(
085: update.getAllAssignmentPairs(), target);
086: }
087:
088: /**
089: * Apply an update to a term or a formula, simplify the result
090: */
091: public Term apply(Update update, Term target) {
092: return getSimplifier().simplify(update, target, services);
093: }
094:
095: /**
096: * Apply an update to another update
097: */
098: public Update apply(Update update, Update target) {
099: final ArrayOfAssignmentPair oldPairs = target
100: .getAllAssignmentPairs();
101:
102: final AssignmentPair[] newPairs = new AssignmentPair[oldPairs
103: .size()];
104: boolean changed = false;
105: for (int i = 0; i != oldPairs.size(); ++i) {
106: newPairs[i] = apply(update, oldPairs.getAssignmentPair(i));
107: changed = changed
108: || newPairs[i] != oldPairs.getAssignmentPair(i);
109: }
110:
111: if (!changed)
112: return target;
113:
114: return Update.createUpdate(newPairs);
115: }
116:
117: /**
118: * Apply an update to an assignment pair
119: */
120: private AssignmentPair apply(Update update, AssignmentPair oriTarget) {
121: final AssignmentPair cleanedTarget = utf.resolveCollisions(
122: oriTarget, update.freeVars());
123:
124: boolean changed = false;
125:
126: final Term[] locSubs = new Term[cleanedTarget.locationSubs().length];
127: for (int i = 0; i != locSubs.length; ++i) {
128: locSubs[i] = apply(update, cleanedTarget.locationSubs()[i]);
129: changed = changed
130: || locSubs[i] != cleanedTarget.locationSubs()[i];
131: }
132:
133: /** unsafe is safe in this case, as the evaluated value will be used on the
134: * right side of an update
135: */
136: final Term newValue = apply(update, cleanedTarget.valueUnsafe());
137: changed = changed || newValue != cleanedTarget.valueUnsafe();
138:
139: final Term newGuard = apply(update, cleanedTarget.guard());
140: changed = changed || newGuard != cleanedTarget.guard();
141:
142: if (!changed)
143: return oriTarget;
144: return new AssignmentPairImpl(cleanedTarget.boundVars(),
145: newGuard, cleanedTarget.location(), locSubs, newValue);
146: }
147:
148: /**
149: * The neutral update (neutral element concerning parallel and sequential
150: * composition) not updating anything
151: */
152: public Update skip() {
153: return Update.createUpdate(new AssignmentPair[0]);
154: }
155:
156: /**
157: * Create an elementary update <tt>leftHandSide := value</code>
158: *
159: * @param leftHandSide
160: * Term describing the location that is updated. The operator of
161: * the term has to implement the interface <code>Location</code>.
162: * @param value
163: * Term describing the new value of the updated location
164: *
165: * @return the resulting update
166: */
167: public Update elementaryUpdate(Term leftHandSide, Term value) {
168: final Term[] subs = new Term[leftHandSide.arity()];
169: for (int i = 0; i != subs.length; ++i)
170: subs[i] = leftHandSide.sub(i);
171:
172: final AssignmentPair ass = new AssignmentPairImpl(
173: (Location) leftHandSide.op(), subs, value);
174:
175: return Update.createUpdate(new AssignmentPair[] { ass });
176: }
177:
178: /**
179: * Compute the parallel composition of two updates,
180: * <tt>update1 | update2</tt>
181: */
182: public Update parallel(Update update1, Update update2) {
183: final ArrayOfAssignmentPair pairs1 = update1
184: .getAllAssignmentPairs();
185: final ArrayOfAssignmentPair pairs2 = update2
186: .getAllAssignmentPairs();
187:
188: final AssignmentPair[] resPairs = new AssignmentPair[pairs1
189: .size()
190: + pairs2.size()];
191:
192: pairs1.arraycopy(0, resPairs, 0, pairs1.size());
193: pairs2.arraycopy(0, resPairs, pairs1.size(), pairs2.size());
194:
195: return Update.createUpdate(resPairs);
196: }
197:
198: /**
199: * Compute the parallel composition of an array of updates.
200: *
201: * TODO: this could be implemented more efficiently
202: */
203: public Update parallel(Update[] updates) {
204: if (updates.length == 0)
205: return skip();
206:
207: Update res = updates[0];
208: for (int i = 1; i != updates.length; ++i)
209: res = parallel(res, updates[i]);
210:
211: return res;
212: }
213:
214: /**
215: * Compute the sequential composition of two updates,
216: * <tt>update1 ; update2</tt>
217: */
218: public Update sequential(Update update1, Update update2) {
219: return parallel(update1, apply(update1, update2));
220: }
221:
222: /**
223: * Compute the sequential composition of an array of updates.
224: */
225: public Update sequential(Update[] updates) {
226: if (updates.length == 0)
227: return skip();
228:
229: Update res = updates[0];
230: for (int i = 1; i != updates.length; ++i)
231: res = sequential(res, updates[i]);
232:
233: return res;
234: }
235:
236: /**
237: * Quantify over <code>var</code>, i.e. carry out the update
238: * <code>update</code> in parallel for all values of <code>var</code>
239: */
240: public Update quantify(QuantifiableVariable var, Update update) {
241: // ensure that no collisions occur later on
242: update = utf.resolveCollisions(update, update.freeVars());
243:
244: final ArrayOfAssignmentPair oldPairs = update
245: .getAllAssignmentPairs();
246:
247: // we create a copy of the update in which <tt>var</tt> is replaced with
248: // a new variable <tt>var'</tt>
249: final LogicVariable varP = createPrime(var);
250: final ArrayOfAssignmentPair oldPairsP = substitute(update, var,
251: varP).getAllAssignmentPairs();
252:
253: // sanity check
254: assert oldPairs.size() == oldPairsP.size();
255:
256: return quantify(var, varP, oldPairs, oldPairsP);
257: }
258:
259: /**
260: * Perform quantification over <code>var</code> for the update described
261: * by <code>oldPairs</code>. Therefore it is necessary to add certain
262: * guards to the elementary updates, and a copy <code>oldPairsP</code> of
263: * the update is needed in which <code>var</code> is renamed to
264: * <code>varP</code>
265: *
266: * @param var
267: * variable to quantify over
268: * @param varP
269: * new variable necessary to render the guards
270: * @param oldPairs
271: * update that is supposed to be quantified
272: * @param oldPairsP
273: * update that differs from <code>oldPairs</code> in the
274: * renaming of <code>var</code> to <code>varP</code>
275: * @return resulting (simplified) update
276: */
277: private Update quantify(QuantifiableVariable var,
278: LogicVariable varP, ArrayOfAssignmentPair oldPairs,
279: ArrayOfAssignmentPair oldPairsP) {
280: final AssignmentPair[] newPairs = new AssignmentPair[oldPairs
281: .size()];
282: for (int locNum = 0; locNum != oldPairs.size(); ++locNum) {
283: final AssignmentPair pair = oldPairs
284: .getAssignmentPair(locNum);
285:
286: assert oldPairs.size() == 1
287: || !(pair.location() instanceof ShadowedOperator) : "UpdateFactory.quantify cannot handle shadowed"
288: + " operators at the time.\n"
289: + "Please ask a wizard to improve me.";
290:
291: final Term newGuard;
292: if (pair.locationAsTerm().freeVars().contains(var)) {
293: final Term clashCond = clashConditions(var, varP, pair,
294: firstNPairs(oldPairsP, locNum));
295: newGuard = tf.createJunctorTermAndSimplify(Op.AND,
296: clashCond, pair.guard());
297: } else {
298: newGuard = pair.guard();
299: }
300:
301: newPairs[locNum] = new AssignmentPairImpl(pushFront(var,
302: pair), newGuard, pair.location(), pair
303: .locationSubs(), pair.value());
304: }
305: return Update.createUpdate(newPairs);
306: }
307:
308: /**
309: * Add <code>var</code> as first bound variable of <code>pair</code>
310: */
311: private ArrayOfQuantifiableVariable pushFront(
312: QuantifiableVariable var, AssignmentPair pair) {
313: final int oldSize = pair.boundVars().size();
314: final QuantifiableVariable[] newBoundVars = new QuantifiableVariable[oldSize + 1];
315: newBoundVars[0] = var;
316: pair.boundVars().arraycopy(0, newBoundVars, 1, oldSize);
317:
318: return new ArrayOfQuantifiableVariable(newBoundVars);
319: }
320:
321: /**
322: * Conditions under which the elementary update <code>pair</code> may be
323: * executed, i.e. conditions under which its application does not collide
324: * with the earlier part <code>prefix</code> of the whole update. It is
325: * necessary to impose these conditions because distributing quantification
326: * through the parallel composition operator changes the order of update
327: * execution
328: */
329: private Term clashConditions(QuantifiableVariable var,
330: LogicVariable varP, AssignmentPair pair, Update prefix) {
331: Term res = getSimplifier().matchingCondition(prefix,
332: pair.locationAsTerm(), services);
333: if (res.op() == Op.FALSE)
334: return UpdateSimplifierTermFactory.DEFAULT.getValidGuard();
335:
336: // Bug in the first implementation: It is wrong to add quanifiers here
337: // if ( pair.boundVars ().size () > 0 )
338: // res = tf.createQuantifierTerm ( Op.EX, pair.boundVars (), res );
339: res = tf.createJunctorTerm(Op.NOT, res);
340:
341: final Term var2varPComparison = wellOrder(tf
342: .createVariableTerm((LogicVariable) var), tf
343: .createVariableTerm(varP));
344:
345: res = tf.createJunctorTermAndSimplify(Op.OR,
346: var2varPComparison, res);
347: return tf.createQuantifierTerm(Op.ALL, varP, res);
348: }
349:
350: private Update firstNPairs(ArrayOfAssignmentPair pairs, int n) {
351: final AssignmentPair[] criticalPairs = new AssignmentPair[n];
352: pairs.arraycopy(0, criticalPairs, 0, n);
353: return Update.createUpdate(criticalPairs);
354: }
355:
356: private LogicVariable createPrime(QuantifiableVariable var) {
357: // TODO: name the new variable in a better way
358: return new LogicVariable(new Name(var.name().toString()
359: + "Prime"), var.sort());
360: }
361:
362: private Update substitute(Update update, QuantifiableVariable var,
363: LogicVariable varPrime) {
364: return utf.substitute(update, var, tf
365: .createVariableTerm(varPrime));
366: }
367:
368: /**
369: * Add the guard <code>guard</code> as a condition to <code>update</code>,
370: * i.e. only carry out the update if <code>guard</code> evaluates to true
371: */
372: public Update guard(Term guard, Update update) {
373: assert guard.sort() == Sort.FORMULA;
374:
375: final Update cleanedUpdate = utf.resolveCollisions(update,
376: guard.freeVars());
377: final ArrayOfAssignmentPair oldPairs = cleanedUpdate
378: .getAllAssignmentPairs();
379:
380: final AssignmentPair[] newPairs = new AssignmentPair[cleanedUpdate
381: .locationCount()];
382: for (int i = 0; i != oldPairs.size(); ++i) {
383: final AssignmentPair pair = oldPairs.getAssignmentPair(i);
384: final Term newGuard = tf.createJunctorTermAndSimplify(
385: Op.AND, guard, pair.guard());
386: newPairs[i] = new AssignmentPairImpl(pair.boundVars(),
387: newGuard, pair.location(), pair.locationSubs(),
388: pair.value());
389: }
390: return Update.createUpdate(newPairs);
391: }
392:
393: private UpdateSimplifier getSimplifier() {
394: return simplifier;
395: }
396: }
|