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.updatesimplifier;
010:
011: import java.util.Iterator;
012: import java.util.LinkedList;
013: import java.util.List;
014:
015: import de.uka.ilkd.key.logic.BoundVariableTools;
016: import de.uka.ilkd.key.logic.ClashFreeSubst;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.TermFactory;
019: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
020: import de.uka.ilkd.key.logic.op.Op;
021: import de.uka.ilkd.key.logic.op.QuantifiableVariable;
022: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
023: import de.uka.ilkd.key.util.Debug;
024:
025: public class UpdateSimplifierTermFactory {
026:
027: /**
028: * Interface for representing an ifEx cascade
029: * <tt> ifEx (...) (phi1) (t1) (ifEx (...) (phi2) (t2) (...))</tt>. This
030: * is essentially an iterator through the ifEx statements, starting with the
031: * outermost one
032: */
033: public static interface IfExCascade {
034: public Term getCondition();
035:
036: public ArrayOfQuantifiableVariable getMinimizedVars();
037:
038: // Information about the current ifEx statement. These methods must only
039: // be called after having invoked <code>next</code> at least once
040:
041: public Term getThenBranch();
042:
043: /**
044: * @return <code>true</code> if a further ifEx statement is following
045: * (within the else-branch of the current statement)
046: */
047: public boolean hasNext();
048:
049: /**
050: * Step forward to the next ifEx statement
051: */
052: public void next();
053: }
054:
055: private final static TermFactory tf = TermFactory.DEFAULT;
056:
057: public final static UpdateSimplifierTermFactory DEFAULT = new UpdateSimplifierTermFactory();
058:
059: private final Term unsatisfiableGuardCache = tf
060: .createJunctorTerm(Op.FALSE);
061:
062: private final Term validGuardCache = tf.createJunctorTerm(Op.TRUE);
063:
064: public Term createIfExCascade(IfExCascade cascade, Term defaultTerm) {
065: final List statements = new LinkedList();
066:
067: while (cascade.hasNext()) {
068: cascade.next();
069: final IfExCascadeEntryBuilder builder = new IfExCascadeEntryBuilder(
070: cascade.getCondition(), cascade.getMinimizedVars(),
071: cascade.getThenBranch());
072: if (builder.isAlwaysElse())
073: // this statement can just be ignored and removed
074: continue;
075:
076: statements.add(0, builder);
077:
078: if (builder.isEndOfCascade())
079: // all further statements can be ignored
080: break;
081: }
082:
083: Term res = defaultTerm;
084:
085: final Iterator it = statements.iterator();
086: while (it.hasNext()) {
087: final IfExCascadeEntryBuilder builder = (IfExCascadeEntryBuilder) it
088: .next();
089: res = builder.createTerm(res);
090: }
091:
092: return res;
093: }
094:
095: /**
096: * creates an update term out of the given internal representation
097: * used by the update simplifier, i.e. the assignmentpairs are made
098: * explicit
099: * @param target the term evaluated under the update
100: * @return the update term <tt>{l1:=r1,...,ln:=rn}target</tt>
101: */
102: public Term createUpdateTerm(ArrayOfAssignmentPair assignmentPairs,
103: Term target) {
104:
105: if (assignmentPairs.size() == 0) {
106: return target;
107: }
108:
109: final Term[] lhss = new Term[assignmentPairs.size()];
110: final ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[assignmentPairs
111: .size()];
112: final Term[] guards = new Term[assignmentPairs.size()];
113: final Term[] values = new Term[assignmentPairs.size()];
114:
115: for (int i = 0; i < assignmentPairs.size(); i++) {
116: final AssignmentPair assignmentPair = assignmentPairs
117: .getAssignmentPair(i);
118: boundVars[i] = assignmentPair.boundVars();
119: guards[i] = assignmentPair.guard();
120: lhss[i] = assignmentPair.locationAsTerm();
121: values[i] = assignmentPair.valueUnsafe();
122: if (assignmentPair.location() == Update.StarLocation.ALL) {
123: Debug
124: .assertTrue(
125: assignmentPairs.size() == 1,
126: "Special star operator tried to escape. "
127: + "(not allowed as long as no generalized terms)");
128: return tf.createAnonymousUpdateTerm(assignmentPair
129: .value().op().name(), target);
130: }
131: }
132: return tf.createQuanUpdateTerm(boundVars, guards, lhss, values,
133: target);
134: }
135:
136: /**
137: * creates an update term out of the given internal representation
138: * used by the update simplifier, i.e. the assignmentpairs are made
139: * explicit
140: * @param update an array of AssignmentPairs <tt>l:=r</tt> of the
141: * simulataneous update to be created
142: * @param target the term evaluated under the update
143: * @return the update term <tt>{l1:=r1,...,ln:=rn}target</tt>
144: */
145: public Term createUpdateTerm(AssignmentPair[] update, Term target) {
146: return createUpdateTerm(new ArrayOfAssignmentPair(update),
147: target);
148: }
149:
150: /**
151: * @return the default termfactory for JavaCardDL terms
152: */
153: public TermFactory getBasicTermFactory() {
154: return tf;
155: }
156:
157: public Term getUnsatisfiableGuard() {
158: return unsatisfiableGuardCache;
159: }
160:
161: public Term getValidGuard() {
162: return validGuardCache;
163: }
164:
165: /**
166: * Compose the formula expressing that at least one of the conditions of an
167: * ifEx-cascade evaluates to <tt>true</tt>, i.e. that the result of the
168: * cascade is one of the then-branches (and not the default branch)
169: */
170: public Term matchingCondition(IfExCascade cascade) {
171: Term res = getUnsatisfiableGuard();
172:
173: while (cascade.hasNext()) {
174: cascade.next();
175: final GuardSatisfiabilityFormulaBuilder builder = new GuardSatisfiabilityFormulaBuilder(
176: cascade.getCondition(), cascade.getMinimizedVars());
177: res = getBasicTermFactory().createJunctorTermAndSimplify(
178: Op.OR, builder.createFormula(), res);
179: }
180:
181: return res;
182: }
183:
184: private AssignmentPair renameBoundVars(AssignmentPair pair,
185: ArrayOfQuantifiableVariable newVars) {
186: final BoundVariableTools bvt = BoundVariableTools.DEFAULT;
187: final ArrayOfQuantifiableVariable oldVars = pair.boundVars();
188:
189: return new AssignmentPairImpl(newVars, bvt.renameVariables(pair
190: .guard(), oldVars, newVars), pair.location(),
191: bvt.renameVariables(pair.locationSubs(), oldVars,
192: newVars), bvt.renameVariables(pair.value(),
193: oldVars, newVars));
194: }
195:
196: private Term[] substitute(Term[] terms, ClashFreeSubst subst) {
197: final Term[] newTerms = new Term[terms.length];
198: boolean changed = false;
199: for (int i = 0; i != terms.length; ++i) {
200: newTerms[i] = subst.apply(terms[i]);
201: changed = changed || newTerms[i] != terms[i];
202: }
203: if (changed)
204: return newTerms;
205: return terms;
206: }
207:
208: /**
209: * Substitute <code>substTerm</code> for the variable <code>var</code> in
210: * the given assignment pair. Ensures that no collisions occur.
211: */
212: public AssignmentPair substitute(AssignmentPair pair,
213: QuantifiableVariable var, Term substTerm) {
214: if (!pair.freeVars().contains(var))
215: return pair;
216:
217: final ClashFreeSubst subst = new ClashFreeSubst(var, substTerm);
218:
219: pair = resolveCollisions(pair, substTerm.freeVars());
220:
221: return new AssignmentPairImpl(pair.boundVars(), subst
222: .apply(pair.guard()), pair.location(), substitute(pair
223: .locationSubs(), subst), subst.apply(pair.value()));
224: }
225:
226: /**
227: * Substitute <code>substTerm</code> for the variable <code>var</code> in
228: * the given update. Ensures that no collisions occur.
229: */
230: public Update substitute(Update update, QuantifiableVariable var,
231: Term substTerm) {
232: if (!update.freeVars().contains(var))
233: return update;
234:
235: final ArrayOfAssignmentPair pairs = update
236: .getAllAssignmentPairs();
237: AssignmentPair newPairs[] = new AssignmentPair[pairs.size()];
238:
239: for (int i = 0; i != pairs.size(); ++i)
240: newPairs[i] = substitute(pairs.getAssignmentPair(i), var,
241: substTerm);
242:
243: return Update.createUpdate(newPairs);
244: }
245:
246: /**
247: * Ensure that none of the variables <code>criticalVars</code> is bound by
248: * <code>pair</code> (turns up in <code>pair.boundVars()</code>). When
249: * necessary, variables are renamed to this end
250: */
251: public AssignmentPair resolveCollisions(AssignmentPair pair,
252: SetOfQuantifiableVariable criticalVars) {
253: final ArrayOfQuantifiableVariable oldVars = pair.boundVars();
254: if (oldVars.size() == 0)
255: return pair;
256:
257: final BoundVariableTools bvt = BoundVariableTools.DEFAULT;
258:
259: final QuantifiableVariable newVars[] = new QuantifiableVariable[oldVars
260: .size()];
261: if (!bvt.resolveCollisions(oldVars, newVars, criticalVars))
262: return pair;
263:
264: return renameBoundVars(pair, new ArrayOfQuantifiableVariable(
265: newVars));
266: }
267:
268: /**
269: * Ensure that none of the variables <code>criticalVars</code> is bound by
270: * <code>update</code>. When necessary, variables are renamed to this end
271: */
272: public Update resolveCollisions(Update update,
273: SetOfQuantifiableVariable criticalVars) {
274: final ArrayOfAssignmentPair pairs = update
275: .getAllAssignmentPairs();
276: AssignmentPair newPairs[] = new AssignmentPair[pairs.size()];
277:
278: boolean changed = false;
279: for (int i = 0; i != pairs.size(); ++i) {
280: newPairs[i] = resolveCollisions(pairs.getAssignmentPair(i),
281: criticalVars);
282: changed = changed
283: || newPairs[i] != pairs.getAssignmentPair(i);
284: }
285:
286: if (!changed)
287: return update;
288: return Update.createUpdate(newPairs);
289: }
290: }
|