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.strategy;
012:
013: import de.uka.ilkd.key.logic.Name;
014: import de.uka.ilkd.key.logic.PosInOccurrence;
015: import de.uka.ilkd.key.proof.Goal;
016: import de.uka.ilkd.key.proof.Proof;
017: import de.uka.ilkd.key.rule.RuleApp;
018: import de.uka.ilkd.key.strategy.feature.Feature;
019: import de.uka.ilkd.key.strategy.feature.SumFeature;
020:
021: /**
022: * Used for OCL Simplification.
023: */
024: public class SimplificationOfOCLStrategy extends
025: AbstractFeatureStrategy {
026:
027: static final int PHASE_1 = 1;
028: static final int PHASE_2 = 2;
029: static final int PHASE_3 = 3;
030: private Feature simplRulesF;
031: private Feature spec2iterateF;
032: private Feature iterate2specF;
033: private Feature completeF;
034: private int phase = PHASE_1;
035:
036: public SimplificationOfOCLStrategy(Proof proof) {
037: super (proof);
038:
039: simplRulesF = ifHeuristics(new String[] { "ocl_simplify" },
040: -3000);
041: spec2iterateF = ifHeuristics(
042: new String[] { "ocl_spec2iterate" }, -3000);
043: iterate2specF = ifHeuristics(
044: new String[] { "ocl_iterate2spec" }, -2000);
045: completeF = SumFeature.createSum(new Feature[] { simplRulesF,
046: spec2iterateF, iterate2specF });
047: }
048:
049: public Name name() {
050: return new Name("SimplificationOfOCLStrategy");
051: }
052:
053: /**
054: * Evaluate the cost of a <code>RuleApp</code>.
055: *
056: * @return the cost of the rule application expressed as a
057: * <code>RuleAppCost</code> object.
058: * <code>TopRuleAppCost.INSTANCE</code> indicates that the rule
059: * shall not be applied at all (it is discarded by the strategy).
060: */
061: public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio,
062: Goal goal) {
063: return completeF.compute(app, pio, goal);
064: }
065:
066: /**
067: * Re-Evaluate a <code>RuleApp</code>. This method is
068: * called immediately before a rule is really applied
069: * @return true iff the rule should be applied, false otherwise
070: */
071: public boolean isApprovedApp(RuleApp app, PosInOccurrence pio,
072: Goal goal) {
073: //The phase in which the simplification is performed
074: if (phase == PHASE_1) {
075: //If no more simplification rules are applicable then give the
076: //highest priority to the "iterate2something" rules and indicate
077: //that the simplification phase is over
078: if (simplRulesF.compute(app, pio, goal).compareTo(
079: LongRuleAppCost.ZERO_COST) == 0
080: && spec2iterateF.compute(app, pio, goal).compareTo(
081: LongRuleAppCost.ZERO_COST) == 0) {
082: spec2iterateF = ifHeuristics(
083: new String[] { "ocl_spec2iterate" }, -1000);
084: completeF = SumFeature.createSum(new Feature[] {
085: simplRulesF, spec2iterateF, iterate2specF });
086: phase = PHASE_2;
087: }
088: }
089:
090: //The phase in which all "iterate" constructs are translated back to
091: //more specialized collection operations
092: else if (phase == PHASE_2) {
093: //If no more "iterate2something" rules are applicable then stop the
094: //automatic rule application
095: if (iterate2specF.compute(app, pio, goal).compareTo(
096: LongRuleAppCost.ZERO_COST) == 0) {
097: //completeF = ConstFeature.createConst(TopRuleAppCost.INSTANCE);
098: phase = PHASE_3;
099: return false;
100: }
101: }
102:
103: //The "listening" phase. If any rules are applied manually or if "Goal Back" is
104: //pressed so that a simplification rule are again applicable, then reset
105: //everything and go back to pahse 1.
106: else {
107: if (simplRulesF.compute(app, pio, goal).compareTo(
108: LongRuleAppCost.ZERO_COST) != 0) {
109: simplRulesF = ifHeuristics(
110: new String[] { "ocl_simplify" }, -3000);
111: spec2iterateF = ifHeuristics(
112: new String[] { "ocl_spec2iterate" }, -3000);
113: iterate2specF = ifHeuristics(
114: new String[] { "ocl_iterate2spec" }, -2000);
115: completeF = SumFeature.createSum(new Feature[] {
116: simplRulesF, spec2iterateF, iterate2specF });
117: phase = PHASE_1;
118: } else {
119: return false;
120: }
121: }
122: return !(completeF.compute(app, pio, goal) instanceof TopRuleAppCost);
123: }
124:
125: protected RuleAppCost instantiateApp(RuleApp app,
126: PosInOccurrence pio, Goal goal) {
127: return TopRuleAppCost.INSTANCE;
128: }
129:
130: public static class Factory extends StrategyFactory {
131: public Factory() {
132: }
133:
134: public Strategy create(Proof proof,
135: StrategyProperties strategyProperties) {
136: return new SimplificationOfOCLStrategy(proof);
137: }
138:
139: public Name name() {
140: return new Name("SimplificationOfOCLStrategy");
141: }
142: }
143: }
|