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.ldt.IntegerLDT;
16: import de.uka.ilkd.key.logic.op.Op;
17: import de.uka.ilkd.key.logic.op.Operator;
18: import de.uka.ilkd.key.proof.Goal;
19: import de.uka.ilkd.key.rule.RuleApp;
20: import de.uka.ilkd.key.strategy.LongRuleAppCost;
21: import de.uka.ilkd.key.strategy.RuleAppCost;
22:
23: /**
24: * Walking from the root of a formula down to the focus of a rule application,
25: * count how often we choose the left branch (subterm) and how the right
26: * branches. This is used to identify the upper/righter/bigger summands in a
27: * polynomial that is arranged in a left-associated way.
28: */
29: public class FindRightishFeature implements Feature {
30:
31: private final Operator add;
32: private final static RuleAppCost one = LongRuleAppCost.create(1);
33:
34: public static Feature create(IntegerLDT numbers) {
35: return new FindRightishFeature(numbers);
36: }
37:
38: private FindRightishFeature(IntegerLDT numbers) {
39: add = numbers.getArithAddition();
40: }
41:
42: public RuleAppCost compute(RuleApp app, PosInOccurrence pos,
43: Goal goal) {
44: assert pos != null : "Feature is only applicable to rules with find";
45:
46: RuleAppCost res = LongRuleAppCost.ZERO_COST;
47: final PIOPathIterator it = pos.iterator();
48:
49: while (it.next() != -1) {
50: final Operator op = it.getSubTerm().op();
51: final int index = it.getChild();
52: if (index == 0 && op == add || index == 1
53: && op == Op.EQUALS)
54: res = res.add(one);
55: }
56:
57: return res;
58: }
59:
60: }
|