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.PosInOccurrence;
14: import de.uka.ilkd.key.proof.Goal;
15: import de.uka.ilkd.key.rule.TacletApp;
16: import de.uka.ilkd.key.strategy.termProjection.ProjectionToTerm;
17:
18: /**
19: * Feature that returns zero iff one term is smaller than another term in the
20: * current term ordering
21: */
22: public class TermSmallerThanFeature extends SmallerThanFeature {
23:
24: private final ProjectionToTerm left, right;
25:
26: public static Feature create(ProjectionToTerm left,
27: ProjectionToTerm right) {
28: return new TermSmallerThanFeature(left, right);
29: }
30:
31: private TermSmallerThanFeature(ProjectionToTerm left,
32: ProjectionToTerm right) {
33: this .left = left;
34: this .right = right;
35: }
36:
37: protected boolean filter(TacletApp app, PosInOccurrence pos,
38: Goal goal) {
39: return lessThan(left.toTerm(app, pos, goal), right.toTerm(app,
40: pos, goal));
41: }
42:
43: }
|