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.ConstrainedFormula;
013: import de.uka.ilkd.key.logic.Constraint;
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.IUpdateOperator;
017: import de.uka.ilkd.key.rule.updatesimplifier.*;
018: import de.uka.ilkd.key.util.Debug;
019:
020: /**
021: * The update simplifier applies updates on tems/formulas. Therefore
022: * it can be initialiazed with a set of simplification rules that
023: * shall be used.
024: *
025: * Calling the simplifier from outside must only be done by using
026: * the apply methods. The simplify methods are only for recursive
027: * calls made by the update simplification rules.
028: */
029: public class UpdateSimplifier {
030:
031: /**
032: * List of rules used for simplifying update terms. The first
033: * applicable rule is taken.
034: */
035: private IUpdateRule[] simplificationRules = new IUpdateRule[0];
036:
037: /**
038: * if set to true, the update simplifier is a bit more eagerly when
039: * applying updates
040: */
041: private boolean eager = true;
042:
043: private Constraint formulaConstraint = Constraint.BOTTOM;
044:
045: public UpdateSimplifier() {
046: this (false, false);
047: }
048:
049: /**
050: * creates an instance of the update simplifier
051: * @param deletionEnable a boolean flag indicating if unused or
052: * effectless assignment pairs should be removed
053: */
054: public UpdateSimplifier(boolean deletionEnabled, boolean eager) {
055: this .eager = eager;
056: ListOfIUpdateRule usRules = SLListOfIUpdateRule.EMPTY_LIST
057: .append(new ApplyOnAnonymousUpdate(this ))
058: .append(new ApplyAnonymousUpdateOnNonRigid(this ))
059: .append(new ApplyOnUpdate(this ))
060: .append(new ApplyOnLocalVariableOrStaticField(this ))
061: .append(new ApplyOnAttributeAccess(this ))
062: .append(new ApplyOnArrayAccess(this ))
063: .append(new ApplyOnModality(this , deletionEnabled))
064: .append(new ApplyOnRigidTerm(this ))
065: .append(new ApplyOnRigidOperatorTerm(this ))
066: .append(
067: new ApplyOnHeapDependentLocation(this ,
068: deletionEnabled))
069: .append(new ApplyOnProgramMethod(this , deletionEnabled))
070: .append(
071: new ApplyOnNonRigidWithExplicitDependencies(
072: this )).append(
073: new ApplyOnNonRigidTerm(this ));
074:
075: this .setSimplificationRules(usRules);
076: }
077:
078: /**
079: * Uses the given rules for update simplification. The order is
080: * important as the first applicable rule is taken.
081: * @param rules a ListOfUpdateRule to use for update
082: * simplification
083: */
084: public void setSimplificationRules(ListOfIUpdateRule rules) {
085: simplificationRules = rules.toArray();
086: }
087:
088: public Term simplify(Update update, Term t, Services services) {
089: Term simplifiedTerm = t;
090: for (int i = 0; i < simplificationRules.length; i++) {
091: if (simplificationRules[i].isApplicable(update,
092: simplifiedTerm)) {
093: return simplificationRules[i].apply(update,
094: simplifiedTerm, services);
095: }
096: }
097: return simplifiedTerm;
098: }
099:
100: /**
101: * Derive a formula that describes in which cases the top-level operator
102: * (location) described by <code>target</code> is updated by the given
103: * update.
104: *
105: * @param update
106: * the modification of function interpretations that is
107: * considered
108: * @param target
109: * description of the location we are interested in;
110: * precondition: <code>target.op() instanceof Location</code>
111: * @param services
112: * services object
113: * @return formula that evaluates to <tt>true</tt> iff <code>update</code>
114: * evaluates to a semantic update that affects the location
115: * described by <code>target</code>
116: */
117: public Term matchingCondition(Update update, Term target,
118: Services services) {
119: for (int i = 0; i < simplificationRules.length; i++) {
120: if (simplificationRules[i].isApplicable(update, target))
121: return simplificationRules[i].matchingCondition(update,
122: target, services);
123: }
124: Debug.fail("Don't know how to handle " + target);
125: return null; // unreachable
126: }
127:
128: /**
129: * applies the update on the given term
130: */
131: public Term apply(Term t, Services services) {
132: formulaConstraint = Constraint.BOTTOM;
133: // simplification and application part
134: return simplify(Update.createUpdate(t), t.sub(t.arity() - 1),
135: services);
136: }
137:
138: /**
139: * returns the formula constraint of the formula to be simpliefied
140: * @return the formula constraint
141: */
142: public Constraint formulaConstraint() {
143: return formulaConstraint;
144: }
145:
146: /**
147: *
148: */
149: public ConstrainedFormula apply(ConstrainedFormula target,
150: Constraint userConstraint) {
151: formulaConstraint = target.constraint();
152: return target;
153: }
154:
155: /**
156: * @param target
157: * @return
158: */
159: public Term simplify(Term target, Services services) {
160: if (target.op() instanceof IUpdateOperator) {
161: target = simplify(Update.createUpdate(target),
162: ((IUpdateOperator) target.op()).target(target),
163: services);
164: if (!eager) {
165: return target;
166: }
167: }
168:
169: final Term[] subs = new Term[target.arity()];
170: final ArrayOfQuantifiableVariable[] vars = new ArrayOfQuantifiableVariable[target
171: .arity()];
172:
173: boolean changed = false;
174: for (int i = 0; i < subs.length; i++) {
175: subs[i] = simplify(target.sub(i), services);
176: // only true as long as no bound variables change
177: vars[i] = target.varsBoundHere(i);
178: if (!changed && !(subs[i].equals(target.sub(i)))) {
179: changed = true;
180: }
181: }
182: return changed ? UpdateSimplifierTermFactory.DEFAULT
183: .getBasicTermFactory().createTerm(target.op(), subs,
184: vars, target.javaBlock()) : target;
185: }
186: }
|