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.*;
019: import de.uka.ilkd.key.strategy.termProjection.AssumptionProjection;
020: import de.uka.ilkd.key.strategy.termProjection.TermBuffer;
021:
022: /**
023: *
024: */
025: public class FOLStrategy extends AbstractFeatureStrategy {
026:
027: private final Feature completeF;
028:
029: private final Feature approvalF;
030:
031: protected FOLStrategy(Proof p_proof) {
032: super (p_proof);
033:
034: final RuleSetDispatchFeature d = RuleSetDispatchFeature
035: .create();
036:
037: bindRuleSet(d, "closure", -9000);
038: bindRuleSet(d, "concrete", -10000);
039: bindRuleSet(d, "alpha", -7000);
040: bindRuleSet(d, "delta", -6000);
041: bindRuleSet(d, "pull_out_quantifier", 5000);
042:
043: bindRuleSet(
044: d,
045: "beta",
046: add(
047: longConst(-2500),
048: ifZero(
049: SimplifyBetaCandidateFeature.INSTANCE,
050: SumFeature
051: .createSum(new Feature[] {
052: longConst(-1070),
053: ifZero(
054: FocusHasConstraintFeature.INSTANCE,
055: longConst(300)),
056: ifZero(
057: PurePosDPathFeature.INSTANCE,
058: longConst(-200)),
059: // ifZero ( ContainsQuantifierFeature.INSTANCE,
060: // longConst ( -2000 ) ),
061: ScaleFeature
062: .createScaled(
063: CountPosDPathFeature.INSTANCE,
064: -3.0),
065: ScaleFeature
066: .createScaled(
067: CountMaxDPathFeature.INSTANCE,
068: 10.0) }))));
069:
070: final Feature introducedByGammaF = FormulaAddedByRuleFeature
071: .create(getFilterFor(new String[] { "gamma",
072: "gamma_destructive" }));
073: bindRuleSet(d, "test_gen", inftyConst());
074:
075: bindRuleSet(d, "gamma", ifZero(introducedByGammaF,
076: longConst(0), add(ifZero(
077: NonDuplicateAppFeature.INSTANCE,
078: longConst(-200)), longConst(-3250))));
079:
080: bindRuleSet(d, "gamma_destructive", ifZero(introducedByGammaF,
081: longConst(-5000)));
082:
083: final Feature replaceKnownF = SumFeature
084: .createSum(new Feature[] {
085: SimplifyReplaceKnownCandidateFeature.INSTANCE,
086: ifZero(
087: ConstraintStrengthenFeature.INSTANCE,
088: add(
089: ifZero(
090: SimplifyBetaCandidateFeature.INSTANCE,
091: inftyConst()),
092: NotBelowQuantifierFeature.INSTANCE,
093: LeftmostNegAtomFeature.INSTANCE),
094: longConst(-800)),
095: longConst(-4000),
096: ScaleFeature.createScaled(
097: CountMaxDPathFeature.INSTANCE, 10.0) });
098: bindRuleSet(d, "replace_known_left", replaceKnownF);
099: bindRuleSet(d, "replace_known_right", replaceKnownF);
100:
101: final TermBuffer equation = new TermBuffer();
102: bindRuleSet(d, "apply_equations", add(ifZero(
103: MatchedIfFeature.INSTANCE,
104: add(CheckApplyEqFeature.INSTANCE, let(equation,
105: AssumptionProjection.create(0),
106: TermSmallerThanFeature.create(sub(equation, 1),
107: sub(equation, 0))))), ifZero(
108: ConstraintStrengthenFeature.INSTANCE, add(ifZero(
109: SimplifyBetaCandidateFeature.INSTANCE,
110: inftyConst()),
111: NotBelowQuantifierFeature.INSTANCE, ifZero(
112: ContainsQuantifierFeature.INSTANCE,
113: inftyConst()))), longConst(-4000)));
114:
115: bindRuleSet(d, "order_terms", add(TermSmallerThanFeature
116: .create(instOf("commEqLeft"), instOf("commEqRight")),
117: longConst(-8000)));
118:
119: bindRuleSet(d, "simplify_literals", ifZero(
120: ConstraintStrengthenFeature.INSTANCE, longConst(-4000),
121: longConst(-8000)));
122:
123: bindRuleSet(d, "try_apply_subst", add(
124: EqNonDuplicateAppFeature.INSTANCE, longConst(-10000)));
125:
126: // delete cast
127: bindRuleSet(d, "cast_deletion", ifZero(
128: implicitCastNecessary(instOf("castedTerm")),
129: longConst(-5000), inftyConst()));
130:
131: // disallow simplification of polynomials and inequations here
132: // (these rules need guidance that is not present in this strategy)
133: bindRuleSet(d, "polySimp_expand", inftyConst());
134: bindRuleSet(d, "polySimp_directEquations", inftyConst());
135: bindRuleSet(d, "polySimp_pullOutGcd", inftyConst());
136: bindRuleSet(d, "polySimp_saturate", inftyConst());
137: bindRuleSet(d, "polySimp_applyEq", inftyConst());
138: bindRuleSet(d, "polySimp_applyEqRigid", inftyConst());
139: bindRuleSet(d, "polySimp_leftNonUnit", inftyConst());
140: bindRuleSet(d, "inEqSimp_expand", inftyConst());
141: bindRuleSet(d, "inEqSimp_directInEquations", inftyConst());
142: bindRuleSet(d, "inEqSimp_saturate", inftyConst());
143: bindRuleSet(d, "inEqSimp_pullOutGcd", inftyConst());
144: bindRuleSet(d, "inEqSimp_propagation", inftyConst());
145: bindRuleSet(d, "inEqSimp_special_nonLin", inftyConst());
146: bindRuleSet(d, "inEqSimp_nonLin", inftyConst());
147: bindRuleSet(d, "inEqSimp_signCases", inftyConst());
148: bindRuleSet(d, "polyDivision", inftyConst());
149: bindRuleSet(d, "defOps_div", inftyConst());
150: bindRuleSet(d, "system_invariant", inftyConst());
151: bindRuleSet(d, "query_normalize", inftyConst());
152: bindRuleSet(d, "cut_direct", inftyConst());
153: bindRuleSet(d, "negationNormalForm", inftyConst());
154: bindRuleSet(d, "moveQuantToLeft", inftyConst());
155: bindRuleSet(d, "conjNormalForm", inftyConst());
156: bindRuleSet(d, "apply_equations_andOr", inftyConst());
157: bindRuleSet(d, "elimQuantifier", inftyConst());
158: bindRuleSet(d, "distrQuantifier", inftyConst());
159: bindRuleSet(d, "swapQuantifiers", inftyConst());
160: bindRuleSet(d, "pullOutQuantifierAll", inftyConst());
161: bindRuleSet(d, "pullOutQuantifierEx", inftyConst());
162:
163: bindRuleSet(d, "javaIntegerSemantics", -100);
164:
165: final Feature simplifierF = selectSimplifier(-10000);
166:
167: final Feature duplicateF = ifZero(
168: NonDuplicateAppFeature.INSTANCE, longConst(0),
169: ifHeuristics(new String[] { "gamma",
170: "gamma_destructive" }, longConst(5),
171: inftyConst()));
172:
173: final Feature ifMatchedF = ifZero(MatchedIfFeature.INSTANCE,
174: longConst(+1));
175:
176: completeF = SumFeature.createSum(new Feature[] {
177: AutomatedRuleFeature.INSTANCE,
178: NotWithinMVFeature.INSTANCE, simplifierF, duplicateF,
179: ifMatchedF, d, AgeFeature.INSTANCE });
180:
181: approvalF = duplicateF;
182: }
183:
184: public Name name() {
185: return new Name("FOLStrategy");
186: }
187:
188: /**
189: * Evaluate the cost of a <code>RuleApp</code>.
190: *
191: * @return the cost of the rule application expressed as a
192: * <code>RuleAppCost</code> object.
193: * <code>TopRuleAppCost.INSTANCE</code> indicates that the rule
194: * shall not be applied at all (it is discarded by the strategy).
195: */
196: public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio,
197: Goal goal) {
198: return completeF.compute(app, pio, goal);
199: }
200:
201: /**
202: * Re-Evaluate a <code>RuleApp</code>. This method is
203: * called immediately before a rule is really applied
204: * @return true iff the rule should be applied, false otherwise
205: */
206: public boolean isApprovedApp(RuleApp app, PosInOccurrence pio,
207: Goal goal) {
208: return !(approvalF.compute(app, pio, goal) instanceof TopRuleAppCost);
209: }
210:
211: protected RuleAppCost instantiateApp(RuleApp app,
212: PosInOccurrence pio, Goal goal) {
213: return TopRuleAppCost.INSTANCE;
214: }
215:
216: public static class Factory extends StrategyFactory {
217: public Factory() {
218:
219: }
220:
221: public Strategy create(Proof p_proof,
222: StrategyProperties strategyProperties) {
223: return new FOLStrategy(p_proof);
224: }
225:
226: public Name name() {
227: return new Name("FOLStrategy");
228: }
229: }
230: }
|