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.rule;
012:
013: import java.util.LinkedList;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.logic.*;
017: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
018: import de.uka.ilkd.key.proof.Goal;
019: import de.uka.ilkd.key.proof.ListOfGoal;
020:
021: /**
022: * Built in rule that starts the update simplifier on the sequent or
023: * selected term. The rule is useful if one has changes the simultaneous
024: * update simplifier settings.
025: */
026: public class UpdateSimplificationRule implements BuiltInRule {
027:
028: // container for old constrained formula and the one used to replace it
029: static class ConstrainedFormulaContainer {
030:
031: private final ConstrainedFormula old;
032: private final ConstrainedFormula replacement;
033: private final boolean oldFormulaInAntecendent;
034:
035: public ConstrainedFormulaContainer(ConstrainedFormula old,
036: boolean oldFormulaInAntecendent,
037: ConstrainedFormula replacement) {
038: this .old = old;
039: this .oldFormulaInAntecendent = oldFormulaInAntecendent;
040: this .replacement = replacement;
041: }
042:
043: public ConstrainedFormula old() {
044: return old;
045: }
046:
047: public boolean oldFormulaInAntecedent() {
048: return oldFormulaInAntecendent;
049: }
050:
051: public ConstrainedFormula replacement() {
052: return replacement;
053: }
054:
055: }
056:
057: private static final ConstrainedFormulaContainer[] EMPTY_CONSTRAINEDFORMULA_ARRAY = new ConstrainedFormulaContainer[0];
058:
059: public static UpdateSimplificationRule INSTANCE = new UpdateSimplificationRule();
060:
061: protected final Name name = new Name("Update Simplification");
062:
063: protected UpdateSimplificationRule() {
064: }
065:
066: /** the rule is applied on the given goal using the
067: * information of rule application. As applications of this rule kind may
068: * not be successful in each case one has to ensure that the goal split is
069: * done only iff the application was successful.
070: * @param goal the goal that the rule application should refer to.
071: * @param services the Services with the necessary information
072: * about the java programs
073: * @param the rule application that is executed.
074: */
075: public ListOfGoal apply(Goal goal, Services services,
076: RuleApp ruleApp) {
077:
078: ListOfGoal result = null;
079: final ConstrainedFormulaContainer[] applicationResult;
080:
081: final PosInOccurrence pio = ruleApp.posInOccurrence();
082: final Sequent sequent = goal.sequent();
083: if (pio == null) {
084: applicationResult = applyOnSequent(sequent, goal
085: .simplifier(), services);
086: } else {
087: applicationResult = applyOnTerm(goal.simplifier(), pio,
088: services);
089: }
090:
091: if (applicationResult.length > 0) {
092: result = goal.split(1);
093: final Goal newGoal = result.head();
094: for (int i = 0, nr = applicationResult.length; i < nr; i++) {
095: final ConstrainedFormulaContainer cfc = applicationResult[i];
096: final PosInOccurrence oldCFPIO = new PosInOccurrence(
097: cfc.old(), PosInTerm.TOP_LEVEL, cfc
098: .oldFormulaInAntecedent());
099: newGoal.changeFormula(cfc.replacement(), oldCFPIO);
100: }
101: }
102: return result;
103: }
104:
105: private ConstrainedFormulaContainer[] applyOnSequent(Sequent seq,
106: UpdateSimplifier sus, Services services) {
107:
108: final LinkedList result = new LinkedList();
109:
110: applyOnSemisequent(seq.antecedent(), true, sus, services,
111: result);
112: applyOnSemisequent(seq.succedent(), false, sus, services,
113: result);
114:
115: return (ConstrainedFormulaContainer[]) result
116: .toArray(new ConstrainedFormulaContainer[result.size()]);
117: }
118:
119: private void applyOnSemisequent(Semisequent semiSeq,
120: boolean semiSeqIsAntecedent, UpdateSimplifier sus,
121: Services services, final LinkedList result) {
122: final IteratorOfConstrainedFormula it = semiSeq.iterator();
123:
124: while (it.hasNext()) {
125: final ConstrainedFormula cf = it.next();
126: final Term simplified = sus
127: .simplify(cf.formula(), services);
128: if (simplified != cf.formula()) {
129: result.add(new ConstrainedFormulaContainer(cf,
130: semiSeqIsAntecedent, new ConstrainedFormula(
131: simplified, cf.constraint())));
132: }
133: }
134: }
135:
136: private ConstrainedFormulaContainer[] applyOnTerm(
137: UpdateSimplifier sus, PosInOccurrence pio, Services services) {
138: final ConstrainedFormulaContainer[] result;
139:
140: ConstrainedFormula cf = pio.constrainedFormula();
141: Term fml = cf.formula();
142:
143: Term simplified = sus.simplify(pio.subTerm(), services);
144: if (simplified != fml) {
145: final ConstrainedFormula new_cf = new ConstrainedFormula(
146: replace(fml, simplified, pio.posInTerm().iterator()),
147: cf.constraint());
148: result = new ConstrainedFormulaContainer[] { new ConstrainedFormulaContainer(
149: cf, pio.isInAntec(), new_cf) };
150: } else {
151: result = EMPTY_CONSTRAINEDFORMULA_ARRAY;
152: }
153:
154: return result;
155: }
156:
157: public String displayName() {
158: return toString();
159: }
160:
161: /**
162: * tests if the rule is applicable at the given position
163: */
164: public boolean isApplicable(Goal goal, PosInOccurrence pio,
165: Constraint userConstraint) {
166: final Services services = goal.proof().getServices();
167: if (pio != null) {
168: final Term fml = pio.subTerm();
169: final Term simplified = goal.simplifier().simplify(fml,
170: services);
171: if (!simplified.equals(fml)) {
172: return true;
173: }
174: } else { // this may be too slow; may be return true always
175: final IteratorOfConstrainedFormula it = goal.sequent()
176: .iterator();
177: while (it.hasNext()) {
178: ConstrainedFormula cf = it.next();
179: final Term simplified = goal.simplifier().simplify(
180: cf.formula(), services);
181: if (!simplified.equals(cf.formula())) {
182: return true;
183: }
184: }
185: }
186: return false;
187: }
188:
189: public Name name() {
190: return name;
191: }
192:
193: private Term replace(Term term, Term with, IntIterator it) {
194: if (it.hasNext()) {
195: int sub = it.next();
196: Term[] subs = new Term[term.arity()];
197: final ArrayOfQuantifiableVariable[] vars = new ArrayOfQuantifiableVariable[term
198: .arity()];
199: for (int i = 0; i < term.arity(); i++) {
200: if (i != sub) {
201: subs[i] = term.sub(i);
202: } else {
203: subs[i] = replace(term.sub(i), with, it);
204: }
205: vars[i] = term.varsBoundHere(i);
206: }
207:
208: return TermFactory.DEFAULT.createTerm(term.op(), subs,
209: vars, term.javaBlock());
210: }
211:
212: return with;
213: }
214:
215: public String toString() {
216: return name().toString();
217: }
218:
219: }
|