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: package de.uka.ilkd.key.strategy.feature;
09:
10: import de.uka.ilkd.key.logic.PosInOccurrence;
11: import de.uka.ilkd.key.proof.Goal;
12: import de.uka.ilkd.key.rule.RuleApp;
13:
14: public abstract class CompareCostsFeature extends BinaryFeature {
15:
16: protected final Feature a, b;
17:
18: private CompareCostsFeature(Feature a, Feature b) {
19: this .a = a;
20: this .b = b;
21: }
22:
23: public static Feature less(Feature a, Feature b) {
24: return new CompareCostsFeature(a, b) {
25: protected boolean filter(RuleApp app, PosInOccurrence pos,
26: Goal goal) {
27: return a.compute(app, pos, goal).compareTo(
28: b.compute(app, pos, goal)) < 0;
29: }
30: };
31: }
32:
33: public static Feature leq(Feature a, Feature b) {
34: return new CompareCostsFeature(a, b) {
35: protected boolean filter(RuleApp app, PosInOccurrence pos,
36: Goal goal) {
37: return a.compute(app, pos, goal).compareTo(
38: b.compute(app, pos, goal)) <= 0;
39: }
40: };
41: }
42:
43: public static Feature eq(Feature a, Feature b) {
44: return new CompareCostsFeature(a, b) {
45: protected boolean filter(RuleApp app, PosInOccurrence pos,
46: Goal goal) {
47: return a.compute(app, pos, goal).equals(
48: b.compute(app, pos, goal));
49: }
50: };
51: }
52:
53: }
|