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.logic.sort.Sort;
12: import de.uka.ilkd.key.proof.Goal;
13: import de.uka.ilkd.key.rule.RuleApp;
14: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
15:
16: public class SortComparisionFeature extends BinaryFeature {
17:
18: public final static int SUBSORT = 0;
19:
20: public static Feature create(ProjectionToTerm s1,
21: ProjectionToTerm s2, int cmp) {
22: return new SortComparisionFeature(s1, s2, cmp);
23: }
24:
25: private final ProjectionToTerm s1;
26: private final ProjectionToTerm s2;
27: private final int comparator;
28:
29: /**
30: * creates a new comparision term feature
31: * @param s
32: */
33: private SortComparisionFeature(ProjectionToTerm s1,
34: ProjectionToTerm s2, int comparator) {
35: this .s1 = s1;
36: this .s2 = s2;
37: this .comparator = comparator;
38: }
39:
40: protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
41: final Sort sort1 = s1.toTerm(app, pos, goal).sort();
42: final Sort sort2 = s2.toTerm(app, pos, goal).sort();
43:
44: return compare(sort1, sort2);
45: }
46:
47: /**
48: * @param sort1
49: * @param sort2
50: * @return
51: */
52: protected boolean compare(final Sort sort1, final Sort sort2) {
53: switch (comparator) {
54: case SUBSORT:
55: return sort1.extendsTrans(sort2);
56: default:
57: return false;
58: }
59: }
60:
61: }
|