01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.strategy.feature;
12:
13: import de.uka.ilkd.key.logic.PIOPathIterator;
14: import de.uka.ilkd.key.logic.PosInOccurrence;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.IfThenElse;
17: import de.uka.ilkd.key.proof.Goal;
18: import de.uka.ilkd.key.rule.RuleApp;
19: import de.uka.ilkd.key.strategy.LongRuleAppCost;
20: import de.uka.ilkd.key.strategy.RuleAppCost;
21: import de.uka.ilkd.key.util.LRUCache;
22:
23: /**
24: * Feature that counts the IfThenElse operators above the focus of a rule
25: * application. When operating in argument 2 or 3 (branches) of IfThenElse, a
26: * malus of 1 is added; when operating in the argument 1 (condition), a bonus of
27: * -1 is added.
28: */
29: public class IfThenElseMalusFeature implements Feature {
30:
31: private static LRUCache cache = new LRUCache(1000);
32:
33: public static final Feature INSTANCE = new IfThenElseMalusFeature();
34:
35: private IfThenElseMalusFeature() {
36: }
37:
38: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
39: Goal goal) {
40: if (pos == null)
41: return LongRuleAppCost.ZERO_COST;
42:
43: RuleAppCost resInt = (RuleAppCost) cache.get(pos);
44: if (resInt != null) {
45: return resInt;
46: }
47:
48: int res = 0;
49:
50: final PIOPathIterator it = pos.iterator();
51: while (true) {
52: final int ind = it.next();
53: if (ind == -1)
54: break;
55:
56: final Term t = it.getSubTerm();
57: if (t.op() instanceof IfThenElse && ind != 0)
58: res++;
59: }
60:
61: resInt = LongRuleAppCost.create(res);
62: cache.put(pos, resInt);
63: return resInt;
64: }
65:
66: }
|